AI 中文总结
该研究引入基于Rocq的Coins评估框架，在HumanEval数据集上开展大规模研究，发现LLMs生成形式化程序规约仍具挑战，准确的规约评估是理解其能力的核心。
AI 中文摘要
形式化验证可为软件正确性提供强保证，但其应用受限于编写精确形式化规约的高成本。尽管近期大型语言模型（LLMs）在定理证明和已验证代码生成方面展现出强大能力，但其生成程序规约的真实能力仍不明确。现有评估要么需要验证实现一致性，要么需要证明规约间的语义等价性，两者都极为困难，且可能混淆证明难度与规约质量。为解决该问题，我们引入Coins，一个基于Rocq的评估框架，通过在可信测试用例上实例化待评估规约并生成具体证明义务来评估规约质量。该设计契合形式化推理的非对称特性：成功的证明提供可靠证据，而证明失败本质上具有歧义性。我们使用Coins在HumanEval数据集上开展大规模研究，该数据集包含经精心筛选的人工编写Rocq规约。结果显示，规约生成仍是一项艰巨挑战，且验证复杂性会掩盖规约质量的真实差异。总体而言，我们发现准确的规约评估（而非仅模型缩放）是理解LLMs规约合成能力的核心，基于测试用例的形式化推理能提供更可靠、更具区分度的进展衡量标准。
英文摘要
Formal verification provides strong guarantees of software correctness, but its adoption is limited by the high cost of writing precise formal specifications. While recent large language models (LLMs) have shown strong capabilities in theorem proving and verified code generation, their true ability to generate program specifications remains unclear. Existing evaluations require either verifying implementation conformance or proving semantic equivalence between specifications, both of which are formidably difficult and may conflate proof difficulty with specification quality. To address this problem, we introduce Coins, a Rocq based evaluation framework that assesses specification quality by instantiating specifications under evaluation on trusted test cases and generating concrete proof obligations. This design aligns with the asymmetric nature of formal reasoning, where successful proofs provide reliable evidence while proof failures are inherently ambiguous. Using Coins, we conduct a large scale study on HumanEval with a curated set of human written Rocq specifications. Our results show that specification generation remains a formidable challenge, and that verification complexity can obscure genuine differences in specification quality. Overall, we find that accurate specification evaluation, rather than model scaling alone, is central to understanding the power of LLMs for specification synthesis, and that test case based formal reasoning offers a more faithful and discriminative measure of progress.
