VeriEquivBench: An Equivalence Score for Ground-Truth-Free Evaluation of Formally Verifiable Code

📄 arXiv: 2510.06296v1 📥 PDF

作者: Lingfei Zeng, Fengdi Che, Xuhan Huang, Fei Ye, Xu Xu, Binhang Yuan, Jie Fu

分类: cs.PL, cs.AI

发布日期: 2025-10-07

💡 一句话要点

提出VeriEquivBench基准，用于无ground-truth评估形式化可验证代码的等价性。

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 形式化验证 代码生成 大型语言模型 基准测试 等价性评估

📋 核心要点

  1. 现有代码生成评估依赖人工标注的ground-truth规范，成本高且规模受限，难以评估复杂算法。
  2. VeriEquivBench提出基于形式化验证的等价性得分，无需ground-truth即可评估代码和规范的质量。
  3. 实验表明，当前LLM在生成形式化可验证代码方面仍面临挑战，凸显了新基准的价值。

📝 摘要（中文）

形式化验证是确保大型语言模型（LLM）生成的代码正确性的下一个前沿。虽然协同生成代码和形式化规范（如Dafny）的方法原则上可以证明与用户意图的一致性，但规范质量评估的瓶颈限制了进展。目前的基准依赖于与ground-truth规范的匹配，这是一个手动且需要专业知识的过程，这限制了现有数据集的规模，仅包含几百个简单问题，并且存在可靠性问题。为了解决这个问题，我们引入了VeriEquivBench，这是一个新的基准，包含2389个复杂的算法问题，用于探测当前模型在代码生成和形式推理方面的局限性。我们的评估框架用形式化基础的度量标准——等价性得分——取代了ground-truth匹配，并严格验证了生成的规范和代码的质量。我们的结果表明，生成形式化可验证的代码对于最先进的LLM来说仍然是一个深刻的挑战。这突显了任务的难度，以及像VeriEquivBench这样的基准对于推动可扩展和可靠的编码代理的进步的必要性。

🔬 方法详解

问题定义：现有评估LLM生成代码和形式化规范的方法主要依赖于与人工标注的ground-truth规范进行匹配。这种方法存在几个痛点：一是标注过程需要大量的人工和专业知识，成本高昂；二是现有数据集规模有限，难以覆盖复杂的算法问题；三是ground-truth规范本身可能存在错误或不完整，影响评估的可靠性。因此，需要一种无需ground-truth即可评估代码和规范质量的方法。

核心思路：VeriEquivBench的核心思路是利用形式化验证技术来评估代码和规范的等价性。具体来说，给定一个问题描述，LLM生成代码和形式化规范。然后，使用形式化验证工具（如Dafny）来验证生成的代码是否满足生成的规范。如果代码满足规范，则认为代码和规范是等价的，并给出一个等价性得分。这种方法无需人工标注的ground-truth规范，可以自动评估代码和规范的质量。

技术框架：VeriEquivBench的整体框架包括以下几个主要模块：1) 问题生成模块：生成包含2389个复杂算法问题的测试集。2) 代码和规范生成模块：使用LLM生成代码和形式化规范。3) 形式化验证模块：使用Dafny等形式化验证工具验证代码是否满足规范。4) 等价性评估模块：根据验证结果计算等价性得分。

关键创新：VeriEquivBench最重要的技术创新点是提出了基于形式化验证的等价性得分，用于无ground-truth评估代码和规范的质量。与现有方法相比，该方法无需人工标注的ground-truth规范，可以自动评估代码和规范的质量，并且可以应用于更复杂的算法问题。

关键设计：VeriEquivBench的关键设计包括：1) 使用Dafny作为形式化验证工具，因为它具有强大的表达能力和自动化验证能力。2) 设计了一套评估指标，包括等价性得分、验证时间和资源消耗等，用于全面评估代码和规范的质量。3) 构建了一个包含2389个复杂算法问题的测试集，用于评估LLM在代码生成和形式推理方面的能力。

🖼️ 关键图片

img_0

📊 实验亮点

实验结果表明，当前最先进的LLM在VeriEquivBench上的表现仍然不佳，生成的代码和规范的等价性得分较低，验证成功率不高。这表明生成形式化可验证的代码对于LLM来说仍然是一个巨大的挑战，同时也突显了VeriEquivBench作为评估和改进LLM代码生成能力的重要工具的价值。

🎯 应用场景

VeriEquivBench可用于评估和改进LLM在代码生成和形式推理方面的能力，推动可信AI的发展。该基准可以应用于软件工程、安全关键系统、智能合约等领域，提高代码的可靠性和安全性，降低开发和维护成本。未来，可以扩展到更复杂的领域和编程语言。

📄 摘要（原文）

Formal verification is the next frontier for ensuring the correctness of code generated by Large Language Models (LLMs). While methods that co-generate code and formal specifications in formal languages, like Dafny, can, in principle, prove alignment with user intent, progress is bottlenecked by specification quality evaluation. Current benchmarks rely on matching against ground-truth specifications, a manual and expertise-intensive process that has limited existing datasets to a few hundred simple problems and also suffers from a reliability issue. To address this, we introduce VeriEquivBench, a new benchmark with $2,389$ complex algorithmic problems that probe the limitations of current models in both code generation and formal reasoning. Our evaluation framework replaces ground-truth matching with a formally grounded metric, the equivalence score, and rigorously verifies the quality of generated specifications and code. Our results show that generating formally verifiable code remains a profound challenge for state-of-the-art LLMs. This underscores both the difficulty of the task and the need for benchmarks like VeriEquivBench to drive progress toward scalable and reliable coding agents.