Title: VeriEquivBench: An Equivalence Score for Ground-Truth-Free Evaluation of Formally Verifiable Code Show Chinese title

Title: VeriEquivBench：一种用于无真实值评估形式可验证代码的等价分数

Abstract: 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. Show Chinese abstract

Abstract: 形式化验证是确保由大型语言模型（LLMs）生成的代码正确性的下一个前沿领域。 虽然在形式语言中共同生成代码和形式规范的方法，如Dafny，原则上可以证明与用户意图的一致性，但进展受到规范质量评估的瓶颈限制。 当前的基准测试依赖于与真实规范的匹配，这是一个手动且需要专业知识的过程，使得现有数据集仅限于几百个简单问题，并且也存在可靠性问题。 为了解决这个问题，我们引入了VeriEquivBench，一个新的基准测试，包含$2,389$个复杂的算法问题，用于探测当前模型在代码生成和形式推理方面的局限性。 我们的评估框架用一个形式基础的度量标准——等价分数，取代了真实规范匹配，并严格验证了生成的规范和代码的质量。 我们的结果表明，生成可形式化验证的代码仍然是最先进的LLMs面临的重大挑战。 这突显了任务的难度以及需要类似VeriEquivBench的基准测试来推动可扩展和可靠的编码代理的发展。