arXiv:2505.05758v2 宣告类型: 修改 摘要: 正式推理和自动定理证明是机器学习的一个具有挑战性的子领域，在这个领域中，机器使用形式语言（如Lean）来证明数学定理。形式验证系统几乎可以瞬时检查一个形式证明是否正确，但使用大型语言模型（LLMs）生成一个完全正确的形式证明仍然是一个艰巨的任务。文献中通常的做法是多次提示LLM（多达几千次），直到其中一个生成的证明通过验证系统。在本文中，我们介绍了APOLLO（Automated PrOof repair via LLM and Lean cOllaboration，通过LLM和Lean协作进行自动证明修复）模块化、模型无感知的管道，该管道结合了Lean编译器的优势和LLM的推理能力，以实现更低采样预算下的更佳证明生成效果。Apollo指导一个完全自动化的过程，在此过程中，LLM为定理生成证明，一组代理分析证明、修正语法错误、使用Lean识别证明中的错误、隔离失败的子引理、利用自动化求解器，并以低Top-K预算在每个剩余的目标上调用LLM。修复的子证明被重新组合和重新验证，迭代到用户控制的最大尝试次数。在miniF2F基准测试中，我们在7B参数模型中建立了75.0%的新最高精度，同时保持采样预算低于一千。此外，Apollo将Goedel-Prover-SFT的最高精度从65.6%提高到从25,600减少到几百个样本。通用模型（o3-mini, o4-mini）的精度从3-7%提高到超过40%。我们的结果表明，面向特定目标、由编译器引导的LLM输出修复能够显著提高效率和正确性，这表明一种大规模自动定理证明的通用范式。