Faithful Autoformalization via Roundtrip Verification and Repair

• URL: http://arxiv.org/abs/2604.25031v1
• Date: Mon, 27 Apr 2026 22:26:01 GMT
• Title: Faithful Autoformalization via Roundtrip Verification and Repair
• Abstract summary: 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.
• Score: 0.4403025166321017
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: When an LLM formalizes natural language, how do we know the output is faithful? We propose a roundtrip verification approach which does not require ground-truth annotations: formalize a statement, translate the result back to natural language, re-formalize, and use a formal tool to check logical equivalence. When the two formalizations agree, this provides evidence of a faithful formalization. When they disagree, a diagnosis step identifies which translation stage failed, and a targeted repair operator attempts to correct that stage. We evaluate our approach on 150 traffic rules using Claude Opus 4.6 and GPT-5.2. Diagnosis-guided repair raises formal equivalence from 45--61% to 83--85% for both models, outperforming a random-repair baseline. An independent NLI analysis confirms that formal equivalence is correlated with less semantic drift.

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)
• Faithful Autoformalization of Natural Language Assertions [2.8921494813790094]
  We present Monty: an autoformalization framework for assertions.<n>Our techniques are based on filtering formalizations using a novel conformance score metric.<n>We show that our technique produces the ground truth more reliably than when using LLMs naively to translate assertions.
  arXiv  Detail & Related papers  (2026-07-14T22:12:14Z)
• ITPEval: Benchmarking Formal Translation Across Interactive Theorem Provers [77.95933562142014]
  ITPEval is the first benchmark for evaluating automated formal proof translation across four major ITPs.<n>We release itpeval, a unified multi-ITP verification infrastructure with state-isolated warm backends.
  arXiv  Detail & Related papers  (2026-07-07T22:05:55Z)
• 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)
• Evaluating the Robustness of Proof Autoformalization in Lean 4 [8.029528831501514]
  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.
  arXiv  Detail & Related papers  (2026-06-12T18:10:21Z)
• Retrieval-Augmented Linguistic Calibration [57.41519309308438]
  We model linguistic confidence as a distribution over plausible perceived probability values that a statement is correct.<n>We present Retrieval-Augmented Linguistic truth (RALC), a lightweight post-hoc pipeline that propagates confidence signals back into natural language.
  arXiv  Detail & Related papers  (2026-05-19T04:31:38Z)
• Do LLMs Game Formalization? Evaluating Faithfulness in Logical Reasoning [20.336209492846752]
  Formal verification guarantees proof validity but not formalization faithfulness.<n>We investigate whether frontier models exploit this gap when generating Lean 4 proofs.<n>We find no evidence of systematic gaming in unified generation.
  arXiv  Detail & Related papers  (2026-04-21T13:37:49Z)
• miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path Forward [16.8655558789989]
  We analyze the formal and informal statements in the miniF2F benchmark from the perspective of an AI system tasked to participate in a math Olympiad consisting of the problems in miniF2F.<n>Our evaluation results reveal that the best accuracy of such pipeline can be about 36% using the SoTA models in the literature.<n>We present the miniF2F-v2 with fully verified formal and informal statements and proofs.
  arXiv  Detail & Related papers  (2025-11-05T01:27:49Z)
• 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)
• StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusion [30.51794514312176]
  We identify two key abilities for effective autoformalization.<n>We introduce ThinkingF, a data synthesis and training pipeline that improves both abilities.<n>The resulting 7B and 32B models exhibit both comprehensive formal knowledge and strong informal-to-formal reasoning.
  arXiv  Detail & Related papers  (2025-08-06T13:28:22Z)
• Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification [56.218970738892764]
  Chain-of-Thought prompting has become the de facto method to elicit reasoning capabilities from large language models (LLMs)<n>To mitigate hallucinations in CoT that are notoriously difficult to detect, current methods operate as opaque boxes and do not provide checkable evidence for their judgments, possibly limiting their effectiveness.<n>We propose a retrospective, step-aware formal verification framework $Safe$. Rather than assigning arbitrary scores, we strive to articulate mathematical claims in formal mathematical language Lean 4 at each reasoning step and provide formal proofs to identify hallucinations.
  arXiv  Detail & Related papers  (2025-06-05T03:16:08Z)
• Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving [72.8626512877667]
  We introduce Goedel-Prover, an open-source language model that achieves state-of-the-art (as of April 5 2025) performance in automated formal proof generation for mathematical problems.<n>First, we train LLMs to convert natural language math problems from the Numina dataset to equivalent formal statements in Lean 4.<n>Next, we develop a large dataset of formal proofs by training a series of provers.<n>Finally, we obtain the dataset Goedel-Pset-v1-solved, which contains proofs for over 800K statements from Goedel-Pset-v1
  arXiv  Detail & Related papers  (2025-02-11T15:27:35Z)
• 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)

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.