PaperlayerView exact revision on arXiv

Source-linked AI summary

SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalization

Hojae Han, Jongyoon Kim, Sanghyuk Park, Dongwook Cheon, Myungjae Jeon, Sunjong Choi, Soonho Kong, Wonseok Heo, Seung-won Hwang, Donghoon Hyeon

arXiv:2608.29270v1cs.CLcs.AI

TL;DR

Autoformalization lacks a scalable evaluator that reliably distinguishes semantically aligned formal statements from merely compilable or formulation-mismatched outputs. The paper introduces SA-PASS, which checks generated statements against complete shadow-theorem sets, and evaluates it in SHADOWBENCH. SA-PASS reaches 98.8% binary agreement with expert judgments, while Claude Code with Numina-Lean-Agent obtains 11.2% SA-PASS despite a 61.8% compile rate.

  • Problem

    Existing automatic metrics can accept type-correct but misaligned statements or reject correct alternative formulations, while expert judgment is too costly to scale.

  • Method

    SA-PASS evaluates a generated formal statement using complete shadow theorems, requiring compilation, forward implication to every shadow, and backward implication from their conjunction.

  • Results

    98.8% binary agreement with expert judgments across six agentic configurations, while Claude Code (Opus 4.8) with Numina-Lean-Agent achieves 61.8% compile rate and 11.2% SA-PASS on SHADOWBENCH.

  • Takeaways & Limitations

    SHADOWBENCH provides a Lean 4 benchmark of 178 postgraduate- to research-level problems across eight mathematical areas with automatic semantic-alignment evaluation.

  • Takeaways & Limitations

    SHADOWBENCH requires one-time construction of shadow statements and checker proofs for each benchmark problem.

Abstract

from arXiv · show

Autoformalization translates informal mathematical theorems into code for proof assistants such as Lean. A central challenge is that current evaluation metrics can accept type-correct but misaligned statements or reject correct statements written in a different formulation. Inspired by Pass@$k$, we propose SA-Pass (*Semantic Alignment Pass*), which tests formal statements using auxiliary statements called *shadows* that characterize the intended statement. A generated statement receives full credit only when it compiles, implies each shadow (forward check), and is implied by their conjunction (backward check). We instantiate SA-Pass in ShadowBench, a Lean 4 full autoformalization benchmark of 178 postgraduate- to research-level problems spanning eight mathematical areas. Claude Code (Opus 4.8) with Numina-Lean-Agent reaches $61.8\%$ compile rate and $11.2\%$ SA-Pass. Across outputs generated by six agentic configurations, SA-Pass achieves $98.8\%$ binary agreement with expert judgments. An early version of ShadowBench served as the benchmark for Track 4 of the ICML 2026 AI4Math Challenge.

1 Introduction

Autoformalization evaluation must distinguish compilable formalizations from statements that preserve the intended mathematics. The paper proposes SA-PASS and introduces SHADOWBENCH to automate this distinction at research-level scale.

  • Motivation: Existing metrics can accept type-correct but misaligned statements, reject correct alternative formulations, or require costly manual review.Compile-based, reference-based, and manual approaches each leave a semantic-alignment gap.
  • SA-PASS: SA-PASS gives maximum credit only when a generated statement compiles, implies every shadow, and is implied by their conjunction.Complete shadow sets are auxiliary theorems whose individual and joint implications characterize the intended theorem.
  • SA-PASS: SA-PASS reuses one expert-constructed, Lean-verified shadow set to evaluate any number of generated formalizations automatically.The shadow set is constructed once per intended theorem, while checker theorems are mechanically verified.
  • SHADOWBENCH: SHADOWBENCH contains 178 postgraduate- to research-level problems across eight mathematical areas and three difficulty levels.The benchmark targets multi-conclusion problems and provides complete shadow theorems for automatic evaluation.
  • Results: 61.8% compile rate contrasted with 11.2% SA-PASS for Claude Code (Opus 4.8) with Numina-Lean-Agent on SHADOWBENCH.Across six agentic configurations, SA-PASS achieved 98.8% binary agreement with expert judgments.

2 Related Work

Prior autoformalization metrics rely on compilation, reference similarity, successor tests, or expert judgments, each with limitations for scalable semantic-alignment evaluation. SA-PASS instead uses complete auxiliary-theorem checks and closely agrees with expert judgments.

  • Compile rate: Compile rate accepts type-checking formalizations but can produce false positives when the formal statement differs from the informal theorem.It counts generated theorem statements and proofs that type-check in Lean as correct.
  • Reference-based metrics: Reference-based metrics compare lexical or structural similarity, or use models to score generated statements against references or informal statements.These approaches include BLEU, TransTED, FormalAlign, and LLM-as-judge.
  • Expert judgments: Manual judgment by mathematicians familiar with Lean remains reliable but does not scale to large or repeated evaluations.This motivates automated semantic-alignment checks that can be reused across outputs.
  • Test-based metrics: Testing Accuracy can accept a generated theorem when successor tests compile, although passing those tests does not guarantee semantic alignment.The limitation is a potential false positive relative to the intended informal statement.
  • Our distinction: SA-PASS evaluates generated statements with complete forward and backward auxiliary-theorem checks and reaches 98.8% binary agreement with expert judgments.Its design addresses both false positives and false negatives in semantic alignment.

3 SA-PASS: Semantic Alignment Pass

SA-PASS formalizes semantic alignment through complete shadow sets: each shadow follows from the intended theorem, while their conjunction implies it. Generated statements must pass Lean compilation and both implication directions.

  • Task and shadow theorems: Full autoformalization generates a formal theorem statement and a machine-checkable proof from an informal theorem statement and proof.The intended semantic-alignment objective is equivalence between the generated and intended formal statements.
  • Task and shadow theorems: A shadow theorem is an auxiliary formal statement with a machine-checkable proof, and its forward checker establishes that the intended theorem implies it.The shadows provide decomposed conditions for checking a generated statement.
  • Complete shadow sets: A shadow set is complete when every shadow follows from T and the conjunction of all shadows implies T.Lean verifies completeness by compiling forward checkers for each shadow and one backward checker for their conjunction.
  • Complete shadow sets: For bundled conclusions, individual shadows can represent each component because the components can be assembled back into the bundled conclusion.For predicates A and B_i, the example uses shadows S_i: A ⇒ B_i.
  • SA-PASS scoring: SA-PASS evaluates a generated theorem by appending forward and backward checkers to its Lean code and compiling the resulting file.The forward checks establish the generated statement implies the shadows, while the backward check rejects extra constraints and completes equivalence.
  • SA-PASS scoring: SA-PASSsoft assigns partial credit by averaging the fraction of successful forward checks and the backward-check indicator.It equals 1 exactly when SA-PASS equals 1, while non-type-checking generated theorems receive 0.

4 SHADOWBENCH

SHADOWBENCH is a Lean 4 full-autoformalization benchmark designed for semantic-alignment evaluation, with broad mathematical coverage and hidden, compiler-verified checker infrastructure. Its targets are challenging for current systems.

  • Each problem is equipped with shadow and checker theorems for automatic SA-PASS evaluation, while the resulting benchmark keeps these checkers hidden.
  • Checker construction combines LLM-generated candidate shadows, Lean completeness verification, and expert-guided revision when initial drafts are incomplete.
  • SHADOWBENCH contains 178 postgraduate- to research-level problems across eight mathematical areas and three difficulty levels.
  • Claude Code (Opus 4.8) with Numina-Lean-Agent achieves a 61.8% compile rate but only 18.3% SA-PASSsoft and 11.2% SA-PASS.

5 Experiment

The experiments evaluate multiple model and agent configurations using compile rate, SA-PASS variants, and agreement-oriented metrics. Results show that compilation substantially overestimates semantic alignment, while performance remains low on the benchmark.

  • The evaluation reports compile rate, SA-PASSsoft, and SA-PASS across methods and difficulty levels, alongside BLEU, BEq+, and LLM-as-judge analyses.
  • 61.8% compile rate is achieved by Claude Code (Opus 4.8) with Numina-Lean-Agent, compared with 18.3% SA-PASSsoft and 11.2% SA-PASS.
  • 41.6 points is the compile-rate gain from adding Numina-Lean-Agent to Claude Code (Opus 4.8), versus 13.2 points for SA-PASSsoft and 8.4 points for SA-PASS.
  • 0.0% SA-PASS is reported for closed-source LLMs, open-source LLMs, and Lean-specialized methods, while the strongest agentic result is 11.2%.
  • SHADOWBENCH reports per-difficulty pass rates separately for compilation, SA-PASSsoft, and the stricter SA-PASS criterion.

6 Analysis

The analysis tests whether metric gaps reflect false positives or false negatives by comparing automatic decisions with expert judgments and by examining transfer to ProofNet. SA-PASS aligns closely with expert labels, while benchmark complexity affects the compile-to-alignment gap.

  • The expert study compares six agentic configurations using precision, recall, F1, and agreement for several automatic metrics.
  • SA-PASS achieves 0.964 F1 and 0.988 agreement, whereas compile rate has 1.000 recall but only 0.178 precision because of false positives.
  • The results indicate that the compile-rate versus SA-PASS gap primarily reflects false positives from compilation rather than false negatives from SA-PASS.
  • On ProofNet, SA-PASS and SA-PASSsoft match every expert judgment for Llama 3.1 8B outputs, while compile rate reaches an F1 of 0.889.
  • Across 16 ProofNet models, compile rate and SA-PASS differ by 2.1 points on average and at most 7.8 points, unlike the larger SHADOWBENCH gap.
  • Forward checks test required consequences, while backward checks test whether the intended theorem implies the generated statement; the two directions can diverge substantially.

7 Conclusion

The paper introduces SA-PASS as an automated semantic-alignment metric and instantiates it in SHADOWBENCH, a challenging Lean 4 benchmark. The strongest reported system compiles many outputs but achieves far fewer full semantic passes, while SA-PASS closely agrees with experts.

  • SA-PASS evaluates generated formal statements with shadows whose conjunction is equivalent to the intended theorem, using forward and backward implication checks.
  • SHADOWBENCH contains 178 postgraduate- to research-level problems spanning eight mathematical areas.
  • 61.8% compile rate and 11.2% SA-PASS are achieved by Claude Code (Opus 4.8) with Numina-Lean-Agent on SHADOWBENCH.
  • 98.8% binary agreement with expert judgments is achieved by SA-PASS across six agentic configurations.

Limitations

SHADOWBENCH spans 178 postgraduate- to research-level problems across eight mathematical areas, while SA-PASS requires one-time construction of shadow statements and checker proofs for each problem.

  • 178 postgraduate- to research-level problems across eight mathematical areas are covered by SHADOWBENCH.
  • SA-PASS requires one-time construction of shadow statements and checker proofs for each benchmark problem.

Potential Risks

The principal identified risk is benchmark leakage: exposing checker artifacts could let systems optimize for checks instead of the informal theorem.

  • Exposed checker artifacts could enable systems to optimize for evaluation checks rather than the informal theorem.The benchmark separates public problem inputs from evaluation checking artifacts to reduce this risk.

A.2 Dataset Statistics

SHADOWBENCH uses longer, more complex reference formalizations than ProofNet and evaluates diverse model configurations, datasets, metrics, and experimental costs across its benchmark.

  • Dataset Statistics: 1.6× longer target statements distinguish SHADOWBENCH from ProofNet by average line count.
  • Dataset Statistics: SHADOWBENCH reference proofs average 72 lines and 4.5 auxiliary declarations, compared with about 3.4 lines and no auxiliary declarations in ProofNet.
  • Experimental Configurations: 19 non-agentic model configurations across nine model families are evaluated, alongside four agentic settings run with and without Numina-Lean-Agent.
  • Compute and Cost: Approximately $3,970 in API spend covers the main-body experiments, excluding self-hosted local GPU runs.

D Per-Configuration Agreement with Expert Judgment

SA-PASS closely tracks expert judgments across configurations and thresholds, while its system ranking matches experts exactly; remaining false negatives arise from checker adaptation failures.

  • False Negatives: Three expert-aligned outputs are missed because auxiliary declarations use names or declaration forms differing from the reference.The checker adaptation step fails to resolve these mismatches, causing every forward check for those problems to fail.
  • Threshold Sensitivity: At threshold t = 0.5, SA-PASSsoft F1 reaches 0.941 for Claude Code with Numina-Lean-Agent and 0.973 for Codex with Numina-Lean-Agent.Below t = 0.5, F1 is 0.552 and 0.623 respectively; above one-half, SA-PASSsoft coincides with SA-PASS.
  • Threshold Sensitivity: BLEU F1 peaks at 0.436 with cutoff 0.05 for Claude Code with Numina-Lean-Agent and 0.427 with cutoff 0.1 for Codex with Numina-Lean-Agent.No BLEU cutoff brings agreement near the level reached by SA-PASS.

G Public Challenge Track

The public challenge track evaluated submissions on a 126-problem snapshot of SHADOWBENCH, with SA-PASSsoft exposing substantial differences from compilation-based rankings and favoring decomposed, agentic solutions.

  • Challenge setup: The early 126-problem version of SHADOWBENCH was released as Track 4 of the ICML 2026 AI4Math Challenge.The public challenge exposed informal theorems and formalization rules, while checker theorems remained hidden; 117 teams registered and 27 participated.
  • Challenge results: 61.6% average compile rate contrasted with 11.1% average SA-PASSsoft, producing an approximately 5.5× gap across participants.The median SA-PASSsoft was 8.1%, and the gap highlighted false positives from compilation-based evaluation.
  • Challenge results: Trivial statements can compile while failing hidden shadows, and the top five teams by compile rate shared no member with the top five by SA-PASSsoft.These submissions can therefore alter rankings, not merely inflate an individual metric.
  • Challenge results: Compile-rate rankings agreed with SA-PASSsoft at only ρ = 0.41, while BEq+ passed 12.4% on the participant submissions.The participant results matched the benchmark’s broader metric-validity gap against expert judgment.
  • Submission strategies: The verified score correlated with declaration count at ρ = 0.59 and turn count at ρ = 0.56, while the strongest submission used an agentic pipeline with auxiliary lemmas.The reported pattern connects higher verified scores with decomposition and multi-turn agentic behavior.
  • Shadow-check behavior: Case studies show SA-PASS rejecting compiling weakenings that replace complex-valued or area statements with materially different real-valued or assumed-hypothesis formulations.The checks detect failures in forward implication, backward implication, or both, despite correct compilation.

J.6 Backup Declarations on ProofNet

The ProofNet case study shows that selecting the final theorem block can reject an otherwise matching declaration when a later backup declaration ends in `sorry`.

  • Backup declaration: Claude Opus 4.6 produced a matching ProofNet theorem followed by a second backup declaration ending in `sorry`.The example concerns finding a nonidentity self-inverse element in a finite group of even order.
  • Evaluation consequence: The evaluator takes the last theorem block as the candidate, so the backup declaration causes rejection despite the earlier matching statement.Claude Haiku 4.5 passes on the same problem with a single declaration.
  • Related checker patterns: ShadowBench’s shadow framework also supports bundled conclusions by projecting a public theorem into specialized hidden checks.Examples include product statements, homology conclusions, and componentwise checks for bundled results.
  • Equality checks: For equality-valued theorems, hidden checkers can compile both inequality consequences using idiomatic lemmas from the relevant ordered structure.The exact lemmas depend on the proof assistant and ordered structure.
  • Saddle-point derivatives: A complete shadow set for a paired conclusion checks each derivative condition separately and verifies that their conjunction recovers Dx = 0 ∧ Dz = 0.The example uses shadows for the x- and z-section derivatives and a completeness certificate combining them.
Loading 2608.29270v1…