Summary (Overview)

• This paper introduces Structure-Aware Equivalence (SAE), a novel formal equivalence relation for evaluating autoformalized mathematical statements that sits between syntactic equivalence and whole-statement logical equivalence.
• The authors present ACE (Autoformalization Correctness Evaluator), a Lean-backed verification framework that operationalizes SAE, providing certified equivalence/inequivalence judgments with an explicit "Inconclusive" outcome.
• SAE preserves translation-relevant mathematical structure—binder correspondence, premise-conclusion roles, and relational content—while allowing formally justified reformulations within those roles.
• On the ProofNetVerif benchmark, ACE achieves 56.5–58.6% coverage on consensus-equivalent pairs while remaining highly conservative on inequivalent pairs (0.1–0.2% false positives).
• Targeted diagnostics reveal complementary failure modes of existing approaches: BEq+ accepts 94–96% of unrelated but logically equivalent pairs, and LeanScorer accepts 42% of localized meaning-changing perturbations; ACE accepts none of either.

Introduction and Theoretical Foundation

Background and Motivation

Large language models (LLMs) can translate informal mathematical statements into formal languages like Lean, but measuring semantic correctness of generated formal statements remains a bottleneck. A statement may compile while altering assumptions, domains, or conclusions; conversely, correct formalizations need not reproduce reference statements syntactically.

Two Evaluation Settings

1. Reference-free evaluation: informal statement + candidate formalization, no trusted formal counterpart
2. Reference-based evaluation: trusted formalization available, candidate evaluated against it

The Core Problem

Existing methods have complementary weaknesses:

• Reference-free learned evaluators (e.g., FormalAlign, Mathesis LeanScorer) estimate semantic agreement but aren't constrained to a formal equivalence relation
• Reference-based proof methods (e.g., BEq, BEq+) use whole-statement logical equivalence, which is too coarse

The paper illustrates this with an extreme example:

$$(1 : \mathbb{N}) + 1 = 2 \leftrightarrow \text{Fermat's Last Theorem}$$

Both propositions are formally provable, and so is their biconditional—yet they clearly don't express the same mathematical statement. The issue is that logical equivalence is too coarse to serve as translation equivalence.

Key Insight

The choice of what relation defines correctness must be separated from the ability of a prover to certify that relation.

Methodology

Normalized Statement Form

Following prenex normal form, statements are normalized as:

$$N(T) = Q_1(x_1 : A_1) \cdots Q_n(x_n : A_n) . H_1 \to \cdots \to H_m \to C_T$$

where $Q_i \in \{\forall, \exists\}$, $\Delta_T$ is the ordered quantifier prefix, $\Gamma_T = (H_1, \ldots, H_m)$ are top-level premises, and $C_T$ is the residual conclusion.

Admissible Variable Alignment

An admissible alignment $\pi$ is a bijection between extracted object variables satisfying four conditions:

1. Binder correspondence: every variable has exactly one counterpart
2. Type preservation: aligned binder types must elaborate in shared context
3. Dependency preservation: each binder follows all binders on which its type depends
4. Quantifier preservation: aligned binders have same quantifier kind; reordering restricted to independent binders within contiguous blocks

Premise-Conclusion Equivalence (Definition 2.1)

Two premise-bearing statements satisfy $T \equiv_B T'$ if there exists $\pi \in \text{Adm}(T, T')$ such that:

$$\Delta_\pi \vdash \left(\bigwedge \Gamma^\pi_T\right) \leftrightarrow \left(\bigwedge \Gamma^\pi_{T'}\right) \quad \text{and} \quad \Delta_\pi \vdash C^\pi_T \leftrightarrow C^\pi_{T'}$$

Premise-Free Equivalence (Definition 2.2)

For premise-free statements, conclusion trees must match recursively with the same connectives, and relational leaves must satisfy either:

• Direct orientation: $\rho = \rho'$, and $\Delta_\pi \vdash E_1 = E'_1$, $\Delta_\pi \vdash E_2 = E'_2$
• Reversed orientation: $\rho' = \text{dual}(\rho)$, and $\Delta_\pi \vdash E_1 = E'_2$, $\Delta_\pi \vdash E_2 = E'_1$

Structure-Aware Equivalence (Definition 2.3)

$$T \equiv_{SA} T' \iff \text{both premise-bearing and } T \equiv_B T', \text{ or both premise-free and } T \equiv_F T'$$

Equivalence Hierarchy

$$T \equiv_S T' \implies T \equiv_{SA} T' \implies T \equiv_L T'$$

ACE Verification Framework

ACE operates in two stages:

1. Normalization and alignment: elaborate theorem types, normalize quantifier structure, enumerate admissible binder alignments
2. Proof search and verification: construct Lean proof obligations, batch positive obligations as disjunction, apply proof-search backends (Aesop, Aristotle, GPT-5.6 Luna)

The comparison proposition is:

$$E(T, T') := \bigvee_{\pi \in \text{Adm}(T,T')} E_\pi$$

with outcomes: Certified SAE-Equivalent, Certified SAE-Inequivalent, or Inconclusive.

Empirical Validation / Results

Datasets

1. ProofNetVerif: 787 Consensus-Equivalent pairs, 340 Disagreement-Equivalent pairs, 2,236 Inequivalent pairs
2. Unrelated Shared-Provability Set: 50 pairs where $T_r \leftrightarrow T_c$ is provable but statements are mathematically unrelated
3. Semantic Perturbation Set: 50 pairs with localized meaning-changing perturbations

Table 1: Decision Distributions on ProofNetVerif

Key Results

RQ1 (General benchmark behavior): ACE reports Eq for 56.5–58.6% of consensus-equivalent pairs, Noneq for 0.3% of disagreement-equivalent pairs, and only 0.1–0.2% false positives on inequivalent pairs.

RQ2 (Role preservation): On the Unrelated Shared-Provability Set, ACE achieves 100% true-negative rate across all backends. BEq+ reports Eq for 94–96% of pairs; LeanScorer reports Eq for 4%.

RQ3 (Sensitivity to perturbations): ACE produces no Eq outcomes on the Semantic Perturbation Set (74% Noneq, 26% Inconclusive). LeanScorer reports 42% Eq rate.

Table 2: Disagreement-Equivalent Subset Reasons

Theoretical and Practical Implications

Separation of Criterion from Certification

The paper makes a critical distinction: the correctness criterion (what relation defines equivalence) must be separate from the prover's ability to certify that relation. Stronger proof search doesn't fix a misaligned criterion—it can actually increase false positives (BEq+ with GPT-5.6 Luna reports more Eq outcomes on inequivalent pairs).

Failure Modes of Existing Approaches

• Whole-statement logical equivalence (BEq+): accepts unrelated but provable statements as equivalent; stronger provers worsen false-positive rates
• Reference-free semantic scoring (LeanScorer): allows unchanged components to outweigh localized semantic mismatches

Design Space Contribution

SAE is positioned as one explicit point in a hierarchy of possible equivalence criteria, demonstrating that:

• Finer intermediate relations are possible (e.g., recursive structure-aware comparison within components)
• The choice of granularity involves trade-offs between preserving structure and admitting reformulations

Conclusion

The paper introduces SAE and ACE for reference-based evaluation of autoformalized mathematical statements. SAE preserves binder correspondence, premise-conclusion roles, and relational structure, while ACE provides Lean-checkable equivalence and inequivalence judgments with an explicit Inconclusive outcome.

Future directions identified:

• Stronger proof-search backends could reduce Inconclusive outcomes without changing the criterion
• Stricter recursive variants of SAE are possible within the same framework
• Extension to statements outside the supported fragment (arbitrary higher-order predicates, more complex logical structure)

Key limitations acknowledged:

• SAE applies only to supported statement structures
• The premise-conclusion boundary may reject valid reformulations
• Resource-bounded proof search may leave obligations unresolved
• SAE fixes a particular granularity of structure preservation