AlphaGeometry2 (AG2) 全面总结

主要观点

Google DeepMind 推出的 AlphaGeometry2 (AG2) 在解决过去25年国际数学奥林匹克（IMO）几何问题中表现优异，成功解决了84%的问题，超过了人类金牌得主的平均表现（约41题）。相较于前代模型 AlphaGeometry (AG1)（解决率为54%），AG2 在性能上实现了显著提升。

关键信息

1. 模型架构与改进：

   • AG2 使用基于 Gemini 的更强大语言模型（LLM），将自然语言问题转化为形式化语言。
   • 采用 符号演绎引擎（Deductive Database Arithmetic Reasoning, DDAR）生成证明。
   • 如果 DDAR 无法找到证明，AG2 会结合语言模型和树搜索算法生成 辅助构造，并重新运行 DDAR，直到找到证明。

2. 性能表现：

   • AG2 解决了2000年至2024年50道 IMO 几何问题中的42道（84%）。
   • 旗舰商业推理 LLM（如 OpenAI 的 o1 和 Gemini Thinking）无法解决任何 IMO 几何问题。

3. 局限性：

   • AG2 尚未解决所有 IMO 和 IMO 短列表问题。
   • 形式化语言覆盖了88%的 IMO 问题，其余问题 AG2 不会尝试解决。

4. 未来改进方向：

   • 将问题分解为子问题，并应用强化学习方法。
   • 通过更多形式化示例和监督微调，进一步改进自动形式化能力。

重要细节

1. 形式化语言：

   • AG2 使用特定领域的谓词描述问题，例如 acompute a b c d 表示“求 AB 和 CD 之间的角”。

2. 自然语言到形式化语言的转换：

   • 使用 Gemini LLM 进行少样本提示（few-shot prompting），提示中包含“几十个”问题翻译示例。
   • 在较简单问题上，这种方法“非常一致且几乎不出错”。

3. 社区反馈：

   • 伯克利计算机科学博士生 Yuxi Liu 指出，AG2 具有“1950年代自动定理证明”的风格，依赖于手工设计的表示语言和逻辑推理引擎。
   • 牛津大学机器学习研究员 Simon Frieder 提到，AG2 和 TongGeometry 是封闭系统，无法与开源系统 Newclid 进行直接比较。

4. 代码可用性：

   • AG2 代码尚未公开，但 AG1 的代码已在 GitHub 上开源。

总结

AlphaGeometry2 在解决国际数学奥林匹克几何问题上展现了强大的能力，但仍存在改进空间。通过结合更强大的语言模型和符号推理引擎，AG2 在自动形式化和问题求解方面取得了显著进展。然而，其封闭性和对特定形式化语言的依赖也引发了一些学术界的讨论。