DeepMind发布AlphaProof：数学证明AI的里程碑

谷歌DeepMind最新发布的IMO金牌模型，以其全面公开的技术细节引起了广泛关注！

遵循DeepMind一贯的命名传统，这款模型被命名为：AlphaProof。

通过Nature期刊，AlphaProof的完整论文得以公开，首次详细披露了其背后的技术架构和训练方法。值得一提的是，无师自通的围棋AI AlphaZero也在论文中被多次提及。

作者Tom Zahavy借此机会分享了一些开发过程中的关键细节：

AlphaProof团队规模相对较小，大部分时间只有大约10人，临近IMO比赛时人员才有所增加。

真正推动突破的核心团队成员是IMO金牌得主Miklós Horváth。

他提出了一种方法，创建AI正在处理问题的各种变体，并将它们作为初始状态，让智能体在这些变体上进行训练。

在长达一年的时间里，这个团队探索了各种研究思路，虽然很多都失败了，但成功的都被整合到了AlphaProof系统中，现在全面公开。

将数学证明视为一种游戏

AlphaProof的核心思路非常直接：将数学证明过程转变为一个可以反复训练的游戏。

系统基于Lean定理证明器构建了一个强化学习环境。在这个环境中，每个数学命题都是一个新的游戏关卡，AI需要通过选择合适的策略（如战术）来推进证明。

如果某个策略成功，就会得到新的子目标；如果所有目标都完成了，就意味着证明完成。

论文显示，AlphaProof使用了一个拥有30亿参数的编码器-解码器transformer模型作为其核心。

这个证明网络不仅要理解当前的证明状态，还要同时输出两个关键信息：

一是建议接下来尝试哪些策略，二是估计完成证明还需要多少步。

这种设计让系统能够更智能地分配计算资源，优先探索最有希望的证明路径。

...（中间部分保持不变）