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. |
Similar Papers
DT-Solver: Automated Theorem Proving with Dynamic-Tree Sampling Guided by Proof-level Value Function (2023.acl-long)
Copied to clipboard
Haiming Wang, Ye Yuan, Zhengying Liu, Jianhao Shen, Yichun Yin, Jing Xiong, Enze Xie, Han Shi, Yujun Li, Lin Li, Jian Yin, Zhenguo Li, Xiaodan Liang
| Challenge: | Recent advances in neural theorem-proving resort to large language models and tree searches. |
| Approach: | They propose a Dynamic-Tree Driven Theorem Solver to accommodate general theoremes by guiding the search procedure with state confidence and proof-level values. |
| Outcome: | The proposed method outperforms state-of-the-art methods on two popular theorem-proving datasets with a 6.65% improvement on average in terms of success rate. |
LeanReasoner: Boosting Complex Logical Reasoning with Lean (2024.naacl-long)
Copied to clipboard
| Challenge: | Large language models (LLMs) often struggle with complex logical reasoning due to logical inconsistencies and the inherent difficulty of such reasoning. |
| Approach: | They propose a method that formalizes logical reasoning problems into theorems within Lean and then proves or disproving the corresponding theorels. |
| Outcome: | The proposed method achieves state-of-the-art performance on the FOLIO dataset and near this level on ProofWriter. |
LogicTree: Structured Proof Exploration for Coherent and Rigorous Logical Reasoning with Large Language Models (2025.emnlp-main)
Copied to clipboard
| Challenge: | Large language models (LLMs) have remarkable multi-step reasoning capabilities, but they still face challenges in complex logical reasoning. |
| Approach: | They propose an algorithm-guided search framework that automates structured proof exploration and ensures logical coherence. |
| Outcome: | The proposed framework outperforms o3-mini and chain-of-thought with average gains of 23.6% and 12.5% on five datasets. |
Towards Advanced Mathematical Reasoning for LLMs via First-Order Logic Theorem Proving (2025.emnlp-main)
Copied to clipboard
Chuxue Cao, Mengze Li, Juntao Dai, Jinluan Yang, Zijian Zhao, Shengyu Zhang, Weijie Shi, Chengzhong Liu, Sirui Han, Yike Guo
| Challenge: | Large language models (LLMs) have shown promising first-order logic (FOL) reasoning capabilities with applications in various areas, but their effectiveness in complex mathematical reasoning involving multi-step FOL deductions remains under-explored. |
| Approach: | They propose a self-adaptive solution that enhances the Diversity and REAsonability of LLMs’ generation strategies by introducing an Axiom-Driven Strategy Diversification mechanism and a Sub-Proposition Error Feedback to help LLM reflect on and correct their proofs. |
| Outcome: | The proposed model improves diversity and REAsonability of LLMs’ generation strategies by introducing an Axiom-Driven Strategy Diversification mechanism and a Sub-Proposition Error Feedback to help LLM reflect on and correct proofs. |
TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts (2024.emnlp-main)
Copied to clipboard
| Challenge: | a framework for formal proof writing using formal languages like Lean4 is needed to prove mathematical theorems using formal language. |
| Approach: | They propose a framework that trains a general-purpose LLM to be a Lean4 expert. |
| Outcome: | The proposed framework achieves cumulative accuracies of 36.48% and 33.61% on MiniF2F-Valid and Test datasets. |
QDTSynth: Quality-Driven Formal Theorem Synthesis for Enhancing Proving Performance of LLMs (2025.acl-long)
Copied to clipboard
| Challenge: | Existing formal languages such as Lean, Coq and Metamath are proving to be useful in formal theorem proving . however, there is a scarcity of high-quality supervised fine-tuning data for formal proofs . |
| Approach: | They propose a Q**uality-**D**riven **T**heorem **S**ynthesis method in Lean4 . they propose diversity screening and the self-assessment method to select theoremas that exhibit diversity and high quality from the initial synthetic statements. |
| Outcome: | The proposed method significantly improves performance of open-source LLMs in theorem proving tasks. |
Don’t Get Lost in the Trees: Streamlining LLM Reasoning by Overcoming Tree Search Exploration Pitfalls (2025.acl-long)
Copied to clipboard
Ante Wang, Linfeng Song, Ye Tian, Dian Yu, Haitao Mi, Xiangyu Duan, Zhaopeng Tu, Jinsong Su, Dong Yu
| Challenge: | Recent advances in tree search algorithms guided by verifiers have significantly enhanced the reasoning capabilities of large language models (LLMs), but at the cost of increased computational resources. |
| Approach: | They propose an e ffici ent tree sear ch framework that is a plug-and-play system compatible with various tree search algorithms. |
| Outcome: | The proposed framework reduces computational costs and prioritizes resource allocation to harder tasks (Levels 3-4) over simpler ones (Level 1-2), addressing both over-exploration in basic problems and under-exploation in complex cases. |
Advancing Process Verification for Large Language Models via Tree-Based Preference Learning (2024.emnlp-main)
Copied to clipboard
| Challenge: | Existing methods for generating step-by-step rationales fail to fully utilize the relative merits of intermediate steps, limiting the effectiveness of feedback provided. |
| Approach: | They propose a tree-based preference learning verifier that constructs reasoning trees via a best-first search algorithm and collects step-level paired data for preference training. |
| Outcome: | The proposed approach outperforms existing benchmarks on arithmetic and commonsense reasoning tasks. |
Chain-in-Tree: Back to Sequential Reasoning in LLM Tree Search (2026.findings-acl)
Copied to clipboard
| Challenge: | Large language models excel at tasks such as mathematical and commonsense reasoning, but their performance improves further when additional test-time compute is allocated. |
| Approach: | They propose a plug-in framework that decides when to branch during search instead of expanding at every step. |
| Outcome: | The proposed framework reduces token generation, model calls, and runtime by 75-85% on GSM8K and Math500, with negligible or no accuracy loss. |
Think Hard Only When Needed: A Hybrid Best-of-N and Beam Search for Efficient Test-Time Compute (2026.findings-eacl)
Copied to clipboard
| Challenge: | Large language models (LLMs) exhibit remarkable reasoning and planning capabilities, yet their substantial inference-time cost significantly impedes deployment in resourceconstrained applications. |
| Approach: | They propose a hybrid inference pipeline that combines beam search and Best-of-N . THROW generates shorter initial trajectories and evaluates them using PRMs . |
| Outcome: | THROW achieves 1.54 and 14.38 latency speedups and 35.7% and 80.4% token reductions on average compared to Best-of-N and beam search . |