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

1. Problem Statement

The paper addresses the task of natural-language-to-Lean statement formalization: automatically translating informal mathematical statements into valid Lean 4 theorem declarations. This task is distinct from theorem proving. In theorem proving benchmarks (e.g., MiniF2F, LeanDojo), the formal statement is fixed and trusted; the system's goal is to generate a proof accepted by the checker. In statement formalization, the system must generate the statement itself.

The core challenge is that compilation is a necessary but insufficient condition for success. A Lean declaration may type-check (compile) while:

• Omitting critical hypotheses.
• Changing the domain of discourse.
• Strengthening or weakening the claim.
• Encoding a vacuous version of the result.

Prior work has often relied on compilation rates or reference-based equivalence metrics (e.g., BEq, back-translation). This paper argues that compilation alone creates a "compile-pass gap" where systems appear successful but fail to preserve the intended mathematical meaning. The authors define the central problem as evaluating faithful statement formalization: generating declarations that both compile and preserve the semantic intent of the natural-language input.

2. Methodology

2.1 Benchmark Construction

The authors curated a graduate-level benchmark consisting of 400 natural-language statements derived from open-source LaTeX lecture notes and textbooks. The dataset is balanced across four domains:

• Real Analysis (100 entries)
• Complex Analysis (100 entries)
• Topology (100 entries)
• Algebra (100 entries)

Crucially, these statements have no accompanying gold Lean declarations, ensuring the task represents genuine translation rather than retrieval.

2.2 Evaluation Protocol

The paper proposes a Consensus LLM-as-Judge metric, calibrated by human experts, to evaluate faithfulness. The protocol involves two stages:

1. Compiler Verification: Any code failing to compile is immediately deemed unfaithful.
2. Semantic Consensus: For compiling code, two independent LLM judges (GPT-5.2 and Gemini-2.5-Pro) compare the generated Lean declaration against the original natural-language statement. They assign a faithfulness score (0–10).
   • Success Metric: A translation is considered Faithful if and only if it compiles AND both judges score it $\ge 9$.
   • This strict consensus approach is designed as a conservative operating point for system comparison, not a formal proof of equivalence.

2.3 Human Calibration

To validate the automated metric, the authors conducted human audits:

• Consensus-Positive: 96.0% of outputs labeled faithful by the strict consensus were confirmed faithful by human reviewers.
• Consensus-Negative (Compile-Pass): 82.4% of outputs that compiled but were rejected by consensus were confirmed as genuine semantic failures by humans.
  This confirms the metric is a high-precision, conservative filter that effectively identifies semantic drift.

2.4 Experimental Setup: Factorial Design

The authors evaluated various systems (general-purpose LLMs, specialized formalizers, prover-oriented models, and tool-augmented agents) using a $2^3$ factorial design to decompose the effects of three common interventions:

1. Parametric Expert Drafting (T): Using a fine-tuned model (Herald) to generate an initial draft.
2. Knowledge Search (S): Using tools to query Mathlib (symbol lookup, namespace resolution) and perform web searches for grounding.
3. Lean Elaboration Feedback (F): Using a REPL to compile code iteratively and receive error messages for repair.

The agent architecture uses a central orchestrator (GPT-5.2) that maintains state and decides which tools to invoke based on the configuration.

3. Key Results

3.1 The Compile-Pass Gap

The most significant empirical finding is the divergence between compilation rates and semantic faithfulness:

• A full tool-augmented agent achieved an 89.5% compilation rate.
• However, under the strict consensus metric, only 60.5% of outputs were deemed faithful.
• This leaves a 29.0-point gap where outputs compile but fail semantic checks. Human audits confirmed that the majority of these "compile-pass, consensus-negative" cases are real semantic failures (e.g., missing hypotheses, vacuous claims).

3.2 Model Performance

• Specialized Formalizers & Prover Models: Dedicated statement formalizers (e.g., Herald, Kimina-Autoformalizer) and prover-oriented models (e.g., Goedel-Prover, Kimina-Prover) performed poorly on statement generation when the formal target was not supplied. Their faithfulness rates ranged from 4.0% to 12.3%.
• General LLMs: One-shot general-purpose LLMs reached 19.8–28.0% faithfulness.
• Tool-Augmented Agents: The full agent framework significantly outperformed one-shot baselines, reaching 60.5% faithfulness. However, different orchestrators (Sonnet 4.5, Gemini-2.5-Pro) converged to similar performance levels (60–65%) despite different baselines, suggesting the gains are structural to the tool-augmented approach rather than specific to the orchestrator model.

3.3 Factorial Decomposition of Interventions

The study isolated the impact of the three tools:

• Elaboration Feedback (F): This was the largest driver of validity (compilation), increasing the compile rate significantly. However, it also expanded the "compile-pass but unfaithful" bucket, as it allowed more syntactically correct but semantically drifted statements to pass.
• Search (S): Search primarily improved grounding and selectivity. It reduced the compile-pass gap (i.e., it helped filter out semantically incorrect statements that managed to compile) and improved efficiency by reducing the number of REPL iterations needed. Its marginal benefit was highest when feedback was absent.
• Expert Drafting (T): The fine-tuned drafting prior was largely substitutable once feedback and grounding were available. In fact, with full feedback, the drafting prior slightly hurt performance, suggesting that a strong orchestrator with compiler feedback can outperform a specialized draft in this specific tool stack.

3.4 Domain-Specific Variations

• Complex Analysis showed the highest gains from compiler feedback (+54.2 points in faithfulness), likely due to mature Mathlib coverage.
• Real Analysis and Algebra showed smaller gains, indicating either limited library support or higher intrinsic formalization difficulty.
• Topology exhibited specific challenges with advanced concepts (e.g., covering spaces), where feedback often led to valid but semantically shifted statements.

4. Significance and Claims

The paper claims that statement formalization must be evaluated as meaning preservation, not merely as Lean acceptance. The primary contributions are:

1. A New Metric: A human-calibrated, consensus-based metric that exposes the "compile-pass gap," revealing that many systems generate syntactically valid but semantically incorrect statements.
2. Diagnostic Decomposition: A factorial analysis showing that tools are not monotone add-ons. While feedback fixes syntax, it can obscure semantic errors; search improves grounding but has diminishing returns when feedback is present; and specialized drafting is not always necessary in a feedback-rich loop.
3. System Comparison: Evidence that current prover-oriented models and specialized formalizers do not automatically transfer their proof capabilities to semantically faithful statement generation without explicit statement-centric training or tool-augmented protocols.

The authors conclude that future systems should pair strong Lean feedback with semantic evaluation and policies that decide when to search, repair, or stop, rather than relying on average accuracy gains alone. The paper explicitly avoids claiming that their metric is a formal proof of equivalence, positioning it instead as a conservative, scalable decision boundary for system comparison.