检测数学自然语言与形式化表达的语义偏差，提升自动形式化准确性。
The Faithfulness Gap: Certifying Semantic Equivalence Between Natural-Language and Formal Mathematical Statements
- 通过双向可证性指纹匹配语义邻域，验证形式化是否忠实于原文
- 新基准测试中89.6%偏差被检测出，误报率仅3.0%
- 适用于需要高精度数学形式化的AI研究者与证明助手开发者
自动形式化将自然语言数学表述转化为形式化证明系统时，瓶颈不在于翻译流畅性，而在于语义忠实性：形式化结果虽可通过类型检查且可证明，却可能与原意不符。本文提出双向可证性指纹（BPF）框架，通过分析候选形式化在理论中的正向与逆向推论邻域，并与源自自然语言的探测信号比对，实现忠实性认证。引入四项新组件：(i) 反事实探测生成（CPG），用于合成针对性偏差探测；(ii) 等价谱，连续评分替代二元判断；(iii) 自适应探测预算分配（APBA），基于信息论优化资源分配；(iv) 忠实度引导解码（FGD），将BPF信号作为解码奖励。证明了漂移检测定理与PAC忠实性结果，表明在温和假设下，仅需$\/mathcal{O}(\log(1/δ)/ε)$次探测即可学习自然语言语句的等价类。发布DriftBench，包含2,183对自然语言/Lean 4配对，覆盖mathlib4六个子领域，带可控漂移标签。BPF+CPG在该基准上检测到89.6%漂移形式化，误报率3.0%，优于类型检查（41.2%）和大模型判别基线（63.3%）；FGD使顶尖自动形式化器的漂移率降低47%。
原文摘要 · Abstract (English)
Autoformalization, 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: (i) \emph{Counterfactual Probe Generation} (\cpg{}), a contrastive procedure that synthesizes probes targeting specific drift directions; (ii) the \emph{Equivalence Spectrum}, a continuous faithfulness score that replaces brittle binary verdicts; (iii) \emph{Adaptive Probe Budget Allocation} (\apba{}), an information-theoretic budget router; and (iv) \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/δ)/\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\%$. https://pmlrbd.github.io/BPF/
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。