PBT-Bench: Benchmarking AI Agents on Property-Based Testing¶
会议: NeurIPS 2026
arXiv: 2605.15229
OpenReview: https://openreview.net/forum?id=wota1ZN4By
代码: https://github.com/ElliotXinqiWang/PBTbench
领域: 其他
关键词: 基于属性的测试, 软件工程, 代码智能体, 评测基准, 语义不变量
一句话总结¶
针对现有代码评测基准仅衡量具体用例重现或补丁生成、无法考核抽象不变量检验能力的缺陷，本文提出了首个专注于基于属性测试（PBT）的评测基准 PBT-Bench，涵盖 40 个真实 Python 库的 100 个问题与 365 个精心设计的隐蔽语义缺陷，配合双容器 \(F \to P\) 自动化评测框架，揭示了当代前沿大模型在文档抽象规则到定向输入生成上的关键能力短板。
研究背景与动机¶
大语言模型在基于具体输入输出样本的代码生成与单元测试合成基准上已展现出极高的通过率，然而在面对现实复杂软件系统的抽象规范时，模型的表现却显著恶化。现实工程中的核心契约往往不是单点输入输出，而是跨整个输入分布普遍成立的语义不变量（如往返一致性、代数交换律、单调性与状态机协议）。基于属性的测试（Property-Based Testing, PBT）正是通过声明通用谓词并由类型化随机输入生成器进行对抗性空间探索，来检验此类不变量的工业界关键测试范式。然而，编写高质量 PBT 测试需要程序员从文档中提炼抽象不变量并构造能击中罕见边缘条件的生成分布，这一认知壁垒正是智能体亟需辅助却从未被单独量化评测的盲区。
现有的代码智能体基准无法有效隔离出 PBT 这一独特技能。SWE-bench 侧重于给定缺陷报告后生成修复补丁，SWT-Bench 和 TestExplora 虽然评估测试生成，但其依赖真实开源项目 PR 挖掘的缺陷分布中充斥着大量依赖具体断言、I/O 耦合、数据库状态或 UI 渲染的非 PBT 可测问题；而基于代码变异（Mutation Testing）的评估则主要依赖机械生成的简单语法变异体，无法模拟深藏于复杂调用链下方、且能绕过现有测试套件的真实语义逻辑漏洞。直接采用挖掘的 PR 缺陷会严重混淆智能体“面对非 PBT 缺陷的规避试错”与“真正的 PBT 不变量建模能力”。
本文的切入角度是：必须摆脱直接挖掘开源 PR 的被动范式，针对 PBT 的形式化特性专门构建语义受控且经严格审查的高质量缺陷基准。通过严格定义语义性、可表达性、隐蔽性与确定性触发等测试准入条件，构建以官方文档为唯一准则（Oracle）的标准化评测场景。核心 idea：构建首个面向代码智能体基于属性测试能力的基准 PBT-Bench，精选 40 个真实 Python 库中的 100 个问题并注入 365 个按三级难度分层的隐蔽语义缺陷，设计双容器可逆补丁 \(F \to P\) 自动化裁判框架，全面评测大模型从文档提炼不变量并合成定向 Hypothesis 输入生成器的能力。
方法详解¶
整体框架¶
PBT-Bench 旨在评估代码智能体在仅给定代码库和官方 API 文档的条件下，能否通过阅读文档推导全局语义不变量，并编写基于 Hypothesis 框架的属性测试以暴露隐蔽语义缺陷。其整体流程由“受控基准构建”、“智能体测试生成”和“双容器单函数 \(F \to P\) 独立裁判”三个核心阶段组成。
%%{init: {'flowchart': {'rankSpacing': 24, 'nodeSpacing': 28, 'padding': 6, 'wrappingWidth': 400}}}%%
flowchart TD
A["输入：目标代码库 + 官方文档 docs/"] --> B["受控基准构建<br/>40个库/100个问题/365个注入缺陷/L1-L3分层"]
B --> C["智能体测试生成<br/>Baseline自由探索 vs PBT框架引导 Prompt"]
C --> D["双容器裁判环境<br/>Agent容器生成 pbt_test.py -> 隔离Eval容器"]
D --> E["可逆补丁独立裁判<br/>逐缺陷还原补丁并执行 F->P (有缺陷失败/修复后成功)"]
E --> F["输出：缺陷召回率 Recall / 覆盖率 / 提示收益 Delta"]在交互过程中，智能体首先在运行目标库和文档的 Agent 容器中工作，以只读文档为真实规范编写测试文件 /workspace/pbt_test.py。随后，系统进入独立的 Eval 容器，针对目标库中注入的每个独立可逆补丁，分别在存在缺陷的库版本和撤回单个补丁的修复版本上单独运行测试函数的断言。只有当某个测试函数在有缺陷版本上运行失败、且在撤回该缺陷补丁后运行通过时，该缺陷才被判定为成功捕获（\(F \to P\) 准则）。
关键设计¶
1. 严格筛选与分层的基于属性测试基准构建
针对挖掘缺陷无法保证 PBT 适用性的痛点，本文制定了四项严苛的筛选准则：语义性（违反文档明确声明的语义契约，而非未定义实现细节）、可表达性（可通过 Hypothesis 内置策略或 @composite 策略生成输入，无需 mock 文件或网络外部副作用）、隐蔽性（藏于公共 API 表面下至少两层调用链，不能通过简单代码静态走查识破）和确定性触发（存在明确输入子空间使得生成器能以概率 1 命中）。全量基准覆盖序列化、数据结构、日期时间、类型系统、数值计算、状态机和语法解析等 7 大领域的 40 个真实纯 Python 库。
每个缺陷按触发输入空间的复杂程度划分为三个难度等级：L1（单约束边界缺陷，共 87 个，占比 24%，默认生成策略边界探索或单一数值/类型约束即可触发）、L2（多约束联合触发缺陷，共 184 个，占比 50%，需同时满足多个文档派生条件如特定数值范围与结构拓扑）、L3（跨函数或跨操作协议违背，共 94 个，占比 26%，需执行多步 API 序列或变态测试/Metamorphic Testing）。所有问题经过三阶段质检流程：自动化检查（补丁干净应用、上游既有测试通过）、基准模型初筛（若 Claude Sonnet 4.6 与 GLM 5.1 单次运行均完全解决则淘汰）、人工对抗性审查，确保缺陷具有高度区分度。
2. 可逆补丁与双容器单函数级独立 F→P 评估判定
在真实软件测试评测中，多缺陷共存往往引发测试污染或相互掩盖。PBT-Bench 采用统一差异文件 bug_N.patch 引入可逆缺陷机制：默认镜像包含全部注入缺陷，而移除补丁 \(b_i\) 则直接恢复该缺陷对应的修复基准。同时，所有注入缺陷必须满足无污染通过准则（Clean-pass criterion），即目标库自带的原有单元测试在缺陷注入后依然 100% 全部通过，严格证明缺陷属于原测试套件未能覆盖的语义盲区。
评测调度采用物理隔离的双容器架构。Agent 容器在 OpenHands 环境下限制 200 次工具调用和 60 分钟时限，禁止联网；当智能体输出测试文件后，Eval 容器加载纯净备份并挂载测试，为每个注入缺陷 \(b_i\) 独立执行判定。评估框架按测试函数逐个隔离执行（单函数限时 30 秒，超时直接记为失败），计算各函数的断言结果。如果至少存在一个测试函数满足在缺陷版本下报错失败而在逆转补丁 \(b_i\) 后顺利通过，则模型获得该缺陷的召回得分。这种单函数粒度打分避免了一处测试断言失败阻断后续缺陷认领的不公。
3. 结构化 PBT 引导范式与框架指令解耦
为了探究大模型在自由代码测试与显式属性约束下的行为差异，基准设计了两种对比提示模式。Baseline 模式采用开放式四阶段指令（理解库、寻找未覆盖行为、编写失败测试、保存交付），完全不提及 Hypothesis 或属性测试，考察通用自发测试能力；PBT 模式则提供强结构化指引，强制引入 @given 装饰器、指定 @settings(max_examples=200, deadline=None)，系统化传授往返一致性（Roundtrip）、参考模型对齐（Model-oracle）、不变量保持（Invariant preservation）等六大经典属性分类学，并要求智能体产出至少 5 个覆盖不同文档契约的聚焦测试函数。
此外，研究进一步设计了仅保留框架指令（Framework-only）的消融提示，保留 Hypothesis 环境与规范覆盖要求，但剥离属性分类学与 5 个函数的模板目标，从而首次定量解耦了“测试工具框架约束”与“属性分类学认知启发”对不同能力层级模型的独立贡献。
损失函数 / 训练策略¶
PBT-Bench 作为评测基准，不引入额外的参数微调损失函数，而是定义了一套严密的基于统计显著性的评测协议与多维聚合指标：
- 缺陷召回率（Bug Recall）：衡量模型在所有问题上的平均缺陷检出比率，为主排行榜核心指标： $\(\text{Recall} = \frac{1}{M} \sum_{j=1}^{M} \frac{\sum_{i=1}^{K_j} \mathbb{I}(b_{j,i} \text{ detected})}{K_j}\)$ 其中 \(M=100\) 为总问题数，\(K_j\) 为第 \(j\) 个问题所包含的缺陷总数，\(\mathbb{I}(\cdot)\) 为通过 \(F \to P\) 验证的指示函数。
- 问题覆盖率（Problem Coverage, \(F \ge 1\)）：找到至少 1 个缺陷的问题比例，衡量测试广度。
- 完全召回率（Full Recall, Perfect）：找全该问题下所有注入缺陷的问题比例，衡量全面性与穷尽测试深度。
- 提示效益差值（Prompt Gain, \(\Delta\)）：定义为 \(\Delta = \text{Recall}_{\text{PBT}} - \text{Recall}_{\text{Baseline}}\)，用以诊断模型对外部显式规范引导的依赖特征。
所有模型配置均执行 3 次独立重复轨迹（每配置 300 轮），报告均值与基于问题级 1,000 次重采样的 95% Bootstrap 置信区间。
实验关键数据¶
主实验¶
在 8 款当代主流模型（Claude Sonnet 4.6、DeepSeek V3.2、Gemini 3 Flash、GLM 5.1、Grok 4.1 Fast、Qwen 3.6 Plus、Qwen3.5-35B-A3B、Step 3.5 Flash）以及后续加入的前沿模型 Claude Opus 4.8（OpenHands 与 Claude Code 原生 CLI 环境）上的综合主榜结果如下：
| 模型 | 评测模式 | 缺陷召回率 (Recall) | 问题覆盖率 (\(F \ge 1\)) | 完全召回率 (Perfect) | 交互轮数 (Turns) | \(\Delta\) (PBT - Base) |
|---|---|---|---|---|---|---|
| Claude Sonnet 4.6 | PBT 引导 | 83.4% \(\pm\) 3.3 | 92.7% \(\pm\) 2.8 | 67.0% \(\pm\) 5.2 | 68.4 | +6.7 |
| Claude Sonnet 4.6 | Baseline | 76.7% \(\pm\) 2.7 | 98.0% \(\pm\) 1.5 | 43.0% \(\pm\) 5.8 | 42.5 | — |
| Claude Opus 4.8 | PBT 引导 | 81.2% \(\pm\) 2.8 | 95.2% \(\pm\) 2.1 | 61.8% \(\pm\) 5.0 | 42.2 | +41.9 |
| Claude Opus 4.8 | Baseline | 39.3% \(\pm\) 3.6 | 96.5% \(\pm\) 2.5 | 11.5% \(\pm\) 4.5 | 20.7 | — |
| Opus 4.8 (Claude Code) | PBT 引导 | 78.6% \(\pm\) 3.3 | 95.7% \(\pm\) 2.2 | 53.7% \(\pm\) 5.8 | — | — |
| Qwen 3.6 Plus | PBT 引导 | 78.0% \(\pm\) 3.5 | 90.3% \(\pm\) 3.2 | 56.0% \(\pm\) 5.7 | 45.1 | +24.5 |
| Qwen 3.6 Plus | Baseline | 53.5% \(\pm\) 3.8 | 85.3% \(\pm\) 4.0 | 18.3% \(\pm\) 4.2 | 27.1 | — |
| GLM 5.1 | PBT 引导 | 72.1% \(\pm\) 4.5 | 77.0% \(\pm\) 4.8 | 63.0% \(\pm\) 5.0 | 89.2 | +5.5 |
| GLM 5.1 | Baseline | 66.6% \(\pm\) 4.3 | 79.7% \(\pm\) 4.5 | 44.0% \(\pm\) 5.3 | 57.4 | — |
| Gemini 3 Flash | PBT 引导 | 62.8% \(\pm\) 3.8 | 84.0% \(\pm\) 4.0 | 37.0% \(\pm\) 5.7 | 34.0 | +6.6 |
| Gemini 3 Flash | Baseline | 56.2% \(\pm\) 4.7 | 71.3% \(\pm\) 5.2 | 38.3% \(\pm\) 5.7 | 44.6 | — |
| DeepSeek V3.2 | PBT 引导 | 61.0% \(\pm\) 4.4 | 79.7% \(\pm\) 4.5 | 38.7% \(\pm\) 5.7 | 50.9 | -3.2 |
| DeepSeek V3.2 | Baseline | 64.2% \(\pm\) 3.8 | 90.0% \(\pm\) 3.5 | 35.3% \(\pm\) 5.5 | 61.8 | — |
| Step 3.5 Flash | PBT 引导 | 58.1% \(\pm\) 4.9 | 70.7% \(\pm\) 5.2 | 41.0% \(\pm\) 5.5 | 83.4 | +20.3 |
| Step 3.5 Flash | Baseline | 37.8% \(\pm\) 3.7 | 67.3% \(\pm\) 5.3 | 14.0% \(\pm\) 4.0 | 51.0 | — |
| Qwen3.5-35B-A3B | PBT 引导 | 54.3% \(\pm\) 4.4 | 77.3% \(\pm\) 4.8 | 25.7% \(\pm\) 4.8 | 48.1 | +22.9 |
| Qwen3.5-35B-A3B | Baseline | 31.4% \(\pm\) 2.9 | 76.0% \(\pm\) 4.7 | 5.3% \(\pm\) 2.7 | 30.2 | — |
| Grok 4.1 Fast | PBT 引导 | 42.1% \(\pm\) 4.3 | 63.0% \(\pm\) 5.5 | 21.0% \(\pm\) 4.7 | 31.8 | -8.0 |
| Grok 4.1 Fast | Baseline | 50.1% \(\pm\) 3.8 | 88.3% \(\pm\) 3.5 | 20.7% \(\pm\) 4.7 | 33.3 | — |
消融实验¶
针对提示工程各要素的解耦消融实验（比较 Baseline、Framework-only 框架约束、Full-PBT 完整提示，以平均召回率及两两差异的 95% Bootstrap 置信区间呈现）：
| 模型名称 | 有效问题数 \(n\) | Baseline 召回率 | Framework-only 召回率 | Full-PBT 召回率 | Framework - Base 增益 | PBT - Framework 增益 | 无测试文件率 |
|---|---|---|---|---|---|---|---|
| Claude Opus 4.8 | 100 | 39.3% | 80.8% | 81.0% | +41.5 pp [+34.2, +47.7] | +0.2 pp [-3.4, +3.7] | 0.4% |
| Qwen 3.6 Plus | 100 | 53.5% | 71.3% | 78.0% | +17.8 pp [+11.4, +24.1] | +6.7 pp [+2.2, +11.6] | 3.9% |
| Claude Sonnet 4.6 | 78 | 78.0% | 79.3% | 84.9% | +1.3 pp [-7.2, +8.7] | +5.6 pp [-0.9, +12.9] | 7.7% |
| DeepSeek V3.2 | 99 | 64.1% | 49.6% | 60.9% | -14.4 pp [-22.9, -6.3] | +11.3 pp [+4.9, +18.0] | 21.6% |
关键发现¶
- 最前沿模型亦未能使基准饱和：最高 PBT 召回率仅为 83.4%（Sonnet 4.6），后续评估的更强模型 Opus 4.8 也仅达 81.2%（在 Claude Code 原生环境下为 78.6%），没有单一配置能在超过 67% 的问题上实现完全召回（Perfect）。
- \(\Delta\) 增益反映任务完成行为偏置而非模型固有能力：Opus 4.8 展现出最极端的 \(\Delta = +41.9\) pp 差异，其核心原因在于在开放式 Baseline 提示下，Opus 4.8 倾向于“找到单个失败用例即宣布完成”，中位数仅写 2 个测试函数（Sonnet 为 8 个），导致其虽覆盖 96.5% 的问题却只有 11.5% 的完全召回率；一旦 PBT 要求覆盖整体规范，召回率骤升至 81.2%。
- 框架约束与属性分类学的解耦分工：消融实验揭示，对于推理顶尖的 Opus 4.8，几乎全部增益均来自于框架级指令（+41.5 pp，强制 Hypothesis 与全面规范覆盖），属性分类学几乎不带来额外收益（+0.2 pp）；而对于中等能力模型（如 Qwen 3.6 Plus、DeepSeek V3.2），属性分类学与模板带来了统计显著的增益（+6.7 pp 至 +11.3 pp），起到了关键的形式化引导作用。
- 不同模型与提示模式存在高度互补性：对 16 个评测单元进行贪心集成，16 个单元的并集缺陷召回率达到 99.5%，比单模型最高值高出 12.7 pp；其中 Sonnet PBT 与 Sonnet Baseline 的双模式组合即贡献了 65% 的增量缺陷，展现了跨模式互补。
- 典型失败模式截然不同：Baseline 模式下的失败有 59% 来自于测试自身断言错误（Incorrect Assertion），32% 来自测试过于具象而错过输入空间；而 PBT 模式下 62% 的失败归结于搜索空间失误，具体为误用
hypothesis.assume()过滤掉触发用例（31%）或生成策略范围受限（31%）。全基准有两个极端缺陷（BIDC-004 bug 3 与 TMLK-005 bug 1）在任意模型的绝大多数运行中均未被检出。
亮点与洞察¶
- 从机械变异与PR挖掘转向语义受控的准入规约：论文明确划定了 PBT 测试能力的准入边界，克服了以往挖掘开源数据带来的测试类型污染问题，为智能体软件工程评测确立了高保真规范。
- 解耦认知启发与行为停机机制：揭示了如 Opus 4.8 等模型在测试任务中的“懒惰”停机行为，证明单一的通过率指标会严重受提示词任务目标的表述偏置干扰。
- 生成空间的反向裁剪陷阱：发现智能体在掌握 Hypothesis 语法后，极度容易滥用
assume()谓词。这一发现指出未来的代码测试智能体训练需特别强调先验生成空间建模与后验过滤的区别。
局限与展望¶
- 语言与生态局限：目前评测聚焦于 Python 及其 Hypothesis 库，受限于单语言单生态，未来可扩展至具备成熟 PBT 工具的其他语言（如 Rust proptest, ScalaCheck, Haskell QuickCheck）。
- 执行预算与生成规模上限：当前统一限制
max_examples=200，对于某些状态极其狭窄的高阶协议缺陷（如伽罗瓦域与有限域代数运算），可能需要更高的随机搜索预算。 - 智能体工作流单一：大部分测试基于单代理在 OpenHands 下的直接交互，尚未深度探究多智能体审计、变异反馈回路等高级测试架构。
相关工作与启发¶
- vs SWE-bench / SWT-Bench: SWE-bench 考核给定 issue 时的补丁合成，SWT-Bench 考核给定缺陷报告时的用例生成；本文不提供缺陷先验报告，只提供完整文档作为 Oracle，强迫模型自主提炼不变量。
- vs TestExplora: TestExplora 同样采用文档为准则，但数据直接源自 GitHub PR，混杂了海量非属性可测的 I/O、UI 和环境依赖缺陷；本文纯化了语义不变量空间。
- vs Agentic PBT (Maaz et al., 2025): Maaz 等人直接在野外开源库挖掘真实缺陷但缺乏真值与可观测召回；本文提供全量真值不变量与触发空间，使得缺陷召回率和漏报率严格可度量。
评分¶
- 新颖性: ⭐⭐⭐⭐⭐ 首次系统性隔离并量化代码智能体在基于属性测试上的抽象与生成短板。
- 实验充分度: ⭐⭐⭐⭐⭐ 涵盖 8+ 款模型、4800 条轨迹、双提示对比、消融分析与深入的失败机理归类。
- 写作质量: ⭐⭐⭐⭐⭐ 逻辑结构严谨清晰，定义精确，问题定义与分析兼具软件工程深度。
- 价值: ⭐⭐⭐⭐⭐ 为自动化测试生成、代码大模型强化学习与规范对齐提供了高质量公开基准。