Elamur Research⌕
☰
home / papers / 2024 / Formal Mathematical Reasoning: A New Frontier in AI

Formal Mathematical Reasoning: A New Frontier in AI

Paper · 2024 · Kaiyu Yang, Gabriel Poesia, Jingxuan He et al.

Summary

This position paper argues that informal AI-for-mathematics is approaching its limits. That approach pretrains LLMs on math text and then finetunes them on worked solutions, but its successes mostly stop around AIME-level school problems. Advanced mathematics lacks plentiful training data, and long proofs are hard to check, so model hallucinations go unnoticed. The authors propose formal mathematical reasoning as a complementary path. In this approach, reasoning rests on formal frameworks like Lean, Coq, Isabelle, or specification-annotated programs, which can verify each step and return automatic feedback. The paper does not introduce a new model or dataset. Instead, it:

  • surveys progress in neural theorem proving and autoformalization, citing AlphaProof and AlphaGeometry as evidence;
  • describes the growing tooling that connects LLMs with proof assistants;
  • outlines open problems in data and algorithms;
  • proposes staged milestones, including capability levels for AI-assisted formal verification of code and hardware.

The authors see the field at a turning point. Verified reasoning could advance mathematical research and make formally certified software affordable beyond safety-critical niches.

Key points

  • Case study: NuminaMath won the first AIMO Progress Prize (July 2024) by solving 29 of 50 private test problems. It and the other top entries built on DeepSeekMath-Base 7B.
  • AlphaProof uses Lean together with autoformalization and reinforcement learning. The authors describe it as the first AI to reach IMO silver-medal level.
  • According to a cited survey, publications on AI for formal reasoning nearly doubled in 2023 and were expected to double again in 2024.
  • The proposed verification roadmap runs from Level 0 to Level 4:
    • lower levels cover verifiable code generation, where no high-quality benchmark yet exists;
    • Level 2 covers project-scale verification, explored by the Selene benchmark built on seL4;
    • Level 3 covers proof maintenance;
    • Level 4 covers help with writing specifications.
  • The authors caution that benchmarks such as LeanDojo and PutnamBench miss how well provers serve evolving projects like the Fermat's Last Theorem formalization. They call for human-centered evaluation.

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

🎓Stanford UniversityStanford · United States567 works · 335,190 citations🎓University of EdinburghEdinburgh · United Kingdom395 works · 81,691 citations🎓University of California, BerkeleyBerkeley · United States243 works · 251,774 citations🎓The University of Texas at AustinAustin · United States126 works · 58,144 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 Kaiyu Yang, Gabriel Poesia, Jingxuan He, Wenda Li, Kristin Lauter, Swarat Chaudhuri and Dawn Song. 2024. Formal Mathematical Reasoning: A New Frontier in AI. arXiv:2412.16075.

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

@misc{yang2024formal,
  title = {{Formal Mathematical Reasoning: A New Frontier in AI}},
  author = {Kaiyu Yang, Gabriel Poesia, Jingxuan He, Wenda Li, Kristin Lauter, Swarat Chaudhuri and Dawn Song},
  year = {2024},
  doi = {10.48550/arxiv.2412.16075},
  eprint = {2412.16075},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2412.16075}
}

References

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

  1. Allen Newell and Herbert Simon. The logic theory machine–a complex information processing system. IRE Transactions on information theory, 1956. 1 — The logic theory machine: A complex information processing system
  2. Alfred North Whitehead and Bertrand Russell. Principia Mathematica. 1927. 1 find
  3. OpenAI. GPT-4 technical report. arXiv preprint arXiv:2303.08774, 2023. 1, 4, 9
  4. Hugo Touvron, Thibaut Lavril, Gautier Izacard, Xavier Martinet, Marie-Anne Lachaux, Timothée Lacroix, Baptiste Rozière, Naman Goyal, Eric Hambro, Faisal Azhar, Aurelien Rodriguez, Armand Joulin, Edouard Grave, and Guillaume Lample. LLaMa: Open and efficient foundation language models. arXiv preprint…
  5. Trieu H Trinh, Yuhuai Wu, Quoc V Le, He He, and Thang Luong. Solving olympiad geometry without human demonstrations. Nature, 2024. 1, 2, 12, 15, 17, 22
  6. XTX Markets. AIMO Prize. https://aimoprize.com/, 2024. 1, 22 ↗
  7. AlphaProof and AlphaGeometry teams. AI achieves silver-medal standard solving international mathematical olympiad problems. https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/, 2024. 1, 2, 3, 10, 13, 15, 22 ↗
  8. Longhui Yu, Weisen Jiang, Han Shi, YU Jincheng, Zhengying Liu, Yu Zhang, James Kwok, Zhenguo Li, Adrian Weller, and Weiyang Liu. MetaMath: Bootstrap your own mathematical questions for large language models. In International Conference on Learning Representations (ICLR), 2024. 1, 3, 12
  9. Xiang Yue, Xingwei Qu, Ge Zhang, Yao Fu, Wenhao Huang, Huan Sun, Yu Su, and Wenhu Chen. MAmmoTH: Building math generalist models through hybrid instruction tuning. In International Conference on Learning Representations (ICLR), 2024. 3
  10. Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, Marco Dos Santos, Stephen Marcus McAleer, Albert Q Jiang, Jia Deng, Stella Biderman, and Sean Welleck. Llemma: An open language model for mathematics. In International Conference on Learning Representations (ICLR), 2024. 3, 12
  11. Zhihong Shao, Peiyi Wang, Qihao Zhu, Runxin Xu, Junxiao Song, Mingchuan Zhang, YK Li, Yu Wu, and Daya Guo. DeepSeekMath: Pushing the limits of mathematical reasoning in open language models. arXiv preprint arXiv:2402.03300, 2024. 1, 3
  12. Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, Brian Ichter, Fei Xia, Ed Chi, Quoc V Le, and Denny Zhou. Chain-of-thought prompting elicits reasoning in large language models. In Neural Information Processing Systems (NeurIPS), 2022. 1, 4, 14, 21
  13. Xuezhi Wang, Jason Wei, Dale Schuurmans, Quoc V Le, Ed H Chi, Sharan Narang, Aakanksha Chowdhery, and Denny Zhou. Self-consistency improves chain of thought reasoning in language models. In International Conference on Learning Representations (ICLR), 2023. 1
  14. Zhibin Gou, Zhihong Shao, Yeyun Gong, Yelong Shen, Yujiu Yang, Minlie Huang, Nan Duan, and Weizhu Chen. ToRA: A tool-integrated reasoning agent for mathematical problem solving. In International Conference on Learning Representations (ICLR), 2024. 1, 3, 4, 22
  15. Karl Cobbe, Vineet Kosaraju, Mohammad Bavarian, Mark Chen, Heewoo Jun, Lukasz Kaiser, Matthias Plappert, Jerry Tworek, Jacob Hilton, Reiichiro Nakano, Christopher Hesse, and John Schulman. Training verifiers to solve math word problems. arXiv preprint arXiv:2110.14168, 2021. 1, 2, 3, 11, 21, 22
  16. 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. In Neural Information Processing Systems (NeurIPS), Datasets and Benchmarks Track, 2021. 1, 3, 14, 21, 22
  17. OpenAI. Learning to reason with LLMs. learning-to-reason-with-llms/, 2024. 2, 3, 15 find
  18. Jordan Hoffmann, Sebastian Borgeaud, Arthur Mensch, Elena Buchatskaya, Trevor Cai, Eliza Rutherford, Diego de Las Casas, Lisa Anne Hendricks, Johannes Welbl, Aidan Clark, et al. Training compute-optimal large language models. In Neural Information Processing Systems (NeurIPS), 2022. 2, 12, 14
  19. Biao Zhang, Zhongtao Liu, Colin Cherry, and Orhan Firat. When scaling meets LLM finetuning: The effect of data, model and finetuning method. In International Conference on Learning Representations (ICLR), 2024. 2, 12, 14 https://openai.com/index/ ↗
  20. Tobias Nipkow, Markus Wenzel, and Lawrence C Paulson. Isabelle/HOL: a proof assistant for higher-order logic. 2002. 2, 5, 20 find
  21. Bruno Barras, Samuel Boutin, Cristina Cornes, Judicaël Courant, Jean-Christophe Filliatre, Eduardo Gimenez, Hugo Herbelin, Gerard Huet, Cesar Munoz, Chetan Murthy, et al. The Coq proof assistant reference manual: Version 6.1. PhD thesis, Inria, 1997. 2, 5, 20 find
  22. K Rustan M Leino. Dafny: An automatic program verifier for functional correctness. In International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR), 2010. 2 find
  23. Timo Schick, Jane Dwivedi-Yu, Roberto Dessì, Roberta Raileanu, Maria Lomeli, Eric Hambro, Luke Zettlemoyer, Nicola Cancedda, and Thomas Scialom. Toolformer: Language models can teach themselves to use tools. In Neural Information Processing Systems (NeurIPS), 2024. 2
  24. Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. The Lean theorem prover (system description). In International Conference on Automated Deduction (CADE), 2015. 2, 5, 6, 20 find
  25. Leonardo de Moura and Sebastian Ullrich. The Lean 4 theorem prover and programming language. In International Conference on Automated Deduction (CADE), 2021. 2, 5, 6, 20
  26. Josef Urban, Jiří Vyskočil, and Petr Štěpánek. MaLeCoP machine learning connection prover. In International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, 2011. 2 find
  27. Cezary Kaliszyk, Josef Urban, Henryk Michalewski, and Miroslav Olšák. Reinforcement learning of theorem proving. In Neural Information Processing Systems (NeurIPS), 2018.
  28. Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, and Michael Norrish. TacticToe: learning to prove with tactics. Journal of Automated Reasoning, 2021. find
  29. Geoffrey Irving, Christian Szegedy, Alexander A Alemi, Niklas Eén, François Chollet, and Josef Urban. DeepMath - deep sequence models for premise selection. In Neural Information Processing Systems (NeurIPS), 2016. 10
  30. Cezary Kaliszyk, François Chollet, and Christian Szegedy. HolStep: A machine learning dataset for higher-order logic theorem proving. In International Conference on Learning Representations (ICLR), 2017.
  31. Sarah Loos, Geoffrey Irving, Christian Szegedy, and Cezary Kaliszyk. Deep Network Guided Proof Search. In International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), 2017.
  32. Daniel Huang, Prafulla Dhariwal, Dawn Song, and Ilya Sutskever. GamePad: A learning environment for theorem proving. In International Conference on Learning Representations (ICLR), 2019. 13
  33. Kaiyu Yang and Jia Deng. Learning to prove theorems via interacting with proof assistants. In International Conference on Machine Learning (ICML), 2019. 2, 19, 20
  34. Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03393, 2020. 2, 9, 14
  35. Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. LeanDojo: Theorem proving with retrieval-augmented language models. In Neural Information Processing Systems (NeurIPS), 2023. 2, 9, 10, 13, 14, 15, 17, 19, 20, 27
  36. Amitayush Thakur, George Tsoukalas, Yeming Wen, Jimmy Xin, and Swarat Chaudhuri. An in-context learning agent for formal theorem-proving. In Conference on Language Modeling (COLM), 2024. 2, 9, 10, 11, 13, 17, 26
  37. Yuhuai Wu, Albert Jiang, Wenda Li, Markus Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models. In Neural Information Processing Systems (NeurIPS), 2022. 2, 9, 13, 14, 19
  38. Albert Q. Jiang, Wenda Li, and Mateja Jamnik. Multi-language diversity benefits autoformalization, 2024. 2, 9, 13 find
  39. Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. DeepSeek-Prover: Advancing theorem proving in LLMs through large-scale synthetic data. arXiv preprint arXiv:2405.14333, 2024. 2, 7, 9, 13, 15
  40. Emily First, Markus N Rabe, Talia Ringer, and Yuriy Brun. Baldur: Whole-proof generation and repair with large language models. In ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE), 2023. 2, 7, 9, 11, 15, 26
  41. Mathlib Community. Completion of the liquid tensor experiment. https://leanprover-community.github.io/blog/posts/lte-final/, 2022. 2, 23 ↗
  42. The mathlib community. The Lean mathematical library. In Certified Programs and Proofs (CPP), 2020. 2, 6, 24
  43. Peiyang Song, Kaiyu Yang, and Anima Anandkumar. Towards large language models as copilots for theorem proving in Lean. arXiv preprint arXiv: Arxiv-2404.12534, 2024. 3, 20 find
  44. Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang, and Xujie Si. A survey on deep learning for theorem proving. In Conference on Language Modeling (COLM), 2024. 3
  45. Andrew W Appel. Verified software toolchain: (invited talk). In European Symposium on Programming, 2011. 3 find
  46. Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. seL4: Formal verification of an OS kernel. In Symposium on Operating systems principles (SOSP)… find
  47. Xavier Leroy, Sandrine Blazy, Daniel Kästner, Bernhard Schommer, Markus Pister, and Christian Ferdinand. CompCert-a formally verified optimizing compiler. In Embedded Real Time Software and Systems (ERTS), 2016. 11, 26 find
  48. Chris Hawblitzel, Jon Howell, Jacob R Lorch, Arjun Narayan, Bryan Parno, Danfeng Zhang, and Brian Zill. Ironclad Apps: End-to-end security via automated full-system verification. In Symposium on Operating Systems Design and Implementation (OSDI), 2014. 3 find
  49. Yann Fleureau, Jia Li, Edward Beeching, Lewis Tunstall, Ben Lipkin, Roman Soletskyi, Shengyi Costa Huang, and Kashif Rasul. How NuminaMath won the 1st AIMO Progress Prize. https://huggingface.co/blog/winning-aimo-progress-prize, 2024. 3, 4 ↗
  50. Aitor Lewkowycz, Anders Andreassen, David Dohan, Ethan Dyer, Henryk Michalewski, Vinay Ramasesh, Ambrose Slone, Cem Anil, Imanol Schlag, Theo Gutman-Solo, et al. Solving quantitative reasoning problems with language models. In Neural Information Processing Systems (NeurIPS), 2022. 3, 14
  51. Huaiyuan Ying, Shuo Zhang, Linyang Li, Zhejian Zhou, Yunfan Shao, Zhaoye Fei, Yichuan Ma, Jiawei Hong, Kuikun Liu, Ziyi Wang, et al. InternLM-Math: Open math large language models toward verifiable reasoning. arXiv preprint arXiv:2402.06332, 2024.
  52. Keiran Paster, Marco Dos Santos, Zhangir Azerbayev, and Jimmy Ba. OpenWebMath: An open dataset of high-quality mathematical web text. In International Conference on Learning Representations (ICLR), 2024. 3
  53. Shuo Yin, Weihao You, Zhilong Ji, Guoqiang Zhong, and Jinfeng Bai. MuMath-Code: Combining tool-use large language models with multi-perspective data augmentation for mathematical reasoning. arXiv preprint arXiv:2405.07551, 2024. 3, 4
  54. Baptiste Roziere, Jonas Gehring, Fabian Gloeckle, Sten Sootla, Itai Gat, Xiaoqing Ellen Tan, Yossi Adi, Jingyu Liu, Tal Remez, Jérémy Rapin, et al. Code Llama: Open foundation models for code. arXiv preprint arXiv:2308.12950, 2023. 3
  55. Jia Li, Edward Beeching, Lewis Tunstall, Ben Lipkin, Roman Soletskyi, Shengyi Huang, Kashif Rasul, Longhui Yu, Albert Q Jiang, Ziju Shen, Zihan Qin, Bin Dong, Li Zhou, Yann Fleureau, Guillaume Lample, and Stanislas Polu. NuminaMath: The largest public dataset in AI4Maths with 860k pairs of competiti… find
  56. Aaron Meurer, Christopher P Smith, Mateusz Paprocki, Ondřej Čertík, Sergey B Kirpichev, Matthew Rocklin, AMiT Kumar, Sergiu Ivanov, Jason K Moore, Sartaj Singh, et al. SymPy: symbolic computing in Python. PeerJ Computer Science, 2017. 4, 22 find
  57. Elliot Glazer, Ege Erdil, Tamay Besiroglu, Diego Chicharro, Evan Chen, Alex Gunning, Caroline Falkman Olsson, Jean-Stanislas Denain, Anson Ho, Emily de Oliveira Santos, et al. FrontierMath: A benchmark for evaluating advanced mathematical reasoning in AI. arXiv preprint arXiv:2411.04872, 2024. 4, 22
  58. Erica Klarreich. Titans of mathematics clash over epic proof of ABC conjecture. https://www.quantamagazine.org/titans-of-mathematics-clash-over-epic-proof-of-abc-conjecture-20180920/, 2018. 5 ↗
  59. Gladys Tyen, Hassan Mansoor, Peter Chen, Tony Mak, and Victor Cărbune. LLMs cannot find reasoning errors, but can correct them! In Findings of the Association for Computational Linguistics: ACL, 2024. 5 find
  60. Ning Miao, Yee Whye Teh, and Tom Rainforth. SelfCheck: Using LLMs to zero-shot check their own step-by-step reasoning. In International Conference on Learning Representations (ICLR), 2024.
  61. Zhan Ling, Yunhao Fang, Xuanlin Li, Zhiao Huang, Mingu Lee, Roland Memisevic, and Hao Su. Deductive verification of chain-of-thought reasoning. In Neural Information Processing Systems (NeurIPS), 2024. 5, 11, 21
  62. Jie Huang, Xinyun Chen, Swaroop Mishra, Huaixiu Steven Zheng, Adams Wei Yu, Xinying Song, and Denny Zhou. Large language models cannot self-correct reasoning yet. In International Conference on Learning Representations (ICLR), 2024. 5
  63. Kaya Stechly, Karthik Valmeekam, and Subbarao Kambhampati. On the self-verification limitations of large language models on reasoning and planning tasks. arXiv preprint arXiv:2402.08115, 2024.
  64. Zhibin Gou, Zhihong Shao, Yeyun Gong, Yelong Shen, Yujiu Yang, Nan Duan, and Weizhu Chen. CRITIC: Large language models can self-correct with tool-interactive critiquing. In International Conference on Learning Representations (ICLR), 2024.
  65. Chujie Zheng, Zhenru Zhang, Beichen Zhang, Runji Lin, Keming Lu, Bowen Yu, Dayiheng Liu, Jingren Zhou, and Junyang Lin. ProcessBench: Identifying process errors in mathematical reasoning. arXiv preprint arXiv:2412.06559, 2024. 21, 22
  66. Alex Gu, Wen-Ding Li, Naman Jain, Theo X Olausson, Celine Lee, Koushik Sen, and Armando Solar-Lezama. The counterfeit conundrum: Can code language models grasp the nuances of their incorrect generations? In Findings of the Association for Computational Linguistics: ACL, 2024. 5 find
  67. Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, 1989. 5 find
  68. Norman Megill and David A Wheeler. Metamath: a computer language for mathematical proofs. 2019. 5, 9
  69. Mike Gordon. From LCF to HOL: a short history. 2000. 5
  70. John Harrison. Metatheory and reflection in theorem proving: A survey and critique. Technical report, 1995. find
  71. Lawrence C Paulson. A formulation of the simple theory of types (for Isabelle). In International Conference on Computer Logic, 1988. 5 find
  72. Per Martin-Löf and Giovanni Sambin. Intuitionistic type theory. Bibliopolis Naples, 1984. 5 find
  73. T. Coquand and Gérard Huet. The calculus of constructions. Technical Report RR-0530, Inria, May 1986. URL https://inria.hal.science/inria-00076024. ↗
  74. Mario Carneiro. Lean4Lean: Towards a formalized metatheory for the Lean theorem prover. arXiv preprint arXiv:2403.14064, 2024. 5 find
  75. William A Howard. The formulae-as-types notion of construction. To HB Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, 1980. 5 find
  76. Abraham Adolf Fraenkel, Yehoshua Bar-Hillel, and Azriel Levy. Foundations of set theory. 1973. 5 find
  77. Feng-Hsiung Hsu. Behind Deep Blue: Building the computer that defeated the world chess champion. Princeton University Press, 2002. 5 find
  78. David Silver, Aja Huang, Chris J Maddison, Arthur Guez, Laurent Sifre, George Van Den Driessche, Julian Schrittwieser, Ioannis Antonoglou, Veda Panneershelvam, Marc Lanctot, et al. Mastering the game of Go with deep neural networks and tree search. Nature, 2016. 5, 9 find
  79. David Thrane Christiansen. Functional programming in Lean, 2023. 5 find
  80. W. T. Gowers, Ben Green, Freddie Manners, and Terence Tao. On a conjecture of Marton. arXiv preprint arXiv:2311.05762, 2023. 6
  81. Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Timothee Lacroix, Jiacheng Liu, Wenda Li, Mateja Jamnik, Guillaume Lample, and Yuhuai Wu. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. In International Conference on Learning Representations (ICLR), 2023. 7, 9, 10,…
  82. Logan Murphy, Kaiyu Yang, Jialiang Sun, Zhaoyu Li, Anima Anandkumar, and Xujie Si. Autoformalizing Euclidean geometry. In International Conference on Machine Learning (ICML), 2024. 7, 9, 13, 17, 24
  83. Jin Peng Zhou, Charles E Staats, Wenda Li, Christian Szegedy, Kilian Q Weinberger, and Yuhuai Wu. Don’t trust: Verify–grounding LLM quantitative reasoning with autoformalization. In International Conference on Learning Representations (ICLR), 2024. 7, 9, 22
  84. Francois Charton. Learning the greatest common divisor: explaining Transformer predictions. In International Conference on Learning Representations (ICLR), 2024. 8 find
  85. François Charton. Linear algebra with Transformers. arXiv preprint arXiv:2112.01898, 2021. 8
  86. Kristin Lauter, Cathy Yuanchen Li, Krystal Maughan, Rachel Newton, and Megha Srivastava. Machine learning for modular multiplication. arXiv preprint arXiv:2402.19254, 2024. 8 — [arXiv:2402.19254](https://arxiv.org/abs/2402.19254) find
  87. Emily Wenger, Mingjie Chen, Francois Charton, and Kristin E Lauter. Salsa: Attacking lattice cryptography with Transformers. In Neural Information Processing Systems (NeurIPS), 2022. 8 find
  88. Tianji Cai, Garrett W Merz, François Charton, Niklas Nolte, Matthias Wilhelm, Kyle Cranmer, and Lance J Dixon. Transforming the bootstrap: Using Transformers to compute scattering amplitudes in planar N = 4 super Yang-Mills theory. Machine Learning: Science and Technology, 2024. 8 find
  89. Alberto Alfarano, François Charton, and Amaury Hayat. Global Lyapunov functions: a long-standing open problem in mathematics, with symbolic Transformers. In Neural Information Processing Systems (NeurIPS), 2024. 8
  90. Maziar Raissi, Paris Perdikaris, and George Em Karniadakis. Physics informed deep learning (part I): Data-driven solutions of nonlinear partial differential equations. arXiv preprint arXiv:1711.10561, 2017. 8 — [arXiv:1711.10561](https://arxiv.org/abs/1711.10561) find
  91. Bernardino Romera-Paredes, Mohammadamin Barekatain, Alexander Novikov, Matej Balog, M Pawan Kumar, Emilien Dupont, Francisco JR Ruiz, Jordan S Ellenberg, Pengming Wang, Omar Fawzi, et al. Mathematical discoveries from program search with large language models. Nature, 2024. 8
  92. Terence Tao and Van H Vu. Additive combinatorics. Cambridge University Press, 2006. 8 find
  93. Sergei Gukov, James Halverson, Fabian Ruehle, and Piotr Sułkowski. Learning to unknot. Machine Learning: Science and Technology, 2021. 8 find
  94. Adam Zsolt Wagner. Constructions in combinatorics via neural networks. arXiv:2104.14516, 2021. 8, 17 — [arXiv:2104.14516](https://arxiv.org/abs/2104.14516) find
  95. François Charton, Jordan S Ellenberg, Adam Zsolt Wagner, and Geordie Williamson. PatternBoost: Constructions in mathematics with a little help from AI. arXiv preprint arXiv:2411.00566, 2024. 8 — [arXiv:2411.00566](https://arxiv.org/abs/2411.00566) find
  96. Gergely Bérczi and Adam Zsolt Wagner. A note on small percolating sets on hypercubes via generative AI. arXiv preprint arXiv:2411.19734, 2024. 8 — [arXiv:2411.19734](https://arxiv.org/abs/2411.19734) find
  97. Hao Wang. Toward mechanical mathematics. IBM Journal of Research and Development, 1960. 8 find
  98. Nicolaas Govert de Bruijn. Automath, a language for mathematics. 1983. 8 find
  99. Anonymous. The QED manifesto. In International Conference on Automated Deduction (CADE), 1994. 8 find
  100. Mohan Ganesalingam. The language of mathematics. Springer, 2013. 8 find
  101. Adam Grabowski, Artur Kornilowicz, and Adam Naumowicz. Mizar in a nutshell. Journal of Formalized Reasoning, 3(2):153–245, 2010. 8 find
  102. Daniel Kühlwein, Marcos Cramer, Peter Koepke, and Bernhard Schröder. The Naproche system. In International Conference on Intelligent Computer Mathematics (CICM), 2009. 8 find
  103. Konstantin Vershinin and Andrey Paskevich. ForTheL—the language of formal theories. International Journal of Information Theories and Applications, 2000. 8 arXiv preprint find
  104. Muhammad Humayoun and Christophe Raffalli. MathNat-mathematical text in a controlled natural language. Special issue: Natural Language Processing and its Applications, 2010. 8 find
  105. Patrick Massot. Teaching mathematics using lean and controlled natural language. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Schloss Dagstuhl–Leibniz-Zentrum für Informatik, 2024. 8 find
  106. Aarne Ranta. Grammatical framework. Journal of Functional Programming, 2004. 8 find
  107. Jan Frederik Schaefer and Michael Kohlhase. GLIF: A declarative framework for symbolic natural language understanding. In Workshop on Formal and Cognitive Reasoning, 2020. 8 find
  108. Shashank Pathak. GFLean: An autoformalisation framework for lean via GF. arXiv:2404.01234, 2024. 8
  109. Cezary Kaliszyk, Josef Urban, and Jiří Vyskočil. Learning to parse on aligned corpora (rough diamond). In International Conference on Interactive Theorem Proving (ITP), 2015. 9 find
  110. Cezary Kaliszyk, Josef Urban, and Jirí Vyskocil. System description: statistical parsing of informalized Mizar formulas. In International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), 2017. 9 find
  111. Qingxiang Wang, Cezary Kaliszyk, and Josef Urban. First experiments with neural translation of informal to formal mathematics. In International Conference on Intelligent Computer Mathematics (CICM), 2018. 9
  112. Qingxiang Wang, Chad Brown, Cezary Kaliszyk, and Josef Urban. Exploration of neural machine translation in autoformalization of mathematics in Mizar. In Certified Programs and Proofs (CPP), 2020. 9
  113. Guillaume Lample, Alexis Conneau, Ludovic Denoyer, and Marc’Aurelio Ranzato. Unsupervised machine translation using monolingual corpora only. In International Conference on Learning Representations (ICLR), 2018. 9
  114. Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W Ayers, Dragomir Radev, and Jeremy Avigad. ProofNet: Autoformalizing and formally proving undergraduate-level mathematics. arXiv preprint arXiv:2302.12433, 2023. 9, 23, 24
  115. Jianqiao Lu, Yingjia Wan, Zhengying Liu, Yinya Huang, Jing Xiong, Chengwu Liu, Jianhao Shen, Hui Jin, Jipeng Zhang, Haiming Wang, Zhicheng Yang, Jing Tang, and Zhijiang Guo. Process-driven autoformalization in Lean 4. arXiv preprint arXiv:2406.01940, 2024. 9, 14
  116. Boyan Li, Yuyu Luo, Chengliang Chai, Guoliang Li, and Nan Tang. The dawn of natural language to SQL: Are we fully ready? arXiv preprint arXiv:2406.01265, 2024. 9 — [arXiv:2406.01265](https://arxiv.org/abs/2406.01265) find
  117. Jiayi Pan, Glen Chou, and Dmitry Berenson. Data-efficient learning of natural language to linear temporal logic translators for robot task specification. In International Conference on Robotics and Automation (ICRA), 2023. 9 find
  118. Angelos Mavrogiannis, Christoforos Mavrogiannis, and Yiannis Aloimonos. Cook2LTL: Translating cooking recipes to LTL formulae using large language models. In International Conference on Robotics and Automation (ICRA), 2024. 9 find
  119. Theo Olausson, Alex Gu, Ben Lipkin, Cedegao Zhang, Armando Solar-Lezama, Joshua Tenenbaum, and Roger Levy. LINC: A neurosymbolic approach for logical reasoning by combining language models with first-order logic provers. In Conference on Empirical Methods in Natural Language Processing (EMNLP), 2023…
  120. Kurt Gödel. Über formal unentscheidbare sätze der Principia Mathematica und verwandter systeme I. Monatshefte für Mathematik und Physik, 1931. 9 find
  121. Daniel Whalen. Holophrasm: a neural automated theorem prover for higher-order logic. arXiv preprint arXiv:1608.02644, 2016. 9
  122. Junyoung Chung, Caglar Gulcehre, KyungHyun Cho, and Yoshua Bengio. Empirical evaluation of gated recurrent neural networks on sequence modeling. arXiv preprint arXiv:1412.3555, 2014. 9 find
  123. Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. Formal mathematics statement curriculum learning. In International Conference on Learning Representations (ICLR), 2023. 10 arXiv preprint
  124. Guillaume Lample, Timothee Lacroix, Marie-Anne Lachaux, Aurelien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, and Xavier Martinet. HyperTree proof search for neural theorem proving. In Neural Information Processing Systems (NeurIPS), 2022. 10, 14, 15
  125. Haohan Lin, Zhiqing Sun, Yiming Yang, and Sean Welleck. Lean-STaR: Learning to interleave thinking and proving. arXiv preprint arXiv:2407.10040, 2024. 10, 14
  126. Kevin Ellis, Lionel Wong, Maxwell Nye, Mathias Sable-Meyer, Luc Cary, Lore Anaya Pozo, Luke Hewitt, Armando Solar-Lezama, and Joshua B Tenenbaum. DreamCoder: growing generalizable, interpretable knowledge with wake–sleep bayesian program learning. Philosophical Transactions of the Royal Society A, 2… find
  127. Huajian Xin, Haiming Wang, Chuanyang Zheng, Lin Li, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, et al. LEGO-Prover: Neural theorem proving with growing libraries. In International Conference on Learning Representations (ICLR), 2023. 10, 16, 25
  128. Gabriel Poesia and Noah D Goodman. Peano: learning formal mathematical reasoning. Philosophical Transactions of the Royal Society A, 2023. 10, 16
  129. SA Schulz. Learning search control knowledge for equational deduction, volume 230. IOS Press, 2000. 10 find
  130. Daniel Kühlwein, Twan van Laarhoven, Evgeni Tsivtsivadze, Josef Urban, and Tom Heskes. Overview and evaluation of premise selection techniques for large theory mathematics. In Automated Reasoning: 6th International Joint Conference, IJCAR 2012, Manchester, UK, June 26-29, 2012. Proceedings 6, pages… find
  131. Jesse Alama, Tom Heskes, Daniel Kühlwein, Evgeni Tsivtsivadze, and Josef Urban. Premise selection for mathematics by corpus analysis and kernel methods. Journal of automated reasoning, 52:191–213, 2014. 10
  132. Bartosz Piotrowski and Josef Urban. Stateful premise selection by recurrent neural networks. arXiv preprint arXiv:2004.08212, 2020. 10
  133. Daniel Kühlwein, Jasmin Christian Blanchette, Cezary Kaliszyk, and Josef Urban. MaSh: machine learning for Sledgehammer. In International Conference on Interactive Theorem Proving (ITP), 2013. 10 find
  134. Jia Meng and Lawrence C Paulson. Lightweight relevance filtering for machine-generated resolution problems. Journal of Applied Logic, 2009. find
  135. Albert Qiaochu Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygóźdź, Piotr Miłoś, Yuhuai Wu, and Mateja Jamnik. Thor: Wielding hammers to integrate language models and automated theorem provers. In Neural Information Processing Systems (NeurIPS), 2022. 10
  136. Hunter Lightman, Vineet Kosaraju, Yuri Burda, Harrison Edwards, Bowen Baker, Teddy Lee, Jan Leike, John Schulman, Ilya Sutskever, and Karl Cobbe. Let’s verify step by step. In International Conference on Learning Representations (ICLR), 2024. 11, 14, 15, 22
  137. Kaiyu Yang, Jia Deng, and Danqi Chen. Generating natural language proofs with verifier-guided search. In Conference on Empirical Methods in Natural Language Processing (EMNLP), 2022. 11, 15, 22 find
  138. Xi Ye, Qiaochu Chen, Isil Dillig, and Greg Durrett. SatLM: Satisfiability-aided language models using declarative prompting. In Neural Information Processing Systems (NeurIPS), 2023. 11, 22
  139. Gabriel Poesia, Kanishk Gandhi, Eric Zelikman, and Noah D Goodman. Certified deductive reasoning with language models. Transactions on Machine Learning Research (TMLR), 2024. 11
  140. Charles Antony Richard Hoare. An axiomatic basis for computer programming. Communications of the ACM, 1969. 11 find
  141. Xavier Leroy. Formal verification of a realistic compiler. Communications of the ACM, 2009. find
  142. Talia Ringer, Karl Palmskog, Ilya Sergey, Milos Gligoric, and Zachary Tatlock. QED at large: A survey of engineering of formally verified software. Foundations and Trends® in Programming Languages, 2019. 11, 19 find
  143. Erik Seligman, Tom Schubert, and MV Achutha Kiran Kumar. Formal verification: an essential toolkit for modern VLSI design. 2023. 11 find
  144. Shilpi Goel and Sandip Ray. Microprocessor assurance and the role of theorem proving. In Handbook of Computer Architecture, pages 1–43. 2022. 11 find
  145. Bishop Brock, Matt Kaufmann, and J Strother Moore. ACL2 theorems about commercial microprocessors. In International Conference on Formal Methods in Computer-Aided Design (FMCAD), 1996. 11 find
  146. Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M Frans Kaashoek, and Nickolai Zeldovich. Using crash Hoare logic for certifying the FSCQ file system. In Symposium on Operating Systems Principles (SOSP), 2015. 11 find
  147. Tej Chajed, Joseph Tassarotti, Mark Theng, M Frans Kaashoek, and Nickolai Zeldovich. Verifying the DaisyNFS concurrent and crash-safe file system with sequential reasoning. In Symposium on Operating Systems Design and Implementation (OSDI), 2022. 11 find
  148. Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan Newman Wu, Jieung Kim, Vilhelm Sjöberg, and David Costanzo. CertiKOS: An extensible architecture for building certified concurrent OS kernels. In Symposium on Operating Systems Design and Implementation (OSDI), 2016. 11, 26 find
  149. Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, and Pierre-Yves Strub. Implementing TLS with verified cryptographic security. In Symposium on Security and Privacy, 2013. 11 find
  150. Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, and Santiago Zanella Béguelin. Computer-aided security proofs for the working cryptographer. In Advances in Cryptology (CRYPTO), 2011. 11 find
  151. Upamanyu Sharma, Ralf Jung, Joseph Tassarotti, Frans Kaashoek, and Nickolai Zeldovich. Grove: a separation-logic library for verifying distributed systems. In Symposium on Operating Systems Principles (SOSP), 2023. 11 find
  152. Karthikeyan Bhargavan, Barry Bond, Antoine Delignat-Lavaud, Cédric Fournet, Chris Hawblitzel, Catalin Hritcu, Samin Ishtiaq, Markulf Kohlweiss, Rustan Leino, Jay R Lorch, et al. Everest: Towards a verified, drop-in replacement of HTTPS. In Summit on Advances in Programming Languages (SNAPL), 2017. 1… find
  153. Naiqian Zheng, Mengqi Liu, Yuxing Xiang, Linjian Song, Dong Li, Feng Han, Nan Wang, Yong Ma, Zhuo Liang, Dennis Cai, et al. Automated verification of an in-production DNS authoritative engine. In Symposium on Operating Systems Principles (SOSP), 2023. 11 find
  154. Gerwin Klein. Proof engineering considered essential. In International Symposium on Formal Methods, 2014. 11 find
  155. Alex Sanchez-Stern, Yousef Alhessi, Lawrence Saul, and Sorin Lerner. Generating correctness proofs with neural networks. In SIGPLAN International Workshop on Machine Learning and Programming Languages, 2020. 11
  156. Alex Sanchez-Stern, Abhishek Varghese, Zhanna Kaufman, Dylan Zhang, Talia Ringer, and Yuriy Brun. QEDCartographer: Automating formal verification using reward-free reinforcement learning. In International Conference on Software Engineering (ICSE), 2025. 11 find
  157. Minghai Lu, Benjamin Delaware, and Tianyi Zhang. Proof automation with large language models. In International Conference on Automated Software Engineering (ASE), 2024. 11 find
  158. Kexin Pei, David Bieber, Kensen Shi, Charles Sutton, and Pengcheng Yin. Can large language models reason about program invariants? In International Conference on Machine Learning (ICML), 2023. 11 find
  159. Haoze Wu, Clark Barrett, and Nina Narodytska. Lemur: Integrating large language models in automated program verification. In International Conference on Learning Representations (ICLR), 2024.
  160. Chloe Loughridge, Qinyi Sun, Seth Ahrenbach, Federico Cassano, Chuyue Sun, Ying Sheng, Anish Mudide, Md Rakib Hossain Misu, Nada Amin, and Max Tegmark. DafnyBench: A benchmark for formal software verification. arXiv preprint arXiv:2406.08467, 2024. 26
  161. Xujie Si, Aaditya Naik, Hanjun Dai, Mayur Naik, and Le Song. Code2Inv: A deep learning framework for program verification. In International Conference on Computer Aided Verification (CAV), 2020. 11 find
  162. Eric Mugnier, Emmanuel Anaya Gonzalez, Ranjit Jhala, Nadia Polikarpova, and Yuanyuan Zhou. Laurel: Generating Dafny assertions using large language models. arXiv preprint arXiv:2405.16792, 2024. 11 — [arXiv:2405.16792](https://arxiv.org/abs/2405.16792) find
  163. Matthias Cosler, Christopher Hahn, Daniel Mendoza, Frederik Schmitt, and Caroline Trippel. nl2spec: interactively translating unstructured natural language to temporal logics with large language models. In International Conference on Computer Aided Verification (CAV), 2023. 11 find
  164. Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Ponde De Oliveira Pinto, Jared Kaplan, Harri Edwards, Yuri Burda, Nicholas Joseph, Greg Brockman, et al. Evaluating large language models trained on code. arXiv preprint arXiv:2107.03374, 2021. 11, 25
  165. Hammond Pearce, Baleegh Ahmad, Benjamin Tan, Brendan Dolan-Gavitt, and Ramesh Karri. Asleep at the keyboard? assessing the security of Github Copilot’s code contributions. In Symposium on Security and Privacy, 2022. 11 find
  166. Rangeet Pan, Ali Reza Ibrahimzada, Rahul Krishna, Divya Sankar, Lambert Pouguem Wassi, Michele Merler, Boris Sobolev, Raju Pavuluri, Saurabh Sinha, and Reyhaneh Jabbarvand. Lost in translation: A study of bugs introduced by large language models while translating code. In International Conference on…
  167. Neil Perry, Megha Srivastava, Deepak Kumar, and Dan Boneh. Do users write more insecure code with AI assistants? In Conference on Computer and Communications Security (CCS), 2023. 11 find
  168. Md Rakib Hossain Misu, Cristina V Lopes, Iris Ma, and James Noble. Towards AI-assisted synthesis of verified Dafny methods. In ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE), 2024. 12, 19
  169. Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, and Chris Hawblitzel. Verus: Verifying rust programs using linear ghost types. Proceedings of the ACM on Programming Languages, 2023. 12 find
  170. Sahil Bhatia, Jie Qiu, Niranjan Hasabnis, Sanjit A Seshia, and Alvin Cheung. Verified code transpilation with LLMs. arXiv preprint arXiv:2406.03003, 2024. 12 find
  171. Jan Jakubuv, Karel Chvalovskỳ, Zarathustra Goertzel, Cezary Kaliszyk, Mirek Olšák, Bartosz Piotrowski, Stephan Schulz, Martin Suda, and Josef Urban. MizAR 60 for Mizar 50. In International Conference on Interactive Theorem Proving (ITP), 2023. 12 find
  172. Gabriel Poesia, David Broman, Nick Haber, and Noah D Goodman. Learning formal mathematics from intrinsic motivation. In Neural Information Processing Systems (NeurIPS), 2024. 13, 25
  173. Luyu Gao, Aman Madaan, Shuyan Zhou, Uri Alon, Pengfei Liu, Yiming Yang, Jamie Callan, and Graham Neubig. PAL: Program-aided language models. In International Conference on Machine Learning (ICML), 2023. 13 find
  174. Daya Guo, Qihao Zhu, Dejian Yang, Zhenda Xie, Kai Dong, Wentao Zhang, Guanting Chen, Xiao Bi, Y. Wu, Y. K. Li, Fuli Luo, Yingfei Xiong, and Wenfeng Liang. DeepSeek-Coder: When the large language model meets programming–the rise of code intelligence. arXiv preprint arXiv:2401.14196, 2024. 13 find
  175. Abhimanyu Dubey, Abhinav Jauhri, Abhinav Pandey, Abhishek Kadian, Ahmad Al-Dahle, Aiesha Letman, Akhil Mathur, Alan Schelten, Amy Yang, Angela Fan, et al. The Llama 3 herd of models. arXiv preprint arXiv:2407.21783, 2024. 13
  176. Ben Athiwaratkun, Sanjay Krishna Gouda, Zijian Wang, Xiaopeng Li, Yuchen Tian, Ming Tan, Wasi Uddin Ahmad, Shiqi Wang, Qing Sun, Mingyue Shang, et al. Multi-lingual evaluation of code generation models. In International Conference on Learning Representations (ICLR), 2023. 13
  177. Federico Cassano, John Gouwar, Francesca Lucchetti, Claire Schlesinger, Carolyn Jane Anderson, Michael Greenberg, Abhinav Jangda, and Arjun Guha. Knowledge transfer from high-resource to low-resource programming languages for code LLMs. arXiv preprint arXiv:2308.09895, 2023. 13 — [arXiv:2308.09895](https://arxiv.org/abs/2308.09895) find
  178. Xiaohan Lin, Qingxing Cao, Yinya Huang, Haiming Wang, Jianqiao Lu, Zhengying Liu, Linqi Song, and Xiaodan Liang. FVEL: Interactive formal verification environment with large language models via theorem proving. In Neural Information Processing Systems (NeurIPS), 2024. 13 find
  179. Kishore Papineni, Salim Roukos, Todd Ward, and Wei-Jing Zhu. BLEU: a method for automatic evaluation of machine translation. In Annual Meeting of the Association for Computational Linguistics (ACL), 2002. 13
  180. Huaiyuan Ying, Zijian Wu, Yihan Geng, Jiayu Wang, Dahua Lin, and Kai Chen. Lean Workbook: A large-scale lean problem set formalized from natural language math problems. arXiv preprint arXiv:2406.03847, 2024. 13
  181. Zenan Li, Yifan Wu, Zhaoyu Li, Xinming Wei, Xian Zhang, Fan Yang, and Xiaoxing Ma. Autoformalize mathematical statements by symbolic equivalence and semantic consistency. In Neural Information Processing Systems (NeurIPS), 2024. 13, 24
  182. Christian Szegedy. A promising path towards autoformalization and general artificial intelligence. In International Conference on Intelligent Computer Mathematics (CICM), 2020. 14 find
  183. Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N. Gomez, Lukasz Kaiser, and Illia Polosukhin. Attention is all you need. In Neural Information Processing Systems (NeurIPS), 2017. 14
  184. Zeyuan Allen-Zhu and Yuanzhi Li. Physics of language models: Part 3.1, knowledge storage and extraction. In International Conference on Machine Learning (ICML), 2024. 14
  185. Fabio Petroni, Tim Rocktäschel, Sebastian Riedel, Patrick Lewis, Anton Bakhtin, Yuxiang Wu, and Alexander Miller. Language models as knowledge bases? In Conference on Empirical Methods in Natural Language Processing (EMNLP), 2019. 14
  186. Mirac Suzgun, Nathan Scales, Nathanael Schärli, Sebastian Gehrmann, Yi Tay, Hyung Won Chung, Aakanksha Chowdhery, Quoc Le, Ed Chi, Denny Zhou, et al. Challenging BIG-Bench tasks and whether chain-of-thought can solve them. In Findings of the Association for Computational Linguistics: ACL, 2023. 14
  187. Iman Mirzadeh, Keivan Alizadeh, Hooman Shahrokhi, Oncel Tuzel, Samy Bengio, and Mehrdad Farajtabar. GSM-Symbolic: Understanding the limitations of mathematical reasoning in large language models. arXiv preprint arXiv:2410.05229, 2024. 14, 22
  188. Boshi Wang, Xiang Yue, Yu Su, and Huan Sun. Grokked Transformers are implicit reasoners: A mechanistic journey to the edge of generalization. In Neural Information Processing Systems (NeurIPS), 2024. 14
  189. Honghua Zhang, Liunian Harold Li, Tao Meng, Kai-Wei Chang, and Guy Van Den Broeck. On the paradox of learning to reason from data. In International Joint Conference on Artificial Intelligence (IJCAI), 2023. 14 find
  190. Karthik Valmeekam, Matthew Marquez, Sarath Sreedharan, and Subbarao Kambhampati. On the planning abilities of large language models: a critical investigation. In Neural Information Processing Systems (NeurIPS), 2023. 14 — On the Planning Abilities of Large Language Models : A Critical Investigation
  191. Karthik Valmeekam, Matthew Marquez, Alberto Olmo, Sarath Sreedharan, and Subbarao Kambhampati. PlanBench: An extensible benchmark for evaluating large language models on planning and reasoning about change. In Neural Information Processing Systems (NeurIPS), 2024.
  192. Jian Xie, Kai Zhang, Jiangjie Chen, Tinghui Zhu, Renze Lou, Yuandong Tian, Yanghua Xiao, and Yu Su. TravelPlanner: A benchmark for real-world planning with language agents. In International Conference on Machine Learning (ICML), 2024. 14, 23, 26
  193. Bo Peng, Eric Alcaide, Quentin Gregory Anthony, Alon Albalak, Samuel Arcadinho, Stella Biderman, Huanqi Cao, Xin Cheng, Michael Nguyen Chung, Leon Derczynski, et al. RWKV: Reinventing RNNs for the Transformer era. In Findings of the Association for Computational Linguistics: EMNLP, 2023. 14 find
  194. Albert Gu and Tri Dao. Mamba: Linear-time sequence modeling with selective state spaces. In Conference on Language Modeling (COLM), 2023. find
  195. Jiacheng Ye, Shansan Gong, Liheng Chen, Lin Zheng, Jiahui Gao, Han Shi, Chuan Wu, Xin Jiang, Zhenguo Li, Wei Bi, and Lingpeng Kong. Diffusion of thoughts: Chain-of-thought reasoning in diffusion language models. arXiv preprint arXiv:2402.07754, 2024. — [arXiv:2402.07754](https://arxiv.org/abs/2402.07754) find
  196. Yilun Du, Jiayuan Mao, and Joshua B. Tenenbaum. Learning iterative reasoning through energy diffusion, 2024.
  197. Matthew Ho, Vincent Zhu, Xiaoyin Chen, Moksh Jain, Nikolay Malkin, and Edwin Zhang. ProofFlow: Preliminary study on generative flow network language model tuning for formal reasoning. arXiv preprint arXiv:2410.13224, 2024. 14 — [arXiv:2410.13224](https://arxiv.org/abs/2410.13224) find
  198. Yuhuai Wu, Albert Jiang, Jimmy Ba, and Roger Baker Grosse. INT: An inequality benchmark for evaluating generalization in theorem proving. In International Conference on Learning Representations (ICLR), 2021. 14, 18
  199. Cem Anil, Yuhuai Wu, Anders Andreassen, Aitor Lewkowycz, Vedant Misra, Vinay Ramasesh, Ambrose Slone, Guy Gur-Ari, Ethan Dyer, and Behnam Neyshabur. Exploring length generalization in large language models. In Neural Information Processing Systems (NeurIPS), 2022. 14
  200. Richard Sutton. The bitter lesson. Incomplete Ideas (blog), 2019. 15, 18 find
  201. Kshitij Bansal, Sarah Loos, Markus Rabe, Christian Szegedy, and Stewart Wilcox. HOList: An environment for machine learning of higher order logic theorem proving. In International Conference on Machine Learning (ICML), 2019. 15 — HOList: An Environment for Machine Learning of Higher-Order Theorem Proving
  202. Allen Newel and Herbert A Simon. Computer science as empirical inquiry: symbols and search. Communications of the ACM, 1976. 15 find
  203. Dan Zhang, Sining Zhoubian, Yisong Yue, Yuxiao Dong, and Jie Tang. ReST-MCTS*: LLM self-training via process reward guided tree search. In Neural Information Processing Systems (NeurIPS), 2024. 15, 22
  204. Yuxi Xie, Anirudh Goyal, Wenyue Zheng, Min-Yen Kan, Timothy P Lillicrap, Kenji Kawaguchi, and Michael Shieh. Monte Carlo tree search boosts reasoning via iterative preference learning. arXiv preprint arXiv:2405.00451, 2024. 15 find
  205. Charlie Snell, Jaehoon Lee, Kelvin Xu, and Aviral Kumar. Scaling LLM test-time compute optimally can be more effective than scaling model parameters. arXiv preprint arXiv:2408.03314, 2024. 15
  206. Yangzhen Wu, Zhiqing Sun, Shanda Li, Sean Welleck, and Yiming Yang. An empirical analysis of compute-optimal inference for problem-solving with language models. arXiv preprint arXiv:2408.00724, 2024. 15
  207. Lasse Blaauwbroek, Mirek Olšák, Jason Rute, Fidel Ivan Schaposnik Massolo, Jelle Piepenbrock, and Vasily Pestun. Graph2Tac: Online representation learning of formal math concepts. In International Conference on Machine Learning (ICML), 2024. 15
  208. Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. MiniF2F: a cross-system benchmark for formal olympiad-level mathematics. In International Conference on Learning Representations (ICLR), 2022. 15, 19, 20
  209. George Tsoukalas, Jasper Lee, John Jennings, Jimmy Xin, Michelle Ding, Michael Jennings, Amitayush Thakur, and Swarat Chaudhuri. PutnamBench: Evaluating neural theorem-provers on the Putnam mathematical competition. In Neural Information Processing Systems (NeurIPS), Datasets and Benchmarks Track, 2…
  210. Zijian Wu, Suozhi Huang, Zhejian Zhou, Huaiyuan Ying, Jiayu Wang, Dahua Lin, and Kai Chen. InternLM2.5-StepProver: Advancing automated theorem proving via expert iteration on large-scale Lean problems. arXiv preprint arXiv:2410.15700, 2024. 15
  211. Shunyu Yao, Dian Yu, Jeffrey Zhao, Izhak Shafran, Tom Griffiths, Yuan Cao, and Karthik Narasimhan. Tree of thoughts: Deliberate problem solving with large language models. In Neural Information Processing Systems (NeurIPS), 2023. 15 find
  212. Timothy Gowers. How can it be feasible to find proofs? https://drive.google.com/file/d/1-FFa6nMVg18m1zPtoAQrFalwpx2YaGK4/view, 2022. 16 ↗
  213. Haiming Wang, Huajian Xin, Zhengying Liu, Wenda Li, Yinya Huang, Jianqiao Lu, Zhicheng Yang, Jing Tang, Jian Yin, Zhenguo Li, and Xiaodan Liang. Proving theorems recursively. In Neural Information Processing Systems (NeurIPS), 2024. 16, 20
  214. Weikun Yang, Grigory Fedyukovich, and Aarti Gupta. Lemma synthesis for automating induction over algebraic data types. In International Conference on Principles and Practice of Constraint Programming (CP), 2019. 16 find
  215. Aishwarya Sivaraman, Alex Sanchez-Stern, Bretton Chen, Sorin Lerner, and Todd Millstein. Data-driven lemma synthesis for interactive proofs. Proceedings of the ACM on Programming Languages, 2022. 16 find
  216. Cezary Kaliszyk and Josef Urban. Lemma mining over HOL Light. In International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR), 2013. 16 find
  217. Jin Peng Zhou, Yuhuai Wu, Qiyang Li, and Roger Baker Grosse. REFACTOR: Learning to extract theorems from proofs. In International Conference on Learning Representations (ICLR), 2024. 16 find
  218. Zhening Li, Gabriel Poesia, Omar Costilla-Reyes, Noah Goodman, and Armando Solar-Lezama. Lemma: Bootstrapping high-level mathematical reasoning with learned symbolic abstractions. arXiv preprint arXiv:2211.08671, 2022. 16 — [arXiv:2211.08671](https://arxiv.org/abs/2211.08671) find
  219. Stephen Robertson, Hugo Zaragoza, et al. The probabilistic relevance framework: BM25 and beyond. Foundations and Trends® in Information Retrieval, 2009. 17 find
  220. Vladimir Karpukhin, Barlas Oguz, Sewon Min, Patrick Lewis, Ledell Wu, Sergey Edunov, Danqi Chen, and Wen-tau Yih. Dense passage retrieval for open-domain question answering. In Conference on Empirical Methods in Natural Language Processing (EMNLP), 2020. 17
  221. Andrew Wiles. Modular elliptic curves and Fermat’s Last Theorem. Annals of mathematics, 1995. 17 find
  222. Chenrui Wei, Mengzhou Sun, and Wei Wang. Proving olympiad algebraic inequalities without human demonstrations. In Neural Information Processing Systems (NeurIPS), 2024. 17, 20
  223. Anonymous. Proving olympiad inequalities by synergizing LLMs and symbolic reasoning. In International Conference on Learning Representations (ICLR), 2025. URL https://openreview.net/forum?id=FiyS0ecSm0. under review. 17 ↗
  224. Christoph Drösser. AI will become mathematicians’ ’co-pilot’. Scientific American, June 2024. URL https://www.scientificamerican.com/article/ai-will-become-mathematicians-co-pilot/. 18 ↗
  225. Renaissance Philanthropy. AI for Math Fund. initiatives/ai-for-math-fund/, 2024. 18 find
  226. Will Crichton, Maneesh Agrawala, and Pat Hanrahan. The role of working memory in program tracing. In Conference on Human Factors in Computing Systems (CHI), 2021. 18 find
  227. Will Crichton, Gavin Gray, and Shriram Krishnamurthi. A grounded conceptual model for ownership types in Rust. Proceedings of the ACM on Programming Languages, 2023. 18 find
  228. Talia Ringer. Proofs and conversations. conversations.pdf. 18 find
  229. Patrick Massot. Lean blueprint. https://github.com/PatrickMassot/leanblueprint. 18, 21, 23 ↗
  230. Vincent A Voelz, Vijay S Pande, and Gregory R Bowman. Folding@home: Achievements from over 20 years of citizen science herald the exascale era. Biophysical journal, 2023. 18 find
  231. Luca Beurer-Kellner, Marc Fischer, and Martin Vechev. Guiding LLMs the right way: Fast, non-invasive constrained generation. In International Conference on Machine Learning (ICML), 2024. 19 find
  232. Shubham Ugare, Tarun Suresh, Hangoo Kang, Sasa Misailovic, and Gagandeep Singh. Improving LLM code generation with grammar augmentation. arXiv preprint arXiv:2403.01632, 2024. 19 find
  233. Kasra Ferdowsi, Ruanqianqian Huang, Michael B James, Nadia Polikarpova, and Sorin Lerner. Validating AI-generated code with live programming. In Conference on Human Factors in Computing Systems (CHI), 2024. 19 find
  234. Chuyue Sun, Ying Sheng, Oded Padon, and Clark Barrett. Clover: Closed-loop verifiable code generation. In International Symposium on AI Verification, 2024. 19
  235. Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Jianan Yao, Weidong Cui, Yeyun Gong, Chris Hawblitzel, Shuvendu Lahiri, Jacob R Lorch, Shuai Lu, et al. AutoVerus: Automated proof generation for Rust code. arXiv preprint arXiv:2409.13082, 2024.
  236. Pranjal Aggarwal, Bryan Parno, and Sean Welleck. AlphaVerus: Bootstrapping formally verified code generation through self-improving translation and treefinement. arXiv preprint arXiv:2412.06176, 2024. 19, 25, 26
  237. The Society of Automotive Engineers (SAE). Taxonomy and definitions for terms related to driving automation systems for on-road motor vehicles. https://www.sae.org/standards/content/j3016_202104/, 2024. 19 ↗
  238. Geoff Sutcliffe and Christian Suttner. The TPTP problem library. Journal of Automated Reasoning, 1998. 19, 20 find
  239. Chengwu Liu, Jianhao Shen, Huajian Xin, Zhengying Liu, Ye Yuan, Haiming Wang, Wei Ju, Chuanyang Zheng, Yichun Yin, Lin Li, Ming Zhang, and Qun Liu. FIMO: A challenge formal dataset for automated theorem proving. arXiv preprint arXiv:2309.04295, 2023. 19, 20 https://renaissancephilanthropy.org/2024.… ↗
  240. Carlos E Jimenez, John Yang, Alexander Wettig, Shunyu Yao, Kexin Pei, Ofir Press, and Karthik R Narasimhan. SWE-bench: Can language models resolve real-world GitTub issues? In International Conference on Learning Representations (ICLR), 2024. 19, 21 find
  241. Ana Bove, Peter Dybjer, and Ulf Norell. A brief overview of Agda–a functional language with dependent types. In International Conference on Theorem Proving in Higher Order Logics (TPHOLs), 2009. 20 find
  242. Freek Wiedijk. Formalizing 100 theorems. https://www.cs.ru.nl/~freek/100/. 20 ↗
  243. Morph Labs. Moogle: Semantic search over mathlib4. https://www.moogle.ai/, 2023. 20 ↗
  244. Joachim Breitner. Loogle!, 2024. URL https://loogle.lean-lang.org/. 20 ↗
  245. Guoxiong Gao, Haocheng Ju, Jiedong Jiang, Zihan Qin, and Bin Dong. A semantic search engine for Mathlib4. arXiv preprint arXiv:2403.13310, 2024. 20 Dohmke. GitHub Copilot X: The AI-powered developer
  246. Thomas experience. https://github.blog/news-insights/product-news/github-copilot-x-the-ai-powered-developer-experience, 2023. 20 ↗
  247. Sascha Böhme and Tobias Nipkow. Sledgehammer: Judgement day. In International Joint Conference on Automated Reasoning (IJCAR), 2010. 20 find
  248. Wang Ling, Dani Yogatama, Chris Dyer, and Phil Blunsom. Program induction by rationale generation: Learning to solve and explain algebraic word problems. In Annual Meeting of the Association for Computational Linguistics (ACL), 2017. 21, 22 find
  249. Ruixin Hong, Hongming Zhang, Xinyu Pang, Dong Yu, and Changshui Zhang. A closer look at the self-verification abilities of large language models in logical reasoning. In Annual Conference of the North American Chapter of the Association for Computational Linguistics (NAACL), 2024. 21, 22 find
  250. XTX Markets. AIMO Progress Prize: July 2024 results. https://aimoprize.com/updates/2024-07-20-progress-prize-results, 2024. 21 ↗
  251. Freda Shi, Xinyun Chen, Kanishka Misra, Nathan Scales, David Dohan, Ed H Chi, Nathanael Schärli, and Denny Zhou. Large language models can be easily distracted by irrelevant context. In International Conference on Machine Learning (ICML), 2023. 21
  252. Tamera Lanham, Anna Chen, Ansh Radhakrishnan, Benoit Steiner, Carson Denison, Danny Hernandez, Dustin Li, Esin Durmus, Evan Hubinger, Jackson Kernion, et al. Measuring faithfulness in chain-of-thought reasoning. arXiv preprint arXiv:2307.13702, 2023. 21
  253. Yixuan Weng, Minjun Zhu, Fei Xia, Bin Li, Shizhu He, Shengping Liu, Bin Sun, Kang Liu, and Jun Zhao. Large language models are better reasoners with self-verification. In Findings of the Association for Computational Linguistics: EMNLP, 2023. 22
  254. Liangming Pan, Michael Saxon, Wenda Xu, Deepak Nathani, Xinyi Wang, and William Yang Wang. Automatically correcting large language models: Surveying the landscape of diverse self-correction strategies. arXiv preprint arXiv:2308.03188, 2023. 22 find
  255. Alon Talmor, Jonathan Herzig, Nicholas Lourie, and Jonathan Berant. CommonsenseQA: A question answering challenge targeting commonsense knowledge. In Annual Conference of the North American Chapter of the Association for Computational Linguistics (NAACL), 2019. 22
  256. Zhilin Yang, Peng Qi, Saizheng Zhang, Yoshua Bengio, William Cohen, Ruslan Salakhutdinov, and Christopher D Manning. HotpotQA: A dataset for diverse, explainable multi-hop question answering. In Conference on Empirical Methods in Natural Language Processing (EMNLP), 2018. 22
  257. Yihong Dong, Xue Jiang, Huanyu Liu, Zhi Jin, and Ge Li. Generalization or memorization: Data contamination and trustworthy evaluation for large language models. In Findings of the Association for Computational Linguistics: ACL, 2024. 22 find
  258. Charles R Harris, K Jarrod Millman, Stéfan J Van Der Walt, Ralf Gommers, Pauli Virtanen, David Cournapeau, Eric Wieser, Julian Taylor, Sebastian Berg, Nathaniel J Smith, et al. Array programming with NumPy. Nature, 2020. 22
  259. Liangming Pan, Alon Albalak, Xinyi Wang, and William Wang. Logic-LM: Empowering large language models with symbolic solvers for faithful logical reasoning. In Findings of the Association for Computational Linguistics: EMNLP, 2023. 22
  260. Huaixiu Steven Zheng, Swaroop Mishra, Hugh Zhang, Xinyun Chen, Minmin Chen, Azade Nova, Le Hou, Heng-Tze Cheng, Quoc V. Le, Ed H. Chi, and Denny Zhou. NATURAL PLAN: Benchmarking LLMs on natural language planning. arXiv preprint arXiv:2406.04520, 2024. 23 find
  261. Guoxiong Gao, Yutong Wang, Jiedong Jiang, Qi Gao, Zihan Qin, Tianyi Xu, and Bin Dong. Herald: A natural language annotated Lean 4 dataset. arXiv preprint arXiv:2410.10878, 2024. 23, 24
  262. Peter Aczel, Benedikt Ahrens, Thorsten Altenkirch, Steve Awodey, Bruno Barras, Andrej Bauer, Yves Bertot, Marc Bezem, Thierry Coquand, Eric Finster, et al. Homotopy Type Theory: Univalent Foundations of Mathematics. 2013. 23 find
  263. Anthony Bordg, Yiannos Stathopoulos, and Lawrence Paulson. A parallel corpus for natural language machine translation to Isabelle. In Work-in-progress papers presented at the Conference on Intelligent Computer Mathematics (CICM) Informal Proceedings, 2022. 23 find
  264. Thomas Hales. Formal abstracts. https://formalabstracts.github.io/, 2017. 23 ↗
  265. Anonymous. Rethinking and improving autoformalization: towards a faithful metric and a dependency retrieval-based approach. In International Conference on Learning Representations (ICLR), 2024. URL https://openreview.net/forum?id=hUb2At2DsQ. under review. 24 ↗
  266. ICML 2024 Challenges on Automated Math Reasoning. ai4mathworkshopicml2024/challenges, 2024. 24 find
  267. Yinya Huang, Xiaohan Lin, Zhengying Liu, Qingxing Cao, Huajian Xin, Haiming Wang, Zhenguo Li, Linqi Song, and Xiaodan Liang. Mustard: Mastering uniform synthesis of theorem and proof data. In International Conference on Learning Representations (ICLR), 2024. 24
  268. Alan Bundy, Mateja Jamnik, and Andrew Fugard. What is a proof? Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences, 2005. 24 find
  269. Jasmin Christian Blanchette and Tobias Nipkow. Nitpick: A counterexample generator for higher-order logic based on a relational model finder. In International Conference on Interactive Theorem Proving (ITP), 2010. 24 find
  270. Yoshua Bengio and Nikolay Malkin. Machine learning and information theory concepts towards an AI mathematician. Bulletin of the American Mathematical Society, 2024. 24
  271. Johannes Hölzl, Fabian Immler, and Brian Huffman. Type classes and filters for mathematical analysis in isabelle/hol. In Interactive Theorem Proving: 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings 4, pages 279–294. Springer, 2013. 24 find
  272. John Harrison. The HOL Light theory of euclidean space. Journal of Automated Reasoning, 50:173–190, 2013. 24 find
  273. Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. Coquelicot: A user-friendly library of real analysis for coq. Mathematics in Computer Science, 9:41–62, 2015. 24 find
  274. Thomas C Hales. Formal proof. Notices of the AMS, 2008. 25 find
  275. Josef Urban and Jan Jakubuv. First neural conjecturing datasets and experiments. In International Conference on Intelligent Computer Mathematics (CICM), 2020. 25
  276. Jacob Austin, Augustus Odena, Maxwell Nye, Maarten Bosma, Henryk Michalewski, David Dohan, Ellen Jiang, Carrie Cai, Michael Terry, Quoc Le, et al. Program synthesis with large language models. arXiv preprint arXiv:2108.07732, 2021. 25
  277. Mingjie Liu, Nathaniel Pinckney, Brucek Khailany, and Haoxing Ren. Verilogeval: Evaluating large language models for Verilog code generation. In International Conference on Computer Aided Design (ICCAD), 2023. 25 find
  278. Evan Lohn and Sean Welleck. miniCodeProps: a minimal benchmark for proving code properties. arXiv preprint arXiv:2406.11915, 2024. 25, 26 — [arXiv:2406.11915](https://arxiv.org/abs/2406.11915) find
  279. Lichen Zhang, Shuai Lu, and Nan Duan. Selene: Pioneering automated proof in software verification. In Annual Meeting of the Association for Computational Linguistics (ACL), 2024. 25, 26 find
  280. Cristiano Calcagno and Dino Distefano. Infer: An automatic program verifier for memory safety of C programs. In NASA Formal Methods Symposium, 2011. 26 https://sites.google.com/view/ ↗
  281. Berkeley Churchill, Oded Padon, Rahul Sharma, and Alex Aiken. Semantic program alignment for equivalence checking. In Programming Language Design and Implementation (PLDI), 2019. 26 find
  282. Aidan ZH Yang, Yoshiki Takashima, Brandon Paulsen, Josiah Dodds, and Daniel Kroening. VERT: Verified equivalent Rust transpilation with few-shot learning. arXiv preprint arXiv:2404.18852, 2024. 26 — [arXiv:2404.18852](https://arxiv.org/abs/2404.18852) find
  283. Sandeep Dasgupta, Sushant Dinesh, Deepan Venkatesh, Vikram S Adve, and Christopher W Fletcher. Scalable validation of binary lifters. In Programming Language Design and Implementation (PLDI), 2020. 26 find
  284. Fengji Zhang, Bei Chen, Yue Zhang, Jacky Keung, Jin Liu, Daoguang Zan, Yi Mao, Jian-Guang Lou, and Weizhu Chen. RepoCoder: Repository-level code completion through iterative retrieval and generation. In Conference on Empirical Methods in Natural Language Processing (EMNLP), 2023. 26
  285. Talia Ringer. Proof Repair. University of Washington, 2021. 26 find
  286. Tom Reichel, R Henderson, Andrew Touchet, Andrew Gardner, and Talia Ringer. Proof repair infrastructure for supervised models: Building a large proof repair dataset. In International Conference on Interactive Theorem Proving (ITP), 2023. 26 find
  287. Jiewen Hu, Thomas Zhu, and Sean Welleck. miniCTX: Neural theorem proving with (long-) contexts. arXiv preprint arXiv:2408.03350, 2024. 26
  288. Kevin Buzzard et al. Fermat’s Last Theorem. https://github.com/ImperialCollegeLondon/FLT, 2024. 27 ↗
  289. Simon Frieder, Luca Pinchetti, Ryan-Rhys Griffiths, Tommaso Salvatori, Thomas Lukasiewicz, Philipp Petersen, and Julius Berner. Mathematical capabilities of ChatGPT. In Neural Information Processing Systems (NeurIPS), Datasets and Benchmarks Track, 2024. 27
  290. Katherine M Collins, Albert Q Jiang, Simon Frieder, Lionel Wong, Miri Zilka, Umang Bhatt, Thomas Lukasiewicz, Yuhuai Wu, Joshua B Tenenbaum, William Hart, et al. Evaluating language models for mathematics through interactions. Proceedings of the National Academy of Sciences (PNAS), 2024. 27

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/yang-2024-formal-mathematical-reasoning-new-frontier/