Solving Formal Math Problems by Decomposition and Iterative Reflection
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , , , , , , , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909712062087168 |
|---|---|
| author | Zhou, Yichi Zhao, Jianqiu Zhang, Yongxin Wang, Bohan Wang, Siran Chen, Luoxin Wang, Jiahui Chen, Haowei Jie, Allan Zhang, Xinbo Wang, Haocheng Trung, Luong Ye, Rong Hoang, Phan Nhat Zhang, Huishuai Sun, Peng Li, Hang |
| author_facet | Zhou, Yichi Zhao, Jianqiu Zhang, Yongxin Wang, Bohan Wang, Siran Chen, Luoxin Wang, Jiahui Chen, Haowei Jie, Allan Zhang, Xinbo Wang, Haocheng Trung, Luong Ye, Rong Hoang, Phan Nhat Zhang, Huishuai Sun, Peng Li, Hang |
| contents | General-purpose Large Language Models (LLMs) have achieved remarkable success in intelligence, performing comparably to human experts on complex reasoning tasks such as coding and mathematical reasoning. However, generating formal proofs in specialized languages like Lean 4 remains a significant challenge for these models, limiting their application in complex theorem proving and automated verification. Current approaches typically require specializing models through fine-tuning on dedicated formal corpora, incurring high costs for data collection and training. In this work, we introduce \textbf{Delta Prover}, an agent-based framework that orchestrates the interaction between a general-purpose LLM and the Lean 4 proof environment. Delta Prover leverages the reflection and reasoning capabilities of general-purpose LLMs to interactively construct formal proofs in Lean 4, circumventing the need for model specialization. At its core, the agent integrates two novel, interdependent components: an algorithmic framework for reflective decomposition and iterative proof repair, and a custom Domain-Specific Language (DSL) built upon Lean 4 for streamlined subproblem management. \textbf{Delta Prover achieves a state-of-the-art 95.9\% success rate on the miniF2F-test benchmark, surpassing all existing approaches, including those requiring model specialization.} Furthermore, Delta Prover exhibits a significantly stronger test-time scaling law compared to standard Best-of-N proof strategies. Crucially, our findings demonstrate that general-purpose LLMs, when guided by an effective agentic structure, possess substantial untapped theorem-proving capabilities. This presents a computationally efficient alternative to specialized models for robust automated reasoning in formal environments. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2507_15225 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Solving Formal Math Problems by Decomposition and Iterative Reflection Zhou, Yichi Zhao, Jianqiu Zhang, Yongxin Wang, Bohan Wang, Siran Chen, Luoxin Wang, Jiahui Chen, Haowei Jie, Allan Zhang, Xinbo Wang, Haocheng Trung, Luong Ye, Rong Hoang, Phan Nhat Zhang, Huishuai Sun, Peng Li, Hang Artificial Intelligence Machine Learning Logic in Computer Science General-purpose Large Language Models (LLMs) have achieved remarkable success in intelligence, performing comparably to human experts on complex reasoning tasks such as coding and mathematical reasoning. However, generating formal proofs in specialized languages like Lean 4 remains a significant challenge for these models, limiting their application in complex theorem proving and automated verification. Current approaches typically require specializing models through fine-tuning on dedicated formal corpora, incurring high costs for data collection and training. In this work, we introduce \textbf{Delta Prover}, an agent-based framework that orchestrates the interaction between a general-purpose LLM and the Lean 4 proof environment. Delta Prover leverages the reflection and reasoning capabilities of general-purpose LLMs to interactively construct formal proofs in Lean 4, circumventing the need for model specialization. At its core, the agent integrates two novel, interdependent components: an algorithmic framework for reflective decomposition and iterative proof repair, and a custom Domain-Specific Language (DSL) built upon Lean 4 for streamlined subproblem management. \textbf{Delta Prover achieves a state-of-the-art 95.9\% success rate on the miniF2F-test benchmark, surpassing all existing approaches, including those requiring model specialization.} Furthermore, Delta Prover exhibits a significantly stronger test-time scaling law compared to standard Best-of-N proof strategies. Crucially, our findings demonstrate that general-purpose LLMs, when guided by an effective agentic structure, possess substantial untapped theorem-proving capabilities. This presents a computationally efficient alternative to specialized models for robust automated reasoning in formal environments. |
| title | Solving Formal Math Problems by Decomposition and Iterative Reflection |
| topic | Artificial Intelligence Machine Learning Logic in Computer Science |
| url | https://arxiv.org/abs/2507.15225 |