Lyra：在自动定理证明中协同双阶段纠错

大型语言模型（Large Language Models, LLMs）为形式化定理证明领域开辟了一个极具前景的研究方向。然而，其在缓解幻觉现象（hallucinations）以及通过定理证明器的错误信息进行迭代优化等方面的潜力，尚未得到充分探索。为提升LLMs在该领域的实际效能，本文提出一种名为Lyra的新框架，该框架引入两种独立的纠错机制：工具纠错（Tool Correction, TC）与猜想纠错（Conjecture Correction, CC）。在形式化证明的后处理阶段，工具纠错机制利用先验知识，调用预定义的定理证明工具（如Sledgehammer）来识别并替换不正确的工具调用。该机制显著降低了模型生成过程中的幻觉现象，从而有效提升了证明的整体准确性。此外，本文提出猜想纠错机制，这是一种基于证明器错误反馈的交互式优化方法，能够根据定理证明器返回的错误信息，动态调整形式化证明中的子目标（subgoals），实现对生成内容的精细化修正。与以往的修正框架相比，所提出的猜想纠错机制在不依赖成对的（生成结果，错误信息，修正结果）提示数据的前提下，通过指令引导完成生成内容的优化。在miniF2F数据集上的实验表明，Lyra在验证集上的表现从48.0%提升至55.3%，在测试集上的准确率从45.5%提升至51.2%，达到了当前最优（SOTA）水平。此外，本文还展示了Lyra成功解决的三道国际数学奥林匹克（IMO）竞赛题目。综上所述，我们认为工具纠错（通过后处理手段抑制幻觉）与猜想纠错（通过与环境交互实现子目标调整）为未来形式化定理证明领域中大模型的应用提供了极具潜力的研究方向。