摘要
自动形式化的瓶颈在于“忠实性”：形式陈述虽可类型检查，却可能偏离原意。本文提出双向可证明指纹框架，通过前后向推论邻域特征来认证语义等价性。引入反事实探针生成、等价谱评分、自适应预算分配及忠实性引导解码四项创新。理论证明了漂移检测定理，并在基准测试中显著优于现有基线，有效减少了形式化过程中的语义漂移。
AI 推荐理由
论文核心解决数学形式化中的语义等价与逻辑推理一致性问题，属于深度推理研究。
研究机构
Department of Computer Science, Istanbul Technical University, Istanbul, Turkey
论文信息