基于引导树搜索的奥数几何命题与求解
人工智能
2024-12-17 v1 机器学习
摘要
数学奥林匹克是享有盛誉的竞赛，其命题与求解备受推崇。构建能够命题和求解奥数的人工智能是自动定理发现与证明中尚未解决的挑战，尤其在几何领域，因其兼具数值与空间元素而尤为困难。我们提出了 TongGeometry，一个支持基于树搜索的引导式命题与求解的欧几里得几何系统。该高效几何系统建立了迄今为止最广泛的几何定理库：在与现有最先进方法相同的计算预算下，TongGeometry 发现了 67 亿条需要辅助构造的几何定理，其中 41 亿条展现出几何对称性。其中，10 条定理被提交至区域数学奥林匹克，3 条被真实竞赛选中，获得中国和美国全国团队选拔赛或顶级公民奥赛的入围资格。在微调大语言模型的引导下，TongGeometry 解决了国际数学奥林匹克几何部分（IMO-AG-30）的所有问题，首次超越了金牌得主。它还在更广泛的奥数级别问题上超越了现有最先进方法。该系统的全部能力可在消费级机器上运行，使模型更具可及性并促进其广泛普及。类比而言，与现有仅像学生一样解题的系统不同，TongGeometry 扮演的是几何教练的角色，发现、呈现并证明定理。
引用
@article{arxiv.2412.10673,
title = {Proposing and solving olympiad geometry with guided tree search},
author = {Chi Zhang and Jiajun Song and Siyu Li and Yitao Liang and Yuxi Ma and Wei Wang and Yixin Zhu and Song-Chun Zhu},
journal= {arXiv preprint arXiv:2412.10673},
year = {2024}
}