AI不仅能解奥数几何题,还能自创题目并被真实竞赛采用。
Proposing and solving olympiad geometry with guided tree search
- 用树搜索结合大模型生成几何定理,支持题目提出与求解。
- 在同等算力下发现67亿个需辅助线的定理,41亿具对称性。
- 3道自创题入选中美奥数赛,首次超越金牌选手解题能力。
数学奥林匹克是备受推崇的竞赛,其命题与解题被视为高阶成就。构建能自主命题与解题的人工智能,在自动化定理发现与证明领域仍是未解难题,尤其在融合数值与空间特征的几何问题中更具挑战。我们提出TongGeometry,一个基于树搜索引导的欧氏几何系统,支持题目生成与求解。该高效系统建立了迄今最广泛的几何定理库:在与现有最先进方法相同的计算预算下,TongGeometry发现了67亿个需辅助构造的几何定理,其中41亿个具有几何对称性。其中有10个定理被提议用于地区数学奥赛,3个实际入选中国与美国的国家级奥赛或顶尖公民奥赛,进入国家队选拔考试。受微调大语言模型引导,TongGeometry成功解出所有IMO-AG-30国际数学奥林匹克几何题,首次超越金牌选手表现。在更广泛的奥数级别问题上也优于现有最先进水平。系统可在消费级机器上运行,提升可及性,推动技术普及。与仅模仿学生解题的系统不同,TongGeometry如教练一般,实现定理的发现、呈现与证明。
原文摘要 · Abstract (English)
Mathematics olympiads are prestigious competitions, with problem proposing and solving highly honored. Building artificial intelligence that proposes and solves olympiads presents an unresolved challenge in automated theorem discovery and proving, especially in geometry for its combination of numerical and spatial elements. We introduce TongGeometry, a Euclidean geometry system supporting tree-search-based guided problem proposing and solving. The efficient geometry system establishes the most extensive repository of geometry theorems to date: within the same computational budget as the existing state-of-the-art, TongGeometry discovers 6.7 billion geometry theorems requiring auxiliary constructions, including 4.1 billion exhibiting geometric symmetry. Among them, 10 theorems were proposed to regional mathematical olympiads with 3 of TongGeometry's proposals selected in real competitions, earning spots in a national team qualifying exam or a top civil olympiad in China and the US. Guided by fine-tuned large language models, TongGeometry solved all International Mathematical Olympiad geometry in IMO-AG-30, outperforming gold medalists for the first time. It also surpasses the existing state-of-the-art across a broader spectrum of olympiad-level problems. The full capabilities of the system can be utilized on a consumer-grade machine, making the model more accessible and fostering widespread democratization of its use. By analogy, unlike existing systems that merely solve problems like students, TongGeometry acts like a geometry coach, discovering, presenting, and proving theorems.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。