大语言模型会利用形式化漏洞吗？评估逻辑推理中的忠实度

形式验证确保证明有效性，但无法保证形式化的忠实度。在自然语言逻辑推理中，模型需从头构建公理系统，有效证明与忠实翻译间的差距尤为显著。本文研究了前沿模型在生成 Lean 4 证明时是否利用此差距（即“形式化博弈”）。实验对比了统一生成与两阶段流水线方法，发现尽管编译率高，但未发现系统性博弈行为。然而，两阶段方法揭示了两种不忠实模式：GPT-5 在证明中虚构公理，而 DeepSeek-R1 在形式化阶段误译前提。研究表明高编译率不等于忠实推理。