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

arXiv: https://arxiv.org/abs/2501.16207 · HTML: https://mlsanity.com/paper/2501.16207/

## Key facts

- Cited by 18 papers in the map (data through 14 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.

## Placed in

- LLM reasoning / [Mathematical reasoning](https://mlsanity.com/lr/mathematical-reasoning/)

## Builds on (most cited first, 30 of 38)

- [Training Verifiers to Solve Math Word Problems](https://mlsanity.com/paper/2110.14168/) (2021)
- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [Efficient Memory Management for Large Language Model Serving with PagedAttention](https://mlsanity.com/paper/2309.06180/) (2023)
- [Measuring Mathematical Problem Solving With the MATH Dataset](https://mlsanity.com/paper/2103.03874/) (2021)
- [Finetuned Language Models Are Zero-Shot Learners](https://mlsanity.com/paper/2109.01652/) (2021)
- [Program Synthesis with Large Language Models](https://mlsanity.com/paper/2108.07732/) (2021)
- [SWE-bench: Can Language Models Resolve Real-World GitHub Issues?](https://mlsanity.com/paper/2310.06770/) (2023)
- [The Curious Case of Neural Text Degeneration](https://mlsanity.com/paper/1904.09751/) (2019)
- [Self-Instruct: Aligning Language Models with Self-Generated Instructions](https://mlsanity.com/paper/2212.10560/) (2022)
- [Challenging BIG-Bench Tasks and Whether Chain-of-Thought Can Solve Them](https://mlsanity.com/paper/2210.09261/) (2022)
- [Multitask Prompted Training Enables Zero-Shot Task Generalization](https://mlsanity.com/paper/2110.08207/) (2021)
- [Qwen2.5-Coder Technical Report](https://mlsanity.com/paper/2409.12186/) (2024)
- [DeepSeek-Coder: When the Large Language Model Meets Programming -- The Rise of Code Intelligence](https://mlsanity.com/paper/2401.14196/) (2024)
- [Enhancing Chat Language Models by Scaling High-quality Instructional Conversations](https://mlsanity.com/paper/2305.14233/) (2023)
- [StarCoder 2 and The Stack v2: The Next Generation](https://mlsanity.com/paper/2402.19173/) (2024)
- [InCoder: A Generative Model for Code Infilling and Synthesis](https://mlsanity.com/paper/2204.05999/) (2022)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [How Far Can Camels Go? Exploring the State of Instruction Tuning on Open Resources](https://mlsanity.com/paper/2306.04751/) (2023)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics](https://mlsanity.com/paper/2302.12433/) (2023)
- [Diverse Data Augmentation with Diffusions for Effective Test-time Prompt Tuning](https://mlsanity.com/paper/2308.06038/) (2023)
- [GitHub Copilot AI pair programmer: Asset or Liability?](https://mlsanity.com/paper/2206.15331/) (2022)
- [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019)
- [Learning to Prove Theorems via Interacting with Proof Assistants](https://mlsanity.com/paper/1905.09381/) (2019)
- [NaturalProofs: Mathematical Theorem Proving in Natural Language](https://mlsanity.com/paper/2104.01112/) (2021)
- [Formal Mathematical Reasoning: A New Frontier in AI](https://mlsanity.com/paper/2412.16075/) (2024)
- [NaturalProver: Grounded Mathematical Proof Generation with Language Models](https://mlsanity.com/paper/2205.12910/) (2022)
- [Clover: Closed-Loop Verifiable Code Generation](https://mlsanity.com/paper/2310.17807/) (2023)
- [Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification](https://mlsanity.com/paper/2404.00762/) (2024)

## Built on by (most cited first, 18 of 18)

- [When LLMs Meet API Documentation: Can Retrieval Augmentation Aid Code Generation Just as It Helps Developers?](https://mlsanity.com/paper/2503.15231/) (2025)
- [OSVBench: Benchmarking LLMs on Specification Generation Tasks for Operating System Verification](https://mlsanity.com/paper/2504.20964/) (2025)
- [Requirements Development and Formalization for Reliable Code Generation: A Multi-Agent Vision](https://mlsanity.com/paper/2508.18675/) (2025)
- [SysMoBench: Evaluating AI on Formally Modeling Complex Real-World Systems](https://mlsanity.com/paper/2509.23130/) (2025)
- [Improving Autoformalization Using Direct Dependency Retrieval](https://mlsanity.com/paper/2511.11990/) (2025)
- [MINIF2F-DAFNY: LLM-Guided Mathematical Theorem Proving via Auto-Active Verification](https://mlsanity.com/paper/2512.10187/) (2025)
- [Spec-Harness: Assessing and Guiding LLM-Synthesized Formal Specifications Beyond Verifiability](https://mlsanity.com/paper/2604.00280/) (2026)
- [Intent-aligned Formal Specification Synthesis via Traceable Refinement](https://mlsanity.com/paper/2604.10392/) (2026)
- [Towards Automated Formal Verification of Backend Systems with LLMs](https://mlsanity.com/paper/2506.10998/) (2025)
- [ModelWisdom: An Integrated Toolkit for TLA+ Model Visualization, Digest and Repair](https://mlsanity.com/paper/2602.12058/) (2026)
- [LLMs as verification oracles for Solidity](https://mlsanity.com/paper/2509.19153/) (2025)
- [AutoICE: Automatically Synthesizing Verifiable C Code via LLM-driven Evolution](https://mlsanity.com/paper/2512.07501/) (2025)
- [LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation](https://mlsanity.com/paper/2605.01394/) (2026)
- [Neurosymbolic Auditing of Natural-Language Software Requirements](https://mlsanity.com/paper/2605.13817/) (2026)
- [Specula: Scaling formal specifications for autonomous model checking of system code](https://mlsanity.com/paper/2607.25333/) (2026)
- [VeriSkill: A Self-Evolution Framework for Program Verification Skills](https://mlsanity.com/paper/2607.27733/) (2026)
- [Verification of PETSc with CIVL using LLM-generated ACSL contracts and deterministic driver generation](https://mlsanity.com/paper/2609.31687/) (2026)
- [Learning to Prove, Not Just to Answer: Reinforcement Learning from Formal Verification for Natural-Language Logical Reasoning](https://mlsanity.com/paper/2609.37203/) (2026)

## 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.