← 返回 PaperDaily 大模型与智能体

COINS最新评测：六大模型写程序规范，Gemini仅28.1%通过

大模型写代码已卷到天际，但让它们写“程序规范”（formal specification）靠谱吗？本论文提出COINS框架，用Rocq证明助手评估六大模型的规范生成能力，结果差距惊人：最强Gemini 3 Pro也仅28.05%通过率，DeepSeek-V3.1直接跌到1.22%。想看懂LLM在形式化验证边界的真实水平，这篇是必读。

龙哥读论文发布于 2026-08-17 00:20:07 阅读 3 查看原文

#大语言模型 #AI科研

原论文信息如下：

论文标题:
How Powerful Are LLMs in Generating Formal Program Specifications?

发表日期:
2026年08月

发表单位:
未明确标注（作者单位含中科院软件所等）

原文链接:
https://arxiv.org/pdf/2608.13077v1.pdf

开源代码链接:
https://github.com/taylor-swift-13/Coins

项目链接:
https://github.com/taylor-swift-13/Coins

想象一个场景：你让大模型写Python代码，它可能轻松通过所有单元测试；但若让它把代码的“行为契约”用形式化语言写出来——规定输入输出必须满足什么关系——它可能瞬间从“编程高手”变成“哑巴”。这不是玩笑，而是本论文揭示的真实图景。

LLM写形式化规范，到底行不行？

形式化验证是软件正确性的“终极保险”，通过机器可检查的证明确保实现满足预期行为。交互式定理证明器如Rocq（原Coq）、Lean等已在编译器、操作系统内核等安全关键系统中大显身手。问题在于：写形式化规范的成本极高。

所谓规范（Specification），是一个逻辑命题，描述“输入和输出之间必须满足的关系”——它独立于任何具体实现。比如对“排序列表”问题，规范要规定：输出是输入的排列、指定索引位置的元素被保留、可被3整除的位置元素有序。每个正确实现都必须满足这些条件，每个错误实现必然违反其中至少一条。

近年来，大语言模型在定理证明、可验证代码生成方面进步神速。那么，LLM能不能自动生成程序规范？这个问题的答案取决于你“怎么判规范好不好”。

现有评估方式有个致命缺陷。传统验证管线验证的是“实现满足规范”，规范只是验证目标，并不关心规范本身是否精确刻画了程序全部语义。一个规范可能足以验证某个特定实现，却过于宽松——无法排除不正确的替代实现。

CLEVER基准尝试用“等价性证明”来强化标准——要求模型同时生成规范、实现，并证明两者与ground truth等价。概念上很完美，但实践上几乎不可行：第一，需要人工维护ground truth规范，成本极高且可能有偏见；第二，非平凡规范之间的完全等价证明极难，顶尖模型成功率极低；第三，规范生成、实现生成、形式化验证耦合在单一管线中，失败了根本分不清是规范错了、实现错了还是证明能力不足。

这引出了论文最核心的一个观察——评估二象性（Evaluation Duality）：当规范验证失败时，你无法判断是规范本身有缺陷，还是证明器能力不足。更强的证明器能更准确暴露规范正确性，而更正确的规范能更可靠评估证明器能力——两者互为前提。

COINS框架：用测试用例评估规范质量

既然全量等价性证明不现实，论文提出了一个务实的新思路：把规范实例化到具体测试用例上，看证明义务（Proof Obligation）能不能被Rocq检查通过。

这抓住了形式推理的不对称性：成功证明是可靠的正向证据，失败证明则天然含糊。一个正确规范，如果LLM能成功证明测试用例上的命题，那说明该规范在这组输入输出上行为正确；如果证明失败，可能是规范错了，也可能是证明太难。所以评估主指标应该聚焦正向可证明性。

COINS（COq-based INstantiated Specification evaluation）评估框架分为两个阶段：

准备阶段要做三件事：一是由形式化验证专家手工编写HumanEval全部164道题的Rocq规范，每道都经过交叉审阅，作为人类基线；二是设计统一的提示词模板，让LLM按相同签名生成规范；三是构建测试套件——正例用HumanEval+的大规模自动生成测试（平均每问题755.98个），负例通过变异测试生成（对每个规范实现做算子级变异，产出与真值行为不同的输入输出对）。

评估阶段是四阶段过滤管线：

第一步，语法验证（SYNTAX），检查规范能否在Rocq中编译通过。第二步，首个正例证明（PASS_first），尝试证明第一个正测试用例的证明义务。第三步，全量正例证明（PASS_all），对所有正测试用例构建证明。第四步，负例拒收（REJECT_all），对每个负测试用例，让LLM判断并尝试构造接受证明——如果规范能证明接受一个错误行为，说明规范过宽；全部负例都不能被证明接受，才算通过。

只有同时通过PASS_all和REJECT_all的规范，才被认定为“候选规范”。

下图展示了COINS整体框架：

图1：COINS评估框架。(a) 准备阶段：来自HumanEval的输入和生成的规范。(b) 评估阶段：多阶段过滤管线，标注数字展示了Gemini 3 Pro Preview的过滤结果（164 → 43个候选）。

六大模型同台竞技：结果令人意外

论文选了六款代表模型：GPT-5（OpenAI）、Claude 4.5 Opus（Anthropic）、Gemini 3 Pro Preview（Google）这三款2025年Q4的前沿模型，加上GPT-4o、Claude 3.7 Sonnet这两个早期模型，以及DeepSeek-V3.1这个开源标杆。

先看第一个研究问题：哪个LLM是最可靠的验证器？

用人类手写规范作为锚点（解决评估二象性的一侧），让六个模型分别担任“证明器”，对全部正测试用例构造证明：

*表格超出部分左右可以滑动

Table 1. Verification Performance Across Different Models (n=164). Models ordered chronologically by release date. Best performing model highlighted. Higher values indicate better performance.

结果很有意思。Gemini 3 Pro Preview以29.88%的全正例通过率排第一，Claude 4.5 Opus以19.51%紧随其后，GPT-5是16.64%。但更扎眼的是DeepSeek-V3.1在人类规范上一个正例都没全证明过——PASS_all 0.00%。这说明什么？即使规范完全正确，让LLM把测试用例全部证明完也远非易事，形式化证明能力仍然是当前大模型的明显短板。最终论文选了Gemini 3 Pro Preview作为后续所有实验的统一验证器。

验证器定了，接下来就让六个模型在完全一致的提示词下生成规范，用COINS管线统一过筛：

表2：规范生成评测结果（n=164）。Syntax表示语法有效的规范数量。数值越高越好。

这张表信息量非常大。看几个关键结论。

第一，语法就是第一道高墙。 Gemini 3 Pro Preview的语法通过率78.05%，GPT-5是67.07%，听着还行；但DeepSeek-V3.1只有7.93%，GPT-4o只有14.63%。大量规范压根活不到语义评估阶段。对弱模型来说，最大的问题不是“意图选错”，而是连Rocq的语法和类型规则都幻觉出了一堆错误。

第二，PASS_first到PASS_all的悬崖式下跌。 Gemini 3 Pro Preview的首例通过率60.98%，到全量正例通过直接跌到28.05%；GPT-5从60.98%跌到15.24%；Claude 3.7 Sonnet从15.24%跌到1.83%。这说明单个测试用例对规范的约束极其有限，大量规范只是“碰巧”过了第一个用例——全面测试套件才能把规范语义真正压实。

第三，Gemini的领先不是自卖自夸。 论文专门做了自验证对照：Claude 4.5 Opus用自己的验证器评估自己的规范，PASS_all只有10.98%，低于Gemini当验证器时的14.63%；GPT-5自验证7.32%，也明显低于Gemini验证时的15.24%。这说明Gemini的领先来自真实的证明和生成能力，而不是“自己给自己打分”的偏向。

而看到DeepSeek-V3.1以1.22%垫底、GPT-4o只有4.27%时，龙哥的表情如上。这个差距比代码生成领域拉得大得多，说明规范生成对模型的逻辑精确性要求更苛刻，不是“多背几道题”就能蒙混过关的。

再把候选规范拿出来做交集分析，还能看到更多细节：

图5：各模型在候选规范生成任务上的表现。(a) 对角线为各模型候选规范总数，非对角线为两个模型的共享成功数；(b) 候选规范总数、对聚合集合的独有贡献数以及专属成功数。

Gemini 3 Pro Preview独占了19道题的规范生成，其他模型基本只有个位数到十几的独占贡献。即便要求最强的模型之间“联手”，候选规范集合也就59道——连HumanEval的36%都不到。规范生成这类任务的水有多深，可见一斑。

规范生成更像数学还是代码？

看到表2里一片惨淡的数据，一个尖锐的问题浮现出来：规范生成失败，到底是模型写得不好，还是验证器的证明能力跟不上？这两者纠缠在一起，正是“评估二象性”的核心矛盾。论文专门设计了一个消融实验来拆解：

基线是“每个模型自己生成规范+自己验证”（Self-Verify + Self Spec）。然后做两个单点干预：一个是把验证器换成更强的Gemini 3 Pro Preview（Gemini-Verify + Self Spec），另一个是把LLM生成规范换成人类参考规范（Self-Verify + Human Spec）。

图2：规范质量与验证能力解耦的消融实验。相比Self-Verify + Self Spec基线，使用人类编写的规范平均提升+5.01%，而将自验证替换为更强的验证器平均提升+3.05%。两者都显著影响最终性能。

结果很清晰：换更好的规范带来+5.01%的提升，换更强的验证器带来+3.05%的提升。这说明在当前阶段，规范生成能力本身是比证明能力更主要的瓶颈，但验证能力的影响也不容忽视。换句话说，LLM写规范这件事，既不是纯数学（逻辑公式推导），也不是纯代码（API调用和类型构造），而是两者的混合体——既要有能力表达出精确的语义，又要有能力驾驭Rocq的语言机制把它写对。

把这个问题放到更大的背景里看更有意思。论文把模型在代码生成（LiveCodeBench、SWE-bench Verified）、数学推理（AIME 2025）和形式化规范生成（Syntax、Reject All）上的表现放在一起对比：

图7：模型在代码生成（LiveCodeBench、SWE-bench Verified）、数学推理（AIME 2025）与形式化规范生成（Syntax和Reject All）上的表现对比。模型按发布时间倒序排列。

可以看到：在代码生成和数学推理上，各家模型虽然有差距，但至少都维持在一个可用的相对区间；而在规范生成上，最好和最差之间拉出了二十多倍的差距（28.05% vs 1.22%）。这说明规范生成是一个独立的、比通用代码生成更陡峭的能力维度，不能拿代码榜的排名直接外推。

可执行组件的重要性：Fixpoint的妙用

在Rocq里写规范，不可避免要处理归纳结构。论文发现有三种主流写法：一是直接用标准库的内置高阶函数，比如length、fold；二是用户自定义Fixpoint递归函数；三是用户自定义Inductive归纳谓词。

其中最关键的区别在于“可执行性”。Fixpoint是计算性的——它在Rocq内部可以实际运行；而Inductive谓词是纯逻辑关系，没有计算内容。一个规范里可以同时混用这两种组件，所以“规范是否可执行”并不是一个良定义的概念。但这并不妨碍我们观察一个具体问题：LLM到底会不会用Fixpoint？

图3：规范中Fixpoint的使用频率对比。LLM的使用比例（31–44%）与人类专家（39.6%）相当。

数据揭示了一条清晰的分界线：弱模型（GPT-4o、DeepSeek-V3.1、Claude 3.7 Sonnet）很少用Fixpoint，而强模型（Gemini 3 Pro Preview、GPT-5、Claude 4.5 Opus）的使用比例达到31–44%，与人类专家39.6%的水平基本持平。这说明前沿模型已经学会了在合适的场景用递归结构来表达复杂语义——因为Fixpoint可以精确地“计算”一个性质，比如“子序列的最大值”“逐位比较的结果”，这比绕开它、用手工定义的逻辑关系去“描述”要自然得多。

图4：禁止在人类规范中使用Fixpoint的影响（n=164）。禁用递归构造后，各项指标均出现大幅下降。

更有说服力的是图4：连人类专家写的规范，一旦被禁止使用Fixpoint，各项指标都会显著下滑。这说明递归构造不是“偷懒”的捷径，而是精确表达某些程序行为不可替代的工具。CLEVER基准之所以强制要求规范不可执行，本质上是为了防止在端到端代码合成时发生“规范泄漏”——规范里藏着实现细节，模型可以直接抄。但如果评估目的就是“规范质量”本身，那么一刀切禁止Fixpoint，只会人为抬高规范生成和证明的难度，并引入与语义无关的偏差。COINS在这一点上的处理显然更合理：提供两套版本（允许Fixpoint和禁止Fixpoint），供研究者在不同目标下使用。

另外，论文还对人类规范和LLM规范做了等价性分析：在29道两类规范都有的题目里，只有9道能证明两者等价。这从另一个侧面说明：LLM即使写对了规范，也往往和人类专家的写法路径不同——它们是“语义上正确、句法上另类”的解题者。

图6：人类规范（N_H=50）与LLM规范（N_L=59）的等价性分析。在29个重叠问题中，只有9个问题产生了可证明等价的规范。

未来展望：从HumanEval到工业级验证

COINS的贡献不只是抛出一个评测框架，更在于它给出了一个可操作的“规范质量”度量标准——测试用例实例化+形式化证明。这个思路让规范评估从“全量等价证明不可行”的泥潭里走了出来，变成一套有明确正负反馈的工程流程。论文也公开了全部164个人类书写的Rocq规范套件，这是目前HumanEval上首套完整的形式化规范集合，仅此一点就有很高的复用价值。

但要清醒地看到局限。HumanEval的164道题属于典型的“小算法题”，而工业级形式化验证面对的是指针别名、循环不变式、并发协议、模块化接口这些更高维度的复杂性。COINS目前统一使用Prop签名，只覆盖输入输出的功能性关系，还没有涉及语言相关的内存契约、异常行为等。另外，COINS的评估精度仍受限于LLM的证明能力——Gemini 3 Pro Preview在人类规范上的PASS_all也才29.88%，这意味着大量规范可能因为“证明不出来”而被误杀。论文把这一点当作已知边界，而不是回避它，这种诚实是值得肯定的。

未来要往工业级走，有三条路值得关注。其一是把证明合成能力做得更强，比如引入更自动化的策略搜索或hammer工具，降低对LLM证明能力的依赖；其二是把评估范围扩展更复杂的数据结构和规范模式，甚至引入并发或指针程序；其三是把“规范生成”和“规范评估”做成闭环——用COINS这种测试用例驱动的方式持续筛选高质量规范，反过来再作为数据增强来训练模型。只要规范生成这个环节被攻破，形式化验证从“专家奢侈品”变成“工程师日用品”的那一天就不远了。

对普通读者来说，这篇文章最大的启示或许是：大模型的“聪明”是有边界形状的。它可能很会写代码、很会做题，但面对需要精确逻辑约束的规范生成时，它的表现可能让所有人大跌眼镜。理解这个边界，比盲目崇拜大模型的能力重要得多。

龙迷三问

下面是龙哥对于大家可能的一些问题的解答：

这篇论文到底在解决什么问题？针对LLM生成正式程序规范的能力评估难题，论文提出COINS框架，基于Rocq证明助手、以测试用例实例化检验规范质量，并构建HumanEval首个完整Rocq规范套件。

这篇工作最值得看的点是什么？Gemini 3 Pro Preview在REJECT_all上达到28.05%的最佳性能，而DeepSeek-V3.1仅为1.22%，展示了显著的模型间性能差距。

这篇工作的边界或风险在哪里？优点：(1)提出了创新的评估框架，避免了全等证明的困难；(2)构建了首个完整的HumanEval Rocq规范套件；(3)通过测试用例基础的形式推理提供了可靠且可区分的评估信号。缺点：(1)仅覆盖Rocq和HumanEval，泛化性有限；(2)依赖LLM作为证明器，证明能力本身成为瓶颈；(3)负例拒绝阶段依赖LLM判断，可能引入偏差。

如果你还有哪些想要了解的，欢迎在评论区留言或者讨论~

龙哥点评

论文创新性分数：★★★★☆

用“测试用例实例化+形式化证明”评估规范质量，绕开等价性证明死胡同，思路新颖且工程可行。

实验合理度：★★★★☆

研究问题设计递进（RQ1→RQ4），有消融、自验证对照、正负例双重约束，数据可信；但负例拒收依赖LLM“判断拒绝”再决定是否构造证明，这一步有主观性。

学术研究价值：★★★★☆

提出“评估二象性”并给出实践解法，为后续规范评估研究提供统一范式；HumanEval上首套完整Rocq规范套件也是高价值资产。

稳定性：★★★☆☆

方法本身稳定，但结果高度依赖LLM证明能力；换一个代际的模型或不同的提示词，绝对数值可能明显浮动，横向排序相对可靠。

适应性以及泛化能力：★★★☆☆

框架设计可推广到其他证明助手和任务，但当前实验限定在HumanEval的简单算法题和统一Prop签名上，距离复杂程序仍有明显距离。

硬件需求及成本：★★★★☆

主要成本是调用商用LLM API，加上Rocq编译器本地跑证明，整体开销可控；大规模全量测试证明时并发会提高成本，但并不离谱。

复现难度：★★★★☆

代码已开源，164个人类规范套件公开，按文档配置好Rocq和API即可复现；只需注意不同Rocq版本的兼容性细节。

产品化成熟度：★★☆☆☆

当前定位是研究评估框架，不是直接可用的验证工具。但其中“测试用例驱动筛选规范”的思路，对做形式化验证平台的同学有直接借鉴意义，离产品化还有一段路。

可能的问题：负例拒收阶段LLM先“判断”再决定是否证明，给评估引入了主观性；PASS_all复用首个证明的结构模式，可能不够普适；变异测试只能生成有限的负例，对特别隐蔽的过宽规范仍可能漏检。

主要参考文献

[1] Yang F, Li X, Wang S, et al. How Powerful Are LLMs in Generating Formal Program Specifications?[J]. arXiv preprint arXiv:2608.13077v1, 2026.

[2] Chen M, Tworek J, Jun H, et al. Evaluating Large Language Models Trained on Code[J]. arXiv preprint arXiv:2107.03374, 2021. (HumanEval)

[3] Thakur A, et al. CLEVER: An End-to-End Benchmark for Specification Generation and Verification[C]. 2025.

[4] Leroy X, et al. The CompCert C Compiler[R]. 2016.

[5] De Moura L, et al. The Lean Theorem Prover[C]. CADE 2015.

[6] Huet G, et al. The Coq Proof Assistant[R]. 1997.

*本文仅代表个人理解及观点，不构成任何论文审核或者项目落地推荐意见，具体以相关组织评审结果为准。欢迎就论文内容交流探讨，理性发言哦～想了解更多原文细节的小伙伴，可以点击"阅读原文"，查看更多原论文细节哦！

规范生成路漫漫，AI写码容易、写对难，欢迎进群一起讨论形式化验证与大模型的新进展～
欢迎加入龙哥读论文粉丝群，扫描下方二维码或者添加龙哥助手微信号加群：kangjinlonghelper。一定要备注：研究方向+地点+学校/公司+昵称（如程序验证+北京+中科院+小王），根据格式备注，可更快被通过且邀请进群。
『龙哥读论文』微信群目前包含：图像处理、大模型及智能体、自动驾驶及机器人、AI医疗及AI金融5个群
wechat_helper