Evaluating the Robustness of Proof Autoformalization in Lean 4

• URL: http://arxiv.org/abs/2606.14867v1
• Date: Fri, 12 Jun 2026 18:10:21 GMT
• Title: Evaluating the Robustness of Proof Autoformalization in Lean 4
• Abstract summary: We argue that a robust proof autoformalizer must remain faithful even for informal proofs that diverge from idealized ones.<n>We build a benchmark with both perturbations on miniF2F and MATH-500.<n>We evaluate seven recent models, all of which are sensitive to global perturbations and mostly fail to remain faithful under local perturbations.
• Score: 8.029528831501514
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Proof autoformalization aims to translate a mathematical informal proof written in natural language into a formal proof in a formal language such as Lean~4. Several works have developed LLM-based models for proof autoformalization. However, existing evaluations have typically focused on translating well-formed informal proofs from curated datasets. We argue that a robust proof autoformalizer must remain faithful even for informal proofs that diverge from these idealized ones, and we present the first study on the robustness of proof autoformalization models. We formulate two categories of perturbations and evaluate robustness under each: a global perturbation paraphrases the informal proof in a different style, under which the formalization should remain consistent; a local perturbation alters a value, symbol, or proof step, possibly in a counterfactual way, and a robust formalization should faithfully reflect the perturbation rather than reverting to the original one or inferring a different one on its own. We build a benchmark with both perturbations on miniF2F and MATH-500, and automatically measure how stable a proof autoformalization's correctness is under global perturbations and how faithfully its output reflects local perturbations. We evaluate seven recent models, all of which are sensitive to global perturbations and mostly fail to remain faithful under local perturbations. Code and data are available via https://github.com/ucr-rai/robust-proof-autoformalization.

Related papers

• FaithSieve: Fine-Grained Evaluation of Math Proofs with Faithful Formal Evidence [9.041607777624504]
  FaithSieve is a Lean-assisted framework for fine-grained evaluation of natural-language mathematical proofs.<n>It decomposes proof steps into local reasoning units, extracts typed proof obligations, and verifies them.<n>On the 350-problem Olympiad dataset, FaithSieve using a GPT-5.4 backbone achieves 81.43% exact first-error accuracy.
  arXiv  Detail & Related papers  (2026-08-26T18:43:30Z)
• Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization [10.775710068605006]
  We study faithful statement formalization as both an evaluation problem and a bottleneck-attribution problem.<n>A full tool-augmented agent reaches 89.5% compilation but only 60.5% consensus faithfulness, exposing a 29.0-point compile-pass but consensus-unfaithful gap.
  arXiv  Detail & Related papers  (2026-06-30T00:27:53Z)
• Casual as an Anchor: Resolving Supervision Misalignment in Formality Transfer Dataset [22.0608497133374]
  Formality transfer is commonly framed as a symmetric bidirectional task between informal and formal registers.<n>We argue that this framing conceals a supervision design flaw in existing benchmarks such as GYAFC.<n>We quantify this misalignment by re-evaluating benchmark formal labels under a human-aligned definition of formality.
  arXiv  Detail & Related papers  (2026-05-28T05:07:02Z)
• Faithful Autoformalization via Roundtrip Verification and Repair [0.4403025166321017]
  We propose a roundtrip verification approach which does not require ground-truth annotations.<n>When the two formalizations agree, this provides evidence of a faithful formalization.<n>We evaluate our approach on 150 traffic rules using Claude Opus 4.6 and GPT-5.2.
  arXiv  Detail & Related papers  (2026-04-27T22:26:01Z)
• Pushing the Boundaries of Natural Reasoning: Interleaved Bonus from Formal-Logic Verification [49.506412445511934]
  Large Language Models (LLMs) show remarkable capabilities, yet their next-token prediction creates logical inconsistencies and reward hacking.<n>We introduce a formal logic verification-guided framework that dynamically interleaves formal symbolic verification with the natural language generation process.<n>We operationalize this framework via a novel two-stage training pipeline that synergizes formal logic verification-guided supervised fine-tuning and policy optimization.
  arXiv  Detail & Related papers  (2026-01-30T07:01:25Z)
• 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)
• 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 Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
  We introduce SAFE, a framework that overcomes the lack of human-written snippets to enable automated proof generation of Rust code.<n> SAFE re-purposes the large number of synthesized incorrect proofs to train the self-ging capability of the fine-tuned models.<n>We achieve a 52.52% accuracy rate in a benchmark crafted by human experts, a significant leap over GPT-4o's performance of 14.39%.
  arXiv  Detail & Related papers  (2024-10-21T08:15:45Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  We present Lean-STaR, a framework for training language models to produce informal thoughts prior to each step of a proof.<n>Lean-STaR achieves state-of-the-art results on the miniF2F-test benchmark within the Lean theorem proving environment.
  arXiv  Detail & Related papers  (2024-07-14T01:43:07Z)
• Reliable Evaluation and Benchmarks for Statement Autoformalization [18.218951526592914]
  We present a comprehensive approach combining improved metrics, robust benchmarks, and systematic evaluation.<n>First, we introduce BEq+, an automated metric that correlates strongly with human judgment, along with ProofNetVerif, a new dataset for assessing the quality of evaluation metrics.<n>We develop two new autoformalization benchmarks: ProofNet#, a corrected version of ProofNet, and RLM25, with 619 new pairs of research-level mathematics from six formalization projects.
  arXiv  Detail & Related papers  (2024-06-11T13:01:50Z)
• AmbiFC: Fact-Checking Ambiguous Claims with Evidence [57.7091560922174]
  We present AmbiFC, a fact-checking dataset with 10k claims derived from real-world information needs. We analyze disagreements arising from ambiguity when comparing claims against evidence in AmbiFC. We develop models for predicting veracity handling this ambiguity via soft labels.
  arXiv  Detail & Related papers  (2021-04-01T17:40:08Z)

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.