VeriContest

VeriContest是一个用于Rust中可验证代码生成的大规模竞争性编程基准测试，包含946个主要基准问题（690个来自LeetCode，256个来自Codeforces），每个问题都配有自然语言描述、专家验证的形式规范、裁判接受的Rust代码和Verus验证的证明，以及全面的正面和负面测试套件。

VeriContest is a large-scale competitive programming benchmark for verifiable code generation in Rust. It includes 946 core benchmark problems, of which 690 are sourced from LeetCode and 256 from Codeforces. Each problem is accompanied by natural language descriptions, expert-validated formal specifications, judge-accepted Rust code, Verus-verified proofs, as well as comprehensive positive and negative test suites.

原始信息汇总

VeriContest 数据集详情

数据集概述

VeriContest 是一个面向 Rust 语言（使用 Verus 验证框架）的可验证代码生成的竞赛编程基准数据集。该数据集随论文 "VeriContest: A Competitive-Programming Benchmark for Verifiable Code Generation"（arXiv:2605.08553）一同发布。

数据集规模

• 主基准问题总数：946 个
  • LeetCode 问题：690 个
  • Codeforces 问题：256 个
• 扩展问题：61 个（经验证但未纳入主基准）

数据集结构

仓库目录布局

benchmark/ codeforces/ # 256 个 Codeforces 主基准问题 leetcode/ # 690 个 LeetCode 主基准问题 extended/ # 61 个经验证但未纳入主基准的问题

每个问题目录包含的文件

每个问题目录（如 benchmark/codeforces/cf1006C/）包含以下文件：

文件名	说明
description.md	来自 LeetCode 或 Codeforces 的自然语言问题描述，包含用于评估的起始代码
tags	元数据（问题ID、难度等级、通过率、算法标签等）
spec.rs	真实形式化规范，包含前置条件和后置条件
code.rs	经在线评测系统接受的真实 Rust 代码
code_spec.rs	用于证明生成任务的代码与规范组合文件
verified.rs	完整的 Verus 验证程序（包含规范、代码和证明）
main.rs	仅 Codeforces 问题包含，用于标准输入/输出处理的可执行入口

数据集的额外资源

完整的测试用例文件（包括正面和突变负面测试用例）可在 Hugging Face 上获取：Gax-c/VeriContest

评估任务

VeriContest 支持以下四种评估模式：

1. SpecGen：从自然语言问题描述生成形式化规范
2. CodeGen：从自然语言、规范或两者生成可执行的 Rust 代码
3. ProofGen：在规范和执行代码固定的情况下生成 Verus 证明
4. End2End：生成完整的验证 Verus 程序（包含规范、执行代码和证明）

数据构建流程

数据集通过三阶段管道构建：

1. 手动验证种子问题：91 个经过手动构建的种子问题，包含完整规范、Rust 代码和 Verus 证明
2. 半自动扩展：通过人机协作的半自动生成，将基准扩展至 946 个问题
3. 测试用例生成与验证：从验证程序中生成正面和负面测试用例，验证后置条件完整性

质量控制维度

每个基准实例至少经过两位人类专家审查，确保：

• 代码正确性与效率：所有代码提交至在线评测系统，确保在时间和内存限制内通过
• 规范可靠性：每个问题包含 Verus 证明，证明通过评测的代码满足规范
• 规范完整性：通过人工审查和负面测试用例自动检查后置条件
• 规范审查：人工审查以避免不必要的实现特定约束
• 高质量测试用例：包含全面的正面和负面测试用例

扩展问题说明

benchmark/extended/ 目录包含 61 个额外验证问题，因不适合仅依赖测试用例的评估管道而被排除。部分问题使用 &mut 等 Rust 模式，或允许多个可行输出，需自定义评测逻辑。

工具：Post2Exe

Post2Exe 是 VeriContest 使用的后置条件测试组件，能将支持的 Verus 后置条件转换为可执行 Rust 程序并在负面测试用例上运行。它依赖于外部开源解析器 secure-foundations/tree-sitter-verus。

许可证

• Apache-2.0：仓库代码和工具（包括 Post2Exe）
• CC-BY-4.0：VeriContest 原创的基准数据（规范、证明、测试、元数据和数据集组织）
• 问题描述：来源于 LeetCode 和 Codeforces，受各自源条款约束

搜集汇总

数据集介绍

构建方式

VeriContest的构建遵循一个严谨的三阶段流水线。首先，研究团队手工构建了91个经过严格验证的种子问题，确保每个问题都包含完备的形式规约、经在线评测系统接受的Rust代码以及通过Verus验证的证明。随后，通过半自动生成与人工循环审查相结合的方式，将基准规模扩展至946个问题。最后，从已验证的程序中生成阳性及阴性测试用例，用于进一步验证后置条件的完备性并评估模型生成的代码与规约的质量。每条基准实例均经由至少两位人类专家在代码正确性、规约可靠性、规约完备性、规约审查及测试用例质量五个维度上进行质量把关。

特点

该数据集的核心特色在于其专注于可验证代码生成领域，精心设计了四大评测任务：从自然语言描述生成形式规约（SpecGen）、根据自然语言或规约生成可执行代码（CodeGen）、在给定规约与代码的条件下生成Verus证明（ProofGen），以及端到端生成包含规约、代码和证明的完整已验证程序（End2End）。数据集囊括了690道来自LeetCode和256道来自Codeforces的题目，并附有计划外的一组扩展问题。此外，数据集包含了全面的阳性与突变阴性测试用例文件，以支持对代码正确性和规约完备性的深度评估。

使用方法

使用者可以通过Hugging Face平台获取包含完整测试用例的数据集，而GitHub仓库则提供了便于审查的题目工件、规约、代码、证明及工具。基准测试的主干部分位于benchmark/codeforces/与benchmark/leetcode/目录下，共包含946道题目。每个题目目录内包含了自然语言描述、元数据标签、正式规约、评测通过的代码、规约与代码的混合文件、完整的Verus验证程序，以及Codeforces题目特有的输入输出处理文件。对于扩展问题目录下的61道题目，由于需要自定义评测逻辑，它们虽不纳入主基准测试，但仍作为有价值的已验证Verus示例供学习与未来扩展使用。

背景与挑战

背景概述

VeriContest是一个面向可验证代码生成的竞争性编程基准，创建于2026年，由Xie Zichen、Mrigank Pawagi等研究人员共同开发，相关论文发表于arXiv。该数据集的核心研究问题在于评估和推动大语言模型在生成经过形式化验证的代码方面的能力，特别是在Rust语言和Verus验证框架下。VeriContest包含946个主基准问题，其中690个源自LeetCode，256个源自Codeforces，每个问题都配有自然语言描述、专家验证的形式规约、评测认可的Rust代码以及Verus证实的正确性证明。该基准在可验证代码生成领域具有重要影响力，为SpecGen、CodeGen、ProofGen和端到端生成等任务提供了统一的评估平台，填补了现有基准在可验证性评估方面的空白。

当前挑战

VeriContest所解决的领域问题核心挑战在于如何确保自动生成的代码不仅功能正确，而且满足严格的形式化规约，即代码的可验证性。当前面临的挑战包括：1) 规约的完备性与无偏性：需要确保后置条件全面覆盖所有正确行为，同时避免引入不必要的实现约束，这要求人工与自动化检测相结合。2) 构建过程中的质量控制：基准通过人工验证的种子问题（91个）和半自动化扩展（946个）构建，每个实例需经过至少两位专家审查，涉及代码正确性、规约可靠性、测试用例质量等多维度评估，过程极为耗时。3) 测试用例的生成与验证：基于后置条件自动生成的正面和负面测试用例需能有效检测代码缺陷，但处理无界量词等复杂后置条件时仍需人工介入。4) 扩展问题的局限性：部分问题因涉及可变引用或多可行输出，难以通过简单字符串比较判断正确性，需要定制化评判支持，限制了基准的规模扩展。

常用场景

经典使用场景

VeriContest作为面向可验证代码生成的竞赛编程基准，最经典的使用场景涵盖两大竞技编程平台——LeetCode与Codeforces上的946道精选题目。研究者可利用该基准系统评估大语言模型在四种核心任务上的表现：从自然语言描述生成形式规约（SpecGen），依据自然语言或规约生成可执行Rust代码（CodeGen），在给定规约与代码条件下生成Verus证明（ProofGen），以及端到端生成包含规约、代码与证明的完整可验证程序（End2End）。基准精心配备了专家验证的原子化规约、经在线评测系统通过的精确代码及经过Verus形式化验证的证明文件，为可验证代码生成研究构建了标准化、可复现的评测框架。

衍生相关工作

VeriContest的发布催生了一系列富有影响力的衍生工作。其核心设计理念被后续研究借鉴，例如将形式规约生成与代码证明解耦的评估范式启发了多个面向特定领域的可验证代码基准构建工作。基准中验证过的正负测试用例与Post2Exe后置条件检验工具促进了规约完备性自动检测技术的革新，推动了诸如自适应测试用例生成及量词感知规约分析工具的发展。同时，VeriContest的大规模标注数据为模型微调与提示工程提供了宝贵资源，支撑了若干在形式化验证辅助代码生成领域的实证研究，包括链式推理增强、少样本证明合成及跨语言可验证程序迁移等前沿课题。

数据集最近研究

最新研究方向

VeriContest专注于可验证代码生成领域，通过构建包含946个竞赛编程问题的大规模基准，推动形式化验证与大语言模型的深度融合。该数据集覆盖LeetCode与Codeforces平台，提供专家验证的形式规约、可执行代码及Verus证明，支持规约生成、代码生成、证明生成及端到端验证任务。其研究前沿聚焦于利用负测试用例与Post2Exe工具自动化检测规约完备性，确保生成代码满足严格形式化约束。这一工作为提升AI生成软件的安全性与正确性奠定了重要基础，尤其在自动驾驶、医疗系统等高可靠性场景中具有深远意义。