mlsanityData to 14 Oct 2026

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

arXiv 2506.10558 ↗First posted 12 Jun 2025cs.LO cs.AIcited by 6

Not on the map. Why?

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.

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

23 of 36 references.

References · 23

  1. 2023GPT-4 Technical Reportcited by 18,396
  2. 2024The Llama 3 Herd of Modelscited by 14,715
  3. 2022Chain-of-Thought Prompting Elicits Reasoning in Large Language Modelscited by 12,459
  4. 2021Training Verifiers to Solve Math Word Problemscited by 10,109
  5. 2021Measuring Mathematical Problem Solving With the MATH Datasetcited by 5,371
  6. 2023A Survey of Large Language Modelscited by 2,576
  7. 2021Pre-train, Prompt, and Predict: A Systematic Survey of Prompting Methods in Natural Language Processingcited by 2,234
  8. 2022Survey of Hallucination in Natural Language Generationcited by 2,075
  9. 2024ChatGLM: A Family of Large Language Models from GLM-130B to GLM-4 All Toolscited by 1,121
  10. 2023Large Language Models Cannot Self-Correct Reasoning Yetcited by 1,017
  11. 2022Decomposed Prompting: A Modular Approach for Solving Complex Taskscited by 558
  12. 2024A Survey on RAG Meeting LLMs: Towards Retrieval-Augmented Large Language Modelscited by 452
11 more
  1. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 291
  2. 2023A Comprehensive Capability Analysis of GPT-3 and GPT-3.5 Series Modelscited by 246
  3. 2023LEGO-Prover: Neural Theorem Proving with Growing Librariescited by 109
  4. 2024A Survey on Deep Learning for Theorem Provingcited by 57
  5. 2024Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalizationcited by 55
  6. 2019Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizarcited by 40
  7. 2020Exploring Neural Models for Parsing Natural Language into First-Order Logiccited by 16
  8. 2024Do Large Language Models Understand Logic or Just Mimick Context?cited by 10
  9. 2019A Survey on Theorem Provers in Formal Methodscited by 8
  10. 2018Comparison of Two Theorem Provers: Isabelle/HOL and Coqcited by 1
  11. 2022Python client for Isabelle servercited by 1

Built on by

Cited by year (2026 to 14 Oct)

Citing papers per year: 2025: 3; 2026: 3.

6 papers.

  1. 2025ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalizationcited by 21
  2. 2025ReProbe: Efficient Test-Time Scaling of Multi-Step Reasoning by Probing Internal States of Large Language Modelscited by 10
  3. 2025Towards a Common Framework for Autoformalizationcited by 7
  4. 2026Do We Need Frontier Models to Verify Mathematical Proofs?cited by 3
  5. 2026Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Basescited by 3
  6. 2026Evaluating the Robustness of Proof Autoformalization in Lean 4cited by 0