mlsanityData to 7 Oct 2026

From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs

arXiv 2501.16207 ↗First posted 27 Jan 2025cs.AI cs.CL cs.PLcited by 17

On the map: LLM reasoning → Mathematical reasoning

Abstract (arXiv)

The research in AI-based formal mathematical reasoning has shown an unstoppable growth trend. These studies have excelled in mathematical competitions like IMO and have made significant progress. This paper focuses on formal verification, an immediate application scenario of formal reasoning, and breaks it down into sub-tasks. We constructed 18k high-quality instruction-response pairs across five formal specification languages (Coq, Lean4, Dafny, ACSL, and TLA+) by distilling gpt-4o and evaluated against ten open-sourced LLMs, including recent popular DeepSeek-R1. We also fine-tuned several 7~8B small models to achieve comparable performance with Deepseek-R1-671B. Interestingly, we observed that fine-tuning with formal data also enhances mathematics, reasoning, and coding capabilities. Fine-tuned models are released at https: //huggingface.co/fm-universe.

Key facts. Cited by 17 papers in the map (data through 7 Oct 2026). Placed in Mathematical reasoning, one of 17 directions in LLM reasoning. Builds on 38 of its 87 references that are in the map. First posted on arXiv 27 Jan 2025.

Builds on

38 of 87 references.

Closest ancestors · 1

Same direction, newest first

  1. 2024Formal Mathematical Reasoning: A New Frontier in AI20 Dec

Other references · 37

  1. 2021Training Verifiers to Solve Math Word Problemscited by 9,743
  2. 2021Evaluating Large Language Models Trained on Codecited by 8,053
  3. 2023Efficient Memory Management for Large Language Model Serving with PagedAttentioncited by 5,767
  4. 2021Measuring Mathematical Problem Solving With the MATH Datasetcited by 5,203
  5. 2021Finetuned Language Models Are Zero-Shot Learnerscited by 3,747
  6. 2021Program Synthesis with Large Language Modelscited by 3,509
  7. 2023SWE-bench: Can Language Models Resolve Real-World GitHub Issues?cited by 3,193
  8. 2019The Curious Case of Neural Text Degenerationcited by 2,881
  9. 2022Self-Instruct: Aligning Language Models with Self-Generated Instructionscited by 2,674
  10. 2022Challenging BIG-Bench Tasks and Whether Chain-of-Thought Can Solve Themcited by 1,767
  11. 2021Multitask Prompted Training Enables Zero-Shot Task Generalizationcited by 1,462
  12. 2024DeepSeek-Coder: When the Large Language Model Meets Programming -- The Rise of Code Intelligencecited by 1,154
25 more
  1. 2024Qwen2.5-Coder Technical Reportcited by 1,151
  2. 2023Enhancing Chat Language Models by Scaling High-quality Instructional Conversationscited by 825
  3. 2022InCoder: A Generative Model for Code Infilling and Synthesiscited by 492
  4. 2024StarCoder 2 and The Stack v2: The Next Generationcited by 484
  5. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
  6. 2023How Far Can Camels Go? Exploring the State of Instruction Tuning on Open Resourcescited by 405
  7. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 380
  8. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 278
  9. 2023ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematicscited by 180
  10. 2022GitHub Copilot AI pair programmer: Asset or Liability?cited by 150
  11. 2023Diverse Data Augmentation with Diffusions for Effective Test-time Prompt Tuningcited by 150
  12. 2019The Lean mathematical librarycited by 127
  13. 2019Learning to Prove Theorems via Interacting with Proof Assistantscited by 107
  14. 2021NaturalProofs: Mathematical Theorem Proving in Natural Languagecited by 80
  15. 2022NaturalProver: Grounded Mathematical Proof Generation with Language Modelscited by 72
  16. 2023Clover: Closed-Loop Verifiable Code Generationcited by 62
  17. 2024Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verificationcited by 55
  18. 2024A Survey on Deep Learning for Theorem Provingcited by 55
  19. 2019Pythia: AI-assisted Code Completion Systemcited by 54
  20. 2024Calibration and Correctness of Language Models for Codecited by 49
  21. 2023A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verificationcited by 42
  22. 2020Natural Language Premise Selection: Finding Supporting Statements for Mathematical Textcited by 13
  23. 2023BERT is not The Count: Learning to Match Mathematical Statements with Proofscited by 9
  24. 2024An Evaluation of Requirements Modeling for Cyber-Physical Systems via LLMscited by 6
  25. 2020iMER: Iterative Process of Entity Relationship and Business Proces Models Extraction from the Requirementscited by 1

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2025: 9; 2026: 8.

17 papers.

Sort:

By area:

  1. 2025When LLMs Meet API Documentation: Can Retrieval Augmentation Aid Code Generation Just as It Helps Developers?cited by 12
  2. 2025OSVBench: Benchmarking LLMs on Specification Generation Tasks for Operating System Verificationcited by 8
  3. 2025Requirements Development and Formalization for Reliable Code Generation: A Multi-Agent Visioncited by 3
  4. 2025SysMoBench: Evaluating AI on Formally Modeling Complex Real-World Systemscited by 2
  5. 2025Improving Autoformalization Using Direct Dependency Retrievalcited by 2
  6. 2025MINIF2F-DAFNY: LLM-Guided Mathematical Theorem Proving via Auto-Active Verificationcited by 2
  7. 2026Spec-Harness: Measuring and Improving Behavioral Adequacy of LLM-Synthesized Formal Specificationscited by 2
  8. 2025Towards Automated Formal Verification of Backend Systems with LLMscited by 1
  9. 2026ModelWisdom: An Integrated Toolkit for TLA+ Model Visualization, Digest and Repaircited by 1
  10. 2026Intent-aligned Formal Specification Synthesis via Traceable Refinementcited by 1
  11. 2025LLMs as verification oracles for Soliditycited by 0
  12. 2025AutoICE: Automatically Synthesizing Verifiable C Code via LLM-driven Evolutioncited by 0
5 more
  1. 2026LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generationcited by 0
  2. 2026Neurosymbolic Auditing of Natural-Language Software Requirementscited by 0
  3. 2026Specula: Scaling formal specifications for autonomous model checking of system codecited by 0
  4. 2026VeriSkill: A Self-Evolution Framework for Program Verification Skillscited by 0
  5. 2026Learning to Prove, Not Just to Answer: Reinforcement Learning from Formal Verification for Natural-Language Logical Reasoningcited by 0

Similar, not cited

Close in wording, no citation either way

  1. 2025FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models
  2. 2025Thinking Machines: Mathematical Reasoning in the Age of LLMs
  3. 2025HERMES: Towards Efficient and Verifiable Mathematical Reasoning in LLMs
  4. 2025ProofCompass: Enhancing Specialized Provers with LLM Guidance
  5. 2025Evaluating Mathematical Reasoning Across Large Language Models: A Fine-Grained Approach
  6. 2025Steering LLMs for Formal Theorem Proving
  7. 2025Towards Advanced Mathematical Reasoning for LLMs via First-Order Logic Theorem Proving
  8. 2025MSC-180: A Benchmark for Automated Formal Theorem Proving from Mathematical Subject Classification