忠实性缺口：自然语言与形式化数学语句间语义等价的认证

自动形式化——把自然语言数学翻译为形式化证明助手——的瓶颈不在翻译流畅而在忠实性：形式化语句可以类型检查通过且可证——却编码与源意图不同的定理。我们介绍双向可证性指纹（BPF）——通过刻画每个候选在环境理论中的前向与后向推论邻域——并与从自然语言语句导出的探针匹配——认证忠实性的框架。我们进一步引入四个新组件：(i) 反事实探针生成（CPG）——合成针对特定漂移方向的对比探针的对比程序；(ii) 等价谱——取代脆弱二元判决的连续忠实性分数；(iii) 自适应探针预算分配（APBA）——信息论预算路由器；(iv) 忠实性引导解码（FGD）——在自动形式化期间以BPF信号为奖励。我们证明漂移检测定理与PAC忠实性结果：温和假设下自然语言语句的等价类可从O(log(1/δ)/ε)个探针学习。我们发布DriftBench——mathlib4六个子域2,183对NL/Lean 4带受控漂移标签的基准。BPF+CPG以3.0%假阳性率检出89.6%的漂移形式化——对照类型检查41.2%与LLM裁判基线63.3%——且FGD把SOTA自动形式化器产出漂移语句的比率降47%。