用AI自动生成辅助引理，提升数学定理证明效率。
Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs
- 结合大模型与形式化工具，动态生成有用辅助引理。
- 在MiniF2F上达88.1%成功率，PutnamBench解决25题。
- 适合对自动化证明感兴趣的研究者与工具开发者。
我们提出Prover Agent，一种基于AI代理的自动化定理证明框架，将大语言模型（LLMs）与形式化证明工具Lean相结合。该框架协调非正式推理的LLM、形式化证明模型以及Lean的反馈，同时自动生成辅助引理。这些引理不仅限于形式证明中的子目标，还可包括从假设中推导出的特殊情形或潜在有用的命题，有助于发现可行的证明策略。在MiniF2F基准上达到88.1%的成功率，并在PutnamBench上解决25个问题，所用样本预算小于此前方法，在使用小语言模型（SLMs）的方法中创下新纪录。我们还提供了理论分析与案例研究，说明生成引理如何助力解决复杂问题。代码已公开于https://github.com/kAIto47802/Prover-Agent。
原文摘要 · Abstract (English)
We present Prover Agent, a novel AI agent for automated theorem proving that integrates large language models (LLMs) with a formal proof assistant, Lean. Prover Agent coordinates an informal reasoning LLM, a formal prover model, and feedback from Lean while also generating auxiliary lemmas. These auxiliary lemmas are not limited to subgoals in the formal proof but can also include special cases or potentially useful facts derived from the assumptions, which help in discovering a viable proof strategy. It achieves an 88.1% success rate on MiniF2F and solves 25 problems on the PutnamBench with a smaller sample budget than previous approaches, establishing a new state-of-the-art on both benchmarks among methods using small language models (SLMs). We also present theoretical analyses and case studies that illustrate how these generated lemmas contribute to solving challenging problems. Our code is publicly available at https://github.com/kAIto47802/Prover-Agent.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。