Summary of SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalization

Summary (Overview)

• Novel evaluation metric (SA-PASS): The paper introduces Semantic Alignment Pass (SA-PASS), an automatic metric that evaluates whether a generated formal statement is semantically equivalent to the intended informal theorem using both forward and backward implication checks against a set of "shadow theorems."
• New benchmark (SHADOWBENCH): A Lean 4 full-autoformalization benchmark containing 178 postgraduate- to research-level problems across eight mathematical areas, each annotated with complete shadow theorem sets.
• Key finding: Current systems achieve high compile rates but low semantic alignment—Claude Code (Opus 4.8) with Numina-Lean-Agent reaches 61.8% compile rate but only 11.2% SA-PASS, revealing that compilation substantially overestimates semantic alignment.
• High reliability: SA-PASS achieves 98.8% binary agreement with expert judgments across six agentic configurations, compared to 17.8% for compile rate and 80.6% for BEq+.
• Transferability: SA-PASS transfers to existing benchmarks like ProofNet, where it achieves perfect agreement with expert judgments.

Introduction and Theoretical Foundation

Background and Motivation

Autoformalization translates informal mathematical theorems written in natural language into code for proof assistants such as Lean. In the full autoformalization setting, the input is an informal theorem statement and proof, and the output is code containing the corresponding formal statement and proof.

The core challenge is assessing whether the generated formal statement expresses the same mathematics as the informal statement. Existing evaluation approaches have significant limitations:

• Compile rate can produce false positives by accepting type-correct but semantically misaligned statements
• Reference-based metrics (BLEU, BEq+) can produce false negatives by rejecting correct statements formulated differently
• Expert judgment is reliable but too costly to scale for repeated evaluations

Theoretical Foundation

The paper formalizes the task as follows:

Definition 1 (Full autoformalization task): Given an informal theorem statement and its proof, generate a formal statement $\widehat{T}$ together with a machine-checkable proof of $\widehat{T}$. Let $T$ denote the intended formal statement. The semantic alignment objective is:

$$\widehat{T} \Longleftrightarrow T$$

Definition 2 (Shadow theorem): For an intended formal statement $T$, a shadow theorem consists of an auxiliary formal statement $S$ and a machine-checkable proof of $S$. Its forward checker theorem states that $T$ implies $S$:

$$T \Rightarrow S$$

Definition 3 (Complete shadow set): Let $T$ be the intended formal statement, and let $\mathcal{S} = \{S_1, \ldots, S_n\}$ be a finite set of shadow statements. The set $\mathcal{S}$ is complete if the shadows jointly characterize $T$, i.e., the backward checker theorem states:

$$S_1 \wedge \dots \wedge S_n \Rightarrow T$$

Together with the forward checker theorems $T \Rightarrow S_i$, this gives:

$$S_1 \wedge \dots \wedge S_n \Leftrightarrow T$$

The key insight is that a complete shadow set characterizes the intended theorem exactly—the shadows are individually implied by $T$ and jointly imply $T$ (Figure 2 in the paper).

Methodology

SA-PASS Scoring

Definition 4 (Passing condition): For a problem whose intended formal statement is $T$, a generated formal theorem with statement $\widehat{T}$ passes if and only if its declaration and proof type-check in Lean and it passes the forward checks:

$$\widehat{T} \Rightarrow S_1, \quad \widehat{T} \Rightarrow S_2, \quad \ldots, \quad \widehat{T} \Rightarrow S_n$$

and the backward check:

$$S_1 \wedge \dots \wedge S_n \Rightarrow \widehat{T}$$

Definition 5 (SA-PASS): For a generated formal theorem with statement $\widehat{T}$ and a complete shadow set $\mathcal{S} = \{S_1, \ldots, S_n\}$:

$$\operatorname{SA-Pass}(\widehat{T}, \mathcal{S}) = \begin{cases} 1, & \text{if } \widehat{T} \text{ compiles}, \widehat{T} \Rightarrow S_i \text{ for all } i, \text{ and } \bigwedge_{i=1}^{n} S_i \Rightarrow \widehat{T}; \\ 0, & \text{otherwise}. \end{cases}$$

Definition 6 (SA-PASS$_{\text{soft}}$): A graded variant that assigns partial credit:

$$\text{SA-PASS}_{\text{soft}}(\widehat{T}, \mathcal{S}) := \frac{1}{2} \cdot \underbrace{\frac{|\{i : \widehat{T} \Rightarrow S_i\}|}{|\mathcal{S}|}}_{\text{forward checks}} + \frac{1}{2} \cdot \underbrace{\mathbf{1}\{\bigwedge_{i=1}^{n} S_i \Rightarrow \widehat{T}\}}_{\text{backward check}}$$

Benchmark Construction

The SHADOWBENCH construction process involves:

1. Informal theorem collection: Sourced from textbooks, lecture notes, and research repositories
2. Reference formalization: LLM-assisted drafting with expert revision until Lean type-checks
3. Checker theorem construction: Qwen3-235B proposes candidate shadow sets; Lean verifies completeness; experts review and guide revisions (initial drafts complete for 85% of problems)
4. Checker diversification: Rules and LLM-based adapters handle binder style, field notation, and declaration name variations

Table 1: SHADOWBENCH problem distribution

Table 2: Checker theorem statistics

Empirical Validation / Results

Main Results on SHADOWBENCH

Table 3 (key results): Per-difficulty pass rates (%) on SHADOWBENCH

Key findings:

• Compilation overestimates semantic alignment: The gap between compile rate (61.8%) and SA-PASS (11.2%) is 50.6 points for the best system
• Numina-Lean-Agent helps compilation more than alignment: Gains of 41.6 points in compile rate but only 8.4 points in SA-PASS for Claude Code (Opus 4.8)
• Semantic alignment remains largely unsolved: All non-agentic methods score 0.0% on SA-PASS

Agreement with Expert Judgment

Table 4: Binary agreement of automatic metrics with expert judgment

SA-PASS achieves perfect precision and near-perfect recall, with 98.8% agreement with expert judgments. Compile rate has perfect recall but extremely low precision (0.178), confirming that most compile-passed outputs are semantically misaligned.

Results on ProofNet

SA-PASS transfers to the existing ProofNet benchmark. Across 16 non-agentic models:

• Compile rate and SA-PASS differ by only 2.1 points on average (max 7.8 points)
• SA-PASS achieves perfect agreement with expert judgments on ProofNet outputs (Table 6)

This smaller gap is attributed to ProofNet's shorter, less compositional targets (single conclusions, no auxiliary declarations) compared to SHADOWBENCH's longer formalizations (~1.6× longer by line count, 4.5 auxiliary declarations per problem on average).

Forward vs. Backward Checker Analysis

Table 7 (key results): Checker metrics for agentic systems

The two implication directions detect different forms of semantic mismatch:

• Failing forward checks: omitted conclusions or added assumptions
• Failing backward checks: added conclusions or omitted assumptions

Theoretical and Practical Implications

Theoretical Contributions

1. Formalization of semantic alignment: The paper provides a rigorous, machine-checkable definition of semantic alignment via complete shadow sets, reducing the problem to provable implication checks in Lean.

2. Reusable expert supervision: Shadow sets are constructed once per intended theorem (not per generated formalization), making expert knowledge reusable across unlimited evaluations.

3. Addresses both false positives and false negatives: Unlike compile rate (false positives) or reference-based metrics (false negatives), SA-PASS provides a balanced evaluation through bidirectional implication checks.

Practical Implications

1. Benchmark design: SHADOWBENCH's separation of public problem inputs from hidden checking artifacts prevents benchmark gaming and enables fair repeated evaluation.

2. System development guidance: The large gap between compile rate and SA-PASS indicates that current systems optimize for type-correctness rather than semantic alignment, suggesting a need for new training objectives and evaluation protocols.

3. Scalable evaluation: SA-PASS enables automatic evaluation at scale, replacing costly expert judgments for routine evaluation while maintaining reliability.

Conclusion

Main Takeaways

• SA-PASS provides a reliable, automatic metric for evaluating semantic alignment in autoformalization through Lean-checkable forward and backward implication checks against complete shadow theorem sets
• SHADOWBENCH reveals that current state-of-the-art systems achieve high compile rates (61.8%) but low semantic alignment (11.2% SA-PASS)
• SA-PASS achieves 98.8% agreement with expert judgments, substantially outperforming existing metrics

Future Directions

• Extending SHADOWBENCH coverage to more mathematical domains and proof styles
• Improving systems to optimize for semantic alignment rather than mere compilation
• Developing methods to further automate shadow set construction

Limitations

• SHADOWBENCH covers 178 problems across eight areas; broader coverage is needed
• SA-PASS requires one-time construction of shadow statements and checker proofs for each problem

Potential Risks

• Benchmark leakage: If checker artifacts are exposed, systems could optimize for the checks rather than the informal theorem. Mitigated by separating public problem inputs from hidden checking artifacts.