Trieu H. Trinh（纽约大学及Google DeepMind）、Yuhuai Wu、Quoc V. Le、He He、Thang Luong（Google DeepMind）等人在 Nature 期刊第625卷（2024年1月18日出版）上发表了一项关于无需人类解题示范即可求解奥林匹克几何问题的研究。该文题为“Solving olympiad geometry without human demonstrations”，报告了一种名为AlphaGeometry的神经符号系统，该系统通过大规模合成定理与证明数据训练语言模型，并结合符号演绎引擎，在国际数学奥林匹克（IMO）几何问题上取得了接近金牌选手的水平。以下从研究背景、工作流程、主要结果、结论、亮点及附加内容等方面对该研究进行详细介绍。
数学定理证明长期被视为人工智能领域的重要挑战，尤其是在奥林匹克级别的几何问题中，其难度不仅体现在逻辑推理的深度，还体现在辅助构造（auxiliary construction）所带来的无限分支搜索空间。传统的机器学习方法依赖于将人类证明转换为机器可验证的格式，但几何领域因翻译困难导致训练数据极度稀缺。几何问题在通用数学语言（如Lean）中缺乏足够的证明示例，而几何专用语言又因表达范围过窄无法覆盖复数、代数等人类常用的证明工具。因此，现有几何证明方法主要依赖符号方法和人工设计的搜索启发式规则，性能提升受限。
本研究的目标是突破数据瓶颈，提出一种无需人类证明示范的定理证明方法。作者聚焦于欧几里得平面几何，排除几何不等式和组合几何等主题，利用大规模合成数据训练神经语言模型，以指导符号演绎引擎在证明搜索中处理辅助构造这一关键难题。
研究的第一阶段是合成数据的生成。作者首先从一组随机定理前提（premises）中采样，构建了接近十亿个前提集合。这些前提的构造动作包括创建共线点、内心/外心、以及带参数的构造（例如给定角度α，构造点X使∠ABX=α）等。采样过程高度并行化，且不使用任何人类设计的问题集。
随后，作者使用符号演绎引擎——演绎数据库（deductive database, DD）结合代数推理（algebraic reasoning, AR）——对采样前提进行演绎。DD基于确定子句形式的几何规则推理新语句，而AR则通过高斯消元等方法进行角度、比例和距离的代数推导。DD+AR的结合是本研究在符号推理上的新贡献，代表了当前几何符号推理的最高水平。该引擎输出一个有向无环图，其中每个节点代表一个可推导的结论，边连接其父节点。通过回溯算法（traceback algorithm），可以从任一结论节点n回溯得到其依赖子图g(n)，其叶节点构成最小前提集p。由此生成合成训练样本（前提，结论，证明）=（p, n, g(n)）。
仅有DD+AR生成的证明受限于符号引擎的可达范围。为解决奥林匹克级别问题中的辅助构造，作者引入了“依赖差异”（dependency difference）的概念。在回溯过程中，如果结论n独立于前提p中的某些对象，则这些对象被识别为依赖差异，并从p中移除，转而作为证明中的辅助构造步骤。这一机制使生成模型能够学习构造新的点或线，从而扩展搜索空间。辅助构造是定理证明中“外生项生成”的典型实例，也是几何证明自1959年以来长期未解的核心挑战。通过这种方式，研究成功生成了近千万条涉及辅助构造的合成证明步骤，远超纯符号演绎的能力。
作者将合成数据序列化为“<前提><结论><证明>”的文本字符串，用于训练Transformer语言模型。该模型首先在所有一亿条合成证明上进行预训练，然后在约九百万条涉及辅助构造的证明（约占总数据9%）上进行微调，以专注于辅助构造生成。
在证明搜索阶段，语言模型与符号引擎交替运行。语言模型根据问题陈述和已有构造生成一条辅助构造（如“构造点X使ABCX为平行四边形”），随后符号引擎接收新输入并扩展演绎闭包。搜索采用集束搜索（beam search），束宽k=512，最大迭代次数16，每个节点的解码批大小为32。该设置可并行化，显著提高搜索效率。
研究构建了IMO-AG-30基准，包含30个自2000年以来可转化为该几何环境的IMO经典几何问题。该基准排除几何不等式和组合几何问题，约75%的非组合几何问题可被表示。评估中还比较了多种基线方法，包括吴方法（Wu’s method）、Gröbner基法、全角法、演绎数据库DD、以及DD+AR+人工启发式等。此外，还测试了GPT-4单独和与DD+AR结合的效果。
在IMO-AG-30上，AlphaGeometry解决了25个问题，远超之前最佳方法（吴方法）的10个问题，并接近IMO金牌选手平均表现（25.9题）。最强的符号基线DD+AR+人工启发式解决了18题，而GPT-4单独解题成功率为0%，即使结合DD+AR也仅解决15题。
消融研究表明，在DD基础上引入AR增加了7个已解决问题，使DD+AR达到14题；语言模型的辅助构造进一步增加11题，最终达到25题。使用仅20%的训练数据时，AlphaGeometry仍解决21题，优于所有基线；在测试时将束宽从512降至8（减少64倍）或将搜索深度从16降至2，AlphaGeometry仍各解决21题。
在更大的231个几何问题测试集上，AlphaGeometry解决了98.7%的问题，而吴方法解决75%，DD+AR+人工启发式解决92.2%。此外，AlphaGeometry解决了2000年和2015年IMO的所有几何问题，符合人类专家评估的满分标准，达到对应年份的奖牌线。在2004年IMO第1题上，AlphaGeometry通过回溯发现了一个未使用的前提，从而证明了该定理的一个更一般形式。
AlphaGeometry是首个在欧几里得平面几何证明中超越IMO平均选手的计算机程序，同时超越了基于计算机代数和搜索的强基线。该研究展示了一种神经符号方法：通过大规模合成数据训练语言模型，规避了对人类证明示例和人工策划问题集的依赖。其核心贡献在于利用依赖差异生成辅助构造训练信号，并有效结合语言模型与符号引擎。
该方法具有重要的科学价值和应用前景。科学上，它证明了在数据稀缺的数学领域，合成数据可以支持高性能定理证明模型的训练。应用上，该框架具有可迁移性。作者提出，只要具备领域对象定义、随机前提采样器、符号引擎及其回溯过程四个要素，即可将该方法应用于其他数学领域。此外，AlphaGeometry输出的证明可读性强，便于人类专家验证和学习。
研究发现，合成数据生成过程能够重新发现一些文献中已知的复杂定理和引理，同时因为不受人类审美偏见的约束，覆盖了更广泛的几何场景。此外，预训练对语言模型的辅助构造能力至关重要：无预训练仅解决21题，无微调则降至23题，说明预训练纯演绎证明有助于模型学习符号引擎的输出规律。
在可读性方面，AlphaGeometry的证明步骤低层级且冗长，与人类使用的高层定理和直觉存在差距。例如在IMO 2004 P1中，AlphaGeometry构造了点K来对称化MN，而人类直接使用现有点R；在IMO 2000 P6中，AlphaGeometry的证明超过100步且极为繁琐，而人类使用复数坐标可大幅简化。这些案例提示未来可引入更高层的演绎规则和定理以提升证明效率和可读性。
该研究在定理证明自动化领域迈出了重要一步，展示了合成数据与神经符号系统在解决高难度数学问题上的巨大潜力。