PaperlayerView exact revision on arXiv

Source-linked AI summary

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

Lushi Pu, Weiming Zhang, Xinheng Xie, Zixuan Fu, Bingxiang He, Hengyu Zhao, Hongya Lyu, Xin Li, Jie Zhou, Yudong Wang

arXiv:2608.14221v1cs.AIcs.CL

TL;DR

Autoformalization must address both Mathlib-specific knowledge and semantic fidelity, but existing one-shot approaches lack retrieval and feedback-driven revision. MathForm combines knowledge retrieval with verification-guided iterative refinement, and MathForm-8B achieves 88.06% Syntax Check and 72.37% Consistency Check average Pass@8 across six benchmarks while outperforming specialized 32B autoformalizers.

  • Problem

    Existing autoformalization approaches rely heavily on parametric library knowledge and commonly judge one-shot outputs after generation, risking formal statements that compile but deviate from their intended meaning.

  • Method

    MathForm combines Mathlib knowledge retrieval with compiler- and semantic-consistency-guided iterative refinement to construct verified Lean 4 training data.

  • Results

    88.06% Syntax Check and 72.37% Consistency Check average Pass@8 across six benchmarks, outperforming multiple specialized 32B autoformalizers.

  • Takeaways & Limitations

    The results support knowledge retrieval and verification-guided iterative refinement as effective components for autoformalization data construction and compact-model performance.

Abstract

from arXiv · show

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.

1 Introduction

MATHFORM addresses autoformalization’s reliance on parametric memory and one-shot filtering by combining Mathlib retrieval, verification, and iterative refinement. The resulting FORMALVERSE dataset and MATHFORM-8B model achieve strong verified-data scale and benchmark performance.

  • Motivation: Autoformalization remains a bottleneck because formal theorem proving needs large, diverse corpora of machine-checkable statements and proofs.Recent advances have improved Lean 4 proof generation, but such corpora remain scarce.
  • Limitations: Existing methods rely heavily on parametric memory, making it difficult to handle Mathlib’s evolving definitions, type system, notation, and formalization patterns.This can lead models to misuse definitions, invoke nonexistent lemmas, or produce library-inconventional expressions.
  • Methodological insight: Faithful formalization requires a knowledge-grounded process that repeatedly verifies and revises candidates rather than treating translation as one-shot generation.Compilable statements can still strengthen conditions or omit key assumptions, causing semantic deviations from the source.
  • MATHFORM: MATHFORM closes this gap by planning Mathlib retrieval before generation and using compiler diagnostics plus semantic-consistency judgments for iterative refinement.The framework integrates retrieval, automated verification, and refinement into a closed loop for reliable natural-language-to-Lean data construction.
  • Results: Approximately 367K verified examples comprise FORMALVERSE, while MATHFORM-8B reaches 88.06% average Pass@8 under Syntax Check and 72.37% under Consistency Check across six benchmarks.The model is trained with supervised fine-tuning followed by reinforcement learning and outperforms multiple specialized 32B autoformalizers; ablations identify retrieval, verification, and reinforcement learning as contributors.

2 Related Work

Related work has shifted from limited rule-based autoformalization toward LLM-based systems, while high-quality formal mathematical data remain scarce. Existing datasets provide benchmarks spanning Olympiad, undergraduate, combinatorial, and other formal reasoning settings.

  • Autoformalization methods: Recent autoformalization research has shifted from rule-based methods toward LLM-based systems such as TheoremLlama, Herald, Kimina-Autoformalizer, and Mathesis.Early rule-based methods were limited in accuracy and coverage.
  • Formal mathematical datasets: High-quality formal mathematical data remain scarce, motivating benchmark construction for formal reasoning and autoformalization.The passage identifies data scarcity as a longstanding challenge.
  • Formal mathematical datasets: MiniF2F and ProofNet formalize Olympiad-level problems and undergraduate theorems as Lean statements, supporting autoformalization and formal theorem-proving evaluation.More recent benchmarks include CombiBench, FATE, and MA-ProofBench, extending formal evaluation to combinatorics and related settings.

3 Method

MATHFORM constructs verified Lean 4 training data through retrieval-augmented formalization, iterative verification and refinement, trajectory reconstruction, and benchmark decontamination, then trains MATHFORM-8B with supervised fine-tuning and reinforcement learning. The resulting FORMALVERSE dataset contains approximately 367K verified NL-FL pairs.

  • 3.1 Data Construction: MATHFORM’s data-construction framework collects and normalizes diverse natural-language mathematics problems, retrieves Mathlib knowledge, generates formalizations, refines them through verification, reconstructs trajectories, and decontaminates the data.Sources include multiple mathematics datasets and classical textbooks; decontamination removes examples sharing at least one 13-gram with evaluation examples.
  • 3.1 Data Construction: The retrieval planner analyzes mathematical objects, relations, and type constraints, issues targeted Mathlib queries when needed, and guides a formalization generator that produces Lean 4 statements.The generator conditions on the original statement and retrieved results, reducing reliance on parametric memory and improving agreement with canonical Mathlib representations.
  • 3.1 Data Construction: 31.0% of retained pairs come from later refinement rounds, which use prior failed attempts, compiler diagnostics, and semantic feedback to revise formalizations.The resulting examples include a natural-language statement, a formalization trajectory, and verified Lean 4 code.
  • 3.1 Data Construction: The pipeline filters non-formal content, compiles candidate statements, records compiler diagnostics, and applies semantic checks for omissions, altered conditions, quantifier errors, inappropriate objects, and mismatched conclusions.Format Check removes proofs, tactics, solution procedures, and other content beyond the formal statement; semantic checking uses QwQ-32B as judge.
  • 3.2 Model Training: Approximately 367K verified NL-FL pairs remain after benchmark decontamination, and MATHFORM-8B is trained through supervised fine-tuning on FORMALVERSE followed by DAPO-based reinforcement learning.Reinforcement-learning statements are sampled from previously unsolved candidates, difficulty-filtered, and optimized with a binary reward requiring both compilation success and semantic consistency.

4 Experiments

The experiments assess MathForm-8B across six benchmarks using syntax and semantic-consistency checks. MathForm-8B achieves leading specialized-autoformalizer results, with especially strong gains on the challenging FATE benchmarks.

  • Evaluation Setup: Six benchmarks span competition mathematics, combinatorics, and algebraic reasoning from elementary abstract algebra through advanced algebraic geometry.The evaluation includes FormalMATH-Lite, ProverBench, CombiBench, FATE-M, FATE-H, and FATE-X.
  • Evaluation Setup: Pass@8 evaluates compilation-based Syntax Check (SC) and semantic-consistency-based Consistency Check (CC), using k = 8 samples at temperature 0.6.Kimina Lean Server provides Lean 4 compilation validation, while consistency is evaluated only for candidates that compile successfully.
  • Main Results: 88.06% SC and 72.37% CC are MathForm-8B’s average Pass@8 rates, exceeding ReForm-32B’s 81.61/68.41 by 6.45 and 3.96 percentage points.These are the best average results among specialized autoformalizers.
  • Main Results: 97.33%, 63.00%, and 37.00% are MathForm-8B’s CC pass rates on FATE-M, FATE-H, and FATE-X, exceeding the strongest specialized baselines by 6, 10, and 12 points.The advantage widens on the more challenging FATE subsets; on mature benchmarks, performance is comparable to or slightly better than the strongest baseline.
  • Training Analysis: Mean@3 on FATE-H rises from 0.30 to about 0.40 during reinforcement learning, an approximately 33% relative gain alongside steadily increasing reward.Human evaluation on FATE-M and FATE-H also places MathForm-8B highest in SC and human-assessed CC among compared models.

5 Conclusion

MathForm combines Mathlib knowledge retrieval with compilation- and semantic-signal-guided iterative refinement to build verified Lean 4 data and train MathForm-8B. The resulting model achieves strong average benchmark pass rates while outperforming multiple specialized 32B autoformalizers.

  • 5 Conclusion: MathForm combines knowledge retrieval with iterative refinement guided by compilation and semantic signals.The framework was used to construct FormalVerse and train MathForm-8B through supervised fine-tuning and reinforcement learning.
  • 5 Conclusion: 367K verified Lean 4 examples comprise the FormalVerse dataset constructed with MathForm.The dataset contains approximately 367K verified examples.
  • 5 Conclusion: 88.06% and 72.37% are MathForm-8B’s average SC and CC pass rates across six benchmarks.These results outperform multiple specialized 32B autoformalizers.

A Implementation Details · A.1 Category Distribution of FORMALVERSE

FORMALVERSE spans ten mathematical categories, providing broad domain coverage for training autoformalizers. Its problems range from competition mathematics to advanced topics.

  • A.1 Category Distribution of FORMALVERSE: FORMALVERSE covers ten mathematical categories, including inequalities, algebra, geometry, arithmetic, calculus, number theory, combinatorics, probability and statistics, and linear algebra.The category distribution is presented in Figure 6.
  • A.1 Category Distribution of FORMALVERSE: The dataset includes inequalities problems.
  • A.1 Category Distribution of FORMALVERSE: The dataset includes algebra, geometry, and arithmetic problems.
  • A.1 Category Distribution of FORMALVERSE: The dataset includes calculus and number theory problems.
  • A.1 Category Distribution of FORMALVERSE: The dataset includes combinatorics and probability and statistics problems.
  • A.1 Category Distribution of FORMALVERSE: The dataset includes linear algebra problems and spans a wide variety of problem types.
  • A Implementation Details: FORMALVERSE ranges from competition mathematics to advanced topics, supporting broad domain coverage for training autoformalizers.

A.2 Training Hyperparameters

The paper summarizes separate hyperparameters for supervised fine-tuning and reinforcement learning, using a shared 16-GPU setup and Lean 4.21.0 for compilation checks.

  • Training stages: Hyperparameters for supervised fine-tuning and reinforcement learning are summarized separately in Tables 5 and 6.Table 5 covers supervised fine-tuning, while Table 6 covers RL.
  • Compute: Both training stages use 16 NVIDIA H100 80GB GPUs.The same hardware configuration is used for supervised fine-tuning and RL.
  • Verification: All Lean compilation checks use Lean 4.21.0.This compiler version is used throughout the work.

B Additional Evaluation Results

This section reports the hyperparameters used for reinforcement learning (RL).

  • Table 6 presents the RL hyperparameters.

B.1 Comparison with General-Purpose LLMs

Across six benchmarks, MATHFORM-8B achieves the highest average SC pass rate among evaluated general-purpose LLMs, but its average CC pass rate trails Qwen3.7-Plus and DeepSeek-V4-Pro. Table 7 reports these Pass@8 SC and CC results using equally weighted macro-averages.

  • Average performance: 88.06% average SC pass rate makes MATHFORM-8B the strongest evaluated model, exceeding Qwen3.7-Plus at 86.33%.The comparison covers all six benchmarks.
  • Average performance: 72.37% average CC pass rate for MATHFORM-8B trails Qwen3.7-Plus at 83.38% and DeepSeek-V4-Pro at 76.54%.DeepSeek-V4-Pro is evaluated under the high reasoning-effort setting.
  • Evaluation protocol: Table 7 reports Pass@8 SC and CC pass rates across six benchmarks using an equally weighted macro-average.The table identifies the best result in each column in bold and the second best as underlined.

B.2 Human Evaluation · C Case Studies

Human experts evaluated randomly sampled formalizations from FATE-M and FATE-H for semantic faithfulness, with disagreements resolved by discussion. MathForm-8B achieved the highest human-assessed SC and CC pass rates on both datasets, preserving its automated-evaluation advantage.

  • B.2 Human Evaluation: For each FATE-M and FATE-H problem, evaluators randomly sampled one candidate from each model’s eight generated formalizations.The evaluation used one randomly sampled candidate per problem.
  • B.2 Human Evaluation: Two human experts assessed whether each sampled formalization faithfully preserved the source statement’s semantics.
  • B.2 Human Evaluation: Disagreements between the two experts were resolved through discussion.
  • B.2 Human Evaluation: Table 8 reports human-evaluation results as percentages for FATE-M and FATE-H.The table is based on one randomly sampled candidate per problem.
  • B.2 Human Evaluation: Human evaluation preserved the relative model ordering observed under automated evaluation.
  • B.2 Human Evaluation: 86.67% SC and 76.67% CC on FATE-M, and 54.00% SC and 42.00% CC on FATE-H, were the highest rates achieved by MATHFORM-8B.These results indicate that MathForm-8B’s advantage on challenging formalizations also holds under human assessment.

C.1 Case Study of the Data Construction Pipeline

A group-theoretic case study shows how verification-guided retrieval and refinement corrects a semantically incorrect but compiling formalization. After feedback prompts an additional subgroup-normality query, the revised code passes both checks.

  • Pipeline case study: The case study records retrieval queries, generated code, and both verification steps across refinement rounds.It examines the complete refinement pipeline on a group-theoretic problem.
  • Round 1: Round 1 compiled but formalized “K is normal in G” instead of “K is normal in H,” introducing a stronger assumption.The semantic consistency check detected the deviation despite successful compilation.
  • Round 2: Round 2 added a subgroup-normality query, clarified Mathlib’s definition scope, and revised the condition to state normality relative to H.The revised code passed both checks.
  • Takeaway: Targeted retrieval triggered by verification feedback supplied the library knowledge needed to correct the semantic deviation and achieve faithful formalization.The example demonstrates feedback-driven correction rather than single-pass filtering.

Case Study of the Data Construction Pipeline … D Prompts

The case studies show how retrieval and semantic feedback refine Lean formalizations, while the prompt designs specify retrieval planning, consistency validation, trajectory reconstruction, and evaluation-time instructions. Together, these components address both library-identifier failures and subtle semantic mismatches.

  • Retrieval: Retrieval queries surface Mathlib definitions for centralizers and normal subgroups before formalization.The planner queries `subgroup.centralizer definition` and `normal subgroup of a subgroup definition`, retrieving corresponding library definitions.
  • Generated formalization: The first formalization compiles but is semantically incorrect because it makes K normal in G rather than normal in H.The centralizer conditions, H’s normality in G, and the conclusion are otherwise correctly formalized.
  • Generated formalization: The revised formalization explicitly states K’s conjugation closure under elements of H and passes both compilation and semantic consistency checks.The corrected code captures K ≤ H, K normal in H, H normal in G, and trivial CH(K).
  • C.2 Case Study of MATHFORM-8B: MATHFORM-8B maps quotient fields to FractionRing and represents isomorphism existence with Nonempty, whereas all three 32B baselines fail on nonexistent identifiers.The baselines use identifiers such as Frac or QuotField, while MATHFORM-8B produces a correct formalization.
  • Model output: The commutative-algebra model output formalizes the problem with CommRing, IsDomain, UniqueFactorizationMonoid, FractionRing, RingEquiv, and Nonempty.Its Lean statement compiles and receives a correct semantic-consistency judgment.
  • D.1 Data Construction Prompts: The formalization-generator and retrieval-planner prompts require faithful Lean translation, relevant Mathlib context, selective new queries, and revision from compiler or semantic feedback.During refinement, both prompts carry diagnostics and semantic-consistency feedback from the previous attempt.
  • D.2 Semantic Consistency Check Prompt: The semantic consistency prompt compares natural language with Lean code using object, logical-structure, type-hierarchy, quantifier, and condition-strength checks, returning `correct` or `incorrect`.The same prompt is used for data-construction validation, the semantic reward term, and evaluation.
  • D.3 Trajectory Reconstruction Prompt: Trajectory reconstruction organizes verified examples into concept understanding, logical analysis, formalization strategy, and syntax translation, while evaluation prompts use model-specific templates and prohibit proof generation when needed.The reconstruction prompt focuses on formalization rather than proof strategy, and general-purpose inference adds an explicit no-proof instruction.
Loading 2608.14221v1…