Elamur Research⌕
☰
home / papers / 2024 / Autoformalizing Euclidean Geometry

Autoformalizing Euclidean Geometry

Paper · 2024 · Logan Murphy, Kaiyu Yang, Jialiang Sun et al.

Summary

The paper addresses autoformalization, which means converting human-written mathematics into statements and proofs that a machine can check. The authors focus on Euclidean geometry. They argue it is a controllable test domain because two problems that are usually hard become manageable there: checking whether outputs are correct, and dealing with the steps that informal proofs leave to the diagram.

They build an SMT-based symbolic reasoning engine, E3, with two uses:

  • Grading theorem statements. It tries to prove that a model's theorem is logically equivalent to a reference formalization. This replaces weak proxies such as BLEU and costly manual review.
  • Filling diagram gaps. Inside Lean, it automatically supplies the facts a reader would normally read off the figure. The authors implement the formal system E (Avigad et al.) for this purpose, so a model only has to translate the explicit textual steps.

They also release LeanEuclid, a hand-formalized benchmark built from Euclid's Elements (Book I) and UniGeo. Experiments with GPT-4 and GPT-4V show low success rates, which marks the task as challenging. Many failed proofs, however, need only small fixes. The work matters because it moves autoformalization evaluation from human inspection toward automatic checking.

Key points

  • LeanEuclid benchmark: 173 examples, each with an informal statement, proof and diagram plus a formal Lean version. It covers all 48 propositions of Elements Book I and problems from UniGeo, and is intended for testing only.
  • Theorem autoformalization (5-shot): GPT-4 gets 18.9% of theorems right and GPT-4V gets 21.0%. E3's automatic equivalence check correlates well with human judgment and produces few false negatives.
  • Proof autoformalization: whole proofs were generated in single queries, without search. Overall success was 18.8% for GPT-4 and 23.1% for GPT-4V. Among the 43 Elements proofs tested, both models fully succeeded only on Propositions 1 and 17.
  • Repair effort: proofs that failed were manually fixed. The median Levenshtein similarity to the repaired versions was 61.7% for GPT-4 and 64.0% for GPT-4V. Typical fixes were simple, such as reordering tactic arguments or slightly strengthening a lemma.
  • Main limitation: the dataset is too small for fine-tuning. The authors suggest translating existing corpora, such as AlphaGeometry's synthetic data, into their formalism.

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 TorontoToronto · Canada121 works · 179,943 citations🎓California Institute of TechnologyPasadena · United States16 works · 1,291 citations

 Fields, topics and concepts

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

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

Cite

Cite as Logan Murphy, Kaiyu Yang, Jialiang Sun, Zhaoyu Li, Anima Anandkumar and Xujie Si. 2024. Autoformalizing Euclidean Geometry. arXiv:2405.17216.

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

@misc{murphy2024autoformalizing,
  title = {{Autoformalizing Euclidean Geometry}},
  author = {Logan Murphy, Kaiyu Yang, Jialiang Sun, Zhaoyu Li, Anima Anandkumar and Xujie Si},
  year = {2024},
  doi = {10.48550/arxiv.2405.17216},
  eprint = {2405.17216},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2405.17216}
}

References

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

  1. Agrawal, A., Gadgil, S., Goyal, N., Narayanan, A., and Tadipatri, A. Towards a mathematics formalisation assistant using large language models. arXiv preprint arXiv:2211.07524, 2022.
  2. Avigad, J. Notes on ”A formal system for Euclid’s Elements”. https://www.andrew.cmu.edu/user/avigad/Papers/euclid_notes.htm. Avigad, J., Dean, E., and Mumma, J. A formal system for Euclid’s Elements. The Review of Symbolic Logic, 2009. ↗
  3. Azerbayev, Z., Piotrowski, B., Schoelkopf, H., Ayers, E. W., Radev, D., and Avigad, J. ProofNet: Autoformalizing and formally proving undergraduate-level mathematics. arXiv preprint arXiv:2302.12433, 2023.
  4. Barras, B., Boutin, S., Cornes, C., Courant, J., Filliatre, J.-C., Gimenez, E., Herbelin, H., Huet, G., Munoz, C., Murthy, C., et al. The Coq proof assistant reference manual: Version 6.1. PhD thesis, Inria, 1997. find
  5. Barrett, C. and Tinelli, C. Satisfiability modulo theories. 2018. find
  6. Beeson, M., Narboux, J., and Wiedijk, F. Proof-checking Euclid. Annals of Mathematics and Artificial Intelligence, 2019. find
  7. Buchberger, B. Applications of gröbner bases in non-linear computational geometry. In Trends in Computer Algebra, 2005. find
  8. Chen, J., Tang, J., Qin, J., Liang, X., Liu, L., Xing, E., and Lin, L. GeoQA: A geometric question answering benchmark towards multimodal numerical reasoning. In Findings of the Association for Computational Linguistics: ACL, 2021a.
  9. Chen, J., Li, T., Qin, J., Lu, P., Lin, L., Chen, C., and Liang, X. UniGeo: Unifying geometry logical reasoning via reformulating mathematical expression. In Conference on Empirical Methods in Natural Language Processing (EMNLP), 2022.
  10. Chen, M., Tworek, J., Jun, H., Yuan, Q., Pinto, H. P. d. O., Kaplan, J., Edwards, H., Burda, Y., Joseph, N., Brockman, G., et al. Evaluating large language models trained on code. arXiv preprint arXiv:2107.03374, 2021b.
  11. Chen, Y., Gandhi, R., Zhang, Y., and Fan, C. NL2TL: Transforming natural languages to temporal logics using large language models. In Conference on Empirical Methods in Natural Language Processing (EMNLP), 2023. find
  12. Cosler, M., Hahn, C., Mendoza, D., Schmitt, F., and Trippel, C. nl2spec: Interactively translating unstructured natural language to temporal logics with large language models. In International Conference on Computer Aided Verification (CAV), 2023. find
  13. Cunningham, G., Bunescu, R. C., and Juedes, D. Towards autoformalization of mathematics and code correctness: Experiments with elementary proofs. arXiv preprint arXiv:2301.02195, 2023. de Moura, L. d. and Ullrich, S. The Lean 4 theorem prover and programming language. In International Conference on…
  14. First, E., Rabe, M., Ringer, T., and Brun, Y. Baldur: Whole-proof generation and repair with large language models. In Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE), 2023.
  15. Gao, J., Pi, R., Zhang, J., Ye, J., Zhong, W., Wang, Y., Hong, L., Han, J., Xu, H., Li, Z., et al. G-LLaVA: Solving geometric problem with multi-modal large language model. arXiv preprint arXiv:2312.11370, 2023.
  16. Hales, T., Adams, M., Bauer, G., Dang, T. D., Harrison, J., Le Truong, H., Kaliszyk, C., Magron, V., McLaughlin, S., Nguyen, T. T., et al. A formal proof of the Kepler conjecture. In Forum of Mathematics, Pi, volume 5, 2017.
  17. Han, J. M., Rute, J., Wu, Y., Ayers, E., and Polu, S. Proof artifact co-training for theorem proving with language models. In International Conference on Learning Representations (ICLR), 2022.
  18. Heiberg, J. L. Euclid’s Elements. 2007. URL https://github.com/rfitzp/Elements. ↗
  19. Hernandez-Espiet, A. feat: synthetic geometry. https://github.com/leanprover-community/ mathlib4/pull/7300, 2023. ↗
  20. Hilbert, D. Grundlagen der geometrie. Springer-Verlag, 2013. find
  21. Jiang, A., Welleck, S., Zhou, J. P., Li, W., Liu, J., Jamnik, M., Lacroix, T., Wu, Y., and Lample, G. Draft, Sketch, and Prove: Guiding formal theorem provers with informal proofs. In International Conference on Learning Representations (ICLR), 2023a.
  22. Jiang, A. Q., Li, W., and Jamnik, M. Multilingual mathematical autoformalization. arXiv preprint arXiv:2311.03755, 2023b.
  23. Kazemi, M., Alvari, H., Anand, A., Wu, J., Chen, X., and Soricut, R. GeomVerse: A systematic evaluation of large models for geometric reasoning. arXiv preprint arXiv:2312.12241, 2023. — [arXiv:2312.12241](https://arxiv.org/abs/2312.12241) find
  24. Lample, G., Lacroix, T., Lachaux, M.-A., Rodriguez, A., Hayat, A., Lavril, T., Ebner, G., and Martinet, X. Hyper-Tree proof search for neural theorem proving. In Neural Information Processing Systems (NeurIPS), 2022. find
  25. Leroy, X., Blazy, S., Kästner, D., Schommer, B., Pister, M., and Ferdinand, C. CompCert—a formally verified optimizing compiler. In Embedded Real Time Software and Systems, 2016. find
  26. Li, Z., Sun, J., Murphy, L., Su, Q., Li, Z., Zhang, X., Yang, K., and Si, X. A survey on deep learning for theorem proving. arXiv preprint arXiv:2404.09939, 2024.
  27. Liang, Z., Yang, T., Zhang, J., and Zhang, X. UniMath: A foundational and multimodal mathematical reasoner. In Conference on Empirical Methods in Natural Language Processing (EMNLP), 2023. find
  28. Lu, P., Gong, R., Jiang, S., Qiu, L., Huang, S., Liang, X., and Zhu, S.-c. Inter-GPS: Interpretable geometry problem solving with formal language and symbolic reasoning. In Annual Meeting of the Association for Computational Linguistics (ACL), 2021.
  29. Miller, N. G. A diagrammatic formal system for Euclidean geometry. 2001. find
  30. Mumma, J. Proofs, pictures, and Euclid. Synthese, 2010. find
  31. Nevins, A. J. Plane geometry theorem proving using forward chaining. Artificial Intelligence, 1975. find
  32. OpenAI. GPT-4 technical report. arXiv:2303.08774, 2023. arXiv preprint Pan, J., Chou, G., and Berenson, D. Data-efficient learning of natural language to linear temporal logic translators for robot task specification. In International Conference on Robotics and Automation (ICRA), 2023.
  33. Papineni, K., Roukos, S., Ward, T., and Zhu, W.-J. BLEU: a method for automatic evaluation of machine translation. In Annual Meeting of the Association for Computational Linguistics (ACL), 2002.
  34. Peng, S., Fu, D., Liang, Y., Gao, L., and Tang, Z. Geo-DRL: A self-learning framework for geometry problem solving using reinforcement learning in deductive reasoning. In Findings of the Association for Computational Linguistics: ACL, 2023. find
  35. Polu, S. and Sutskever, I. Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03393, 2020.
  36. Schulz, S. System description: E 1.8. In International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, 2013. find
  37. Schwabhäuser, W., Szmielew, W., and Tarski, A. Metamath-ematische methoden in der geometrie. Springer-Verlag, 2013. find
  38. Song, P., Yang, K., and Anandkumar, A. Towards large language models as copilots for theorem proving in Lean. arXiv preprint arXiv: Arxiv-2404.12534, 2024. find
  39. The mathlib Community. The Lean mathematical library. In Certified Programs and Proofs (CPP), 2020.
  40. Trinh, T., Wu, Y., Le, Q., He, H., and Luong, T. Solving olympiad geometry without human demonstrations. Nature, 2023.
  41. Wang, Q., Kaliszyk, C., and Urban, J. First experiments with neural translation of informal to formal mathematics. In Conferences on Intelligent Computer Mathematics (CICM), 2018.
  42. Wu, W.-t. On the decision problem and the mechanization of theorem-proving in elementary geometry. In Selected Works Of Wen-Tsun Wu. 2008. find
  43. Wu, Y., Jiang, A., Li, W., Rabe, M., Staats, C., Jamnik, M., and Szegedy, C. Autoformalization with large language models. In Neural Information Processing Systems (NeurIPS), 2022.
  44. Yang, K. and Deng, J. Learning to prove theorems via interacting with proof assistants. In International Conference on Machine Learning (ICML), 2019.
  45. Yang, K., Swope, A., Gu, A., Chalamala, R., Song, P., Yu, S., Godil, S., Prenger, R., and Anandkumar, A. Lean-Dojo: Theorem proving with retrieval-augmented language models. In Neural Information Processing Systems (NeurIPS), 2023. find
  46. Zhang, J.-Z., Chou, S.-C., and Gao, X.-S. Automated production of traditional proofs for theorems in Euclidean geometry I. the Hilbert intersection point theorems. Annals of Mathematics and Artificial Intelligence, 1995. find
  47. A. The Formal System E We describe our variant of the formal system E in Lean-like pseudocode, including the complete list of axioms. Our design mostly follows E’s original specification (Avigad et al., 2009) with a few minor deviations. find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/murphy-2024-autoformalizing-euclidean-geometry/