谷歌旗下的AI研究机构DeepMind和纽约大学的研究人员联合开发了一个AI模型——AlphaGeometry。

AlphaGeometr是一种神经符号模型,内置了大语言模型和符号推理引擎等功能,主要用于解决各种超难几何数学题，同时可以自动生成易于查看的解题原理。

为了验证AlphaGeometr的性能，研究人员使用了正规国际奥数比赛的规则对其进行测试。

结果显示，AlphaGeometry 在官方奥林匹克竞赛时间限制下正确解决了，30道题中的25 道，接近人类金牌得主的25.9道。

而之前最先进的模型只能解决30道中的10道题。AlphaGeometry成为目前功能最强的解决几何难题模型。

论文地址：https://www.nature.com/articles/s41586-023-06747-5?ref=maginative.com

AlphaGeometry的核心技术创新在于，破除了定理证明，对人类证明示例数据的严重依赖。

数学定理证明一直是检验逻辑思维和问题求解能力的关键任务，一直是AI研究的重要方向。尽管当前机器学习方法在许多领域取得长足进步,但是面对大部分数学任务仍然束手无策。

主要原因是，翻译人类证明样本到机器可验证的格式是极其耗时、耗力的，这在几何证明中尤其突出,翻译难度加大导致了严重的数据稀缺。

AlphaGeometry通过大规模随机生成几何定理和相应的证明，来解决数据稀疏的问题,产生了上亿组训练数据。

具体来说,AlphaGeometry 首先使用图形构建语言随机生成大量候选定理陈述,然后利用符号演绎引擎(如演绎数据库 DD)推导出所有可能的新结论,递归地回溯每个新结论所依赖的前提,提取出最小依赖集作为该定理的证明。

为了扩大证明的范围,除了纯符号演绎,该方法还通过代数推理引擎新增了许多依赖代数操作的证明步骤。最终，得到了大约1亿组合成的定理证明训练数据。

在获得大规模训练数据后,AlphaGeometry使用 Transformer 大语言模型进行预训练,学习预测证明的序列。

此外,它还进行了针对性微调,集中优化辅助构造的生成。以解决几何证明中一个关键难题,定理证明中的外生项生成问题。

在实际应用时,AlphaGeometry采用了交互式的神经符号框架。简单来说,大语言模型会首先生成一组辅助构造候选,然后符号引擎基于新构造判断定理是否得证。

如果仍未成功,则迭代上述流程,语言模型会在更丰富的上下文中生成新的辅助构造候选。

这个框架设计的非常巧妙,大语言模型负责开拓解空间,提出新的假设,而符号引擎则保证精确正确的推理。完美地结合神经网络的创造力和符号系统的解释性、精确性。

AlphaGeometry基本解决了几何定理证明领域数据稀疏的关键难题,开创了不依赖人类证明示例、利用合成数据训练AI模型的创新方法。

本文素材来源AlphaGeometry论文，如有侵权请联系删除