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

Abstract: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.

Revised version: adds expanded human calibration, a same-sample comparison with LeanScorer, independent-judge and threshold-sensitivity analyses, and a BEq formal cross-check; reframes the main contribution around semantic-faithfulness evaluation. 5 figures

Artificial Intelligence (cs.AI); Computation and Language (cs.CL); Logic in Computer Science (cs.LO)

arXiv:2606.31002 [cs.AI]

(or arXiv:2606.31002v2 [cs.AI] for this version)