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:

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:

Main Results

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

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)

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

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.