Prover Agent: An Agent-based Framework for Formal Mathematical Proofs

我们提出了 Prover Agent，这是一种用于自动定理证明的新型人工智能代理系统，它将大语言模型（LLMs）与形式化证明助手 Lean 相结合。Prover Agent 协调一个进行非形式化推理的语言模型、一个形式化证明模型，以及来自 Lean 的反馈，同时还能生成辅助引理，以帮助发现整体的证明策略。该系统在 MiniF2F 基准测试中达到了 86.1% 的成功率，在使用小型语言模型（SLMs）的方法中树立了新的最先进水平，并且相比之前的方法所需样本数量要少得多。我们还提供了案例研究，说明这些生成的引理是如何帮助解决具有挑战性的问题的。

论文试图解决自动化定理证明中的一个核心问题：如何有效结合大型语言模型（LLMs）与形式化证明助手（如Lean），以提高在数学定理证明任务上的成功率。这个问题是当前AI和形式化验证交叉领域的一个重要且具有挑战性的问题。

论文的关键思路是提出一种名为Prover Agent的AI代理，它通过协调非正式推理的语言模型、形式化证明模型以及来自Lean系统的反馈，动态生成辅助引理来构建整体证明策略。这一方法的新意在于将多组件协同机制引入定理证明系统，并利用小模型实现高效推理，显著降低了样本预算。

{在MiniF2F基准上取得了86.1%的成功率，成为使用小型语言模型（SLMs）方法中的新SOTA。,通过案例研究展示了生成的辅助引理在解决复杂问题中的关键作用。,相比之前的LLM驱动定理证明方法，样本使用效率更高，显示出更强的实际应用潜力。,未来值得深入的方向包括优化引理生成机制、增强与证明助手的交互策略，以及探索更多形式化数据的应用。}

{"Towards Understanding and Mitigating the Impact of Finite Sampling in Theorem Proving","Lean Together: An Integrated System for Reading, Writing, and Executing Formal Mathematics","Language Models are Few-Shot Learners (GPT-3 Paper)","Proof Artifact Co-training for Theorem Proving with Language Models","AlphaGeometry: A Symbolic Reasoning Engine for Geometry Problem Solving"}