Aligning Faithfulness for Theory-Scale Autoformalization

Authors: Yuming Feng, Tadd Mao, Dhruva Arekar, Tianjun Zhong, Jiani Huang, Xujie Si, Ziyang Li
Affiliations: Johns Hopkins University, University of Toronto, University of Pennsylvania

---

Summary (Overview)

• Novel problem formulation: The paper introduces align-then-label, a context-aware formulation for faithfulness evaluation in autoformalization, which requires identifying phrase-level correspondences between informal and formal statements and labeling each link's faithfulness under explicitly specified contextual interpretations.

• New benchmark: FaithAlign, the first theory-scale faithfulness benchmark, comprises 460 items with 4,982 annotated phrase-level links across five formalization sources, plus FaithAlign-Gap, a companion set of 146 items with informal context and assumptions withheld.

• Key empirical findings: Across 8 models, GPT-6 Astra achieves the highest defect F1 at only 47.8% and identifies all defects in just 4.5% of items with two or more defects. Models frequently miss contextual links and fail to recognize undecidable cases.

• Critical gap identified: The best model recognizes only 28.2% of undecidable items as such, revealing that models often commit to definite verdicts unsupported by available information.

• Three contributions: (1) operationalizing faithfulness as align-then-label, (2) creating FaithAlign with fine-grained correspondence annotations, (3) empirical evaluation revealing systematic model failures.

---

Introduction and Theoretical Foundation

Background and Motivation

Autoformalization (AF) aims to translate mathematical writing into formal statements while preserving meaning—a property called faithfulness. This task is inherently theory-scale: formalizing a mathematical definition requires tracing dependencies on other definitions, standing assumptions, and conventions. A formalization may appear faithful in isolation but narrow a domain, omit an assumption, or misstate a definition in context, causing cascading failures.

Limitations of Existing Approaches

Existing faithfulness evaluations suffer from several critical limitations:

• Statement-level verdicts: Most methods produce scalar scores or binary verdicts for whole statement pairs, failing to map informal context to formal dependencies or show whether all defects have been localized.
• No coverage measurement: AriaScorer grounds binary judgments in retrieved library definitions but doesn't measure coverage of contextual correspondences.
• No informal-formal linking: FormalRx localizes problematic formal code without linking it to informal expressions and dependencies.
• No undecidable label: Binary labels used by MA-Align and FormalRx cannot represent cases where context is underspecified.

Motivating Example

The paper illustrates the problem with an example from Axler (2015) where a formalization from ProofNet instantiates the scalar field over ℂ while omitting ℝ, despite the natural language target intending both ℝ and ℂ. The faithful formalization correctly uses {F} [RCLike F] to quantify over both fields. This error compounds at theory scale when downstream theorems reference this result.

Key insight: "The fact that a formalization accepted in one expert-curated benchmark was flagged as defective in another shows how easily these ambiguities slip past human review."

---

Methodology

Problem Formulation: Align-then-Label

Faithfulness evaluation is formulated as a context-aware align-then-label problem with the following components:

Inputs

Each item pairs informal and formal targets with disambiguating context:

• $T_N$ — the informal target statement to be formalized
• $T_F$ — the formal target in Lean
• $C_N$ — informal context (definitions, notation, standing assumptions from the source)
• $C_F$ — formal context (referenced declarations, e.g., Mathlib definitions)
• $I$ — implicit assumptions (explicit statements resolving ambiguities left open by sources)

Labeled Alignments

• Region: a set of selected characters (possibly multiple disjoint spans)
• Link: pairs an informal region $\sigma$ with a formal region $\tau$; either endpoint may be empty (one-sided links) but not both
• Link roles: implicit (endpoint in $I$), context (endpoint in $C_N$ or $C_F$), or target (otherwise)
• Labels: faithful (1), unfaithful (0), or undecidable (⊥) when supplied material cannot settle the judgment

This yields six link types (Figure 3 in the paper), combining label with whether the link is paired or one-sided.

Findings and Verdicts

• A labeled link is a finding $y = (a, \ell)$
• Verdict rule: unfaithful if any finding is unfaithful; otherwise undecidable if any finding is undecidable; otherwise faithful

Evaluation Metrics

F1 scores with graded endpoint-overlap credit:

$$Credit_S = \sum_{(\hat{y}, y) \in \Pi, \hat{\ell} = \ell \in S} w(\hat{y}, y)$$ $$Prec_S = \frac{Credit_S}{|\hat{Y}_S|}, \quad Rec_S = \frac{Credit_S}{|Y_S|}, \quad F1_S = \frac{2 \cdot Prec_S \cdot Rec_S}{Prec_S + Rec_S}$$

where $\Pi$ is the set of matched prediction-reference pairs, $w(\hat{y}, y)$ is the overlap weight, and $S \subseteq \{0, 1, \bot\}$.

Key variants:

• Joint F1 ($S = \{0, 1, \bot\}$): recovery and correct labeling of all links
• Defect F1 ($S = \{0\}$): isolates recovery of defects
• Undecidable-link F1 ($S = \{\bot\}$): recognition of undecidable links
• Defect F1@0.5: stricter variant requiring substantial overlap (≥ half recall and precision at every endpoint)

Item-level rates:

• All-defects rate: fraction of defective items where every reference defect is matched to an unfaithful prediction
• Verdict accuracy: fraction of items whose inferred verdict matches reference
• Undecidable-item rate: verdict accuracy restricted to undecidable items

Benchmark Construction

FaithAlign draws on five sources: LeanEuclid, Pistis, MA-Align, LCS-Bench, and ProofNet-Verified. Four graduate-level Lean experts annotated over ~8 person-months using a browser-based visual tool in three steps: (1) broad region selection and linking, (2) narrowing unfaithful regions for precision, (3) supplying context and assumptions.

FaithAlign-Gap withholds $C_N$ and $I$, creating: 85 undecidable items, 12 faithful, 49 unfaithful. For each undecidable item, an opposite-verdict counterpart is constructed, forming triplets for controlled comparison.

---

Empirical Validation / Results

Dataset Statistics

Models Evaluated

8 models: GPT-6 Astra (GPT6), GPT-5.6 Sol (GPT56), Kimi K3 (KK3), Opus 5 (CO5), Opus 4.8 (CO48), DeepSeek V3.2 (DS32), GLM-5 (GLM5), MiniMax M2.5 (MM25), with three repetitions per model on both tasks.

RQ1: Can models identify faithfulness defects?

• GPT-6 Astra achieves the highest defect F1 at 47.8%, dropping under F1@0.5
• Astra's inferred verdicts reach 93.1% balanced accuracy but identifies every defect in only 34.3% of defective items
• On items with 2+ defects, all-defects rate falls to 4.5%
• On two-defect items, Astra finds exactly one defect in 68% of cases (vs. 48% under independence), showing correlated failures
• ~⅔ of defects are never identified in any of three repetitions

RQ2: How well do models identify contextual links?

• Context links have joint F1 15.7 percentage points below the overall 37.6% pooled score
• ~75% of contextual defects are never aligned
• Defects involving implicit assumptions are similarly omitted
• "Supplying the surrounding material does not ensure that a model uses it"

RQ3: Can models recognize underspecification?

Table 1: GPT6 verdicts for the 85 triplets

Key finding: Astra judges both faithful and unfaithful versions correctly in 96.9% of triplets when context is supplied, yet gives definite verdicts in all repetitions for 52 of 85 triplets when context is withheld. "The failure lies in recognizing that a judgment depends on context the model has not been given."

RQ4: Can models produce fine-grained alignments?

• Predicted links grow much more slowly than annotated links
• ~60% of annotated links remain unaligned on average
• ~⅓ of failures are overmerged links (one prediction spans several annotated links)
• Remaining failures: omitted endpoints or disconnected selections

---

Theoretical and Practical Implications

Theoretical Contributions

1. Operationalization of faithfulness: The align-then-label formulation moves beyond binary verdicts to make judgments traceable and localizable, enabling systematic error analysis.

2. Context-dependence formalized: The framework explicitly separates targets ($T_N$, $T_F$), context ($C_N$, $C_F$), and implicit assumptions ($I$), recognizing that faithfulness is not a property of isolated statements.

3. Undecidability as a first-class label: The ⊥ label acknowledges that some judgments cannot be settled by available material, preventing unsupported definitive verdicts.

Practical Implications

• Benchmark for evaluator development: FaithAlign provides a testbed for developing fine-grained, context-aware faithfulness evaluation methods.
• Error localization: The link-level annotations enable identifying where defects occur, not just whether they exist—crucial for theory-scale formalization where errors propagate through dependency graphs.
• Model limitations revealed: Current models' failures in aligning contextual dependencies and recognizing underspecification highlight specific areas needing improvement.

---

Conclusion

The paper formulates theory-scale faithfulness evaluation as a context-aware align-then-label problem and introduces FaithAlign and FaithAlign-Gap benchmarks. Key takeaways:

1. Models frequently miss defects, especially when multiple defects exist per item
2. Models overlook contextual links, failing to use supplied context even when available
3. Models commit to definite verdicts when essential information is absent, rarely recognizing undecidability
4. Models produce coarser alignments than human annotations, merging distinct mathematical objects

Future directions: Developing evaluators that systematically trace dependencies, actively search for additional defects, and identify missing definitions or assumptions needed to resolve undecidable judgments.

---

Key Mathematical Notation