通过形式验证自动解决猜想

大语言模型 的最新进展显着提高了他们执行数学推理的能力，从解决基本问题扩展到解决研究级问题的能力越来越强。然而，由于自然语言推理固有的模糊性，可靠地解决和验证此类问题仍然具有挑战性。在本文中，我们提出了一种自动化框架，将自然语言推理与形式验证相结合，以解决研究级数学问题。我们的框架由两个组件组成：非正式推理代理 Rethlas 和正式验证代理 Archon。 Rethlas 将推理原语与我们的定理搜索引擎 Matlas 相结合，以探索解决方案策略并构建候选证明。 Archon 配备了 LeanSearch，通过任务分解、迭代细化和自动证明合成，将非正式论证转化为形式化的 Lean 4 项目，确保机器可检查的正确性。使用这个框架，我们解决了交换代数中的一个开放问题，并在 Lean 4 中正式验证了所得的证明，基本上不需要人工参与。其他案例研究说明了 Rethlas 在非正式数学推理和发现方面的能力，以及 Archon 在 Lean 4 中形式化研究级证明的能力。我们的实验表明，强大的定理检索工具能够发现和应用跨领域数学技术，而形式代理可以自主填补非正式论证中的重要空白。更广泛地说，我们的工作展示了一种有前途的数学研究范式，其中配备定理检索工具的非正式和正式推理系统协同运行以产生可验证的结果，减少人类工作量并支持人类与人工智能协作数学研究。