提出无需真实规范的等价评分，评估大模型生成可形式化验证代码的能力
VeriEquivBench: An Equivalence Score for Ground-Truth-Free Evaluation of Formally Verifiable Code
- 用等价分数替代真实规范匹配，实现自动化评估
- 覆盖2389个复杂算法题，揭示当前大模型在形式推理上的不足
- 适合研究形式化验证与可信代码生成的学者使用
形式化验证是确保大语言模型生成代码正确性的关键前沿。尽管通过联合生成代码和形式语言（如Dafny）中的形式规范可在理论上证明与用户意图对齐，但进展受限于规范质量的评估。现有基准依赖与真实规范的匹配，该过程需人工且依赖专业知识，导致现有数据集仅涵盖数百个简单问题，且可靠性不足。为此，我们提出VeriEquivBench，一个包含2,389个复杂算法问题的新基准，用于探测当前模型在代码生成与形式推理方面的局限性。我们的评估框架以形式化基础的等价分数取代真实规范匹配，严格验证生成规范与代码的质量。结果表明，生成可形式化验证的代码对当前最先进的大模型仍是巨大挑战，凸显任务难度及类似VeriEquivBench类基准对推动可扩展、可靠的编码智能体发展的必要性。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。