CoChat
Sign Up
Cited by 1Logic, programming, and type systemsMathematics, Computing, and Information ProcessingLogic, Reasoning, and Knowledge

Towards a Common Framework for Autoformalization

Open access
Mensfelt, Agnieszka, Tena Cucala, David, Franco, Santiago, Koutsoukou-Argyraki, Angeliki, Trencsenyi, Vince, Stathis, Kostas·2026·Proceedings of the AAAI Conference on Artificial Intelligence
DOI 10.1609/aaai.v40i48.42132
Open this paper in CoChat — free accountOpen PDF

Abstract

Autoformalization has emerged as a term referring to the automation of formalization in the context of the formalization of mathematics using interactive theorem provers (proof assistants). Its rapid development has been driven by progress in deep learning, especially large language models (LLMs). More recently, usage of the term has expanded beyond mathematics to describe tasks that involve translating natural language input into verifiable logical representations. At the same time, a growing body of research explores using LLMs to translate informal language into formal representations for reasoning, planning, and knowledge representation, but without explicitly referring to this process as autoformalization. As a result, despite addressing similar tasks, the largely independent development of these research areas has limited opportunities for shared methodologies, benchmarks, and theoretical frameworks that could accelerate progress. Our goal is to review - explicit or implicit - instances of what can be considered autoformalization and to propose a unified framework, encouraging cross-pollination between different fields to advance the development of next generation AI systems.

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Integrity signals

Registry

Crossref · 10.1609/aaai.v40i48.42132

Cites

Statistics

Claims the paper makes

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Claims other papers make about this one

Each is checked against this paper’s own text: does it say what the citing paper says it does?

  • A recent unifying account [12] parameterises autoformalization by an informal language Li and a formalizable subset thereof, a formal reasoning language Lf with precise semantics, and a semantic equivalence criterion E specifying which aspects of meaning must be preserved.

    “A recent unifying account [12] parameterises autoformalization by an informal language 𝐿 𝑖 and a formalizable subset thereof, a formal reasoning language 𝐿 𝑓 with precise semantics, and a semantic equivalence criterion 𝐸 specifying which aspects of meaning must be preserved.”

    From PrologMCP: A Standardized Prolog Tool Interface for LLM Agents (2026) · cites this paper as [12]

Self-check

Percentages, sums and reported differences re-computed from the paper’s own numbers.

The self-check needs the paper’s full text.

Cites

No references could be resolved yet.

Research works printed but not linked: 72

  1. Abolhasani, M. S.; and Pan, R. 2024. Leveraging LLM for Automated Ontology Extraction and Knowledge Graph Generation. CoRR, abs/2412.00608. · arXiv
  2. Agrawal, A.; Gadgil, S.; Goyal, N.; Narayanan, A.; and Tadipatri, A. 2022. Towards a Mathematics Formalisation Assistant using Large Language Models. ArXiv:2211.07524. · arXiv
  3. Borazjanizadeh, N.; and Piantadosi, S. T. 2024. Reli- able Reasoning Beyond Natural Language. arXiv preprint arXiv:2407.11373. · arXiv
  4. Borroto Santana, M.; Kareem, I.; and Ricca, F. 2024. To- wards Automatic Composition of ASP Programs from Nat- ural Language Specifications. Proceedings of the Thirty- Third International Joint Conference on Artificial Intelli- gence (IJCAI-24).
  5. Brunello, A.; Ferrarese, R.; Geatti, L.; Marzano, E.; Monta- nari, A.; and Saccomanno, N. 2025. Evaluating LLMs Capa- bilities at Natural Language to Logic Translation: A Prelim- inary Investigation. In Proceedings of the Logic and Engi- neering of Natural Language Semantics (LENLS) Workshop 2025.
  6. Chaturvedi, A.; and Asher, N. 2024. Learning Seman- tic Structure through First-Order-Logic Translation. arXiv preprint arXiv:2410.03203. · arXiv
  7. Chen, Y.; Gandhi, R.; Zhang, Y.; and Fan, C. 2023. NL2TL: Transforming Natural Languages to Temporal Logics using Large Language Models. In Proceedings of the 2023 Con- ference on Empirical Methods in Natural Language Pro- cessing, 15880-15903.
  8. Clarke, E. M.; Emerson, E. A.; and Sistla, A. P. 1986. Au- tomatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Pro- gramming Languages and Systems, 8(2): 244-263.
  9. Coppolillo, E.; Calimeri, F.; Manco, G.; Perri, S.; and Ricca, F. 2024. LLASP: Fine-tuning Large Language Models for Answer Set Programming. Proceedings of the 21st Interna- tional Conference on Principles of Knowledge Representa- tion and Reasoning.
  10. Iliadis, L. S.; MacIntyre, J.; Avlonitis, M.; and Papaleonidas, A., eds., Artificial Intelli- gence Applications and Innovations -20th IFIP WG 12.5 International Conference, AIAI 2024, Corfu, Greece, June 27-30, 2024, Proceedings, Part IV, volume 714 of IFIP Advances in Information and Communication Technology, 360-374. Springer.
  11. Eells, A.; Dave, B.; Hitzler, P.; and Shimizu, C. 2024. Commonsense Ontology Micropatterns. In Besold, T. R.; d'Avila Garcez, A.; Jiménez-Ruiz, E.; Confalonieri, R.; Madhyastha, P.; and Wagner, B., eds., Neural-Symbolic Learning and Reasoning -18th International Conference, NeSy 2024, Barcelona, Spain, September 9-12, 2024, Pro- ceedings, Part II, volume 14980 of Lecture Notes in Com- puter Science, 51-59. Springer.
  12. Fox, M.; and Long, D. 2003. PDDL2. 1: An extension to PDDL for expressing temporal planning domains. Journal of artificial intelligence research, 20: 61-124.
  13. Gadgil, S.; Tadipatri, A. R.; Agrawal, A.; Narayanan, A.; and Goyal, N. 2022. Towards automating formalisation of theorem statements using large language models. In 36th Conference on Neural Information Processing Systems (NeurIPS 2022) Workshop on MATH-AI.
  14. Guan, L.; Valmeekam, K.; Sreedharan, S.; and Kambham- pati, S. 2023. Leveraging pre-trained large language models to construct and utilize world models for model-based task planning. Advances in Neural Information Processing Sys- tems, 36: 79081-79094.
  15. Helmert, M. 2006. The fast downward planning system. Journal of Artificial Intelligence Research, 26: 191-246.
  16. Hu, X.; Zhou, Q.; Grechuk, B.; and Tyukin, I. Y. 2025b. StepProof: Step-by-step verification of natural language mathematical proofs. arXiv preprint arXiv:2506.10558. · arXiv
  17. Ishay, A.; Yang, Z.; and Lee, J. 2023. Leveraging Large Language Models to Generate Answer Set Programs. Pro- ceedings of the 20th International Conference on Principles of Knowledge Representation and Reasoning.
  18. Jiang, A. Q.; Li, W.; and Jamnik, M. 2024. Multi-language diversity benefits autoformalization. Advances in Neural In- formation Processing Systems, 37: 83600-83626.
  19. Jiang, A. Q.; Welleck, S.; Zhou, J. P.; Li, W.; Liu, J.; Jamnik, M.; Lacroix, T.; Wu, Y.; and Lample, G. 2022. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. arXiv preprint arXiv:2210.12283. · arXiv
  20. Kaliszyk, C.; Urban, J.; and Vyskočil, J. 2015. Learning to parse on aligned corpora (rough diamond). In Interactive Theorem Proving: 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings 6, 227- 233. Springer.
  21. Kaliszyk, C.; Urban, J.; and Vyskočil, J. 2017. Automating formalization by statistical and semantic parsing of mathe- matics. In International Conference on Interactive Theorem Proving, 12-27. Springer.
  22. Kaliszyk, C.; Urban, J.; Vyskočil, J.; and Geuvers, H. 2014. Developing corpus-based translation methods between in- formal and formal mathematics: Project description. In In- ternational Conference on Intelligent Computer Mathemat- ics, 435-439. Springer.
  23. Kamath, A.; and Das, R. 2018. A Survey on Semantic Pars- ing. arXiv preprint arXiv:1812.00978. · arXiv
  24. Karatarakis, M. 2024. Leveraging Large Language Mod- els for Autoformalizing Theorems: A Case Study. In 9th Conference on Artificial Intelligence and Theorem Proving (AITP).
  25. Lee, J.; Katz, M.; and Sohrabi, S. 2023. On k* search for top-k planning. In Proceedings of the International Sympo- sium on Combinatorial Search, volume 16, 38-46.
  26. Li, J.; and Tian, M. T. 2025. Automatic Generation of Safety-compliant Linear Temporal Logic via Large Lan- guage Model: A Self-supervised Framework. arXiv preprint arXiv:2503.15840. · arXiv
  27. Li, N.; Liu, P.; Liu, Z.; Dai, T.; Jiang, Y.; and Xia, S.- T. 2025. Logic-of-Thought: Empowering Large Language Models with Logic Programs for Solving Puzzles in Natural Language. arXiv preprint arXiv:2505.16114. · arXiv
  28. Lin, K.; Agia, C.; Migimatsu, T.; Pavone, M.; and Bohg, J. 2023. Text2Motion: from natural language instructions to feasible plans. Autonomous Robots, 47(8): 1345-1365.
  29. Lippolis, A. S.; Saeedizade, M. J.; Keskisärkkä, R.; Zup- piroli, S.; Ceriani, M.; Gangemi, A.; Blomqvist, E.; and Nuzzolese, A. G. 2025. Ontology Generation Using Large Language Models. In Curry, E.; Acosta, M.; Poveda- Villalón, M.; van Erp, M.; Ojo, A. K.; Hose, K.; Shimizu, C.; and Lisena, P., eds., The Semantic Web -22nd European Semantic Web Conference, ESWC 2025, Portoroz, Slovenia, June 1-5, 2025, Proceedings, Part I, volume 15718 of Lec- ture Notes in Computer Science, 321-341. Springer.
  30. Liu, C.; Yuan, Y.; Yin, Y.; Xu, Y.; Xu, X.; Chen, Z.; Wang, Y.; Shang, L.; Liu, Q.; and Zhang, M. 2025a. Safe: En- hancing Mathematical Reasoning in Large Language Mod- els via Retrospective Step-aware Formal Verification. arXiv preprint arXiv:2506.04592. · arXiv
  31. Liu, J. 2025. Few-Shot Natural Language to First-Order Logic Translation via In-Context Learning. In Proceed- ings of the 2025 Conference of the Nations of the Americas Chapter of the Association for Computational Linguistics: Human Language Technologies (Volume 1: Long Papers), 10939-10960.
  32. Liu, J. X.; Shah, A.; Konidaris, G.; Tellex, S.; and Paulius, D. 2024a. Lang2LTL-2: Grounding Spatiotemporal Navigation Commands Using Large Language and Vision-Language Models. In 2024 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), 2325-2332. ISSN: 2153-0866.
  33. Liu, Q.; Zheng, X.; Lu, X.; Cao, Q.; and Yan, J. 2024b. Rethinking and Improving Autoformalization: Towards a Faithful Metric and a Dependency Retrieval-based Ap- proach. In Proceedings of The Thirteenth International Con- ference on Learning Representations.
  34. Liu, Q.; Zheng, X.; Lu, X.; Cao, Q.; and Yan, J. 2025b. Rethinking and Improving Autoformalization: Towards a Faithful Metric and a Dependency Retrieval-based Ap- proach. In The Thirteenth International Conference on Learning Representations (ICLR). Spotlight paper.
  35. Lu, J.; Wan, Y.; Huang, Y.; Xiong, J.; Liu, Z.; and Guo, Z. 2025. FormalAlign: Automated Alignment Evaluation for Autoformalization. In The Thirteenth International Confer- ence on Learning Representations (ICLR). Preprint accepted to ICLR 2025.
  36. Mateiu, P.; and Groza, A. 2023. Ontology engineering with Large Language Models. In 25th International Symposium on Symbolic and Numeric Algorithms for Scientific Comput- ing, SYNASC 2023, Nancy, France, September 11-14, 2023, 226-229. IEEE.
  37. Mavrogiannis, A.; Mavrogiannis, C.; and Aloimonos, Y. 2024. Cook2LTL: Translating Cooking Recipes to LTL For- mulae using Large Language Models. In 2024 IEEE Inter- national Conference on Robotics and Automation (ICRA), 17679-17686.
  38. Stathis, K.; and Trencsenyi, V. 2025. Gener- ative Agents for Multi-Agent Autoformalization of Interac- tion Scenarios. Accepted at European Conference on Artifi- cial Intelligence (ECAI) 2025.
  39. Newell, A.; and Simon, H. A. 1976. Computer science as empirical inquiry: Symbols and search. Communications of the ACM, 19(3): 113-126.
  40. Nipkow, T.; Wenzel, M.; and Paulson, L. C. 2002. Is- abelle/HOL: a proof assistant for higher-order logic. Springer.
  41. Oates, T.; Alford, R.; Johnson, S.; and Hall, C. 2024. Us- ing Large Language Models to Extract Planning Knowledge from Unstructured Text. In Proceedings of the ICAPS Work- shop on Knowledge Engineering for Planning and Schedul- ing (KEPS).
  42. Olausson, T.; Gu, A.; Lipkin, B.; Zhang, C.; Solar-Lezama, A.; Tenenbaum, J.; and Levy, R. 2023. LINC: A Neurosym- bolic Approach for Logical Reasoning by Combining Lan- guage Models with First-Order Logic Provers. In Proceed- ings of the 2023 Conference on Empirical Methods in Nat- ural Language Processing, 5153-5176. Singapore: Associ- ation for Computational Linguistics.
  43. Oswald, J.; Srinivas, K.; Kokel, H.; Lee, J.; Katz, M.; and Sohrabi, S. 2024. Large Language Models as Planning Do- main Generators. Proceedings of the International Confer- ence on Automated Planning and Scheduling, 34: 423-431.
  44. OWL Working Group. 2012. OWL 2 Web Ontology Lan- guage Document Overview (Second Edition). W3c recom- mendation, World Wide Web Consortium (W3C). Accessed: 2025-07-28.
  45. Pan, J.; Chou, G.; and Berenson, D. 2023. Data-Efficient Learning of Natural Language to Linear Temporal Logic Translators for Robot Task Specification. Proceedings of the 2023 IEEE International Conference on Robotics and Automation (ICRA).
  46. Pan, L.; Albalak, A.; Wang, X.; and Wang, W. Y. 2023. Logic-LM: Empowering Large Language Models with Sym- bolic Solvers for Faithful Logical Reasoning. In The 2023 Conference on Empirical Methods in Natural Language Processing.
  47. Papineni, K.; Roukos, S.; Ward, T.; and Zhu, W.-J. 2002. Bleu: a method for automatic evaluation of machine trans- lation. In Proceedings of the 40th annual meeting of the Association for Computational Linguistics, 311-318.
  48. Pnueli, A. 1977. The temporal logic of programs. 18th An- nual Symposium on Foundations of Computer Science, 46- 57.
  49. Poiroux, A.; Weiss, G.; Kunčak, V.; and Bosselut, A. 2024a. Improving Autoformalization using Type Checking. arXiv preprint arXiv:2406.07222. · arXiv
  50. Dimou, A.; Troncy, R.; Hartig, O.; Acosta, M.; Alam, M.; Paulheim, H.; and Lisena, P., eds., The Semantic Web -21st International Conference, ESWC 2024, Hersonissos, Crete, Greece, May 26-30, 2024, Pro- ceedings, Part I, volume 14664 of Lecture Notes in Com- puter Science, 143-161. Springer.
  51. Shojaee, P.; Mirzadeh, I.; Alizadeh, K.; Horton, M.; Ben- gio, S.; and Farajtabar, M. 2025. The illusion of thinking: Understanding the strengths and limitations of reasoning models via the lens of problem complexity. arXiv preprint arXiv:2506.06941. · arXiv
  52. Sikes, K.; Fine-Morris, M.; Sreedharan, S.; Smith, L. N.; and Roberts, M. 2025. Creating PDDL Models from Javascript using LLMs: Preliminary Results. In AAAI 2025 Workshop LM4Plan.
  53. Silver, T.; Dan, S.; Srinivas, K.; Tenenbaum, J. B.; Kael- bling, L.; and Katz, M. 2024. Generalized Planning in PDDL Domains with Pretrained Large Language Models. Proceedings of the AAAI Conference on Artificial Intelli- gence, 38(18): 20256-20264.
  54. Soroco, M.; Song, J.; Xia, M.; Emond, K.; Sun, W.; and Chen, W. 2025. PDE-Controller: LLMs for Auto- formalization and Reasoning of PDEs. arXiv preprint arXiv:2502.00963. · arXiv
  55. Szegedy, C. 2020. A promising path towards autoformaliza- tion and general artificial intelligence. In Intelligent Com- puter Mathematics: 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings 13, 3-20. Springer.
  56. Tang, Y.; da Costa, A. A. B.; Zhang, X.; Irvine, P.; Khast- gir, S.; and Jennings, P. A. 2023. Domain Knowledge Dis- tillation from Large Language Model: An Empirical Study in the Autonomous Driving Domain. In 26th IEEE Inter- national Conference on Intelligent Transportation Systems, ITSC 2023, Bilbao, Spain, September 24-28, 2023, 3893- 3900. IEEE.
  57. Tarrach, G.; Jiang, A. Q.; Raggi, D.; Li, W.; and Jamnik, M. 2024. More details, please: Improving autoformalization with more detailed proofs. In AI for Math Workshop@ ICML 2024.
  58. Wang, H.; Unsal, M.; Lin, X.; Baksys, M.; Liu, J.; San- tos, M. D.; Sung, F.; Vinyes, M.; Ying, Z.; Zhu, Z.; et al. 2025a. Kimina-prover preview: Towards large formal rea- soning models with reinforcement learning. arXiv preprint arXiv:2504.11354. · arXiv
  59. Wang, J.; Sundarsingh, D. S.; Deshmukh, J. V.; and Kan- taros, Y. 2025b. ConformalNL2LTL: Translating Natural Language Instructions into Temporal Logic Formulas with Conformal Correctness Guarantees. ArXiv:2504.21022. · arXiv
  60. Wang, Q.; Brown, C.; Kaliszyk, C.; and Urban, J. 2020. Ex- ploration of neural machine translation in autoformalization of mathematics in Mizar. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, 85-98.
  61. Wang, Q.; Kaliszyk, C.; and Urban, J. 2018. First experi- ments with neural translation of informal to formal mathe- matics. In Intelligent Computer Mathematics: 11th Interna- tional Conference, CICM 2018, Hagenberg, Austria, August 13-17, 2018, Proceedings 11, 255-270. Springer.
  62. Wang, R.; Li, Y.; Fung, Y. R. M.; and Zhang, T. 2025c. Let's Reason Formally: Natural-Formal Hybrid Reason- ing Enhances LLM's Math Capability. arXiv preprint arXiv:2505.23703. · arXiv
  63. Warren, D. H.; and Pereira, F. C. 1982. An Efficient Eas- ily Adaptable System for Interpreting Natural Language Queries. American Journal of Computational Linguistics, 8(3-4): 110-122.
  64. Weizenbaum, J. 1966. ELIZA -A Computer Program For the Study of Natural Language Communication Between Man and Machine. Communications of the ACM, 9(1): 36- 45.
  65. Weng, K.; Du, L.; Li, S.; Lu, W.; Sun, H.; Liu, H.; and Zhang, T. 2025. Autoformalization in the Era of Large Lan- guage Models: A Survey. arXiv preprint arXiv:2505.23486. · arXiv
  66. William, M.; Nikolaus, H.; Koenig, N.; Leyi, C.; Rothkopf, R.; Qiao, F.; and Santolucito, M. 2024. Guiding LLM Tem- poral Logic Generation with Explicit Separation of Data and Control. arXiv preprint arXiv:2406.07400. · arXiv
  67. Winograd, T. 1972. Understanding Natural Language. Cog- nitive Psychology, 3(1): 1-191.
  68. Wu, Y.; Jiang, A. Q.; Li, W.; Rabe, M.; Staats, C.; Jamnik, M.; and Szegedy, C. 2022. Autoformalization with Large Language Models. Advances in Neural Information Pro- cessing Systems, 35: 32353-32368.
  69. Xu, Y.; Feng, J.; and Miao, W. 2024. Learning from Failures: Translation of Natural Language Requirements into Linear Temporal Logic with Large Language Models. In 2024 IEEE 24th International Conference on Software Quality, Reliability and Security (QRS), 204-215. ISSN: 2693-9177.
  70. Yang, K.; Poesia, G.; He, J.; Li, W.; Lauter, K.; Chaudhuri, S.; and Song, D. 2024. Formal mathematical reasoning: A new frontier in ai. arXiv preprint arXiv:2412.16075. · arXiv
  71. Yu, Z.; Peng, R.; Ding, K.; Li, Y.; Peng, Z.; Liu, M.; Zhang, Y.; Yuan, Z.; Xin, H.; Huang, W.; Wen, Y.; Zhang, G.; and Liu, W. 2025. FormalMATH: Benchmarking For- mal Mathematical Reasoning of Large Language Models. arXiv:2505.02735. · arXiv
  72. Zhang, L.; Quan, X.; and Freitas, A. 2024. Consistent Aut- oformalization for Constructing Mathematical Libraries. In Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing (EMNLP).

Cited by

Sorted by citations

Authors
Mensfelt, A., Tena Cucala, D., Franco, S., Koutsoukou-Argyraki, A., Trencsenyi, V., & Stathis, K.
Affiliations
Royal Holloway University of London (GB)
ORCID
Venue
Proceedings of the AAAI Conference on Artificial Intelligence
Publisher
Association for the Advancement of Artificial Intelligence (AAAI)
Published
2026-03-14
Volume
40
Issue
48
Pages
40971-40980
ISSN
  • 2159-5399 (ISSN-L)
  • 2374-3468
DOI
10.1609/aaai.v40i48.42132
OpenAlex
W7138894926
Cited by
0
References
0
FWCI
0.00
Type
conference paper
Language
en
Open access
Locations
  • Proceedings of the AAAI Conference on Artificial Intelligence (publishedVersion)
  • AAAI Publications (The Association for the Advancement of Artificial Intelligence (AAAI)) (submittedVersion)
Funders
Leverhulme Trust (LIP-2022-001)
Topics
  • Physical Sciences › Computer Science › Artificial Intelligence › Logic, programming, and type systems
  • Physical Sciences › Computer Science › Computational Theory and Mathematics › Mathematics, Computing, and Information Processing
  • Physical Sciences › Computer Science › Artificial Intelligence › Logic, Reasoning, and Knowledge
Keywords
autoformalization, mathematical formalization, proof assistants, large language models, knowledge representation, reasoning, planning, benchmark, unified framework

About these checks

Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.

Statistics and arithmetic are recomputed, not judged.

Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.

What counts as a claim ›How we measure confidence ›How we check this ›

Are you an author, or do you see a problem with this page? Request a review