arXiv:2505.05758v1 宣告类型: 新 摘 要: 形式推理和自动定理证明是机器学习的一个具有挑战性的子领域，在该领域中，机器使用如Lean这样的形式语言来证明数学定理。形式验证系统几乎可以瞬时检查一个形式证明是否正确，但用大规模语言模型（LLMs）生成完全正确的形式证明仍然是一项艰巨的任务。文献中通常的方法是多次（多达数千次）提示LLM，直到其中一个生成的证明通过验证系统。在这项工作中，我们提出了APOLLO（Automated PrOof repair via LLM and Lean cOllaboration），一个模块化、模型无关的管道，结合了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输出的靶向修复在效率和正确性方面带来了巨大的增益，表明了一种可扩展的自动定理证明的一般范式。