claimcheck
一种通过反向翻译与独立裁判机制检测LLM生成的代码与形式化规约之间语义偏差的方法，旨在解决形式化验证中'规约是否忠实于需求'的缺口
时间轴 (近 90 天)
论文将自然语言需求与形式化产物之间语义不匹配的缺口命名为'spec formalization problem'（规约形式化问题）。
作者构建了覆盖四种形式语言的端到端基准，包括Dafny契约、Lean 4、Isabelle和Rocq的定理陈述，共计3,234行配对数据。
基准中三分之一的样本是对形式化产物的语义保持重写，标签仍为忠实，以防止判断器通过'被编辑过'来简单给分。
claimcheck的核心方法是将形式化产物翻译回自然语言，且翻译模型从未见过原始需求；然后由独立裁判模型判断非形式化产物与原始需求是否表达相同保证。
在四种形式语言上，claimcheck相比单次调用取得了8.2到9.8个百分点的宏观召回率提升。
即使基线拿到了同样的语义保持重写列表，claimcheck仍领先4.2到6.0个百分点。
让裁判同时看到形式化产物，会损失1.4到4.5个百分点的性能。
在四个同时看到产物的裁判中，模型越强，claimcheck的增益越小，最强的裁判已接近'知情单次调用'的水平。
claimcheck可以嵌入CI流程，作为形式化验证之前的一道语义关卡，自动触发语义等价性检查。
全部知识事实 (9)
论文将自然语言需求与形式化产物之间语义不匹配的缺口命名为'spec formalization problem'（规约形式化问题）。
50%待验证作者构建了覆盖四种形式语言的端到端基准，包括Dafny契约、Lean 4、Isabelle和Rocq的定理陈述，共计3,234行配对数据。
50%待验证基准中三分之一的样本是对形式化产物的语义保持重写，标签仍为忠实，以防止判断器通过'被编辑过'来简单给分。
50%待验证claimcheck的核心方法是将形式化产物翻译回自然语言，且翻译模型从未见过原始需求；然后由独立裁判模型判断非形式化产物与原始需求是否表达相同保证。
50%待验证在四种形式语言上，claimcheck相比单次调用取得了8.2到9.8个百分点的宏观召回率提升。
50%待验证即使基线拿到了同样的语义保持重写列表，claimcheck仍领先4.2到6.0个百分点。
50%待验证让裁判同时看到形式化产物，会损失1.4到4.5个百分点的性能。
50%待验证在四个同时看到产物的裁判中，模型越强，claimcheck的增益越小，最强的裁判已接近'知情单次调用'的水平。
50%待验证claimcheck可以嵌入CI流程，作为形式化验证之前的一道语义关卡，自动触发语义等价性检查。
50%