谷歌深度思维公司推出一个能证明复杂数学理论的AI系统，并将该系统命名为AlphaProof，该系统在2024年国际数学奥林匹克竞赛（IMO）中取得了相当于银牌的成绩。该公司11月13日在《自然》发表了相关研究成果。

数学家利用计算工具解决复杂问题、证明理论。AI系统则可以加速这一过程。虽然一些大语言模型在能力上很有潜力，但我们很难验证它们推理的正确性，因为它们是用非正式的自然语言文本进行训练和操作的。谷歌深度思维的研究人员演示了如何让增强学习在一个正式数学软件环境（名为Lean）中工作，从而生成推理过程能被自动验证的证明，有望克服上述挑战。

AlphaProof为证明数学命题而设计。该系统在对8000万个命题进行自动形式化后，通过增强学习找出这些证明方法。该系统被证明能提升之前先进AI系统在既往数学竞赛问题上的结果。2024年，AlphaProof解出了IMO的复杂问题，IMO是一项权威的高中水平数学竞赛。AlphaProof联合名为AlphaGeometry的几何解题系统，解出了6个竞赛问题中的4个，取得了相当于银牌水平的高分。

虽然AlphaProof在竞赛级数学推理领域的表现令人惊艳，但研究者指出，它在求解其他形式难题上仍存在一些局限性，并建议将其作为未来的研究方向。他们总结道，克服这些局限将使AlphaProof成为一个重要的复杂数学问题解题工具。

相关论文信息：

https://doi.org/10.1038/s41586-025-09833-y