本节内容主要整理自 AITP 会议以及 Lean 社区相关的讨论。

AITP 与 LEAN 社区

自 2016 年以来，AITP（自动化定理证明）会议每年举办一届，与 IMO 相关报告包括：

• AITP 2024：Math Olympiad – to the geometry and beyond
• AITP 2020：The IMO Grand Challenge
• AITP 2018：Project Proposal: Who cares about Euclidean geometry?

此外，LEAN 的 Zulip 社区在数学形式化领域非常活跃，影响力大的工作都有相关讨论，比如今年的帖子：

1. OpenAI o1 模型：OpenAI “Learning to Reason with LLMs”
2. DeepMind IMO2024：IMO results from Google DeepMind
3. AI-MO：AI Math Olympiad Prize
4. 阿里巴巴数学竞赛 AI 赛道：Alibaba competition 2024 - AI track
5. DeepSeek：DeepSeek-Prover 和 DeepSeek-Prover-V1.2
6. IMO 频道：IMO Grand Challenge
7. 机器学习与自动证明 频道：Machine Learning for Theorem Proving

欧式几何

IMO 竞赛的四大题型包括几何、数论、代数和组合数学。这里的几何特指欧式几何，相关工作包括：

1. 上世纪 70 年代，吴文俊先生开创了机械定理证明，通过将几何问题代数化来实现自动定理证明。
2. 2000 年，Shang-Ching Chou 提出的合成推理方法，开发了 Deduction database 系统。
3. 2020 年，GeoLogic 由 Miroslav Olšák 开发，它是一个支持交互的逻辑核心系统，能够解决许多标准的高中几何问题。
4. 2024 年初，DeepMind 的 AlphaGeometry 系统解决了 IMO 30 道题中的 25 道。最新版本的 AlphaGeometry2 进一步提升，能够解决过去 25 年间 83% 的 IMO 几何题。

注：欧式几何在现代数学的实际应用很有限，现代数学家更关注庞加莱猜想、微分流形，代数几何等更复杂更抽象的几何空间，这些更加考验数学家的想象力、理解能力与推理能力。

IMO Grand Challenge

IMO Grand Challenge 是微软研究院在 AITP 2020 上提出的重大挑战，旨在构建一个能够在 IMO 比赛中赢得金牌的人工智能系统。

规则与评分标准：

1. F2F（Formal-to-Formal）：接收形式化的问题陈述，生成机器可检查的证明。
2. 评分：证明须在 10 分钟内通过 Lean 核心的验证，这个时间约等于人类裁判审核人类解答的时间。证明没有部分得分，要么全对，要么全错。
3. 资源限制：AI 参赛者拥有与人类相同的时间限制（每组三道题目需在 4.5 小时内完成），但可以使用无限的计算资源。
4. 可复现性要求：AI 必须在比赛开始前开源，并允许公众访问和复现。在比赛期间，AI 不能访问互联网。

该挑战的组织委员会由来自 OpenAI、微软、谷歌等机构的研究者组成，包括：

• Daniel Selsam（OpenAI）
• Leonardo de Moura（微软研究院）
• Kevin Buzzard（伦敦帝国理工学院）
• Reid Barton（匹兹堡大学）
• Percy Liang（斯坦福大学）
• Sarah Loos（谷歌 AI）
• Freek Wiedijk（奈梅亨大学）

2021 年 OpenAI 发布的 MiniF2F 基准与该挑战相关，以 F2F 的形式，扩展支持了更多的形式系统。

尽管 IMO Grand Challenge 为数学和 AI 社区提供了一个富有挑战性的任务，但遗憾的是，该项目目前并未设置奖项或表彰部分进展的机制。

AI-MO

2024 年 4 月，XTX Markets（一家金融科技公司）推出了人工智能数学奥林匹克奖（AI Math Olympiad Prize, AIMO），并设立了 1000 万美元的奖励基金，旨在推动开发一个能够在 IMO 中赢得金牌的公开共享的 AI 模型。

与 IMO Grand Challenge 的 F2F 模式不同，AIMO 采用的是 informal-to-informal 形式，赛题难度介于 AMC12 和 AIME 之间，每道题目的答案是 0 到 999 之间的整数，类似 AIME 的题目形式。

比赛内容：竞赛使用由专业题目设计团队创建的全新数据集，包含 110 道原创数学问题，难度从基础算术到高级代数和几何推理不等。题目被划分为三个部分：10 道“训练题”公开提供，50 道“测试题”用于评估提交质量（不公开），另有 50 道“验证题”决定最终排名（不公开）。这些问题都为原创，避免了数据泄露的风险。

评分形式：该竞赛在 Kaggle 平台上进行，详见 AI Mathematical Olympiad - Progress Prize 1。参赛者需使用官方提供的 Python API 进行评估，并按标准规范提交代码。

官方基准模型 Gemma 7B 在测试集和验证集上的通过率为 3/50。比赛的最佳成绩由 Numina 取得，该模型基于 DeepSeekMath-Base 7B 微调，结合自然语言与 Python REPL 解决数学问题，通过率达到 29/50。

第一阶段微调得到中间模型，第二阶段用工具集成推理的合成数据集，将问题分解为一系列基本原理、Python 程序及其输出。

Project-Numina 开放共享了模型代码，模型参数，以及由 86 万条数学问题构成的数据集 AI-MO/NuminaMath-CoT。完整技术报告可在 Kaggle 的讨论区中找到。

此外，可以在 AI-MO 提供的在线模型服务体验 Numina 模型的效果：

题解过程：COT + Python 代码 => 生成最后答案

注：该模型服务似乎下架了。

AlphaProof

与 AIMO 这类非形式化、只检验答案的竞赛不同，F2F（Formal-to-Formal）模式可能更能真正消除 AI 在数学推理中的幻觉。

比如前段时间大火的 OpenAI 的 o1 系列，其在 AIME 数据集上，从 GPT-4o 的 13% 准确率提升到 83%（cons@64），即使是 pass@1 的准确率也达到了 74.4%。

个人实测 o1-preivew 在 IMO2024 第一题的表现，相比于 GPT-4o，o1 模型在推理加持下确实能解答正确，但证明过程仍存在错误，关键步骤胡言乱语，蒙混过关。

相比之下，DeepMind 的工作在推理证明方面更加出色。今年的 IMO 比赛结束后，DeepMind 推出了 AlphaProof，一种用于形式数学推理的强化学习系统；同时发布了 AlphaGeometry2，几何求解系统 AlphaGeometry 的改进版本。凭借这两个系统，DeepMind 成功解决了今年 IMO 六道题中的四道（p1、p2、p4、p6），这意味着 AI 首次达到了与银牌最高分相当的水平。

更具体地，AlphaProof 在几分钟内解决了一道题，随后花费了三天时间解决了另外两道；而 AlphaGeometry2 在收到形式化命题后的 19 秒内解决了第四题。

技术原理：数据合成 + 强化学习 + 搜索

左侧：将大量非形式的数学问题通过“形式化网络”（微调的 Gemini 模型）翻译成形式数学语言。
右侧：使用“求解网络”来探索证明或反证，系统通过 AlphaZero 算法自我增强，从而能够解决越来越复杂的问题。每当系统找到一个新的证明，都会对模型进行强化，使其在处理后续问题时表现得更好。

DeepMind 并未具体说明 AlphaProof 几分钟内解决的是哪一道题。从题目难度来看，p1 是一道人类几分钟内就能解决的简单题目，但 AlphaProof 在这道题上构造了繁复的证明，反而 p2 的证明相对简洁，因此可能 p2 对 AlphaProof 来说更容易。关于 IMO 2024 的详细题解分析，稍后我们将进一步展开讨论。