claimcheck：形式化规范忠实性检测工具与基准

研究者 Martin Amster 等人发布基准与工具 claimcheck，用于检测形式化规范是否忠实表达自然语言需求。基准覆盖 Dafny contracts、Lean 4、Isabelle 和 Rocq 四种形式语言，共 3,234 行，每行配自然语言需求、形式化产物及由执行、证明或原基准确立的标签；其中三分之一为保持语义的改写，仍保留忠实标签，使判断器无法靠识别“被改过”来打分。 claimcheck 的做法是让模型把形式化产物回译成英文，再由独立 judge 判断其与原需求是否表达同一保证。研究称，在四种语言上宏召回率较单次调用提升 8.2 至 9.8 个百分点。

AI 根据报道生成 · 1 小时前更新

还没有足够的连续观测数据，暂不绘制趋势。