<p>Mathematics olympiads are prestigious competitions in which both proposing and solving problems are highly honoured. Building artificial intelligence systems capable of addressing these olympiad-level challenges remains an open frontier in automated reasoning, particularly in geometry due to its unique blend of numerical precision and spatial intuition. Here we show that TongGeometry, a neuro-symbolic system using guided tree search, both discovers and proves olympiad-level geometry theorems. Within the same computational budget as existing state-of-the-art systems, TongGeometry establishes a larger repository of geometry theorems: 6.7 billion requiring auxiliary constructions, including 4.1 billion exhibiting geometric symmetry. Among these, three of TongGeometry’s discoveries were selected for regional mathematical olympiads, appearing in a national team qualifying exam in China and a top civil olympiad in the USA. Guided by fine-tuned large language models, TongGeometry solved all International Mathematical Olympiad geometry problems in the IMO-AG-30 benchmark, outperforming average top human competitors on this specific dataset. It also surpasses the existing state of the art across a broader spectrum of olympiad-level problems and requires only consumer-grade computing resources. These results demonstrate that TongGeometry operates as both a mathematical discoverer and a solver, becoming an artificial intelligence system to achieve this dual capability. The deployment of a preliminary system based on TongGeometry demonstrates practical applications and opens fresh possibilities for artificial-intelligence-assisted mathematical research and education.</p>

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Proposing and solving olympiad geometry with guided tree search

  • Chi Zhang,
  • Jiajun Song,
  • Siyu Li,
  • Yitao Liang,
  • Yuxi Ma,
  • Wei Wang,
  • Yixin Zhu,
  • Song-Chun Zhu

摘要

Mathematics olympiads are prestigious competitions in which both proposing and solving problems are highly honoured. Building artificial intelligence systems capable of addressing these olympiad-level challenges remains an open frontier in automated reasoning, particularly in geometry due to its unique blend of numerical precision and spatial intuition. Here we show that TongGeometry, a neuro-symbolic system using guided tree search, both discovers and proves olympiad-level geometry theorems. Within the same computational budget as existing state-of-the-art systems, TongGeometry establishes a larger repository of geometry theorems: 6.7 billion requiring auxiliary constructions, including 4.1 billion exhibiting geometric symmetry. Among these, three of TongGeometry’s discoveries were selected for regional mathematical olympiads, appearing in a national team qualifying exam in China and a top civil olympiad in the USA. Guided by fine-tuned large language models, TongGeometry solved all International Mathematical Olympiad geometry problems in the IMO-AG-30 benchmark, outperforming average top human competitors on this specific dataset. It also surpasses the existing state of the art across a broader spectrum of olympiad-level problems and requires only consumer-grade computing resources. These results demonstrate that TongGeometry operates as both a mathematical discoverer and a solver, becoming an artificial intelligence system to achieve this dual capability. The deployment of a preliminary system based on TongGeometry demonstrates practical applications and opens fresh possibilities for artificial-intelligence-assisted mathematical research and education.