TongGeometry：北大等推出的几何问题生成与求解系统

TongGeometry简介

TongGeometry是由北京通用人工智能研究院（BIGAI）和北京大学人工智能研究所联合开发的欧几里得几何问题生成与求解系统。该系统通过树搜索技术实现几何问题的自主提出和证明，建立了迄今为止最广泛的几何定理库，发现了67亿个需要辅助构造的几何定理，其中41亿个具有几何对称性。TongGeometry在国际数学奥林匹克竞赛（IMO）级别的几何问题解决中表现出色，首次超越了IMO金牌得主的平均水平，并成功将问题选入中国国家队选拔赛和美国顶级民间数学奥林匹克竞赛。该系统不仅能够高效生成和证明定理，还具备在普通消费级机器上运行的能力，为几何问题的自动化求解和教育应用提供了新的可能性。

TongGeometry主要功能

1. 几何问题生成：
   • TongGeometry能够自动生成欧几里得几何问题，涵盖广泛的几何定理和问题空间。
   • 系统生成的问题包括需要辅助构造的复杂几何问题，并且具有几何对称性。
2. 几何问题求解：
   • 系统能够自主解决生成的几何问题，提供完整的证明过程。
   • 在国际数学奥林匹克竞赛（IMO）级别的几何问题上，TongGeometry的表现超过了金牌得主。
3. 问题筛选和评估：
   • TongGeometry使用特定的评分标准对生成的问题进行评估，筛选出适合数学竞赛的问题。
   • 系统生成的问题已被选入中国国家队选拔赛和美国顶级民间数学奥林匹克竞赛。
4. 高效性和可访问性：
   • 该系统能够在普通消费级机器上运行，使其在教育和研究领域具有广泛的应用潜力。

TongGeometry技术原理

1. 树搜索技术：
   • TongGeometry采用树搜索算法，通过反向追踪提出问题，通过正向推理证明定理。
   • 系统利用生成的数据指导树搜索，填补初始状态和目标之间的差距。
2. 神经符号系统：
   • 系统结合了神经网络和符号推理，利用微调的大语言模型（LLMs）进行问题求解。
   • 策略模型用于完成辅助构造，价值模型用于估计解决问题所需的步数。
3. 大规模并行计算：
   • TongGeometry在大规模并行计算环境中进行问题搜索，利用多核CPU和GPU加速计算。
   • 系统在30天内遍历了超过1.4亿条独特路径，生成了67亿个几何问题。
4. 数据驱动方法：
   • 系统使用196个现有竞赛问题作为引导统计，通过大规模数据生成和筛选，构建了广泛的几何定理库。
   • 通过数据驱动的方法，TongGeometry能够有效地探索奥林匹克几何问题空间。
5. 辅助构造生成：
   • 系统生成的几何问题包含丰富的辅助构造，这些辅助构造对于成功证明几何定理至关重要。
   • TongGeometry通过神经模型有效地处理辅助构造，提升了问题求解的能力。

TongGeometry应用场景

1. 数学竞赛问题生成：为国际和国内数学奥林匹克竞赛提供高质量的几何问题，帮助竞赛组织者丰富题库，提升竞赛的难度和趣味性。
2. 竞赛培训与教学：作为教练工具，为数学竞赛选手提供针对性的几何问题训练，帮助他们熟悉竞赛题型，提升解题能力。
3. 教育资源开发：生成多样化的几何问题及其详细证明，用于开发教学材料，辅助教师设计课程和练习，丰富教学内容。
4. 数学研究辅助：为数学研究者提供几何定理的发现和验证工具，帮助探索新的几何性质和定理，推动数学理论的发展。
5. 在线教育平台：集成到在线学习平台，为学生提供个性化的几何学习资源和练习，支持自主学习和能力提升。
6. 人工智能研究：作为几何问题求解的基准系统，为人工智能和机器学习领域的研究提供测试环境，推动自动化定理证明技术的发展。

TongGeometry项目入口

• arXiv技术论文：https://arxiv.org/pdf/2412.10673