Structure-Aware Equivalence for Evaluating Autoformalized Statements
Yi Yu, Yu-Hsuan Wu, Guang Lin, Yuhui Zhang, Yuxiang Peng
cs.PL
Oct 18, 2026 · v3
TL;DR
ACE normalizes and aligns Lean statement pairs, generates Lean proof obligations, and certifies equivalence or inequivalence only when Lean checks the proofs.
Abstract
Evaluating autoformalized mathematical statements requires determining whether a candidate preserves the mathematical claim intended by a trusted reference. Existing methods approach this problem from complementary directions: reference-free learned evaluators estimate semantic agreement but are not constrained to a formal equivalence relation, while reference-based proof methods typically employ whole-statement logical equivalence to provide formal certificates, which is too coarse for translation fidelity and may identify mathematically unrelated statements. We introduce Structure-Aware Equivalence (SAE), a role-preserving formal equivalence relation between syntactic and whole-statement logical equivalence that allows formally justified reformulations while preserving translation-relevant mathematical structure. We operationalize SAE in the Autoformalization Correctness Evaluator (ACE), which provides certified equivalence or inequivalence judgments and reports Inconclusive otherwise. On ProofNetVerif, a benchmark introduced with BEq+, ACE retains substantial equivalent-case coverage while remaining highly conservative in certifying disputed or inequivalent pairs. On targeted diagnostics, BEq+ accepts 94-96% of unrelated but whole-statement logically equivalent pairs, while Mathesis LeanScorer accepts 42% of localized meaning-changing perturbations; ACE accepts none of either set as equivalent.
Problem
Evaluating whether an autoformalized Lean statement preserves the claim of a trusted reference is hard. Learned evaluators are not tied to a formal relation. Whole-statement logical equivalence, as used by BEq+, is too coarse and can accept mathematically unrelated statements.
Approach
Structure-Aware Equivalence (SAE) is a role-preserving equivalence relation that sits between syntactic and whole-statement logical equivalence. It normalizes statements to a prenex-style form and preserves binder correspondence, the premise–conclusion boundary, and relational structure. The Autoformalization Correctness Evaluator (ACE) elaborates and aligns statement pairs and encodes the resulting obligations as synthetic Lean theorems. Proof-search backends (Aesop, Aristotle, an LLM) then attempt them, yielding Certified Equivalent, Certified Inequivalent, or Inconclusive.
Results
On ProofNetVerif, ACE certifies about 56-59% of consensus-equivalent pairs and almost no disputed or inequivalent pairs as equivalent. On targeted diagnostics, BEq+ accepts 94-96% of unrelated but logically equivalent pairs and LeanScorer accepts 42% of meaning-changing perturbations, while ACE accepts none of either set.
| Evaluator | Config | Consensus-Equiv Eq | Disagreement-Equiv Eq | Inequivalent Eq |
|---|
| ACE | Aesop | 56.5% | 0.3% | 0.1% |
| ACE | GPT-5.6 Luna | 58.6% | 0.3% | 0.2% |
| BEq+ | Default | 60.7% | 2.4% | 0.1% |
| LeanScorer | GPT-5.6 Luna | 81.4% | 43.8% | 5.1% |
Equivalence-acceptance rate (Eq) by ProofNetVerif subset (selected configurations)
