# StepProof: Step-by-step verification of natural language mathematical proofs

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

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- Builds on 23 of its 36 references that are in the map.
- First posted on arXiv 12 Jun 2025.

## Builds on (most cited first, 23 of 23)

- [GPT-4 Technical Report](https://mlsanity.com/paper/2303.08774/) (2023)
- [The Llama 3 Herd of Models](https://mlsanity.com/paper/2407.21783/) (2024)
- [Chain-of-Thought Prompting Elicits Reasoning in Large Language Models](https://mlsanity.com/paper/2201.11903/) (2022)
- [Training Verifiers to Solve Math Word Problems](https://mlsanity.com/paper/2110.14168/) (2021)
- [Measuring Mathematical Problem Solving With the MATH Dataset](https://mlsanity.com/paper/2103.03874/) (2021)
- [A Survey of Large Language Models](https://mlsanity.com/paper/2303.18223/) (2023)
- [Pre-train, Prompt, and Predict: A Systematic Survey of Prompting Methods in Natural Language Processing](https://mlsanity.com/paper/2107.13586/) (2021)
- [Survey of Hallucination in Natural Language Generation](https://mlsanity.com/paper/2202.03629/) (2022)
- [ChatGLM: A Family of Large Language Models from GLM-130B to GLM-4 All Tools](https://mlsanity.com/paper/2406.12793/) (2024)
- [Large Language Models Cannot Self-Correct Reasoning Yet](https://mlsanity.com/paper/2310.01798/) (2023)
- [Decomposed Prompting: A Modular Approach for Solving Complex Tasks](https://mlsanity.com/paper/2210.02406/) (2022)
- [A Survey on RAG Meeting LLMs: Towards Retrieval-Augmented Large Language Models](https://mlsanity.com/paper/2405.06211/) (2024)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [A Comprehensive Capability Analysis of GPT-3 and GPT-3.5 Series Models](https://mlsanity.com/paper/2303.10420/) (2023)
- [LEGO-Prover: Neural Theorem Proving with Growing Libraries](https://mlsanity.com/paper/2310.00656/) (2023)
- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalization](https://mlsanity.com/paper/2403.18120/) (2024)
- [Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar](https://mlsanity.com/paper/1912.02636/) (2019)
- [Exploring Neural Models for Parsing Natural Language into First-Order Logic](https://mlsanity.com/paper/2002.06544/) (2020)
- [Do Large Language Models Understand Logic or Just Mimick Context?](https://mlsanity.com/paper/2402.12091/) (2024)
- [A Survey on Theorem Provers in Formal Methods](https://mlsanity.com/paper/1912.03028/) (2019)
- [Comparison of Two Theorem Provers: Isabelle/HOL and Coq](https://mlsanity.com/paper/1808.09701/) (2018)
- [Python client for Isabelle server](https://mlsanity.com/paper/2212.11173/) (2022)

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

- [ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalization](https://mlsanity.com/paper/2510.15981/) (2025)
- [ReProbe: Efficient Test-Time Scaling of Multi-Step Reasoning by Probing Internal States of Large Language Models](https://mlsanity.com/paper/2511.06209/) (2025)
- [Towards a Common Framework for Autoformalization](https://mlsanity.com/paper/2509.09810/) (2025)
- [Do We Need Frontier Models to Verify Mathematical Proofs?](https://mlsanity.com/paper/2604.02450/) (2026)
- [Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases](https://mlsanity.com/paper/2607.13292/) (2026)
- [Evaluating the Robustness of Proof Autoformalization in Lean 4](https://mlsanity.com/paper/2606.14867/) (2026)

## Abstract (arXiv)

Interactive theorem provers (ITPs) are powerful tools for the formal verification of mathematical proofs down to the axiom level. However, their lack of a natural language interface remains a significant limitation. Recent advancements in large language models (LLMs) have enhanced the understanding of natural language inputs, paving the way for autoformalization - the process of translating natural language proofs into formal proofs that can be verified. Despite these advancements, existing autoformalization approaches are limited to verifying complete proofs and lack the capability for finer, sentence-level verification. To address this gap, we propose StepProof, a novel autoformalization method designed for granular, step-by-step verification. StepProof breaks down complete proofs into multiple verifiable subproofs, enabling sentence-level verification. Experimental results demonstrate that StepProof significantly improves proof success rates and efficiency compared to traditional methods. Additionally, we found that minor manual adjustments to the natural language proofs, tailoring them for step-level verification, further enhanced StepProof's performance in autoformalization.