Abstract
Autoformalization, the process of translating natural-language mathematics into formal proof assistants, is bottlenecked not by translation fluency but by \emph{faithfulness}: a formal statement can typecheck and be provable, yet still encode a different theorem than the source intended.
We introduce \emph{Bidirectional Provability Fingerprinting} (\bpf{}), a framework that certifies faithfulness by characterizing each candidate through its forward and backward consequence neighborhoods in the ambient theory and matching these against probes derived from the natural-language statement.
We further introduce four novel components:
- \emph{Counterfactual Probe Generation} (\cpg{}), a contrastive procedure that synthesizes probes targeting specific drift directions;
- the \emph{Equivalence Spectrum}, a continuous faithfulness score that replaces brittle binary verdicts;
- \emph{Adaptive Probe Budget Allocation} (\apba{}), an information-theoretic budget router;
- \emph{Faithfulness-Guided Decoding} (\fgd{}), which uses \bpf{} signals as a reward during autoformalization.
We prove a \emph{drift detection theorem} and a \emph{PAC-faithfulness} result establishing that the equivalence class of a natural language statement is learnable from \mathcal{O}(\log(1/\delta)/\varepsilon) probes under mild assumptions.
We release \driftbench{}, a benchmark of $2{,}183$ NL/Lean~4 pairs with controlled drift labels across six subfields of mathlib4. \bpf{} + \cpg{} detects $89.6\%$ of drifted formalizations at a $3.0\%$ false-positive rate—against $41.2\%$ for typecheck and $63.3\%$ for LLM-judge baselines, and \fgd{} reduces the rate at which a state-of-the-art autoformalizer emits drifted statements by $47\%$.
Blogger's Review: This research significantly enhances the faithfulness between natural language and formal mathematics through the Bidirectional Provability Fingerprinting framework, improving the accuracy and reliability of the autoformalization process. The introduction of new components allows the model to be more adaptive and flexible when handling complex mathematical statements, showing great potential for widespread application.