深度思维正式推出“数学做题家AI” 其在奥赛中取得相当于银牌的成绩

尽管AlphaProof在竞赛级数学推理方面展现出惊人能力，但团队坦承其目前仍存在局限，例如在处理某 些非标准或高度抽象的数学问题时表现不足。他们指出，未来的研究应聚焦于拓展系统的通用性和适应 性。一旦这些障碍被克服，AlphaProof有望成为协助数学家攻克复杂数学难题的有力工具，推动形式化 证明与AI的深度融合。 《自然》杂志12日发表了一项重要成果：英国深度思维正式推出其开发的"数学做题家AI"AlphaProof， 其成功证明了复杂的数学定理，并在2024年国际数学奥林匹克竞赛（IMO）中取得了相当于银牌的优异 成绩。这项研究展示了AI在高难度数学推理领域的显著进步。 目前，许多大型语言模型虽然具备强大的生成能力，却难以验证其推理是否正确，因为它们通常基于非 正式的自然语言进行训练和输出，缺乏严格的逻辑结构。为应对这一挑战，深度思维团队将强化学习引 入一个名为Lean的正式数学证明环境，在该系统中，所有推理步骤都必须符合形式化逻辑规则，从而能 够被自动验证。 AlphaProof是专为证明数学命题而设计的系统。团队首先对约8000万个数学命题进行了自动形式化处 理，随后利用强化学习让AlphaProo ...