# The Faithfulness Gap: Certifying Semantic Equivalence Between Natural-Language and Formal Mathematical Statements

> Bidirectional Provability Fingerprinting detects 89.6% of semantically drifted autoformalizations at 3% false positives, outperforming typechecking and LLM-judge baselines by over 40%.

- **Source:** [arXiv](https://arxiv.org/abs/2606.16541)
- **Published:** 2026-08-18
- **Permalink:** https://picx.dev/p/pVtDfk
- **Whiteboard:** https://picx.dev/p/pVtDfk/image

## Summary

## Summary (Overview)

- **Core Problem**: Autoformalization (translating natural-language mathematics into formal proof assistants like Lean 4) is bottlenecked by the **faithfulness gap**—formal statements can typecheck and be provable yet encode a different theorem than intended.
- **Main Contribution**: Introduces **Bidirectional Provability Fingerprinting (BPF)**, a reference-free framework that certifies faithfulness by comparing forward/backward consequence neighborhoods of candidate formalizations against semantic probes derived from the natural-language statement.
- **Key Innovations**: Four novel components—Counterfactual Probe Generation (CPG), the Equivalence Spectrum (a continuous faithfulness score), Adaptive Probe Budget Allocation (APBA), and Faithfulness-Guided Decoding (FGD).
- **Theoretical Results**: Proves a drift detection theorem and a PAC-faithfulness result showing the equivalence class of a natural-language statement is learnable from $O(\log(1/\delta)/\varepsilon)$ probes.
- **Empirical Results**: BPF + CPG detects 89.6% of drifted formalizations at 3.0% false-positive rate (vs. 41.2% for typecheck and 63.3% for LLM-judge baselines); FGD reduces drifted outputs from a state-of-the-art autoformalizer by 47%. Releases **DRIFTBENCH**, a benchmark of 2,183 NL/Lean 4 pairs with controlled drift labels.

## Introduction and Theoretical Foundation

### Background
Modern autoformalization systems translate natural-language theorem statements into formal proof assistants such as Lean 4, Rocq, or Isabelle/HOL. The dominant quality signal used to gate outputs is whether the formal statement **typechecks** and optionally whether a downstream prover can close it. Both signals are necessary but insufficient:

> "A formal statement can be syntactically well-formed, provable, and wrong: it can mean something other than what the mathematician wrote. We call this the **faithfulness gap**."

Unlike code—where unit tests and runtime semantics offer an executable oracle—faithfulness in formalization is a relation between two semantic objects in different universes: a natural-language sentence interpreted under tacit mathematical convention and a formal expression under a precisely specified dependent type theory.

### Formalizing Faithfulness

**Definition 3.1 (Interpretation distribution)**: An interpretation distribution $\mathcal{D}_N$ for $N \in \mathcal{N}$ is a probability distribution over formal statements in $\mathcal{F}$ whose support consists of formalizations that competent mathematicians would accept as expressing $N$ in the theory $T$.

**Definition 3.2 (ε-Faithfulness)**: A candidate $F \in \mathcal{F}$ is $\varepsilon$-faithful to $N$ under $\mathcal{D}_N$ if

$$
\operatorname{Pr}_{I \sim \mathcal{D}_N} \left[ \mathcal{T} \vdash F \leftrightarrow I \right] \geq 1 - \varepsilon.
$$

This weakens equality to provable equivalence, accommodating notational variation while remaining strict about semantic content.

### Taxonomy of Drift
Four canonical classes of semantic drift are identified:

| Drift Class | Description |
|---|---|
| $\Delta_{\forall}$ | Quantifier drift (e.g., swapping order of adjacent quantifiers) |
| $\Delta_{H}$ | Hypothesis drift (dropping or weakening a stated hypothesis) |
| $\Delta_{C}$ | Conclusion drift (altering the conclusion) |
| $\Delta_{T}$ | Type coercion drift (changing types, e.g., Set vs. Finset) |

These four classes account for 94% of human-labeled drift instances in a pilot study of 400 randomly sampled outputs from a state-of-the-art autoformalizer.

## Methodology

### Bidirectional Provability Fingerprinting (BPF)

**Definition 4.1 (Provability fingerprint)**: Let $F \in \mathcal{F}$ and let $\mathcal{P} \subseteq \mathcal{F}$ be a set of probes. The forward fingerprint of $F$ over $\mathcal{P}$ is

$$
\Phi_F^{+}(\mathcal{P}) = \{P \in \mathcal{P}: \mathcal{T} \vdash F \to P\},
$$

and the backward fingerprint is

$$
\Phi_F^{-}(\mathcal{P}) = \{P \in \mathcal{P}: \mathcal{T} \vdash P \to F\}.
$$

The full fingerprint is $\Phi_F(\mathcal{P}) = (\Phi_F^{+}(\mathcal{P}), \Phi_F^{-}(\mathcal{P}))$.

**Why bidirectional matters**: Forward-only fingerprints fail to distinguish a strict strengthening of $N$ from $N$ itself (a strictly stronger $F$ entails everything $N$ entails). Backward-only fingerprints dually fail to catch strict weakenings. Bidirectional matching is the minimum sufficient signal.

**Proposition 4.2**: Let $F$ be a candidate for $N$, and let $\mathcal{P}$ be a probe set closed under $T$-equivalence. Then $\mathcal{T} \vdash F \leftrightarrow N$ if and only if $\Phi_F(\mathcal{P}) = \Phi_N(\mathcal{P})$ and for each pair $(P, P') \in \mathcal{P}^2$ with $\mathcal{T} \vdash P \to P'$, the entailment also holds in $F$'s fingerprint.

### Counterfactual Probe Generation (CPG)

CPG treats probe generation as a contrastive problem. For each drift class $D \in \{\Delta_{\forall}, \Delta_H, \Delta_C, \Delta_T\}$, a counterfactual pair is constructed consisting of the natural-language statement $N$ and a drifted twin $N^D$, obtained by mechanically perturbing $N$ (e.g., swapping adjacent quantifiers or dropping a hypothesis). The probe distribution for drift class $D$ is:

$$
\mathcal{Q}_D(P) \propto \mathrm{Pr}[P \text{ entailed by } N] \cdot \mathrm{Pr}[P \text{ not entailed by } N^D]
$$

Key design choice: $N^D$ is generated **mechanically**, not by an LLM, ensuring the drift class label is unambiguous and that $N^D$ exhibits exactly the targeted failure.

### The Equivalence Spectrum

**Definition 6.1 (Equivalence Spectrum)**: Let $\mathcal{P}$ be a probe set with predicted labels $\ell: \mathcal{P} \to \{+, -, \bot\}$ and class weights $w: \{\Delta_{\forall}, \Delta_H, \Delta_C, \Delta_T\} \to \mathbb{R}_{>0}$. The equivalence spectrum score is

$$
\mathcal{E}(F, N) = 1 - \frac{\sum_{P \in \mathcal{P}} w(D_P) \cdot \mathbb{1}[\mathrm{cell}_P(F) \neq \ell(P)]}{\sum_{P \in \mathcal{P}} w(D_P)},
$$

where $D_P$ is the drift class targeted by probe $P$ and $\mathrm{cell}_P(F)$ is the observed fingerprint cell at $P$.

Three calibrated decision regions: $\mathcal{E} \geq 0.93$ (ACCEPT), $\mathcal{E} \in [0.78, 0.93)$ (REVIEW), $\mathcal{E} < 0.78$ (REJECT).

### Adaptive Probe Budget Allocation (APBA)

APBA routes budget by expected information gain. For drift class $D$ with current posterior $p_D$, the expected information gain from a probe targeting $D$ is:

$$
\operatorname{IG}(D) = H(p_D) - \mathbb{E}_{r \sim \pi_D} \left[ H(p_D \mid r) \right],
$$

where $r$ is the predicted oracle outcome and $\pi_D$ is the empirical witnessability distribution.

**Theorem 7.1 (APBA budget reduction)**: Let $k^{\star}$ be the budget required by uniform allocation to reach detection rate $\rho$ on DRIFTBENCH. Then APBA reaches the same $\rho$ with budget $k_{APBA} \leq k^{\star}/\gamma$, where $\gamma$ is the heterogeneity ratio of witnessability rates across drift classes. On DRIFTBENCH, $\gamma \approx 3.2$.

## Empirical Validation / Results

### DRIFTBENCH Benchmark

DRIFTBENCH contains 2,183 natural language/Lean 4 pairs with controlled drift labels across six mathlib4 subfields:

| Subfield | Faith. | $\Delta_{\forall}$ | $\Delta_{H}$ | $\Delta_{C}$ | $\Delta_{T}$ | Comb. |
|---|---|---|---|---|---|---|
| Analysis | 198 | 64 | 71 | 58 | 33 | 31 |
| Algebra | 173 | 51 | 68 | 49 | 28 | 27 |
| Topology | 162 | 49 | 59 | 47 | 30 | 25 |
| Number Th. | 144 | 42 | 55 | 41 | 22 | 22 |
| Combinator. | 138 | 43 | 51 | 39 | 24 | 21 |
| Category | 117 | 35 | 44 | 33 | 19 | 19 |
| **Total** | **932** | **284** | **348** | **267** | **156** | **145** |

### Main Results

**Table 2: Drift detection on the controlled DRIFTBENCH split (Det@3%FPR = detection rate at 3% false-positive rate)**

| Method | F1 | Det@3%FPR | FPR | Cost |
|---|---|---|---|---|
| Typecheck only | 0.27 | 0.114 | 0.020 | 1× |
| Provability | 0.42 | 0.412 | 0.030 | 18× |
| BLEU-ref | 0.55 | 0.301 | 0.030 | 1× |
| Back-translation | 0.66 | 0.589 | 0.030 | 4× |
| LLM-judge | 0.71 | 0.633 | 0.030 | 2× |
| BPF-naive | 0.85 | 0.832 | 0.031 | 22× |
| **BPF + CPG** | **0.91** | **0.896** | **0.030** | 26× |
| BPF + CPG + APBA | 0.91 | 0.894 | 0.031 | **8×** |

BPF + CPG reduces the residual error rate of the best non-fingerprinting baseline (LLM-judge) by approximately 72% at matched FPR. Adding APBA preserves detection performance while reducing wall-clock cost by 3.2×.

### Per-Class Detection

**Table 3: Detection rate by drift class (at 3% FPR overall)**

| Method | $\Delta_{\forall}$ | $\Delta_{H}$ | $\Delta_{C}$ | $\Delta_{T}$ |
|---|---|---|---|---|
| Typecheck | 0.07 | 0.05 | 0.04 | 0.31 |
| Provability | 0.46 | 0.62 | 0.33 | 0.18 |
| Back-translation | 0.66 | 0.61 | 0.59 | 0.40 |
| LLM-judge | 0.74 | 0.67 | 0.64 | 0.42 |
| BPF-naive | 0.89 | 0.88 | 0.84 | 0.55 |
| **BPF + CPG** | **0.94** | **0.93** | **0.91** | **0.66** |

The type-coercion class ($\Delta_T$) is hardest for every method, consistent with its lower witnessability rate $\alpha(\Delta_T) \approx 0.31$.

### Ablations

**Table 4: Ablations of BPF + CPG on the controlled split**

| Variant | F1 |
|---|---|
| Full BPF + CPG | 0.91 |
| - counterfactual probes (CPG) | 0.85 |
| - bidirectional (forward only) | 0.80 |
| - hypothesis-drop probes | 0.82 |
| - boundary probes | 0.88 |
| - adversarial probes | 0.87 |
| probe budget k = 8 (vs. 32) | 0.83 |
| probe budget k = 8 + APBA | 0.89 |

Removing bidirectional matching costs 11 F1 points; removing CPG costs 6 points; removing hypothesis-drop probes costs 9 points, almost all on $\Delta_H$.

### FGD Downstream Impact

FGD reduces the drifted-output rate from a state-of-the-art autoformalizer from 19.4% to 10.3% at $m = 4$ candidates (47% relative reduction), and to 8.7% at $m = 8$. The re-prompt component contributes most of the improvement at small $m$; pure reranking saturates at ~14%.

## Theoretical and Practical Implications

### Drift Detection Theorem

**Theorem 8.1 (Drift Detection)**: Fix $\delta \in (0, 1)$ and drift class $D \in \{\Delta_{\forall}, \Delta_H, \Delta_C, \Delta_T\}$. Suppose the probe generator samples probes from a distribution $\mathcal{Q}_D$ such that

$$
\operatorname{Pr}_{P \sim \mathcal{Q}_D} \left[ P \text{ witnesses } D \text{ for } (N, F) \right] \geq \alpha(D),
$$

where $\alpha(D) \in (0, 1]$ is the witnessability rate for class $D$. Then, with probe budget

$$
k \geq \frac{1}{\alpha(D)} \log \frac{1}{\delta},
$$

BPF flags $F$ as drifted with probability at least $1 - \delta$, provided the entailment oracle is complete on the chosen probes.

Empirical witnessability rates: $\alpha(\Delta_{\forall}) \approx 0.62$, $\alpha(\Delta_H) \approx 0.55$, $\alpha(\Delta_C) \approx 0.48$, $\alpha(\Delta_T) \approx 0.31$. A budget of $k = 32$ probes gives $\delta \leq 0.01$ for the first three classes.

### PAC-Faithfulness

**Theorem 8.2 (PAC-Faithfulness)**: Let $[N]_{\mathcal{T}}$ denote the equivalence class $\{F \in \mathcal{F} : \mathcal{T} \vdash F \leftrightarrow N\}$. Assume CPG probes are drawn from a distribution $\mathcal{Q}$ such that for every $F \notin [N]_{\mathcal{T}}$ reachable by an LLM autoformalizer, $\mathrm{Pr}_{P \sim \mathcal{Q}}[P \text{ witnesses } F\text{'s drift}] \geq \alpha_0 > 0$. Then with $k \geq (1/\alpha_0) \log(1/\delta\varepsilon)$ probes, BPF produces a hypothesis $\hat{H} \subseteq \mathcal{F}$ such that with probability at least $1 - \delta$,

$$
\operatorname{Pr}_{F \sim \mathcal{D}_\mu} \left[ F \in \hat{H} \iff F \in [N]_{\mathcal{T}} \right] \geq 1 - \varepsilon,
$$

where $\mathcal{D}_\mu$ is the autoformalizer's output distribution.

### Incomplete Oracle and Undetectable Drift

Lean's tactic stack is incomplete. Let $\eta(\tau)$ be the probability that the oracle returns "?" on a probe that admits a $\tau$-cost proof. The detection bound degrades to $1 - \delta - k\eta(\tau)$; empirically $\eta(30s) \approx 0.07$ on DRIFTBENCH probes. BPF cannot detect **convention drift**—where $F$ adopts a different notational convention invisible to provability—for which a complementary structural test is developed.

### Practical Implications

1. **Deployment as triage tool**: BPF should be deployed as a triage tool that prioritizes expert review (via the REVIEW band), not a replacement for human verification.
2. **Cross-system generality**: The framework is system-agnostic—preliminary experiments on Isabelle/HOL show comparable detection rates (F1 = 0.88 vs. 0.91 on Lean 4).
3. **Computational efficiency**: APBA provides 3.2× practical speedup; caching fingerprints for canonical statements and learned entailment classifiers are identified as future optimization paths.

## Conclusion

This paper introduced **Bidirectional Provability Fingerprinting (BPF)**, a framework for certifying faithfulness in autoformalization that requires no reference formalization. The four supporting innovations—counterfactual probe generation (CPG), the equivalence spectrum, adaptive probe budget allocation (APBA), and faithfulness-guided decoding (FGD)—collectively address distinct facets of the faithfulness problem.

Key takeaways:
- **BPF + CPG** detects 89.6% of drifted formalizations at 3.0% false-positive rate, substantially outperforming typecheck (41.2%), provability, BLEU-ref, back-translation, and LLM-judge baselines.
- **FGD** reduces drifted-output rates from a state-of-the-art autoformalizer by 47%.
- **Theoretical guarantees** (drift detection and PAC-faithfulness theorems) characterize what is and is not detectable, with polynomial probe budgets.
- **DRIFTBENCH** provides the first benchmark with controlled drift labels for evaluating autoformalization faithfulness end-to-end.

The faithfulness gap is identified as the bottleneck for trustworthy autoformalization at the scale of full mathematical libraries. The authors view BPF as a concrete step toward closing it, with future directions including stronger entailment oracles, cross-system validation, and integration with library-scale formalization workflows.

---

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