claimcheck：让LLM写形式化规约不再"跑偏"

形式化验证能证明程序满足规约，却无法告诉我们规约是否真的表达了作者的意图。当LLM开始同时撰写代码和规约，自然语言需求与形式化产物之间的语义鸿沟就成了真实风险——一个比需求更窄的属性的机器证明毫无价值，却能通过所有检查。这篇论文提出的claimcheck，正是为填补这一缺口而来。

规约形式化：一个被忽视的系统性风险

论文将这一缺口明确命名为"spec formalization problem"（规约形式化问题）：给定自然语言需求，产出语义与之匹配的形式化产物。问题的核心在于验证链条的方向性——形式化验证只保证"代码满足规约"，却对"规约是否忠实于需求"不置一词。

当人类工程师手动撰写规约时，这个缺口尚可通过反复沟通弥合。但LLM大规模生产代码与规约的场景下，验证通过了但验证了错误的东西，成为一个系统性风险。一个被形式化证明的属性如果比需求更窄，证明的技术成功反而制造了虚假的安全感。

形式化验证（formal verification）指用数学方法证明程序满足其形式化规约的技术，常见手段包括定理证明（如Coq、Isabelle、Lean）和模型检验。其核心是构造一个机器可检查的证明，确认程序的所有可能行为都落在规约允许的集合内。

规约（specification）则是描述程序“应该做什么”的形式化陈述，通常写成前置条件、后置条件和不变式。验证的可靠性完全依赖于规约的正确性：验证工具只回答“代码是否满足规约”，而不回答“规约是否符合意图”。这正是论文所指问题的技术根源——一个形式化证明的成立，与这个证明是否有意义，是两件独立的事。

四语言端到端基准：3,234行数据的设计巧思

为量化这一缺口，作者构建了一个覆盖四种形式语言的端到端基准：Dafny契约、Lean 4、Isabelle和Rocq的定理陈述。每一行将自然语言需求与形式化产物配对，标签由执行、证明或基准来源建立，共计3,234行。

基准设计中最值得注意的一点是防作弊机制：三分之一的样本是对形式化产物的语义保持重写（meaning-preserving rewrites），标签仍为忠实。这意味着一个判断器无法简单地通过"这行被编辑过"来给分——它必须真正理解语义等价性。这个设计把基准从模式匹配的舒适区推向了语义理解的深水区。

Dafny是微软研究院开发的验证感知编程语言，将程序与规约写在同一处，由内置 verifier 自动生成验证条件并调用 Z3 求解。Lean 4是函数式编程语言与交互式定理证明器的结合，近年因数学形式化项目而广受关注。Isabelle是基于高阶逻辑的通用定理证明器，强调人类可读的证明脚本。Rocq（原 Coq）是基于归纳构造演算的证明助手，在程序验证与数学形式化领域有长期积累。

四种语言覆盖了“编程语言内嵌验证”与“独立定理证明”两类范式，使基准能够检验方法对语言风格的泛化性。

claimcheck如何工作：反向翻译+独立裁判

claimcheck的核心思路是"反向验证"：先将形式化产物翻译回自然语言，且翻译模型从未见过原始需求；再由一个独立的裁判模型判断这个"非形式化产物"与原始需求是否表达了相同的保证。

这一设计的巧妙之处在于切断了信息泄漏路径。如果翻译模型看到需求，它可能无意识地向需求靠拢，掩盖形式化产物的真实语义。让翻译模型只面对形式化产物，才能获得一份"诚实的译文"。

反向翻译（back-translation）在机器翻译中原本指将译文再译回源语言以评估质量。claimcheck 借用了这一思路，但关键区别在于：翻译模型看不到原始需求，因此译文不会受需求“污染”。

独立裁判的设计则借鉴了评估中的“隔离原则”——判断者不应接触可能引入偏差的信息。让裁判只看到自然语言需求与反向翻译结果，避免其被形式化产物的语法结构或证明状态吸引，从而更专注于语义等价性的判断。

实验结果：宏观召回率显著提升

在四种形式语言上，claimcheck相比单次调用（同时展示需求和产物）取得了8.2到9.8个百分点的宏观召回率提升；即使基线拿到了同样的语义保持重写列表，claimcheck仍领先4.2到6.0个百分点。

一个关键发现是：让裁判同时看到形式化产物，会损失1.4到4.5个百分点的性能。这暗示了独立裁判的价值——当裁判被形式化产物的表面结构吸引时，它对语义鸿沟的敏感度反而下降。

研究还揭示了一个随模型能力变化的有趣趋势：在四个同时看到产物的裁判中，模型越强，claimcheck的增益越小，最强的裁判已接近"知情单次调用"的水平。这说明能力足够强的模型可能内化了部分语义等价判断能力，但对于当前主流模型，claimcheck的结构化流程仍带来实质收益。

对AI编程工具链的启示

这项工作指向一个更广泛的工程实践问题：在LLM辅助编程的工作流中，规约的正确性检查不能与代码验证割裂。claimcheck提供的思路——用独立模型反向翻译形式化产物、再与需求比对——可以嵌入CI流程，作为形式化验证之前的一道语义关卡。

对于正在引入形式化方法的团队，这篇论文的基准本身也有实用价值：四语言、3,234行、带防作弊设计的测试集，可作为评估自家规约生成流程的标尺。当形式化验证的成本不断下降，保证"验证的是正确的东西"将成为下一个瓶颈。

**CI（持续集成）**是软件开发中自动构建、测试与验证的流水线。将 claimcheck 嵌入 CI，意味着每次规约变更都自动触发一次语义等价性检查，在形式化验证之前拦截“规约偏离需求”的问题。

这种“语义关卡”与传统的类型检查、单元测试形成互补：类型检查保证结构合法，单元测试抽样行为，形式化验证覆盖全部行为，而 claimcheck 则守护验证的前提——规约本身是否被正确理解。