本报讯 一个名为AlphaProof的能证明复杂数学理论的人工智能（AI）系统，在2024年国际数学奥林匹克竞赛（IMO）中取得了相当于银牌的成绩。

数学家利用计算工具解决复杂问题、证明理论，AI系统则可以加速这一过程。虽然一些大语言模型很有潜力，但很难验证其推理正确性，因为它们是用非正式的自然语言文本进行训练和操作的。

在这项研究中，谷歌深度思维公司的研究人员演示了如何让增强学习在一个正式数学软件中工作，进而生成推理过程能被自动验证的证明。11月13日，相关研究成果发表于《自然》。

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

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

相关论文信息：

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