证明代理：一种基于代理的形式数学证明框架

于红博

摘要: 我们提出了Prover Agent，这是一种集成了大型语言模型（LLMs）与形式证明助手Lean的新型人工智能代理，用于自动定理证明。Prover Agent协调了一个非正式推理LLM、一个形式证明模型以及来自Lean的反馈，同时生成辅助引理。这些辅助引理不仅限于形式证明中的子目标，还可以包括从假设中推导出的特殊情况或潜在有用的事实，这有助于发现可行的证明策略。它在MiniF2F基准测试中实现了88.1%的成功率，建立了一种新的最先进方法，使用小型语言模型（SLMs）比以前的方法具有更低的样本预算。我们还提供了理论分析和案例研究，说明这些生成的引理如何有助于解决具有挑战性的问题。我们的代码可以在以下网址公开获取：https://github.com/kAIto47802/Prover-Agent。

更新时间: 2025-10-23 16:48:37

领域: cs.AI,cs.LG

下载: http://arxiv.org/abs/2506.19923v4