Elamur Research⌕
☰
home / papers / 2024 / Proposing and solving olympiad geometry with guided tree search

Proposing and solving olympiad geometry with guided tree search

Paper · 2024 · Chi Zhang, Jiajun Song, Siyu Li et al.

Summary

Automatically creating and proving olympiad-level geometry problems is hard. Geometry mixes numeric and spatial reasoning, the search space branches enormously, and few past problems exist to learn heuristics from. The authors present TongGeometry, a synthetic system for planar Euclidean geometry built around a finite search tree. It generates problems by tracing backward from discovered facts and proves them by forward chaining with a redesigned deductive database (DD) engine.

The search was steered by statistics from 196 olympiad problems and ran massively in parallel. It produced billions of readable problems whose proofs need auxiliary constructions. That data was then used to fine-tune two LLMs: one proposes which construction to try next, and the other estimates how many steps remain.

The guided system proves every problem in IMO-AG-30 on a single consumer workstation, which the authors present as the first result beating an average IMO gold medalist. It also beats AlphaGeometry on a broader olympiad set. Several of its generated problems were accepted by real competitions. The work matters because it covers both proposing and solving at olympiad level while needing only modest hardware.

Key points

  • Data generation: The search ran for 30 days on 10,368 CPU cores. It yielded about 6.7 billion problems requiring auxiliary constructions, about 4.1 billion of which have geometric symmetry.
  • Competition use: Of 10 proposals sent to competitions, 3 were used. One was selected as the sole geometry question at the Beijing round of the 2024 national high school math league, and two were shortlisted for the 2024 US Ersatz Math Olympiad.
  • IMO-AG-30 results: All 30 problems were solved, each in under 38 minutes, on 32 CPU cores and one NVIDIA RTX 4090.
    • The DD backend alone solved 18 problems.
    • The value model was decisive for IMO 2000 P6 and IMO 2008 P6.
    • For comparison, AlphaGeometry needed 246 CPU cores and 4 V100 GPUs.
  • MO-TG-225 results: On this new benchmark of olympiad problems, TongGeometry solved 81.3% of problems versus 45.3% for AlphaGeometry. GPT-4 and o1 were also evaluated and frequently produced flawed proofs.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Institutions

🎓Peking UniversityBeijing · China335 works · 43,758 citations🏛️Beijing Institute for General Artificial IntelligenceBeijing · China14 works · 692 citations

 Fields, topics and concepts

📚 Shelves 5The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksMathematics · 233 worksComputational Theory and Mathematics · 496 worksGeometry and Topology · 9 works

🧭 Topics 1Research subjects and languages the work is about.Reasoning · 1,948 works

Cite

Cite as Chi Zhang, Jiajun Song, Siyu Li, Yitao Liang, Yuxi Ma, Wei Wang, Yixin Zhu and Song-Chun Zhu. 2024. Proposing and solving olympiad geometry with guided tree search. arXiv:2412.10673.

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.48550/arxiv.2412.10673 · arXiv 2412.10673

@misc{zhang2024proposing,
  title = {{Proposing and solving olympiad geometry with guided tree search}},
  author = {Chi Zhang, Jiajun Song, Siyu Li, Yitao Liang, Yuxi Ma, Wei Wang, Yixin Zhu and Song-Chun Zhu},
  year = {2024},
  doi = {10.48550/arxiv.2412.10673},
  eprint = {2412.10673},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2412.10673}
}

References

18 references, 8 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. D. Selsam, et al., IMO Grand Challenge. URL https://imo-grand-challenge.github.io (2020). ↗
  2. T. H. Trinh, Y. Wu, Q. V. Le, H. He, T. Luong, Solving olympiad geometry without human demonstrations. Nature 625 (7995), 476–482 (2024).
  3. S. Polu, I. Sutskever, Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03393 (2020).
  4. K. Zheng, J. M. Han, S. Polu, Minif2f: a cross-system benchmark for formal olympiad-level mathematics. arXiv preprint arXiv:2109.00110 (2021).
  5. S. Polu, et al., Formal mathematics statement curriculum learning. arXiv preprint arXiv:2202.01344 (2022).
  6. G. Lample, et al., Hypertree proof search for neural theorem proving. Advances in neural information processing systems 35, 26337–26349 (2022).
  7. J. Achiam, et al., Gpt-4 technical report. arXiv preprint arXiv:2303.08774 (2023).
  8. H. Touvron, et al., Llama: Open and efficient foundation language models. arXiv preprint arXiv:2302.13971 (2023).
  9. W. W. R. Ball, A short account of the history of mathematics (Courier Corporation) (1960). find
  10. F. Marić, et al., Formalizing IMO problems and solutions in Isabelle/HOL. arXiv preprint arXiv:2010.16015 (2020). — [arXiv:2010.16015](https://arxiv.org/abs/2010.16015) find
  11. L. d. Moura, S. Ullrich, The Lean 4 theorem prover and programming language, in Automated Deduction–CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings 28 (Springer) (2021), pp. 625–635. find
  12. S.-C. Chou, X.-S. Gao, J.-Z. Zhang, An introduction to geometry expert, in Automated Deduction—Cade-13: 13th International Conference on Automated Deduction New Brunswick, NJ, USA, July 30–August 3, 1996 Proceedings 13 (Springer) (1996), pp. 235–239. find
  13. C. Sangwin, A brief review of GeoGebra: dynamic mathematics. MSor Connections 7 (2), 36 (2007). find
  14. P. Bak, R. S. Krajči, M. M. Rolı́nek, Automated generation of planar geometry Olympiad problems, Ph.D. thesis, Master Thesis (2020). find
  15. D. Guo, et al., DeepSeek-Coder: When the Large Language Model Meets Programming–The Rise of Code Intelligence. arXiv preprint arXiv:2401.14196 (2024). find
  16. J. Hoffmann, et al., Training compute-optimal large language models. arXiv preprint arXiv:2203.15556 (2022).
  17. J. S. Mackay, History of the Nine-point Circle. Proceedings of the Edinburgh Mathematical Society 11, 19–57 (1892). find
  18. E. Chen, Euclidean geometry in mathematical olympiads, vol. 27 (American Mathematical Soc.) (2021). find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/zhang-2024-proposing-solving-olympiad-geometry-guided/