Elamur Research⌕
☰
home / papers / 2024 / Wu's Method can Boost Symbolic AI to Rival Silver Medalists and AlphaGeometry to Outperform Gold Medalists at IMO Geometry

Wu's Method can Boost Symbolic AI to Rival Silver Medalists and AlphaGeometry to Outperform Gold Medalists at IMO Geometry

Paper · 2024 · Shiven Sinha, Ameya Prabhu, Ponnurangam Kumaraguru et al.

Summary

Automated proving of olympiad geometry is often treated as a milestone for machine reasoning. AlphaGeometry is a neuro-symbolic system trained on 100 million synthetic proofs. It solved 25 of the 30 problems in the IMO-AG-30 benchmark, while the Wu's method baseline reported alongside it managed only ten. The authors revisit this algebraic technique, which turns geometric premises and goals into polynomial equations. They manually rewrote the benchmark problems for the JGEX software, and 26 of the 30 could be expressed there. They also reproduced the DD+AR symbolic engine from the AlphaGeometry codebase. Wu's method alone proved 15 problems, mostly within seconds on an ordinary laptop. Combining it with DD+AR yields Wu&DD+AR, a system with no neural component that solves 21 problems, close to silver-medalist level. Wu's method also handles two problems AlphaGeometry missed, so a simple ensemble, Wu&AG, reaches 27 of 30 and exceeds the average gold medalist. The authors argue that algebraic provers complement synthetic and LLM-based approaches. In their view, these provers have been undervalued even though they do not yield human-readable proofs.

Key points

  • Wu's method solved 15 problems on IMO-AG-30, up from the 10 previously reported. Evaluation covered the 26 problems translatable into JGEX. Fourteen were solved in under 5 seconds, and 2015 P4 took about 3 minutes. Unsolved cases usually exhausted memory within 5 minutes.
  • Hardware was a CPU-only laptop with an AMD Ryzen 7 5800H and 16 GB RAM, using a 5-minute limit per problem.
  • Wu&DD+AR solves 21/30. That is 6 more than the best earlier traditional method and equal to AlphaGeometry without fine-tuning (FT-9M only).
  • Wu&AG solves 27/30. Problems 2008 P1B and 2021 P3 are solved by no prover other than Wu's method. Human reference averages are 15.2 for all contestants, 19.3 for bronze, 22.9 for silver and 25.9 for gold.
  • The problem translations are released at huggingface.co/datasets/bethgelab/simplegeometry. The authors note that existing algebraic tools are limited, mainly through missing constructions and weak performance.

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

🎓University of CambridgeCambridge · United Kingdom243 works · 121,396 citations🎓University of TübingenTübingen · Germany75 works · 41,081 citations🎓International Institute of Information Technology, HyderabadHyderabad · India38 works · 1,821 citations🎓Tübingen AI CenterTübingen · Germany3 works · 30 citations

 Fields, topics and concepts

📚 Shelves 5The field of science this work belongs to (OpenAlex fields).Computer Science · 16,667 worksArtificial Intelligence · 16,194 worksMathematics · 177 worksComputational Theory and Mathematics · 252 worksGeometry and Topology · 3 works

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

💡 Concepts 1Key ideas and methods explained on our concept pages.Artificial intelligence · 49 works

Cite

Cite as Shiven Sinha, Ameya Prabhu, Ponnurangam Kumaraguru, Siddharth Bhat and Matthias Bethge. 2024. Wu's Method can Boost Symbolic AI to Rival Silver Medalists and AlphaGeometry to Outperform Gold Medalists at IMO Geometry. arXiv:2404.06405.

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

@misc{sinha2024wu,
  title = {{Wu's Method can Boost Symbolic AI to Rival Silver Medalists and AlphaGeometry to Outperform Gold Medalists at IMO Geometry}},
  author = {Shiven Sinha, Ameya Prabhu, Ponnurangam Kumaraguru, Siddharth Bhat and Matthias Bethge},
  year = {2024},
  doi = {10.48550/arxiv.2404.06405},
  eprint = {2404.06405},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2404.06405}
}

References

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

  1. Aimo prize. https://aimoprize.com/. 1 ↗
  2. Imo grand challenge. https://imo-grand-challenge.github.io/. 1 ↗
  3. Peter novotný’s masters thesis. https://skmo.sk/cvika/ukazpdf.php?pdf=diplomka.pdf. 4 ↗
  4. Jeremy Avigad, Edward Dean, and John Mumma. A formal system for euclid’s elements. The Review of Symbolic Logic, 2009. 1 find
  5. Michael Beeson, Pierre Boutry, Gabriel Braun, Charly Gries, and Julien Narboux. Geocoq. 2018. 1 find
  6. S.C. Chou, X.S. Gao, and J.Z. Zhang. A deductive database approach to automated geometry theorem proving and discovering. Journal of Automated Reasoning, 2000. doi: 10.1023/A:1006171315513. 2 find
  7. Shang-Ching Chou. Proving elementary geometry theorems using wu’s algorithm. In Woodrow Wilson Bledsoe and Donald W Loveland, editors, Automated Theorem Proving: After 25 Years, volume 89. American Mathematical Soc., 1984. 2 find
  8. Shang-Ching Chou. An introduction to wu’s method for mechanical theorem proving in geometry. Journal of Automated Reasoning, 1988. 2 find
  9. Shang-Ching Chou, Xiao-Shan Gao, and Jing-Zhong Zhang. Automated production of traditional proofs in solid geometry. Journal of Automated Reasoning, 14(2):257–291, 1995. 2 find
  10. Nicolaas Govert de Bruijn. AUTOMATH, a language for mathematics. 1983. 1 find
  11. Giuseppa Carr‘a Ferro, Giovanni Gallo, and Rosario Gennaro. Probabilistic verification of elementary geometry statements. In Automated Deduction in Geometry, 1997. doi: 10.1007/BFb0022721. 1 — [doi:10.1007/bfb0022721](https://doi.org/10.1007/bfb0022721) find
  12. H. Gelernter. Realization of a geometry-theorem proving machine. Computers & Thought, 1995. doi: 10.5555/ 207644.207647. 1, 2 find
  13. W. T. Gowers. How can it be feasible to find proofs? https://drive.google.com/file/d/ 1-FFa6nMVg18m1zPtoAQrFalwpx2YaGK4/view. Accessed: 7 April 2024. 2 ↗
  14. Thomas Little Heath et al. The thirteen books of Euclid’s Elements. 1956. 1 find
  15. Deepak Kapur. Using gröbner bases to reason about geometry problems. Journal of Symbolic Computation, 1986. 2 find
  16. Deepak Kapur. A refutational approach to geometry theorem proving. Artificial Intelligence, 1988. 2 find
  17. Michelle Y. Kim. Visual reasoning in geometry theorem proving. In Proceedings of the Eleventh International Joint Conference on Artificial Intelligence, 1989. 1 find
  18. Zoltán Kovács and Alexander Vujic. Open source prover in the attic. arXiv preprint arXiv:2401.13702, 2024. 3 — [arXiv:2401.13702](https://arxiv.org/abs/2401.13702) find
  19. Zoltán Kovács, Tomas Recio, Luis F Tabera, and M Pilar Vélez. Dealing with degeneracies in automated theorem proving in geometry. Mathematics, 2021. 2 find
  20. Arthur J Nevins. Plane geometry theorem proving using forward chaining. Artificial Intelligence, 6(1):1–23, 1975. 2 find
  21. Jürgen Richter-Gebert and Ulrich Kortenkamp. The Interactive Geometry Software Cinderella. 1999. 1 find
  22. Max Schindler and Evan Chen. Barycentric coordinates in olympiad geometry. Olympiad Articles, 2012. 1 find
  23. Justin Stevens. Coordinate and trigonometry bashing. http://services.artofproblemsolving.com/ download.php?id=YXR0YWNobWVudHMvYi9kLzRmMTA5OWJhNmI1MTg2YzM2ODdkZTVhYTJjMGU0NjdmYmViNGRk&rn= Q29vcmRpbmF0ZSBhbmQgVHJpZ29ub21ldHJ5IEJhc2hpbmcucGRm. Accessed: 4 April 2024. 1 ↗
  24. Trieu H Trinh, Yuhuai Wu, Quoc V Le, He He, and Thang Luong. Solving olympiad geometry without human demonstrations. Nature, 2024. 2, 3, 7
  25. Dongming Wang. Reasoning about geometric problems using an elimination method. Automated practical reasoning: Algebraic approaches, pages 147–185, 1995. 2 find
  26. Wu Wen-Tsün. On the decision problem and the mechanization of theorem proving in elementary geometry. Scientia Sinica, 1978. 2 find
  27. Wenjun Wu. On zeros of algebraic equations–an application of ritt principle. Kexue Tongbao, 1986. 2 find
  28. Z. Ye, S.C. Chou, and X.S. Gao. An introduction to java geometry expert – (extended abstract). 2011. doi: 10.1007/978-3-642-21046-4 10. 3 — [doi:10.1007/978-3-642-21046-4](https://doi.org/10.1007/978-3-642-21046-4) find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/sinha-2024-wu-s-method-can-boost/