Elamur Research⌕
☰
home / papers / 2023 / A New Approach Towards Autoformalization

A New Approach Towards Autoformalization

Paper · 2023 · Nilay Patel, Rahul Saha and Jeffrey Flanigan

Summary

Autoformalization means automatically converting informal mathematical text into a formal language that a proof checker can verify. Earlier datasets and systems focus on olympiad or undergraduate problems. Research-paper mathematics is harder because even short theorems rely on extensive background definitions and context. Patel, Saha and Flanigan argue that formalizing such statements directly is impractical. They split the problem into four simpler stages:

  1. Translate theorems into Lean using placeholder names.
  2. Translate the paper's definitions the same way.
  3. Use entity linking to connect placeholders to real library definitions.
  4. Repair type mismatches with the Lean type checker.

To support the first stage, they release arXiv2Formal. This beta benchmark pairs 50 LaTeX theorems from random arXiv math papers with Lean 3 versions. The authors built it semi-automatically: GPT-3.5 turbo produced drafts, humans corrected them, and the corrected items became prompt examples for later drafts. Baseline experiments show that a few in-context examples greatly improve GPT-3.5's output. The decomposition matters because it lowers annotation costs and lets autoformalization reuse established NLP techniques such as coreference resolution and entity linking.

Key points

  • Four-subtask pipeline: unlinked theorem formalization, unlinked definition formalization, entity linking to mathlib or paper-level definitions, and type adjustment. Theorem proving is left for future work.
  • arXiv2Formal (Lean 3): 50 theorems in the beta release. Natural-language statements average about 140 tokens versus about 113 for the Lean versions. A Lean 4 version is planned. Code is at github.com/jlab-nlp/arxiv2formal.
  • GPT-3.5 turbo (16k) results: BLEU rises from 17.2 with no examples to 41.7 with 10 ICL examples. TER falls from 140.5 to 83.9, and TrueSkill climbs from 10.9 to 33.1.
  • Metric validity: in a small check on 10 examples, BLEU/TER scores correlated strongly with human judgments (R = .99). The authors still recommend combining automatic and human evaluation.
  • Observed failure modes: the model guesses types of under-specified objects, often wrongly, which stage 4 is meant to fix. It also struggles with multipart theorems, which motivates automatic theorem splitting.

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 California, Santa CruzSanta Cruz · United States36 works · 3,515 citations

 Fields, topics and concepts

📚 Shelves 5The field of science this work belongs to (OpenAlex fields).Computer Science · 16,667 worksArtificial Intelligence · 16,194 worksArts and Humanities · 16,039 worksLanguage and Linguistics · 15,891 worksComputational Theory and Mathematics · 252 works

Cite

Cite as Nilay Patel, Rahul Saha and Jeffrey Flanigan. 2023. A New Approach Towards Autoformalization. arXiv:2310.07957.

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

@misc{patel2023new,
  title = {{A New Approach Towards Autoformalization}},
  author = {Nilay Patel, Rahul Saha and Jeffrey Flanigan},
  year = {2023},
  doi = {10.48550/arxiv.2310.07957},
  eprint = {2310.07957},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2310.07957}
}

References

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

  1. Ayush Agrawal, Siddhartha Gadgil, Navin Goyal, Ashvni Narayanan, and Anand Tadipatri. Towards a mathematics formalisation assistant using large language models. (arXiv:2211.07524), Nov 2022. URL http://arxiv.org/abs/2211.07524. arXiv:2211.07524 [cs]. ↗
  2. Zhangir Azerbayev, Bartosz Piotrowski, and Jeremy Avigad. Proofnet: A benchmark for autoformalizing and formally proving undergraduate-level mathematics problems. NeurIPS 2022. find
  3. Tom B. Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, Sandhini Agarwal, Ariel Herbert-Voss, Gretchen Krueger, Tom Henighan, Rewon Child, Aditya Ramesh, Daniel M. Ziegler, Jeffrey Wu, Clemens Winter,… — Language Models are Few-Shot Learners
  4. Davide Castelvecchi et al. Mathematicians welcome computer-assisted proof in ‘grand unification’theory. Nature, 595(7865):18–19, 2021. find
  5. Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Pondé de Oliveira Pinto, Jared Kaplan, Harrison Edwards, Yuri Burda, Nicholas Joseph, Greg Brockman, Alex Ray, Raul Puri, Gretchen Krueger, Michael Petrov, Heidy Khlaaf, Girish Sastry, Pamela Mishkin, Brooke Chan, Scott Gray, Nick Ryder, Mik… — Evaluating Large Language Models Trained on Code
  6. Mathlib Community. Completion of the liquid tensor experiment, Jul 2022. URL https://leanprover-community.github.io/blog/posts/lte-final/. ↗
  7. Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The lean theorem prover (system description). In CADE, 2015. URL https://api.semanticscholar.org/CorpusID:232990. ↗
  8. Chelsea Edmonds. Hypergraphs. Archive of Formal Proofs, September 2023. ISSN 2150-914x. https://isa-afp.org/entries/Hypergraph_Basics.html, Formal proof development. ↗
  9. Siddhartha Gadgil, Anand Rao Tadipatri, Ayush Agrawal, Ashvni Narayanan, and Navin Goyal. Towards automating formalisation of theorem statements using large language models. find
  10. Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W. Ayers, and Stanislas Polu. Proof artifact co-training for theorem proving with language models. (arXiv:2102.06203), Mar 2022. URL http://arxiv.org/abs/2102.06203. arXiv:2102.06203 [cs]. ↗
  11. Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. Measuring mathematical problem solving with the math dataset. arXiv preprint arXiv: 2103.03874, 2021.
  12. Albert Q. Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, and Guillaume Lample. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. (arXiv:2210.12283), Feb 2023. URL http://arxiv.org/abs/2210.12283. arXiv:2210.12283… ↗
  13. Laura Luzzi, Stefano Marmi, Hitoshi Nakada, and Rie Natsui. Generalized brjuno functions associated to α-continued fractions. arXiv preprint arXiv: Arxiv-0705.1690, 2007. find
  14. Dana Mackenzie. The poincaré conjecture–proved. Science, 314(5807):1848–1849, 2006. doi: 10.1126/science.314.5807.1848. URL https://www.science.org/doi/abs/10.1126/ science.314.5807.1848. — [doi:10.1126/science.314.5807.1848](https://doi.org/10.1126/science.314.5807.1848) ↗
  15. The mathlib Community. The lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, page 367–381, New York, NY, USA, 2020. Association for Computing Machinery. ISBN 9781450370974. doi: 10.1145/3372885.3373824. URL https://d… find
  16. OpenAI. Chatgpt, 2020. URL https://www.openai.com/research/chatgpt. ↗
  17. Kishore Papineni, Salim Roukos, Todd Ward, and Wei-Jing Zhu. Bleu: a method for automatic evaluation of machine translation. In Proceedings of the 40th Annual Meeting of the Association for Computational Linguistics, pages 311–318, Philadelphia, Pennsylvania, USA, July 2002. Association for Computat…
  18. Peter Scholze. Liquid tensor experiment, Dec 2020. URL https://xenaproject.wordpress.com/2020/12/05/liquid-tensor-experiment/. ↗
  19. Matthew Snover, Bonnie Dorr, Rich Schwartz, Linnea Micciulla, and John Makhoul. A study of translation edit rate with targeted human annotation. In Proceedings of the 7th Conference of the Association for Machine Translation in the Americas: Technical Papers, pages 223–231, Cambridge, Massachusetts,…
  20. Christian Szegedy, editor. A Promising Path Towards Autoformalization and General Artificial Intelligence, 2020. find
  21. Yuhuai Wu, Albert Q. Jiang, Wenda Li, Markus N. Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models. (arXiv:2205.12615), May 2022. URL http://arxiv.org/abs/2205.12615. arXiv:2205.12615 [cs]. ↗
  22. Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. Leandojo: Theorem proving with retrieval-augmented language models. arXiv preprint arXiv: 2306.15626, 2023.
  23. Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. Minif2f: a cross-system benchmark for formal olympiad-level mathematics. arXiv preprint arXiv:2109.00110, 2021. *Figure 3: An example pair from an arXiv paper ([14]) from the benchmark dataset and its formalized versions. Note that we don’t know t…

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/patel-2023-new-approach-towards-autoformalization/