MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement

• URL: http://arxiv.org/abs/2608.14221v1
• Date: Fri, 14 Aug 2026 11:51:12 GMT
• Title: MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement
• Abstract summary: We introduce MathForm, an autoformalization framework for constructing verified training data.<n>We construct FormalVerse, a Lean 4 dataset containing approximately 367K verified examples.<n>MathForm-8B achieves average Pass@8 rates of 88.06% under Syntax Check and 72.37% under Consistency Check.
• Score: 28.062085562858098
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Autoformalization is commonly framed as translating natural-language mathematical statements into machine-verifiable formal languages such as Lean 4. However, faithful formalization requires more than translation. Models must map mathematical concepts to the complex hierarchy of types and definitions in formal libraries such as Mathlib, while ensuring that generated statements preserve the meaning of the source propositions. Existing approaches struggle because they rely heavily on the model's parametric memory for library-specific knowledge, while common data construction pipelines often resort to filtering single-pass outputs and lack mechanisms for feedback-driven revision. To address these challenges, we introduce MathForm, an autoformalization framework for constructing verified training data through Mathlib knowledge retrieval and verification-guided iterative refinement. Before generation, a retrieval planner gathers relevant definitions and existing formalizations from Mathlib to guide the formalization generator. Generated statements are then revised using compiler diagnostics and semantic-consistency feedback. Using this framework, we construct FormalVerse, a Lean 4 dataset containing approximately 367K verified examples across diverse mathematical domains and sources. We then train MathForm-8B through supervised fine-tuning followed by reinforcement learning. Across six benchmarks, MathForm-8B achieves average Pass@8 rates of 88.06% under Syntax Check (SC) and 72.37% under Consistency Check (CC), outperforming multiple specialized 32B autoformalizers. On the challenging FATE-H and FATE-X subsets, it attains CC pass rates of 63% and 37%, exceeding the strongest specialized baselines in both cases.

Related papers

• AMTFV: Agentic Mathematical Tool-Flow Verification for LLM Self-Correction [58.27846292449026]
  Large language models have demonstrated strong mathematical problem-solving capabilities, yet reliably verifying their candidate answers remains challenging.<n>We propose AMTFV (Agentic Mathematical Tool-Flow Verification), which decouples verification modeling from concrete execution.<n>We evaluate AMTFV on five challenging mathematical reasoning datasets with seven model configurations from DeepSeek, GPT, and Gemini.
  arXiv  Detail & Related papers  (2026-07-31T15:42:00Z)
• Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics [20.90238876313568]
  Large Language Models (LLMs) produce subtle errors that evade human detection.<n>Recent trends indicate that general-purpose LLMs now outperform smaller models explicitly fine-tuned for Lean.<n>We introduce an agentic autoformalization framework powered by general coding LLMs.
  arXiv  Detail & Related papers  (2026-06-30T05:05:03Z)
• Formalizing Numerical Analysis: An Agent Pipeline and Quality Audit Beyond Kernel Acceptance [0.3624700141426058]
  coding agents can formalize entire advanced mathematics textbooks in Lean 4.<n>We introduce a framework for evaluating the quality of agent-produced formalizations beyond compilation.<n>Our results suggest that compilation-based metrics substantially overstate formalization quality.
  arXiv  Detail & Related papers  (2026-06-12T00:45:42Z)
• TaoBench: Do Automated Theorem Prover LLMs Generalize Beyond MathLib? [104.38098884163541]
  We evaluate the robustness of current ATP systems when applied to a novel definitional framework.<n>We introduce TaoBench, an undergraduate-level benchmark derived from Terence Tao's Analysis I.<n>For fair evaluation, we build an agentic pipeline that automatically extracts a compilable, self-contained local environment for each problem.
  arXiv  Detail & Related papers  (2026-03-13T07:39:47Z)
• ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization [73.0780809974414]
  We propose a Reflective Autoformalization method that integrates semantic consistency evaluation into the autoformalization process.<n>This enables the model to iteratively generate formal statements, assess its semantic fidelity, and self-correct identified errors.<n>Experiments show that ReForm achieves an average improvement of 22.6 percentage points over the strongest baselines.
  arXiv  Detail & Related papers  (2025-10-28T16:22:54Z)
• DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theorems [14.568293842955065]
  DRIFT is a framework that decomposes informal mathematical statements into smaller, more tractable ''sub-components''<n>It retrieves illustrative theorems to help models use premises more effectively in formalization tasks.<n>We evaluate DRIFT across diverse benchmarks (ProofNet, ConNF, and MiniF2F-test) and find that it consistently improves premise retrieval.
  arXiv  Detail & Related papers  (2025-10-12T21:42:04Z)
• Autoformalizer with Tool Feedback [52.334957386319864]
  Autoformalization addresses the scarcity of data for Automated Theorem Proving (ATP) by translating mathematical problems from natural language into formal statements.<n>Existing formalizer still struggles to consistently generate valid statements that meet syntactic validity and semantic consistency.<n>We propose the Autoformalizer with Tool Feedback (ATF), a novel approach that incorporates syntactic and consistency information as tools into the formalization process.
  arXiv  Detail & Related papers  (2025-10-08T10:25:12Z)
• Automated Formalization via Conceptual Retrieval-Augmented LLMs [19.328918823576153]
  CRAMF is a Concept-driven Retrieval-Augmented Mathematical Formalization framework.<n>We introduce a framework for automatically constructing a concept-definition knowledge base from Mathlib4.<n>Experiments on miniF2F, ProofNet, and our newly proposed AdvancedMath benchmark show that CRAMF can be seamlessly integrated into LLM-based autoformalizers.
  arXiv  Detail & Related papers  (2025-08-09T10:54:25Z)
• FMC: Formalization of Natural Language Mathematical Competition Problems [12.86616278136374]
  We propose an autoformalization pipeline based on large language models with error feedback.<n>We curate an Olympiad-level dataset aligning natural language problems with Lean formalizations.<n>We show that few-shot learning, error feedback, and increasing sampling numbers enhance the autoformalization process.
  arXiv  Detail & Related papers  (2025-07-15T12:52:47Z)
• Enumerate-Conjecture-Prove: Formally Solving Answer-Construction Problems in Math Competitions [39.102692814217086]
  LLMs can tackle difficult answer-construction tasks but are prone to errors from hallucinations and unverifiable steps.<n>This raises a key understudied question: how to solve answer-construction problems while preserving both creativity and mathematical rigor?<n>We introduce the LLM-Conjecture-Prove (ECP) framework, a neuro-symbolic method integrating pattern-driven conjecturing with formal theorem proving.<n>On ConstructiveBench, ECP achieves 33.1% end-to-end state-of-the-art accuracy (up from 32.5%), demonstrating its potential to advance formal mathematical reasoning.
  arXiv  Detail & Related papers  (2025-05-24T03:52:25Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARD is a framework that masters uniform synthesis of theorem and proof data of high quality and diversity. We present a theorem-and-proof benchmark MUSTARDSAUCE with 5,866 valid data points. We perform extensive analysis and demonstrate that MUSTARD generates validated high-quality step-by-step data.
  arXiv  Detail & Related papers  (2024-02-14T05:57:58Z)
• TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models [68.65075559137608]
  We propose TRIGO, an ATP benchmark that not only requires a model to reduce a trigonometric expression with step-by-step proofs but also evaluates a generative LM's reasoning ability on formulas. We gather trigonometric expressions and their reduced forms from the web, annotate the simplification process manually, and translate it into the Lean formal language system. We develop an automatic generator based on Lean-Gym to create dataset splits of varying difficulties and distributions in order to thoroughly analyze the model's generalization ability.
  arXiv  Detail & Related papers  (2023-10-16T08:42:39Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.