近日，华中科技大学软件学院 2022 级本科生曾凌飞同学以共同第一作者身份参与完成的学术论文"VeriEquivBench: An Equivalence Score for Ground-Truth-Free Evaluation of Formally Verifiable Code"被第十四届国际学习表征会议（The Fourteenth International Conference on Learning Representations, ICLR 2026）录用并发表。论文由曾凌飞、车枫荻等合作完成，相关研究工作在上海人工智能实验室付杰老师指导下开展。

ICLR是机器学习和人工智能领域具有重要影响力的国际学术会议之一，长期汇聚表示学习、深度学习、大语言模型与智能体等方向的前沿研究成果，是学术界和工业界广泛关注的重要交流平台。该论文被 ICLR 2026 录用，体现了相关研究在coding agent、形式化验证与自动化评测方向的创新性和学术价值。

论文简介

论文题目：VeriEquivBench: An Equivalence Score for Ground-Truth-Free Evaluation of Formally Verifiable Code

研究方向：

随着大语言模型在代码生成任务中表现不断提升，如何可靠判断生成代码是否真正符合用户意图，成为人工智能在工业界落地的重要问题。传统代码评测通常依赖单元测试，但单元测试覆盖不足时难以提供严格的正确性保证；形式化验证可以借助Dafny等工具证明代码与形式化规约之间的一致性，但现有评测基准大多依赖人工编写的标准规约，存在标注成本高、专业门槛高、数据规模有限以及规约本身可能不完整或存在歧义等问题。

针对这一挑战，论文提出了 VeriEquivBench，一个面向形式化可验证代码生成的大规模评测基准，并提出无需依赖人工 ground-truth 规约的 equivalence score（等价性评分）。该指标通过 Dafny 验证器检查代码与形式化规约之间的双向蕴含关系：一方面验证代码是否满足规约，另一方面验证规约是否足够完整、能够精确刻画代码行为。只有当代码与规约在形式意义上相互等价时，生成结果才会获得等价性评分，从而缓解弱规约、错误规约以及“通过验证但并未真正满足需求”等评测漏洞。

在数据集构建方面，VeriEquivBench 包含 2,389 个复杂算法问题，并进一步构建了 1,678 个合成算法问题，覆盖自然语言描述、Python/Dafny 实现、单元测试、强弱两类形式化规约，以及难度、算法、数据结构等元信息。论文通过 LeetCode 题库转换和标签组合生成两条路径扩展数据规模，使评测问题在复杂度和多样性上显著高于以往依赖小规模人工标注的基准。

实验结果显示，当前先进大语言模型在端到端生成“可验证且与用户意图一致”的代码方面仍面临显著挑战。即便模型能够生成语法正确的 Dafny 代码，也很难同时保证代码、形式化规约和自然语言意图三者一致。该研究为高质量代码生成和先进 coding agent 评测提供了更强的自动化评测信号，也为后续构建大型Agentic RL系统提供了重要基础。

曾凌飞同学的这项研究聚焦大语言模型代码生成评测这一人工智能前沿问题，围绕形式化验证、自动化评测与智能代码生成机制开展深入探索，提出了兼具理论价值与应用潜力的评测基准及评分方法，彰显了软件学院学生在人工智能、形式化方法与软件工程交叉领域的科研创新能力和学术探索精神。

近年来，软件学院坚持紧跟软件技术前沿、对接国家战略需求，持续深耕人工智能、软件工程等方向的人才培养与科研实践，引导学生在真实科研场景中锤炼创新思维、攻坚能力与学术表达素养。未来，学院将继续以高质量人才培养为核心，鼓励更多青年学子勇闯国际学术前沿、敢攀科研创新高峰，为助力高水平科技自立自强、赋能数字中国建设贡献青春智慧与奋进力量。