Papers with Lean4
FANS: Formal Answer Selection for LLM Natural Language Math Reasoning Using Lean4 (2025.emnlp-main)
Copied to clipboard
| Challenge: | Existing frameworks that use Lean4 to enhance LLMs' NL reasoning abilities have been controversial in the field of math reasoning. |
| Approach: | They propose a framework that utilizes Lean4 to enhance LLMs’ NL math reasoning ability by generating a Lean 4 theorem statement and a proof-generating LLM. |
| Outcome: | The proposed framework improves LLMs' NL math reasoning ability by 2% across several math benchmarks and higher further based on reward models or in subfields such as algebra and number theory. |
BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving (2025.acl-long)
Copied to clipboard
| Challenge: | Existing approaches to theorem proving in large language models rely on value functions and/or Monte Carlo Tree Search (MCTS), but the potential of simpler methods like Best-First Tree Search remains underexplored. |
| Approach: | They propose a scalable expert iteration framework that implements strategic data filtering at each expert iteration round, excluding problems solvable via beam search node expansion to focus on harder cases. |
| Outcome: | The proposed framework achieves a state-of-the-art score of 72.95 on the MiniF2F test set and challenges the perceived necessity of complex tree search methods. |