Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization

• URL: http://arxiv.org/abs/2606.31002v1
• Date: Tue, 30 Jun 2026 00:27:53 GMT
• Title: Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization
• Abstract summary: 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.
• Score: 10.775710068605006
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Theorem-proving benchmarks evaluate proof search against fixed formal statements, but natural-language-to-Lean formalization must generate the formal statement itself. In this setting, compilation is only a validity check: a Lean declaration may type-check while omitting hypotheses, changing domains, or expressing a vacuous claim. We study faithful statement formalization as both an evaluation problem and a bottleneck-attribution problem. On a 400-entry graduate-level benchmark spanning real analysis, complex analysis, topology, and algebra, our protocol combines Lean compilation, cross-model semantic judging, and human expert calibration. The resulting picture is different from compile-rate evaluation: 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. Targeted human audits support the metric as a conservative decision boundary: across available case-level audits, 96.0% of consensus-positive outputs are human-confirmed faithful, while 82.4% of compile-pass consensus-negative outputs are human-confirmed semantic failures. Under this metric, existing one-shot formalizer models and prover-oriented Lean models remain low, suggesting that formal validity, proof-oriented Lean competence, and faithful statement generation should be reported separately. We then use a full $2^3$ factorial design to decompose three recurring interventions in formalization pipelines: parametric expert drafting, Mathlib/context search, and Lean elaboration feedback. Elaboration feedback is the largest validity intervention, but it also exposes a larger compile-pass semantic-failure bucket; search mainly improves grounding and selectivity; and fine-tuned drafting is largely substitutable in this tool stack once feedback and grounding are available.

Related papers

• Autoformalizing Argumentative Material Inferences [26.35292656634472]
  We develop an autoformalization for argumentative material inference as guard completion.<n>GUARD yields significant improvements in verified-faithful.<n>We show that the symbolic soft critique and the explicit assumption layer account for most of these gains.
  arXiv  Detail & Related papers  (2026-09-15T11:05:26Z)
• 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)
• 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)
• 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)
• Benchmarking Testing in Automated Theorem Proving [39.65133452374143]
  T is a framework that evaluates the semantic correctness of formal theorems.<n>We construct a benchmark from 5 real-world Lean 4 repositories.<n>Experiments demonstrate that while state-of-the-art models achieve high compilation success, they perform significantly worse under our semantic metric.
  arXiv  Detail & Related papers  (2026-04-26T13:24:20Z)
• HLE-Verified: A Systematic Verification and Structured Revision of Humanity's Last Exam [63.84155758655084]
  Humanity's Last Exam (HLE) has become a widely used benchmark for evaluating frontier large language models.<n>We introduce HLE-Verified, a verified and revised version of HLE with a transparent verification protocol and fine-grained error taxonomy.<n>We evaluate seven state-of-the-art language models on HLE and HLE-Verified, observing an average absolute accuracy gain of 7--10 percentage points.
  arXiv  Detail & Related papers  (2026-02-15T02:50:15Z)
• 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)
• Localizing Factual Inconsistencies in Attributable Text Generation [74.11403803488643]
  We introduce QASemConsistency, a new formalism for localizing factual inconsistencies in attributable text generation.<n>We show that QASemConsistency yields factual consistency scores that correlate well with human judgments.
  arXiv  Detail & Related papers  (2024-10-09T22:53:48Z)
• Logical Satisfiability of Counterfactuals for Faithful Explanations in NLI [60.142926537264714]
  We introduce the methodology of Faithfulness-through-Counterfactuals. It generates a counterfactual hypothesis based on the logical predicates expressed in the explanation. It then evaluates if the model's prediction on the counterfactual is consistent with that expressed logic.
  arXiv  Detail & Related papers  (2022-05-25T03:40:59Z)

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.