~

index.html

@@ -402,7 +402,7 @@ <h2 class="title is-3"><span class="dvima">ReProver: Retrieval-Augmented Theorem
             <div class="rows is-centered ">
                 <div class="row is-full-width">
                     <h2 class="title is-3"><span class="dvima">Experiments</span></h2>
-                    <p style="font-size: 125%">We use LeanDojo Benchmark to train and evaluate ReProver. During testing, the tactic generator is combined with best-first search to search for complete proofs. The table below shows the percentage of theorem proved within 10 minutes. The \(\texttt{novel_premises}\) spilt is much more challenging. On both data splits, ReProver outperforms Lean's built-in proof automation tactic (tidy), a baseline that generates tactics directly without retrieval, and another baseline using GPT-4 to generate tactics in a zero-shot manner.</p>
+                    <p style="font-size: 125%">We use LeanDojo Benchmark to train and evaluate ReProver. During testing, the tactic generator is combined with best-first search to search for complete proofs. The table below shows the percentage of theorem proved within 10 minutes. The \(\texttt{novel_premises}\) spilt is much more challenging than the \(\texttt{random}\) split. On both data splits, ReProver outperforms Lean's built-in proof automation tactic (tidy), a baseline that generates tactics directly without retrieval, and another baseline using GPT-4 to generate tactics in a zero-shot manner.</p>
                     <br />
                     <img src="images/results.png" width="50%" class="interpolation-image" alt="" style="display: block; margin-left: auto; margin-right: auto"/>
                 </div>