VeriEquivBench：一种无需真实地面真相的正式可验证代码评估等价分数
VeriEquivBench: An Equivalence Score for Ground-Truth-Free Evaluation of Formally Verifiable Code
AI总结：
本文提出VeriEquivBench，通过2389个复杂算法问题评估正式可验证代码的生成与推理能力，揭示当前LLM在生成正式规范和代码方面的挑战，推动可扩展可靠编码代理的发展。
摘要：
形式验证是确保大型语言模型生成代码正确性的前沿领域。尽管像Dafny这样的方法可以共生成代码和形式规范，但规范质量评估成为瓶颈。现有基准依赖于与真实规范匹配，这一手动且专家密集的过程限制了现有数据集仅包含几百个简单问题，并存在可靠性问题。为此，我们引入VeriEquivBench，一个包含2389个复杂算法问题的新基准，测试当前模型在代码生成和形式推理方面的局限性。我们的评估框架用正式 grounded 的指标等价分数取代真实匹配，并严格验证生成的规范和代码质量。我们的结果表明，生成正式可验证代码仍然是最先进的LLM的深刻挑战。这突显了该任务的难度以及需要像VeriEquivBench这样的基准来推动向可扩展和可靠编码代理发展的重要性。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
