VeriContest: A Competitive-Programming Benchmark for Verifiable Code Generation
本文介绍了 VeriContest，这是一个包含 946 个使用 Verus 编写的 Rust 竞赛编程问题的综合性基准测试，它将自然语言描述与专家验证的形式化规范及机器可验证的证明相结合，揭示了当前模型的编码能力与其生成可验证代码的能力之间存在显著差距。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
想象一下，你正在聘请一位才华横溢但缺乏经验的建筑师来建造一座房子。
在标准代码基准测试的世界里，你给这位建筑师一个简单的描述：“建造一座拥有三间卧室和一个厨房的房子。”建筑师绘制出蓝图，建造了房子，然后你检查门是否能打开、灯是否能亮。如果一切正常，建筑师就能获得及格分数。这就像当前的 AI 模型编写代码：它们非常擅长制造那些在外观和行为上看起来正确的东西。
但如果你需要一座即使在飓风中也能数学上保证永不倒塌的房子呢？你光检查灯是不够的；你需要一个形式化证明来证实结构的稳固性。这正是论文"VeriContest"登场之处。
问题：“它能运行，但它是真的吗？”
当前的 AI 模型就像那些有才华的建筑师，能建造出通过视觉检查的房子。然而，它们往往跳过了严谨的工程数学。它们可能会建造一座外观完好但地基存在隐藏缺陷的房子，而这类缺陷只有在特定压力下才会显现。
该论文的作者认为，我们需要一种测试 AI 的新方法。我们不应只问“代码能运行吗？”，而应问“你能以数学上的确定性证明，这段代码确实只做了它该做的事，且没有做任何多余的事吗？”
解决方案：VeriContest
团队创建了一场名为VeriContest的大型“考试”。你可以将其视为一场针对 AI 建筑师的高风险竞赛，但必须遵守三条严格规则：
- 蓝图（规范）： AI 必须首先编写一份数学合同。这不仅仅是一个描述；它是一套严格的规则，精确定义输入是什么以及输出必须是什么。
- 施工（代码）： AI 必须编写遵循这些规则的实际代码（使用 Rust 编程语言）。
- 工程证明（验证）： AI 必须提供数学证明，表明代码不可能失败。这就像展示证明屋顶不会掉落的数学推导，而不仅仅是希望它不掉。
他们在来自著名编程竞赛（LeetCode 和 Codeforces）的946 道难题上测试了这一方法。这些可不是简单的“你好，世界”任务；它们是涉及数据模式查找或路径优化等内容的复杂逻辑问题。
构建过程
构建这场考试非常困难。团队并没有只是让 AI 出题，而是分三个阶段构建：
- 阶段 1（种子）： 人类专家手动编写了 91 个带有完美证明的完美示例。
- 阶段 2（扩展）： 他们利用 AI 助手生成更多问题，但人类专家充当“编辑”，检查每一个问题，确保数学正确无误。
- 阶段 3（压力测试）： 他们创建了“负面测试用例”——旨在欺骗 AI 的场景。如果 AI 的证明不完整，这些陷阱题就会暴露其缺陷。
结果：巨大的差距
当他们让世界上最聪明的 AI 模型参加这场考试时，结果令人惊讶且严峻。
- “普通”测试： 当仅要求根据描述编写代码（无需证明）时，最佳 AI 的准确率达到92%。它是一位精通建造的工匠。
- “蓝图”测试： 当要求编写数学合同（规范）时，得分降至48%。AI 难以精确地定义规则。
- “证明”测试： 当要求提供代码有效的数学证明时，得分暴跌至14%。AI 无法承担繁重的数学工作。
- “全考”（端到端）： 当要求一次性完成所有三个步骤（蓝图 + 代码 + 证明）时，最佳 AI 的成功率仅为5.3%。
类比：“完美的房子”
想象 AI 是一位厨师。
- 标准编码： 你点了一份汉堡。厨师做了一份味道不错的汉堡。你吃掉了它。成功！
- 可验证编码： 你点了一份汉堡，但你还要求提供一份证书，证明肉类来自特定农场，面包是在恰好 350 度下烘烤的，且汉堡中不含任何隐藏过敏原。厨师能做出汉堡，但他们非常不擅长撰写证书或证明烹饪过程背后的数学原理。
结论
该论文得出结论，虽然 AI 在“猜测”能让程序运行的正确代码方面变得越来越擅长，但在证明代码正确性方面仍然非常糟糕。最大的瓶颈不在于编写代码，而在于编写形式化规则和数学证明，以保障代码的安全性。
VeriContest 现在已成为研究人员的一项工具，用于精确衡量 AI 在达到能够被信任地构建数学上保证无缺陷的软件之前，还有多远的路要走。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。