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. |
Similar Papers
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. |
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. |
RLMEval: Evaluating Research-Level Neural Theorem Proving (2025.findings-emnlp)
Copied to clipboard
| Challenge: | RLMEval evaluates large language models for research-level neural theorem proving and proof autoformalization . the best model achieves only a 10.3% pass rate on existing benchmarks . |
| Approach: | They propose a new evaluation suite for large language models . it evaluates research-level theorems from real-world Lean formalization projects . |
| Outcome: | RLMEval evaluates research-level theorems from real-world Lean formalization projects. |
Local Look-Ahead Guidance via Verifier-in-the-Loop for Automated Theorem Proving (2025.findings-acl)
Copied to clipboard
| Challenge: | Recent methods for AI reasoning require applying variants of reinforcement learning (RL) on rolled out trajectories, even for step-wise rewards, or large quantities of human-annotated trajectory data. |
| Approach: | They propose a verifier-in-the-loop design that uses an automated verifier to give intermediate feedback at each step of the reasoning process. |
| Outcome: | The proposed model improves on the Automatic Theorem Proving task using Lean as the verifier. |
Theorem Prover as a Judge for Synthetic Data Generation (2025.acl-long)
Copied to clipboard
| Challenge: | Recent studies show that large language models are increasingly capable of tackling mathematical problems. |
| Approach: | They propose an approach that iteratively refines theorem prover formalisation to mitigate errors. |
| Outcome: | The proposed method increases execution rate on the Lean prover from 60% to 87%, while human annotation is replaced with theorem prover feedback. |
BC-Prover: Backward Chaining Prover for Formal Theorem Proving (2024.emnlp-main)
Copied to clipboard
| Challenge: | Existing methods for interactive theorem proving in formal logic lack robustness and robustness. |
| Approach: | They propose a backward chaining framework guided by pseudo steps for proofstep generation that prioritizes pseudo steps. |
| Outcome: | The proposed framework improves on the miniF2F benchmark. |
DSG-MCTS: A Dynamic Strategy-Guided Monte Carlo Tree Search for Diversified Reasoning in Large Language Models (2025.emnlp-main)
Copied to clipboard
| Challenge: | Large language models (LLMs) have shown strong potential in complex reasoning tasks, but their performance often degrades, resulting in hallucinations, errors, and logical inconsistencies. |
| Approach: | They propose a framework that integrates multiple reasoning strategies to expand the reasoning space and a dynamic strategy selection mechanism that adapts to the task context. |
| Outcome: | The proposed framework outperforms existing state-of-the-art methods on a set of reasoning benchmarks. |
ProofInfer: Generating Proof via Iterative Hierarchical Inference (2022.emnlp-main)
Copied to clipboard
| Challenge: | Existing proof generation models focus on generating several proof paths instead of a whole tree. |
| Approach: | They propose a method that generates the proof tree via iterative hierarchical inference . they propose coding the proof as plain text without losing structure information . |
| Outcome: | The proposed proof generation model significantly improves performance on widely-used datasets. |
Diffusion Language Model Inference with Monte Carlo Tree Search (2026.findings-eacl)
Copied to clipboard
Zheng Huang, Kiran Ramnath, Yueyan Chen, Aosong Feng, Sangmin Woo, Balasubramaniam Srinivasan, Zhichao Xu, Kang Zhou, Shuai Wang, Haibo Ding, Lin Lee Cheong
| Challenge: | Existing methods for inference use heuristics to determine which positions to unmask and which tokens to commit . MEDAL is an inference-time scaling framework that integrates Monte Carlo Tree SEarch initialization for Diffusion Language Model inference. |
| Approach: | They propose a framework that integrates Monte Carlo Tree SEarch initialization for Diffusion Language Model inference. |
| Outcome: | The proposed framework achieves 22.0% improvement over existing inference strategies across multiple benchmarks. |
Dynamic Parallel Tree Search for Efficient LLM Reasoning (2025.acl-long)
Copied to clipboard
Yifu Ding, Wentao Jiang, Shunyu Liu, Yongcheng Jing, Jinyang Guo, Yingjie Wang, Jing Zhang, Zengmao Wang, Ziwei Liu, Bo Du, Xianglong Liu, Dacheng Tao
| Challenge: | Recent methods focus on search accuracy while overlooking computational efficiency. |
| Approach: | They propose a parallelism framework that dynamically optimizes reasoning path in inference. |
| Outcome: | The proposed framework improves efficiency by 2-4 on average while maintaining or even surpassing existing reasoning algorithms in accuracy. |