LLM 在生成正式程序规范方面有多强大？

形式验证为软件正确性提供了强有力的保证，但其采用受到编写精确形式规范的高成本的限制。虽然最近的 大语言模型 (LLM) 在定理证明和验证代码生成方面表现出了强大的能力，但它们生成程序规范的真正能力仍不清楚。现有的评估需要验证实现一致性或证明规范之间的语义等效性，这两者都非常困难，并且可能会将证明难度与规范质量混为一谈。为了解决这个问题，我们引入了 Coins，这是一个基于 Rocq 的评估框架，它通过在受信任的测试用例上实例化评估规范并生成具体的证明义务来评估规范质量。这种设计符合形式推理的不对称性质，成功的证明提供可靠的证据，而证明失败本质上是不明确的。我们使用 Coins 对 HumanEval 进行了大规模研究，并使用了一组精选的人类编写的 Rocq 规范。我们的结果表明，规范生成仍然是一个艰巨的挑战，验证的复杂性可能会掩盖规范质量的真正差异。总体而言，我们发现准确的规范评估（而不是单独的模型缩放）对于理解 LLM 在规范综合方面的强大功能至关重要，并且基于测试用例的形式推理提供了更忠实和更具辨别力的进度衡量标准。