潘禺：今年有另一场更值得关注的数学竞赛

　　AI的数学能力

　　ChatGPT这样的大语言模型在简单的算术计算上会犯错，因为模型并不是从基本原理推导出答案，而是根据输入猜测最可能的输出，这种方法有时候并不奏效。GPT-4的研究人员测试了数百道国际数学奥林匹克（IMO）级别的问题，成功率只有1%，只有一个被简化后的特定问题答对了。大型语言模型在生成回答时依赖于训练数据中学习到的模式，尽管训练数据集非常庞大，但它们可能不包含足够的逻辑推理或数学证明的示例。

　　DeepMind的AlphaProof和AlphaGeometry 2这两个更专门的系统，这次的表现就好得多。

　　AlphaProof是用于形式化数学推理的系统，结合了预训练的语言模型和AlphaZero强化学习算法，也就是之前自学掌握了国际象棋、将棋和围棋的算法。它在Lean中训练自己证明数学陈述，并通过自动将自然语言陈述翻译成形式化的数学语言陈述，创建了一个不同难度的形式化问题库。AlphaProof通过在Lean中搜索可能的证明步骤来生成候选解决方案，然后证明或反驳它们。在IMO比赛前几周内，它证明或反驳了数百万问题进行自我训练，涵盖不同的难度和广泛的数学领域。

　　AlphaGeometry是一个神经符号系统，由神经语言模型和符号推导引擎组成，它们协同工作以查找复杂几何定理的证明。一个系统提供快速、 “直观 ”的想法，而另一个系统则提供更深思熟虑、更理性的决策。

　　语言模型擅长识别数据中的一般模式和关系，可以快速预测可能有用的结构，但通常缺乏严格推理或解释其决策的能力。符号推导引擎基于形式逻辑，并使用明确的规则来得出结论，但缓慢而不灵活。语言模型指导符号推导引擎寻找几何问题的可能解决方案，从无限的可能性中预测哪些像点、线或圆这样的新几何结构最有用。如果未找到解决方案，语言模型将添加一个可能有用的结构，为符号引擎开辟新的推导路径。此循环一直持续，直到找到解决方案。

　　这有点像诺贝尔经济学奖得主丹尼尔·卡尼曼在《思考，快和慢》一书中提出的人类思维的两种系统，快速思考系统是一种快速、直觉式的思维方式，慢速思考系统是一种缓慢、逻辑性强、需要集中注意力的思维方式。

　　AlphaGeometry 2采用的符号引擎比上一代快两个数量级。当遇到新问题时，使用一种新的知识共享机制来实现不同搜索树的高级组合，以解决更复杂的问题。在今年的比赛之前，AlphaGeometry 2可以解决过去25年中83%的历史IMO几何问题，而上一代为53%。在今年的IMO 2024中，AlphaGeometry 2在收到形式化后的问题后，19秒内解决了第4题（下图，要求证明∠KIL 和 ∠XPY 之和等于 180°，AlphaGeometry 2 提议构造 E，即 BI上的一个点，使 ∠AEB = 90°）。