# Aligning Faithfulness for Theory-Scale Autoformalization

> The align-then-label framework and FaithAlign benchmark reveal state-of-the-art models miss most autoformalization defects, overlook contextual links, and rarely recognize undecidable cases.

- **Source:** [arXiv](https://arxiv.org/abs/2610.18498)
- **Published:** 2026-10-17
- **Permalink:** https://picx.dev/p/3CckFG
- **Whiteboard:** https://picx.dev/p/3CckFG/image

## Summary

# 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

| Property | FaithAlign | FaithAlign-Gap |
|---|---|---|
| Items | 460 (164 faithful, 296 unfaithful) | 146 (85 undecidable, 12 faithful, 49 unfaithful) |
| Links | 4,982 (4,232 faithful, 750 unfaithful) | 1,481 (954 faithful, 103 unfaithful, 424 undecidable) |
| Links per item | 2–34 | — |
| Context/assumption links | 25.5% | — |

### 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**

| Input | F | U | ND |
|---|---|---|---|
| Full F | 96.9% ± 0.7% | 3.1% ± 0.7% | — |
| Full U | 0.0% ± 0.0% | 100.0% ± 0.0% | — |
| Gap | 25.5% ± 0.7% | 46.3% ± 1.8% | **28.2% ± 2.0%** |

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

| Symbol | Meaning |
|---|---|
| $T_N$, $T_F$ | Informal target, formal target |
| $C_N$, $C_F$ | Informal context, formal context |
| $I$ | Implicit assumptions |
| $\sigma$, $\tau$ | Informal region, formal region |
| $\ell$ | Faithfulness label (0, 1, or ⊥) |
| $y = (a, \ell)$ | Finding (alignment + label) |
| $Y$, $\hat{Y}$ | Reference, predicted finding sets |
| $w(\hat{y}, y)$ | Overlap weight for matched pair |
| $\Pi$ | Set of matched prediction-reference pairs |

---

_Markdown view of https://picx.dev/p/3CckFG, served by PicX — AI-generated visual whiteboard summaries of research papers._