Skip to content

Commit

Permalink
~
Browse files Browse the repository at this point in the history
  • Loading branch information
Kaiyu Yang committed Jun 26, 2023
1 parent d65ac45 commit 5f5547d
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions index.html
Original file line number Diff line number Diff line change
Expand Up @@ -300,8 +300,8 @@ <h2 class="title is-3">Abstract</h2>
Furthermore, we construct a new benchmark consisting of 96,962 theorems and proofs extracted from Lean's math library.
It features challenging data split requiring the prover to generalize to theorems relying on novel premises that are never
used in training. We use this benchmark for training and evaluation, and experimental results demonstrate the effectiveness
of ReProver over non-retrieval baselines and GPT-4. We thus provide the first set of open-source LLM-based theorem provers without
any proprietary datasets and release it under a permissive MIT license to facilitate further research.
of ReProver over non-retrieval baselines and GPT-4. <b>We thus provide the first set of open-source LLM-based theorem provers without
any proprietary datasets and release it under a permissive MIT license to facilitate further research.</b>
</p>
</div>
</div>
Expand Down

0 comments on commit 5f5547d

Please sign in to comment.