摘要
Autoformalization，即将自然语言数学翻译为形式证明助手的过程，并非受制于翻译流畅性，而是受制于\emph{信任性}：一个形式陈述可能通过类型检查并可证明，但仍可能编码与源意图不同的定理。
我们提出了\emph{双向可证明性指纹}（\bpf{}）框架，通过表征每个候选项在环境理论中的前向和后向后果邻域，并将这些与来自自然语言陈述的探针进行匹配，从而认证信任性。
此外，我们引入了四个新组件：
- \emph{反事实探针生成}（\cpg{}），一种对比程序，用于合成针对特定漂移方向的探针；
- \emph{等价谱}，一个连续的信任性评分，取代了脆弱的二元判决；
- \emph{自适应探针预算分配}（\apba{}），一种信息论预算路由器；
- \emph{信任性引导解码}（\fgd{}），利用\bpf{}信号作为自动形式化过程中的奖励。
我们证明了一个\emph{漂移检测定理}和一个\emph{PAC-信任性}结果，建立了在温和假设下，自然语言陈述的等价类可以通过\mathcal{O}(\log(1/\delta)/\varepsilon)个探针学习。
我们发布了\driftbench{}，这是一个包含$2{,}183$个NL/Lean~4对的基准，具有跨六个mathlib4子领域的可控漂移标签。\bpf{}与\cpg{}以$3.0\%$的假阳性率检测到$89.6\%$的漂移形式化，而类型检查基准为$41.2\%$，LLM-judge基准为$63.3\%$。\fgd{}将最先进的自动形式化工具产生漂移陈述的速率降低了$47\%$。
博主点评： 该研究通过双向可证明性指纹框架有效提升了自然语言与形式数学之间的信任性，显著改善了自动形式化过程的准确性和可靠性。特别是新组件的引入，使得模型在处理复杂数学陈述时更具适应性与灵活性，具有广泛的应用前景。