LLM会在形式化上投机吗？评估逻辑推理中的忠实性

形式化验证保证证明的有效性，却不保证形式化的忠实性。对于自然语言逻辑推理——模型在无库约束下从零构建公理系统——有效证明与忠实翻译之间的鸿沟尤为尖锐。我们研究前沿模型在生成Lean 4证明时是否会利用这一鸿沟，并将这种行为称为形式化投机（formalization gaming）。我们在303道一阶逻辑题（203道来自FOLIO，100道来自Multi-LogiEval）上评测GPT-5与DeepSeek-R1，将统一生成与把形式化和证明分离的两阶段流水线进行对比。尽管编译率达87-99%，我们未发现统一生成中存在系统性投机的证据：即便在使用专为诱导投机而设计的提示词时，模型也宁可报告失败也不强行给出证明。然而，逃避我们检测信号的不忠实行为仍可能出现。两阶段流水线揭示了两种不同的不忠实模式：GPT-5在证明生成阶段凭空捏造公理，这是一种可通过跨阶段比对发现的事后补救；DeepSeek-R1则在形式化阶段错误翻译前提，产生完全逃过检测的内部自洽输出。这些发现表明，不应把高编译率或高准确率等同于忠实的推理。代码与数据见https://github.com/koreankiwi99/formalization-gaming。