---
title: "Consistent Autoformalization for Constructing Mathematical"
description: "The authors propose a three-stage pipeline: MS-RAG retrieves the most similar already-formalized… 44 references, cited by 9 papers here."
authors: ["Lan Zhang", "Xin Quan", "Andre Freitas"]
year: 2024
venue: "Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing"
source: "https://aclanthology.org/2024.emnlp-main.233/"
doi: "10.18653/v1/2024.emnlp-main.233"
arxiv: "2410.04194"
licence: "CC BY 4.0 (ACL Anthology)"
licence_url: "https://creativecommons.org/licenses/by/4.0/"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/zhang-2024-consistent-autoformalization-constructing-mathematical-libraries/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/zhang-2024-consistent-autoformalization-constructing-mathematical-libraries/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2024](https://md.research.elamur.ai/free/en/papers/2024/page/13/) / Consistent Autoformalization for Constructing Mathematical Libraries

# Consistent Autoformalization for Constructing Mathematical Libraries

**Authors:** [Lan Zhang](https://md.research.elamur.ai/free/en/authors/lan-zhang/), [Xin Quan](https://md.research.elamur.ai/free/en/authors/xin-quan/) and [Andre Freitas](https://md.research.elamur.ai/free/en/authors/andre-freitas/) · **Year:** 2024 · **Venue:** [Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing](https://md.research.elamur.ai/free/en/venues/emnlp/) ([EMNLP 2024](https://md.research.elamur.ai/free/en/venues/emnlp/2024/)) · **Publisher:** [Association for Computational Linguistics](https://md.research.elamur.ai/free/en/publishers/association-for-computational-linguistics/) · **Licence:** [CC BY 4.0 (ACL Anthology)](https://creativecommons.org/licenses/by/4.0/)

**Links:** [Publisher's page](https://aclanthology.org/2024.emnlp-main.233/) · [PDF](https://aclanthology.org/2024.emnlp-main.233.pdf) · [DOI 10.18653/v1/2024.emnlp-main.233](https://doi.org/10.18653/v1/2024.emnlp-main.233) · [arXiv 2410.04194](https://arxiv.org/abs/2410.04194) · [OpenAlex](https://openalex.org/W4404783316)

**Citations:** 2 citations (OpenAlex, 2026-10-14) · [9](https://md.research.elamur.ai/free/en/papers/zhang-2024-consistent-autoformalization-constructing-mathematical-libraries/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## Summary
The paper addresses autoformalization: converting natural-language mathematics into formal code that a theorem prover can check. Its focus is building large, specialized libraries, where generated statements must reuse the library's existing terms and syntax and remain correct on unfamiliar material. LLMs used alone handle this poorly. The authors propose a three-stage pipeline:
- **MS-RAG** retrieves the most similar already-formalized items from a knowledge base and uses them as prompt examples.
- **Denoising** strips extraneous model output, either through rule-based code cleanup (CBD) or a second prompt (PBD).
- **Auto-SEF** returns Isabelle syntax errors to the model over several repair rounds.

To evaluate the pipeline, they built MathLibForm from IsarMathLib (Isabelle/ZF) and compared several LLMs using syntactic and similarity metrics. The combined mechanisms raise syntactic correctness by between 5.47% and 33.58%. Smaller instruction-tuned models gain the most, which suggests these mechanisms could help close the gap between smaller and larger models in building formal libraries.

## Key points
- **MathLibForm dataset:** 2,744 items (lemmas, definitions, corollaries, theorems with their comments) were extracted from IsarMathLib and split 90/10 into 2,470 training and 274 test samples. The formal statements were also informalized with Mistral to add extra descriptions.
- **Auto-SEF iterations:** the repair loop runs for at most nine rounds. The first round gives the biggest Pass-rate improvement (+2.56% for Mistral, +4.38% for GPT-3.5), and later rounds add little.
- **Trade-off for smaller models:** under Auto-SEF, Mistral's BLEU-2 drops in the early rounds while GPT-3.5's stays stable. This suggests the smaller model gains syntactic validity at some cost in semantic fidelity.
- **Metric analysis:** all pairwise Pearson correlations between metrics exceed 0.6, and RUBY correlates most strongly with the others (>0.85). The authors recommend reporting Pass rate together with BLEU, since BLEU-2 tracks Pass most closely.
- **Availability:** code and data are released on GitHub (lanzhang128/retrieval_augmented_autoformalization).

*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 Manchester](https://md.research.elamur.ai/free/en/universities/university-of-manchester/) — University, Manchester, United Kingdom · 97 works · 45,240 citations

📚 Shelves (5): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 19,503 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 18,805 works · [🎭 Arts and Humanities](https://md.research.elamur.ai/free/en/shelves/arts-and-humanities/) · 17,959 works · [🗣️ Language and Linguistics](https://md.research.elamur.ai/free/en/shelves/arts-and-humanities/language-and-linguistics/) · 17,789 works · [🧮 Computational Theory and Mathematics](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-theory-and-mathematics/) · 496 works

🧭 Topics (1): [🧮 Reasoning](https://md.research.elamur.ai/free/en/topics/reasoning/) · 1,948 works

## Cite

Cite as: Lan Zhang, Xin Quan and Andre Freitas. 2024. Consistent Autoformalization for Constructing Mathematical Libraries. Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing.

The paper itself, not this page. BibTeX from the library's record of the work.

```bibtex
@inproceedings{zhang2024consistent,
  title = {{Consistent Autoformalization for Constructing Mathematical Libraries}},
  author = {Lan Zhang, Xin Quan and Andre Freitas},
  booktitle = {Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing},
  year = {2024},
  doi = {10.18653/v1/2024.emnlp-main.233},
  eprint = {2410.04194},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.18653/v1/2024.emnlp-main.233}
}
```

- [← previous Can LLMs assist with Ambiguity? A Quantitative Evaluation of various Large Language Models on Word Sense Disambiguation](https://md.research.elamur.ai/free/en/papers/sumanathilaka-2024-llms-assist-ambiguity-quantitative-evaluation/)
- [next → Dialogue Discourse Parsing as Generation: A Sequence-to-Sequence LLM-based Approach](https://md.research.elamur.ai/free/en/papers/li-2024-dialogue-discourse-parsing-as-generation/)
- [↑ back to papers of 2024](https://md.research.elamur.ai/free/en/papers/2024/page/13/)

## References

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

1. Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W. Ayers, Dragomir Radev, and Jeremy Avigad. 2023. [Proofnet: Autoformalizing and formally proving undergraduate-level mathematics](https://md.research.elamur.ai/free/en/papers/azerbayev-2023-proofnet-autoformalizing-formally-proving-undergraduate/). Preprint, arXiv:2302.12433.
2. Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, Marco Dos Santos, Stephen Marcus McAleer, Albert Q. Jiang, Jia Deng, Stella Biderman, and Sean Welleck. 2024. [Llemma: An open language model for mathematics](https://md.research.elamur.ai/free/en/papers/azerbayev-2023-llemma-open-language-model-mathematics/). In The Twelfth International Conference on Learning Representations.
3. Steven Bird and Edward Loper. 2004. [NLTK: The natural language toolkit](https://md.research.elamur.ai/free/en/papers/bird-2006-nltk-natural-language-toolkit/). In Proceedings of the ACL Interactive Poster and Demonstration Sessions, pages 214–217, Barcelona, Spain. Association for Computational Linguistics.
4. Tom Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared D 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 Ziegler, Jeffrey Wu, Clemens Winter, Chri… — [Language Models are Few-Shot Learners](https://md.research.elamur.ai/free/en/papers/brown-2020-language-models-few-shot-learners/)
5. Garett Cunningham, Razvan Bunescu, and David Juedes. 2022. [Towards autoformalization of mathematics and code correctness: Experiments with elementary proofs](https://md.research.elamur.ai/free/en/papers/cunningham-2022-autoformalization-mathematics-code-correctness-experiments/). In Proceedings of the 1st Workshop on Mathematical Natural Language Processing (MathNLP), pages 25–32, Abu Dhabi, United Arab Emirates (Hybrid…
6. Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. 2015. The lean theorem prover (system description). In Automated Deduction - CADE-25, pages 378–388, Cham. Springer International Publishing. [find](https://scholar.google.com/scholar?q=Leonardo+de+Moura%2C+Soonho+Kong%2C+Jeremy+Avigad%2C+Floris+van+Doorn%2C+and+Jakob+von+Raumer%2E+2015%2E+The+lean+theorem+prover+%28system+description%29%2E+In+Automated+Deduction+%2D+CADE%2D25%2C+pages+378%E2%80%93388%2C+Cham%2E+Spring)
7. Mikhail Evtikhiev, Egor Bogomolov, Yaroslav Sokolov, and Timofey Bryksin. 2023. Out of the bleu: How should we assess quality of the code generation models? J. Syst. Softw., 203(C). [find](https://scholar.google.com/scholar?q=Mikhail+Evtikhiev%2C+Egor+Bogomolov%2C+Yaroslav+Sokolov%2C+and+Timofey+Bryksin%2E+2023%2E+Out+of+the+bleu%3A+How+should+we+assess+quality+of+the+code+generation+models%3F+J%2E+Syst%2E+Softw%2E%2C+203%28C%29%2E)
8. Emily C First, Markus Norman Rabe, Talia Ringer, and Yuriy Brun. 2023. [Baldur: Whole-proof generation and repair with large language models](https://md.research.elamur.ai/free/en/papers/first-2023-baldur-whole-proof-generation-repair/). Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering.
9. Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward Ayers, and Stanislas Polu. 2022. [Proof artifact co-training for theorem proving with language models](https://md.research.elamur.ai/free/en/papers/han-2021-proof-artifact-co-training-theorem/). In International Conference on Learning Representations.
10. Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. 2021. [Measuring mathematical problem solving with the MATH dataset](https://md.research.elamur.ai/free/en/papers/hendrycks-2021-measuring-mathematical-problem-solving-math/). In Thirty-fifth Conference on Neural Information Processing Systems Datasets and Benchmarks Track (Round 2).
11. Albert Q. Jiang, Alexandre Sablayrolles, Arthur Mensch, Chris Bamford, Devendra Singh Chaplot, Diego de las Casas, Florian Bressand, Gianna Lengyel, Guillaume Lample, Lucile Saulnier, Lélio Renard Lavaud, Marie-Anne Lachaux, Pierre Stock, Teven Le Scao, Thibaut Lavril, Thomas Wang, Timothée Lacroix,… [find](https://scholar.google.com/scholar?q=Albert+Q%2E+Jiang%2C+Alexandre+Sablayrolles%2C+Arthur+Mensch%2C+Chris+Bamford%2C+Devendra+Singh+Chaplot%2C+Diego+de+las+Casas%2C+Florian+Bressand%2C+Gianna+Lengyel%2C+Guillaume+Lample%2C+Lucile+Saulnier%2C+L%C3%A9lio+Renard+Lav)
12. Albert Q. Jiang, Alexandre Sablayrolles, Antoine Roux, Arthur Mensch, Blanche Savary, Chris Bamford, Devendra Singh Chaplot, Diego de las Casas, Emma Bou Hanna, Florian Bressand, Gianna Lengyel, Guillaume Bour, Guillaume Lample, Lélio Renard Lavaud, Lucile Saulnier, Marie-Anne Lachaux, Pierre Stock,… [find](https://scholar.google.com/scholar?q=Albert+Q%2E+Jiang%2C+Alexandre+Sablayrolles%2C+Antoine+Roux%2C+Arthur+Mensch%2C+Blanche+Savary%2C+Chris+Bamford%2C+Devendra+Singh+Chaplot%2C+Diego+de+las+Casas%2C+Emma+Bou+Hanna%2C+Florian+Bressand%2C+Gianna+Lengyel%2C+Guill)
13. Albert Qiaochu Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygóźdź, Piotr Mił oś, Yuhuai Wu, and Mateja Jamnik. 2022. [Thor: Wielding hammers to integrate language models and automated theorem provers](https://md.research.elamur.ai/free/en/papers/jiang-2022-thor-wielding-hammers-integrate-language/). In Advances in Neural Information Processing Systems, volume 35, pages 8360…
14. Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Timothee Lacroix, Jiacheng Liu, Wenda Li, Mateja Jamnik, Guillaume Lample, and Yuhuai Wu. 2023b. [Draft, sketch, and prove: Guiding formal theorem provers with informal proofs](https://md.research.elamur.ai/free/en/papers/jiang-2022-draft-sketch-prove-guiding-formal/). In The Eleventh International Conference on Learning Representations.
15. Dongwei Jiang, Marcio Fonseca, and Shay B. Cohen. 2024b. [Leanreasoner: Boosting complex logical reasoning with lean](https://md.research.elamur.ai/free/en/papers/jiang-2024-leanreasoner-boosting-complex-logical-reasoning/). Preprint, arXiv:2403.13312.
16. Patrick Lewis, Ethan Perez, Aleksandra Piktus, Fabio Petroni, Vladimir Karpukhin, Naman Goyal, Heinrich Küttler, Mike Lewis, Wen-tau Yih, Tim Rocktäschel, Sebastian Riedel, and Douwe Kiela. 2020. [Retrieval-augmented generation for knowledge-intensive nlp tasks](https://md.research.elamur.ai/free/en/papers/lewis-2020-retrieval-augmented-generation-knowledge-intensive/). In Advances in Neural Information Proc…
17. Jiayu Liu, Zhenya Huang, ChengXiang Zhai, and Qi Liu. 2023. Learning by applying: A general framework for mathematical reasoning via enhancing explicit knowledge learning. Proceedings of the AAAI Conference on Artificial Intelligence, 37(4):4497–4506. [find](https://scholar.google.com/scholar?q=Jiayu+Liu%2C+Zhenya+Huang%2C+ChengXiang+Zhai%2C+and+Qi+Liu%2E+2023%2E+Learning+by+applying%3A+A+general+framework+for+mathematical+reasoning+via+enhancing+explicit+knowledge+learning%2E+Proceedings+of+the+AAAI+Conf)
18. Jianqiao Lu, Zhengying Liu, Yingjia Wan, Yinya Huang, Haiming Wang, Zhicheng Yang, Jing Tang, and Zhijiang Guo. 2024. [Process-driven autoformalization in lean 4](https://md.research.elamur.ai/free/en/papers/lu-2024-process-driven-autoformalization-lean-4/). arXiv preprint arXiv:2406.01940.
19. Pan Lu, Liang Qiu, Wenhao Yu, Sean Welleck, and Kai-Wei Chang. 2023. A survey of deep learning for mathematical reasoning. In Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pages 14605– 14631, Toronto, Canada. Association for Computat… [find](https://scholar.google.com/scholar?q=Pan+Lu%2C+Liang+Qiu%2C+Wenhao+Yu%2C+Sean+Welleck%2C+and+Kai%2DWei+Chang%2E+2023%2E+A+survey+of+deep+learning+for+mathematical+reasoning%2E+In+Proceedings+of+the+61st+Annual+Meeting+of+the+Association+for+Computationa)
20. Shuai Lu, Nan Duan, Hojae Han, Daya Guo, Seung-won Hwang, and Alexey Svyatkovskiy. 2022. [ReACC: A retrieval-augmented code completion framework](https://md.research.elamur.ai/free/en/papers/lu-2022-reacc-retrieval-augmented-code-completion/). In Proceedings of the 60th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pages 6227–6240, Dublin, Ireland. Assoc…
21. Aman Madaan, Niket Tandon, Prakhar Gupta, Skyler Hallinan, Luyu Gao, Sarah Wiegreffe, Uri Alon, Nouha Dziri, Shrimai Prabhumoye, Yiming Yang, Shashank Gupta, Bodhisattwa Prasad Majumder, Katherine Hermann, Sean Welleck, Amir Yazdanbakhsh, and Peter Clark. 2023. Self-refine: Iterative refinement with… [find](https://scholar.google.com/scholar?q=Aman+Madaan%2C+Niket+Tandon%2C+Prakhar+Gupta%2C+Skyler+Hallinan%2C+Luyu+Gao%2C+Sarah+Wiegreffe%2C+Uri+Alon%2C+Nouha+Dziri%2C+Shrimai+Prabhumoye%2C+Yiming+Yang%2C+Shashank+Gupta%2C+Bodhisattwa+Prasad+Majumder%2C+Katherine+Her)
22. Jordan Meadows and André Freitas. 2023. Introduction to mathematical language processing: Informal proofs, word problems, and supporting tasks. Transactions of the Association for Computational Linguistics, 11:1162–1184. [find](https://scholar.google.com/scholar?q=Jordan+Meadows+and+Andr%C3%A9+Freitas%2E+2023%2E+Introduction+to+mathematical+language+processing%3A+Informal+proofs%2C+word+problems%2C+and+supporting+tasks%2E+Transactions+of+the+Association+for+Computational+Lingui)
23. Long Ouyang, Jeffrey Wu, Xu Jiang, Diogo Almeida, Carroll Wainwright, Pamela Mishkin, Chong Zhang, Sandhini Agarwal, Katarina Slama, Alex Ray, John Schulman, Jacob Hilton, Fraser Kelton, Luke Miller, Maddie Simens, Amanda Askell, Peter Welinder, Paul F Christiano, Jan Leike, and Ryan Lowe. 2022. Tra… — [Training language models to follow instructions with human feedback](https://md.research.elamur.ai/free/en/papers/ouyang-2022-training-language-models-follow-instructions/)
24. Liangming Pan, Alon Albalak, Xinyi Wang, and William Wang. 2023. [Logic-LM: Empowering large language models with symbolic solvers for faithful logical reasoning](https://md.research.elamur.ai/free/en/papers/pan-2023-logic-lm-empowering-large-language/). In Findings of the Association for Computational Linguistics: EMNLP 2023, pages 3806–3824, Singapore. Association for Computational Lingui…
25. Liangming Pan, Michael Saxon, Wenda Xu, Deepak Nathani, Xinyi Wang, and William Yang Wang. 2024. [Automatically correcting large language models: Surveying the landscape of diverse automated correction strategies](https://md.research.elamur.ai/free/en/papers/pan-2024-automatically-correcting-large-language-models/). Transactions of the Association for Computational Linguistics, 11:484–506.
26. Kishore Papineni, Salim Roukos, Todd Ward, and Wei-Jing Zhu. 2002. [Bleu: a method for automatic evaluation of machine translation](https://md.research.elamur.ai/free/en/papers/papineni-2002-bleu-method-automatic-evaluation-machine/). In Proceedings of the 40th Annual Meeting of the Association for Computational Linguistics, pages 311–318, Philadelphia, Pennsylvania, USA. Association for Computational…
27. Lawrence C. Paulson. 2000. [Isabelle: The next 700 theorem provers](https://md.research.elamur.ai/free/en/papers/paulson-2000-isabelle-next-700-theorem-provers/). Preprint, arXiv:cs/9301106.
28. Stanislas Polu and Ilya Sutskever. 2020. [Generative language modeling for automated theorem proving](https://md.research.elamur.ai/free/en/papers/polu-2020-generative-language-modeling-automated-theorem/). Preprint, arXiv:2009.03393.
29. Maja Popović. 2015. [chrF: character n-gram F-score for automatic MT evaluation](https://md.research.elamur.ai/free/en/papers/popovic-2015-chrf-character-n-gram-f/). In Proceedings of the Tenth Workshop on Statistical Machine Translation, pages 392–395, Lisbon, Portugal. Association for Computational Linguistics.
30. Xin Quan, Marco Valentino, Louise Dennis, and Andre Freitas. 2024a. Enhancing ethical explanations of large language models through iterative symbolic refinement. In Proceedings of the 18th Conference of the European Chapter of the Association for Computational Linguistics (Volume 1: Long Papers), p… [find](https://scholar.google.com/scholar?q=Xin+Quan%2C+Marco+Valentino%2C+Louise+Dennis%2C+and+Andre+Freitas%2E+2024a%2E+Enhancing+ethical+explanations+of+large+language+models+through+iterative+symbolic+refinement%2E+In+Proceedings+of+the+18th+Conference)
31. Xin Quan, Marco Valentino, Louise A. Dennis, and André Freitas. 2024b. [Verification and refinement of natural language explanations through llm-symbolic theorem proving](https://md.research.elamur.ai/free/en/papers/quan-2024-verification-refinement-natural-language-explanations/). Preprint, arXiv:2405.01379.
32. Stephen E. Robertson, Steve Walker, Susan Jones, Micheline Hancock-Beaulieu, and Mike Gatford. 1994. [Okapi at trec-3](https://md.research.elamur.ai/free/en/papers/robertson-1994-okapi-trec-3/). In TREC, volume 500-225 of NIST Special Publication, pages 109–126. National Institute of Standards and Technology (NIST).
33. David Saxton, Edward Grefenstette, Felix Hill, and Pushmeet Kohli. 2019. [Analysing mathematical reasoning abilities of neural models](https://md.research.elamur.ai/free/en/papers/saxton-2019-analysing-mathematical-reasoning-abilities-neural/). ArXiv, abs/1904.01557.
34. Peter Scholze. 2022. Liquid tensor experiment. Experimental Mathematics, 31(2):349–354. [find](https://scholar.google.com/scholar?q=Peter+Scholze%2E+2022%2E+Liquid+tensor+experiment%2E+Experimental+Mathematics%2C+31%282%29%3A349%E2%80%93354%2E)
35. Boris Shminke. 2022. Python client for isabelle server. Preprint, arXiv:2212.11173. — [arXiv:2212.11173](https://arxiv.org/abs/2212.11173) [find](https://scholar.google.com/scholar?q=Boris+Shminke%2E+2022%2E+Python+client+for+isabelle+server%2E+Preprint%2C+arXiv%3A2212%2E11173%2E+%E2%80%94+%5BarXiv%3A2212%2E11173%5D%28https%3A%2F%2Farxiv%2Eorg%2Fabs%2F2212%2E11173%29)
36. Ngoc Tran, Hieu Tran, Son Nguyen, Hoan Nguyen, and Tien N. Nguyen. 2019. Does bleu score work for code migration? In Proceedings of the 27th International Conference on Program Comprehension, ICPC ’19, page 165–176. IEEE Press. [find](https://scholar.google.com/scholar?q=Ngoc+Tran%2C+Hieu+Tran%2C+Son+Nguyen%2C+Hoan+Nguyen%2C+and+Tien+N%2E+Nguyen%2E+2019%2E+Does+bleu+score+work+for+code+migration%3F+In+Proceedings+of+the+27th+International+Conference+on+Program+Comprehension%2C+ICPC+%E2%80%9919)
37. Mingzhe Wang and Jia Deng. 2020. [Learning to prove theorems by learning to generate theorems](https://md.research.elamur.ai/free/en/papers/wang-2020-learning-prove-theorems-learning-generate/). In Advances in Neural Information Processing Systems, volume 33, pages 18146–18157. Curran Associates, Inc.
38. Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, brian ichter, Fei Xia, Ed Chi, Quoc V Le, and Denny Zhou. 2022. [Chain-of-thought prompting elicits reasoning in large language models](https://md.research.elamur.ai/free/en/papers/wei-2022-chain-thought-prompting-elicits-reasoning/). In Advances in Neural Information Processing Systems, volume 35, pages 24824–24837. Curran Associates, Inc.
39. Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Norman Rabe, Charles E Staats, Mateja Jamnik, and Christian Szegedy. 2022. [Autoformalization with large language models](https://md.research.elamur.ai/free/en/papers/wu-2022-autoformalization-large-language-models/). In Advances in Neural Information Processing Systems.
40. Huajian Xin, Haiming Wang, Chuanyang Zheng, Lin Li, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, Jian Yin, Zhenguo Li, Xiaodan Liang, and Heng Liao. 2023. [Lego-prover: Neural theorem proving with growing libraries](https://md.research.elamur.ai/free/en/papers/wang-2023-lego-prover-neural-theorem-proving/). ArXiv, abs/2310.00656.
41. Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chala-mala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. 2023. [LeanDojo: Theorem proving with retrieval-augmented language models](https://md.research.elamur.ai/free/en/papers/yang-2023-leandojo-theorem-proving-retrieval-augmented/). In Neural Information Processing Systems (NeurIPS).
42. Kun Zhang, Xiexiong Lin, Yuanzhuo Wang, Xin Zhang, Fei Sun, Cen Jianhe, Hexiang Tan, Xuhui Jiang, and Huawei Shen. 2023. ReFSQL: A retrieval-augmentation framework for text-to-SQL generation. In Findings of the Association for Computational Linguistics: EMNLP 2023, pages 664–673, Singapore. Associat… [find](https://scholar.google.com/scholar?q=Kun+Zhang%2C+Xiexiong+Lin%2C+Yuanzhuo+Wang%2C+Xin+Zhang%2C+Fei+Sun%2C+Cen+Jianhe%2C+Hexiang+Tan%2C+Xuhui+Jiang%2C+and+Huawei+Shen%2E+2023%2E+ReFSQL%3A+A+retrieval%2Daugmentation+framework+for+text%2Dto%2DSQL+generation%2E+In+Findi)
43. Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. 2022. [minif2f: a cross-system benchmark for formal olympiad-level mathematics](https://md.research.elamur.ai/free/en/papers/zheng-2021-minif2f-cross-system-benchmark-formal/). In International Conference on Learning Representations.
44. Shuyan Zhou, Uri Alon, Sumit Agarwal, and Graham Neubig. 2023. CodeBERTScore: Evaluating code generation with pretrained models of code. In Proceedings of the 2023 Conference on Empirical Methods in Natural Language Processing, pages 13921– 13937, Singapore. Association for Computational Linguistics… [find](https://scholar.google.com/scholar?q=Shuyan+Zhou%2C+Uri+Alon%2C+Sumit+Agarwal%2C+and+Graham+Neubig%2E+2023%2E+CodeBERTScore%3A+Evaluating+code+generation+with+pretrained+models+of+code%2E+In+Proceedings+of+the+2023+Conference+on+Empirical+Methods+in+N)

*Updated 3 November 2026*