【AI系统在国际数学奥林匹克竞赛中获得银牌级成绩

国际数学奥林匹克竞赛（IMO）是历史最悠久、规模最大、最负盛名的年轻数学家竞赛。每年，各国都会派出顶尖的年轻数学家参加为期两天、包含六道题目的考试。几年前，数学AI系统很幸运能够解决过去IMO问题中的1%。今年，@头秃搞学习 构建了一个系统来解决今年的IMO问题，这个系统结合了两个系统：改进版的AlphaGeometry 2和基于强化学习的新系统AlphaProof，用于形式化数学推理。

结果如何？在竞赛周期间，这个系统成功解决了今年IMO考试的6道题目中的4道，取得了28分的成绩（每道题目7分），达到了IMO银牌水平的上限（今年的IMO中有609名参赛者中有58人达到了该水平）。
AlphaProof使用了经过微调的Gemini模型自动将自然语言问题陈述翻译成形式陈述，创建了一个难度不一的大量形式问题库。在比赛前的几周内，它通过证明或反驳数百万个问题，涵盖了各种难度和数学主题区域，学习了解决类似IMO的问题。

“这个程序能够提出如此非显而易见的构建方式，非常令人印象深刻，远超我所认为的当前技术水平。”
—— Timothy Gowers 教授，IMO金牌得主，菲尔兹奖获得者

以下是6道题目中的第4题，一个AlphaGeometry在收到形式化后19秒解决的几何问题：

这代表了AI系统在正确执行复杂数学推理方面的重大进步，达到了世界顶尖年轻数学家的水平。我们对未来充满期待，在这个未来中，数学家与AI工具合作，探索假设，尝试解决长期问题的新大胆方法，并快速完成证明的耗时部分——而像Gemini这样的AI系统在数学和更广泛的推理方面将变得更加强大。

详情请参见以下博客文章：
https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/】