PaperlayerView exact revision on arXiv

Source-linked AI summary

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

Ke Zhang, Patricio Gallardo Candela, Sudhir Murthy, Yi Xie, Zhi Wang, Maziar Raissi

arXiv:2606.31002v2cs.AIcs.CLcs.LO

TL;DR

A Lean declaration can compile without expressing the user's intended statement, and open-ended formalization lacks a canonical target for reference-based evaluation. The paper combines compilation with strict GPT–Gemini semantic consensus, calibrates that criterion against human review, and finds nonzero gaps across systems alongside 89.7% human agreement.

  • Problem

    In statement autoformalization, the generated declaration itself must be judged for faithfulness, but multiple faithful Lean encodings may exist and no canonical target is available.

    Source: §2 · p. 2

  • Method

    The authors evaluate declarations using Lean validity and strict GPT–Gemini consensus, calibrating a reference-free protocol with human review and complementary model and formal checks.

    Source: §1 · p. 2, §2.4 · p. 3

  • Results

    Every headline system showed a compile–faithfulness gap of 3.0–29.0 percentage points, and the independent audit found 89.7% human-majority agreement.

    Source: §1 · p. 2, §7 · p. 10

  • Takeaways & Limitations

    LLM judging is usable as a human-calibrated aggregate measurement instrument, not as ground truth or a semantic equivalence oracle.

    Source: §7 · p. 10

    The criterion is a semantic proxy rather than an equivalence proof, and region-conditional audits do not establish population-wide recall.

    Source: §6 · p. 9

Abstract

from arXiv · show

Lean verifies that a generated declaration is well typed, but not that it expresses the statement a user intended. We study two questions for autoformalization without canonical Lean targets: whether LLM judges can provide a usable proxy for human semantic review, and how much compilation overstates faithfulness across systems. Our criterion combines Lean compilation with strict semantic consensus between GPT-5.2 and Gemini-2.5-Pro. On an independently audited random sample, it agrees with human majority on 89.7\% of cases (Wilson 95\% CI: 82.1--94.3\%). Across eight systems evaluated on 400 graduate-level statements, every system has a nonzero compile--faithfulness gap, whose observed magnitude ranges from 3.0 to 29.0 percentage points. The full GPT-5.2 tool-augmented agent shows the largest gap, compiling 89.5\% while satisfying the semantic criterion on 60.5\%. Human review, an independent third-family judge, and a BEq formal cross-check provide complementary evidence that the accepted core is reliable and that most audited outputs in the gap are genuine semantic mismatches. A secondary $2^3$ factorial analysis shows that elaboration feedback is the largest validity intervention, yet does not eliminate semantic drift. LLM judging is therefore useful as a human-calibrated, conservative aggregate measure, not as an equivalence oracle.

1 Introduction

Lean compilation checks whether a declaration is valid, not whether it expresses the intended statement. The paper evaluates human-calibrated semantic judging and measures compile–faithfulness gaps across systems.

1 Introduction

  • Compilation can accept a declaration that omits a hypothesis, changes the domain, or weakens the conclusion, because it checks the theorem written rather than the user's intent.Without a canonical Lean declaration, exact-match or reference-dependent evaluation is unavailable for open-ended statements.Source: §1 · pp. 1–2
  • The study asks whether LLM semantic judging can approximate human review and whether compile–faithfulness gaps recur across model families.It evaluates general LLMs, specialized formalizers, prover-oriented models, and tool-augmented agents on 400 graduate-level statements.Source: §1 · p. 2
  • 89.7% human-majority agreement accompanied compile–faithfulness gaps of 3.0–29.0 percentage points across systems; the full agent compiled 89.5% but was faithful on 60.5%.The audit confirmed 95/114 rejected compile-pass outputs as genuine semantic failures.Source: §1 · p. 2
  • The contributions are a reference-free, human-calibrated protocol, an eight-system benchmark, and a factorial diagnostic of drafting, search, and elaboration feedback.The authors also release the benchmark, outputs, evaluation scripts, human annotations, and tool-call logs.Source: §1 · p. 2

2 Evaluation without Canonical Lean Targets

Statement formalization generates Lean declarations from natural-language statements, so compilation checks validity but not whether the generated claim matches the intended meaning. The section defines a reference-free evaluation setting, a four-domain benchmark, and a strict cross-judge protocol calibrated as a conservative faithfulness measure.

2.1 Task Definition

  • Statement formalization evaluates generated declarations against natural-language intent, unlike theorem proving, which checks proofs against fixed formal statements.The task requires syntactic validity, statement-centricity without proofs, and semantic faithfulness.Source: §2 · p. 2, §2.1 · p. 2

2.2 Evaluation Context

  • Prior evaluation approaches include references, back-translation, semantic scoring, human review, alignment, and formal checks; this paper contributes an audited reference-free protocol.The protocol uses human review alongside LeanScorer, an independent model family, threshold tests, and BEq checks.Source: §2.2 · pp. 2–3

2.3 Dataset Construction

  • The benchmark contains 400 graduate-level statements, balanced across Algebra, Real Analysis, Complex Analysis, and Topology with 100 entries per domain.Sources lack accompanying formal code, and rates are reported per entry rather than per unique theorem schema.Source: §2.3 · p. 3, Table 1 · p. 3

2.4 Evaluation Protocol

  • The protocol compiles outputs in Lean 4 with Mathlib, then has GPT-5.2 and Gemini-2.5-Pro independently grade semantic faithfulness on a 0–10 scale.Grades 9–10 indicate matching meaning with at most a tiny discrepancy; the strict intersection is calibrated against human judgments, not treated as proof of equivalence.Source: §2.4 · p. 3
  • Strict GPT-5.2/Gemini-2.5-Pro consensus is supported as a conservative faithfulness measure, with Table 2 comparing cross-judge coverage rather than system accuracy.The table aggregates different numbers of outputs, so the consensus/GPT ratio is more relevant than raw counts.Source: §2.4 · p. 3, Table 2 · p. 4

3 Formalization Pipeline and Tool Factors

The pipeline separates drafting, grounding, and elaboration feedback so their effects on validity, faithfulness, and efficiency can be studied independently. Tool access varies while the task prompt and output requirements remain fixed.

3 Formalization Pipeline and Tool Factors

  • The GPT-5.2 orchestrator uses Lean 4 feedback, retrieved information, and draft translations while remaining responsible for preserving the statement’s mathematical meaning.The architecture is designed as a controlled implementation of common pipeline remedies, not as an architectural novelty.Source: §3 · p. 4
  • The full agent is configuration 111; configuration 000 is the One-Shot Baseline, with the other seven settings selectively toggling tools.The architecture exposes separable information channels to examine which boundary—validity, faithfulness, or efficiency—each moves.Source: §3 · p. 4

3.1 Tools and the Bottlenecks They Target

  • Expert Drafting (T) supplies a specialized Lean statement draft for the general orchestrator to edit or verify.Knowledge Search (S) grounds the agent in Mathlib and context; Compiler Feedback (F) supplies whole-statement elaboration checks and error messages.Source: §3.1 · pp. 4–5
  • Table 3 reports human calibration of the compile + GPT∩Gemini criterion, with Wilson 95% confidence intervals and descriptive conditional ranges.The conditional ranges are not pooled intervals.Source: Table 3 · p. 5
  • Search returns identifier candidates, types, and definitions, but is not a dedicated semantic retrieval system such as LeanSearch Gao et al. [2024].The implemented tools include Mathlib symbol lookup, namespace resolution, and general web search.Source: §3.1 · p. 5
  • The three binary factors are drafting (T), search (S), and elaboration feedback (F), evaluated in a 2^3 factorial study.Detailed design and notation are deferred to Section 5.Source: §3.1 · p. 5

3.2 Controlled Prompt Assembly

  • All configurations hold the task prompt and output requirements fixed, varying only which tools the agent may call.The agent must produce a theorem declaration ending in := by sorry, import Mathlib, and translate rather than prove.Source: §3.2 · p. 5

4 Evaluation Results

Across the evaluated systems, compilation exceeds semantic acceptance, while human audits and complementary checks support the usefulness—but not oracle status—of the semantic criterion. The gap is largest for the full agent, and prover-oriented runs are a transfer diagnostic rather than a general test of formalization ability.

4.1 Q1: Can LLM Judges Approximate Human Review?

  • Across the independent random audit, the criterion agrees with human majority on 87/97 cases (89.7%, 95% CI: 82.1–94.3%).Conditional audits confirm 92.8–97.7% of automatic positives and 77.3–83.3% of compile-pass negatives, supporting a high-precision but conservative and imperfect per-case proxy.Source: §4.1 · p. 5
  • On the same Batch-B sample, the rule agrees with human majority on 87/97 cases versus 75/97 for LeanScorer; this supports this operating point, not universal superiority.The paired comparison reports exact McNemar p = 0.0118.Source: §4.1 · p. 5
  • The independent Sonnet judge agrees on 91.8% of resolved full-agent outputs and 88.3% across all eight tool configurations; threshold changes preserve the ordering Feedback > Search > Translation.The winning configuration can change with the judge, so the supported robustness claim concerns the gap and bottleneck ordering, not universal system ranking.Source: §4.1 · pp. 5–6
  • BEq certifies 219/350 pairs (62.6%) among selected accepted outputs, including 128 pairs with different normalized encodings; the other 131 remain unresolved, not disproved.Human review, Sonnet, and BEq provide complementary evidence for a reliable accepted core, but none is an equivalence oracle.Source: §4.1 · p. 6, Table 6 · p. 7

4.2 Q2: How Large Is the Compile–Faithfulness Gap?

  • Absolute faithful rates are 19.8–28.0% for general-purpose one-shot LLMs, 9.0–12.3% for specialized formalizers, and 4.0–5.0% for prover-oriented models, versus 60.5% for the full agent.The benchmark covers 400 graduate-level statements.Source: §4.2 · p. 6
  • Prover-oriented runs are a transfer diagnostic: proof-oriented Lean competence does not automatically transfer to prompt-following, statement-centric formalization when the target statement is not supplied.These runs often produce proof-oriented reasoning, tactic bodies, malformed declarations, or no extractable Lean statement.Source: §4.2 · p. 6
  • 89.5% of full-agent outputs compile, but only 60.5% satisfy the semantic criterion; human reviewers confirmed 95/114 audited rejected compile-pass cases as genuine mismatches.This validates at least 23.8 percentage points of the 29.0-point gap as mismatches.Source: §4.2 · p. 6
  • 3.0–29.0 percentage points: compilation exceeds semantic acceptance for every system on the same 400 statements, with the full GPT-5.2 agent showing the largest gap.The figure compares seven one-shot systems and the full agent; alternative full-agent orchestrators have gaps of 15.0 and 27.5 points.Source: §4.2 · p. 6, Figure 3 · p. 7

5 Bottleneck Decomposition

The factorial analysis separates validity, faithfulness, and tool cost across configurations that vary drafting, search, and elaboration feedback. Feedback drives the largest validity gains, but tool effects depend on context and can accompany semantic drift and nonmonotone repair trajectories.

5 Bottleneck Decomposition

  • The diagnostic separates whether an output compiles, preserves the intended statement, and incurs tool interaction cost; tools can move these boundaries differently.A higher compile rate can enlarge the compile-pass but semantically rejected bucket.Source: §5 · p. 7

5.1 Factorial Design over (T,F,S)

  • The 2^3 design evaluates all eight combinations of drafting (T), feedback (F), and search (S), with 111 as the full agent and 000 as the One-Shot Baseline.Every benchmark item is run under each configuration; the union row is an oracle diagnostic, not a deployed selector.Source: §5.1 · pp. 7–8, Table 7 · p. 8
  • Factorial main effects compare high and low levels of a factor, averaged over the other factors; Table 8 compares feedback conditions at fixed T and S.The analysis reports compile rate, consensus-faithful rate, and tool cost.Source: §5.2 · p. 8, §5.1 · p. 8, Table 8 · p. 8

5.2 Main Effects: Validity vs. Faithfulness

  • Feedback increases compiled outputs from 105 to 366 and faithful outputs from 79 to 245, while increasing the compile-pass semantic gap from 26 to 121.This is the (000) to (010) comparison.Source: §5.2 · p. 8
  • Search improves final faithfulness mainly without feedback, by 12.4 points at F=0 versus 1.2 points at F=1; with feedback, it mainly improves selectivity and efficiency.With feedback, REPL calls fall by 29.8% for (010) → (011) and 26.6% for (110) → (111).Source: §5.2 · p. 8
  • Feedback’s validity gains convert into faithful statements more often in Complex Analysis than in Algebra or Topology; the Topology pattern is consistent with encoding and coverage constraints.With feedback, the translation prior slightly lowers faithfulness by 2.0 points, while without feedback it raises it by 3.9 points.Source: §5.2 · p. 8, Table 10 · p. 9

5.3 Interactions and Per-Item Trajectory Churn

  • Feedback and search partially substitute in this setup: their interaction is −11.1 points (95% CI: −15.8 to −6.4), while feedback and translation interact at −5.9 points (95% CI: −10.0 to −1.6).The authors attribute the pattern to both tools exposing Mathlib-grounded information, through targeted symbol/type information or whole-statement elaboration diagnostics.Source: §5.3 · p. 9
  • Per-item transitions are strongly nonmonotone, so small net interaction effects can hide substantial trajectory churn and motivate per-instance routing or early stopping.Table 11 tracks new and lost faithful cases before and after adding a tool under fixed context.Source: §5.3 · p. 9

6 Limitations

The paper’s conclusions are limited to statement formalization and a defined benchmark and tool setup; its semantic criterion is a proxy rather than a formal equivalence test.

6 Limitations

  • The task is generating valid Lean 4 statement declarations, not proofs; provability is neither necessary nor sufficient for statement faithfulness.The strict LLM criterion is a scalable proxy, not a formal equivalence proof, and may reject some human-accepted outputs.Source: §6 · p. 9
  • The audits do not establish population-wide recall, and proprietary judges or overlap between the orchestrator and a judge may introduce dependence.Human review and Sonnet mitigate but do not eliminate this dependence; the single-sample LeanScorer comparison does not establish universal metric superiority.Source: §6 · p. 9
  • The benchmark covers 400 statements from four open mathematical sources and four graduate areas, not broader textbook coverage or research-level statements.Search tests implemented symbol lookup, namespace resolution, and general web search rather than dedicated semantic retrieval; the full REPL loop remains a real-time-use cost barrier.Source: §6 · p. 9

7 Conclusion

Compilation systematically overstates semantic success in this setting, while human-calibrated LLM judging provides a useful aggregate measure rather than ground truth. The factorial analysis shows that feedback is the largest validity intervention but does not eliminate semantic drift.

7 Conclusion

  • The observed compile–faithfulness gap spans 3.0–29.0 percentage points, and the strongest agent’s 89.5% compile rate falls to 60.5% under semantic evaluation.The authors conclude that compilation systematically overstates semantic success in this setting.Source: §7 · p. 10
  • The criterion reaches 89.7% human agreement on an independent audit, but remains a calibrated measurement instrument rather than ground truth.Human, third-judge, and formal checks support a reliable accepted core while exposing non-negligible false negatives.Source: §7 · p. 10
  • Lean feedback is the largest validity intervention, yet can move outputs into both faithful and compile-pass-but-wrong buckets.The authors recommend reporting validity and faithfulness separately and pairing verifier-driven repair with semantic auditing, routing, and stopping policies.Source: §7 · p. 10

B Agent Implementation Details

The agent implementation holds its translation objective and coding guidance fixed while selectively enabling tools, and its judging rubric assesses whether compiled declarations preserve the natural-language statement’s meaning.

B.1 Prompt Assembly

  • The prompt separates a fixed task definition and Lean usage guide from a capability block that varies with the factorial configuration.This modular structure is intended to isolate the effect of enabling or disabling external tools.Source: §B.1 · p. 11

B.2 Shared Base Prompt

  • The shared prompt requires one final Lean statement that compiles and is semantically faithful, while explicitly excluding proof generation.It also specifies Mathlib import and ends the declaration with := by sorry.Source: §B.2 · pp. 11–12

B.3 Tool-Availability Blocks

  • Each T, F, S configuration exposes tools by including or omitting their corresponding entries in the prompt’s available-tools block.The fully enabled (1, 1, 1) configuration is shown as the complete block; other configurations delete disabled tools.Source: §B.3 · p. 12

B.4 Tool Interfaces

  • The tool interfaces support drafting, file writing, compilation, Mathlib symbol inspection and resolution, and external search.The compiler returns diagnostics, while name-resolution tools check symbols or suggest likely identifiers.Source: §B.4 · p. 12

B.5 Example Execution Trace

  • The example trace shows the agent writing and compiling a statement, inspecting polynomial identifiers, patching the declaration, and compiling again.The trace includes checks of Polynomial.IsConstant, Polynomial.eval, Polynomial.isConstant, and Polynomial.natDegree.Source: §B.5 · p. 13

C LLM-as-a-Judge Prompt and Rubric

  • The judge compares the natural-language statement with the Lean declaration, ignores proof completeness, and accepts only compiling translations scoring at least 9.Its rubric treats missing key meaning as a mismatch and disallows vacuous placeholders used to make a theorem appear to match.Source: C LLM-as-a-Judge Prompt and Rubric · pp. 13–14

D Additional Metric Validation Results

The additional validation examines GPT–Gemini judge disagreements, including their domain distribution and the frequency of GPT-positive labels not accepted by Gemini.

D Additional Metric Validation Results

E Human-Check Validation Details

The audits support strict GPT∩Gemini consensus as a conservative, human-calibrated measure: it usually aligns with human majority, while many rejected compile-pass outputs are genuine mismatches. Case studies illustrate both semantic errors and faithful translations, including outputs that compilation alone cannot settle.

E Human-Check Validation Details

  • Audits kept Reviewer 1, Batch A, and Batch B identities separate, with rates computed within each blinded batch and case.The compile-aware human rubric treated compilation failures as unfaithful; majority labels required at least two numeric scores.Source: E Human-Check Validation Details · pp. 15–16
  • Strict consensus is a high-precision, conservative decision boundary, not a formal equivalence proof or recall guarantee.In the audited negative bucket, 24/136 cases were rescued by human majority.Source: E Human-Check Validation Details · p. 15
  • Reviewer judgments varied: Reviewer 2 more often rescued Batch-A negatives, while Reviewer 4 aligned more strictly with the LLM boundary.The reported three-reviewer estimate uses majority labels rather than relying on one unusually permissive reviewer.Source: E Human-Check Validation Details · p. 16
  • 95/114 compile-passing, consensus-negative cases were confirmed unfaithful by human majority; 19/114 were rescued as faithful.The audit therefore supports the compile-pass semantic gap while showing strict consensus is conservative.Source: Table 16 · p. 17, E Human-Check Validation Details · p. 17
  • 87/97 cases (89.7%) had matching automatic and human-majority labels in Batch B, with five disagreements in each direction.The headline agreement is based on same-case labels from the separate full-evaluation audit.Source: Table 17 · p. 17, E Human-Check Validation Details · p. 17
  • 19/114 Batch-A negatives and 5/22 Batch-B compile-pass negatives were rescued, so strict consensus is not complete.The Batch-B negative-bucket interval is wider because only 22 cases had majority coverage.Source: E Human-Check Validation Details · p. 18

E.1 Compact Human-Check Case Studies

  • Case studies include a loop-obstruction condition reviewers found vacuous and an intended product-group isomorphism that failed compilation.Conversely, reviewers accepted direct formulations of the complex-sine bound and convexity inequality.Source: §E.1 · pp. 19–21

E.2 Four-Reviewer Theorem-Name Overlap Diagnostic

The four-reviewer comparison is a theorem-name diagnostic, not a repeated-measures estimate, because none of its overlapping cases reused the exact Lean code. Supplementary tables separately describe tool configurations, usage counts, and trajectory-length groupings.

E.2 Four-Reviewer Theorem-Name Overlap Diagnostic

  • 0/32 theorem-name overlaps had exact Lean-code overlap, so these rows cannot replace the within-batch same-case estimates.The overlap comparison is diagnostic of reviewer strictness and theorem-level consistency, not four reviews of the same declaration.Source: §E.2 · p. 22, Table 21 · p. 22
  • 29/32 theorem-name overlaps had a four-reviewer majority faithful label, and 25/32 were unanimous faithful.These are theorem-name occurrences, not identical generated Lean outputs.Source: §E.2 · p. 22, Table 21 · p. 22

F Additional Factorial and Tool-Usage Details

  • The supplementary tables cover validity and semantic selectivity by configuration, tool-use counts, and faithfulness by trajectory length.Tool-call totals use N = 384 complete logs, while accuracy results use N = 400.Source: Table 22 · p. 23, Table 23 · p. 23, Table 24 · p. 23

G.1 Domain Metrics under Full Configuration

The appendix breaks results down by domain and tool configuration, including feedback and search effects, and tests whether tool-augmented gains extend beyond GPT-5.2. All three orchestrators converge to similar consensus-faithful rates despite different one-shot baselines.

G.1 Domain Metrics under Full Configuration

  • Under configuration 111, Table 25 reports domain metrics with conditional faithfulness defined as Faithful/Compile.The supplied passages provide the table scope but not its domain-specific values.Source: Table 25 · p. 23

G.2 Judge Scores by Domain

  • Complex Analysis has the highest scores under tool-enabled settings, while Real Analysis remains lowest.Table 26 gives average faithfulness scores by domain and tool configuration.Source: Table 26 · p. 24, §G.2 · p. 24

G.3 Domain-Level Feedback Effects

  • Compiler feedback raises Complex Analysis faithfulness by 53 points, compared with 20-point gains in Algebra and Topology.Figure 5 and Table 27 present domain-level feedback effects.Source: Figure 5 · p. 24, Table 27 · p. 24, §G.3 · p. 24

G.4 Domain-Level Effects of Search (S)

  • Search adds 10.8 points on average without full REPL feedback but only 1.0 point when it is enabled.The authors attribute the reduced marginal effect to overlap between whole-program diagnostics and symbol-level information in this implementation.Source: Table 28 · p. 25, §G.4 · p. 25

G.5 Multi-Model Orchestrator Comparison

  • Under config 111 on N = 400, all three models gained 148–163 faithful translations with tool augmentation and reached 60–65% consensus-faithful outputs, versus one-shot baselines of 19–28%.Consensus-faithful means strict GPT∩Gemini consensus.Source: §G.5 · p. 25, Table 29 · p. 25

Related papers

Loading 2606.31002v2…