AgentProofBench: Benchmarking Reusable Verifiers for Web Agents

Jingjie Ning; Xueqi Li; Yi Lu; Yibo Kong

cs.MAOct 25, 2026

AgentProofBench: Benchmarking Reusable Verifiers for Web Agents

Authors: Jingjie Ning, Xueqi Li, Yi Lu, Yibo Kong

Abstract

Reusable Web-agent verification requires a rule to follow changing requirements and support subsequent execution. We introduce AgentProofBench, which connects paired tests of a frozen acceptance rule to execution from identical saved openings. The resource spans 97 tasks, 79 families, and four Web services. Experiments with DeepSeek Flash/Pro establish two linked measurements. Across 48 families, complete-panel and decision-replay tests retain 82/96 Flash and 79/96 Pro source programs; paired reuse-rebuild BA intervals are [-5.47, 1.57] and [-10.16, 0.00] percentage points. Across 22 execution families, deployment-state panel correctness separates program assignments whose two saved openings are both delivered correctly: 32/33 assignments with error-free panels, versus 1/11 with panel errors. All reference-defined program-gate regressions and withheld deliveries occur in the latter group. Neutral continuation attains the highest correct delivery under the tested generic feedback, providing a concrete baseline for measuring the value added by a gate. Released instructions, states, programs, reference rules, and trajectories connect each test failure to its execution consequences. AgentProofBench makes reusable verification assessable at both the requirement and policy levels.

Figures & tables

Figure 1. One instruction, a changed required identity, and an acceptance rule frozen on the old identity. The illustrated Linear45 mechanism connects matched outcome tests to an observed regression after generic rejection. Team labels A/B and the displayed rule are schematic; saved code and states provide the exact instance. Schematic team identities A and B illustrate the Linear45 binding change. The frozen program, reference outcomes, and generic-rejection or neutral branches connect the state change to the observed execution consequence.

Figure 2. Related settings and the measurement units in AgentProofBench. Paired initial requirements test a frozen acceptance program; matched histories connect its decisions to subsequent execution ( Yin et al., 2026 ; Suh et al., 2026 ) . Three illustrated workflow lanes distinguish executable verifier tests, reusable guarded execution policies, and paired verifier transfer with matched-history execution.

Table 1. Matched P1 results on 48 families. Values are task-averaged percentages with two program replicas or online judgments. Related reuse-minus-rebuild intervals are [-5.47, 1.57] for Flash and [-10.16, 0.00] for Pro.

Figure 3. The same 96 source programs pass through source-panel, related-panel, and joint tests. Blue denotes complete correctness and gray the remaining programs. Separate rings compare related rebuilds. The lower panel retains the paired BA contrasts and original 95% family-bootstrap intervals. Related main-panel correctness is 83 of 96 Flash and 81 of 96 Pro source programs, versus 85 and 87 rebuilds. Joint correctness is 82 and 79 for source programs, versus 82 and 86 rebuilds.

Figure 4. Deployment-state panel correctness and execution outcomes. Each program assignment supplies a natural ending and checkpoint; the upper panel groups all 44 assignments by related-panel correctness. Incorrect and withheld delivery are separate from state regression. The lower policy lanes restart from 22 shared openings per actor and cohort. Panel-perfect programs deliver both openings correctly in 32 of 33 assignments, compared with 1 of 11 assignments containing panel errors. The policy flows retain correct, incorrect, and withheld delivery at every opening.

Figure 5. Task-level fault-acceptance distributions. Faint curves are normalized shape guides for groups with at least ten tasks. Large points and bars retain the published means and 95% family-bootstrap intervals. Program and online acceptance are compared across identity, collection completeness, relation direction, preservation, and value faults. Both failed-state rejection and valid-anchor acceptance appear for every method and category.

Figure 6. Repeated-check costs. Top: 80/83 matched Flash/Pro units. Bottom: amortized

c+C/k

and interquartile bands, including actor-prefix cost. Flash natural online uses 21 complete records; each other P2 cell uses 22. Empirical break-even distributions and four amortization curves expose construction, warm operation, and recorded comparison costs.

Figure 7. Four complementary evidence views. Counts refer to each panel; successful anchors can be shared. The natural panel uses the frozen six-state cap and has 72 dual-class tasks. Illustrated natural trajectories, native prefixes, targeted faults, and legal alternatives show valid/failed counts and task/family support.

Appendix figures & tables2 assets

Supplementary material from the paper’s appendix.

Appendix

Figure 8. The complete construction/assessment matrix. Circle color gives task-averaged BA on a common 80–100% scale; all 18 values retain two replicas and 48 families. Outlined cells assess the same condition used for construction. The matrix contains 6,696 program predictions. Two three-by-three circle maps show directional cross-condition performance for Flash and Pro.

Figure 9. Every assigned program linked to its execution outcomes. Horizontal position gives related-panel errors; filled markers pass every source-panel test. Circles show natural endings, diamonds checkpoints, and stars mark reference-defined regressions. Color gives correct, incorrect, or withheld delivery. Labels identify task and replica; curves pair openings of the same assignment. All 22 task pairs retain source qualification, related-panel errors, replica identity, and both cohorts of observed delivery.

LLM Agent Verification

LLM agent verification checks whether agents’ actions, evidence, policies, and completion claims satisfy explicit requirements.

See all 145 papers

An Executable Benchmarking Suite for Tool-Using Agents
May 10, 2026Zhiqing Zhong, Zhijing Ye, Jiamin Wang +1Computer-Use Agent Benchmarks Tool-Use Evaluation
Stevens Institute of Technology
VerifierBench: Benchmarking the Generation of Executable Verifiers for LLM Agents
Oct 19, 2026Jianing Yin, Ziyi Chen, Hao Wang +4LLM Agent Verification AI Agent Benchmarks
University of Pennsylvania · University of Illinois at Urbana-Champaign · University of California, Berkeley +2
Evidence-First Agentic Verification
Oct 13, 2026Reza Sanayei, Razvan-Gabriel Dumitru, Sunjie Hou +7LLM Agent Verification AI Agent Evaluation
Scale AI · University of Arizona

May 10, 2026J/K move · Enter open · S save

An Executable Benchmarking Suite for Tool-Using Agents

Zhiqing Zhong, Zhijing Ye, Jiamin Wang, Xiaodong Yu

Stevens Institute of Technology

Computer-Use Agent Benchmarks Tool-Use Evaluation Benchmark Design Web Agent Benchmarks Software Engineering Benchmarks AI Agent Benchmarks

Open paper AskPDF arXiv

Closed-loop tool-using agents are increasingly evaluated in executable web, code, and micro-task environments, but benchmark reports often conflate workloads, action-generating drivers, and the evidence admitted for systems-facing claims. We present an executable benchmarking suite that makes these objects explicit under a shared evidence-admission contract. The suite connects WebArena Verified, a SWE-Gym slice with SWE-bench-compatible verification, and MiniWoB++ through common workload adapters, task manifests, event schemas, replay/freeze policy, declared drivers, and reporting pipelines. In the canonical release, the gate separates paper-facing evidence from preflight, fixture, smoke, and diagnostic rows while preserving non-admitted artifacts for audit and onboarding. The admitted evidence records latency, invalid-action behavior, patch-generation cost, verifier metadata, replay bindings, and provenance under one auditable contract. The gate is decision-relevant rather than merely clerical: in a separate WebArena Verified controller study, clean-baseline and medium live-stressed evaluation select different fixed controller variants under the same workload and admission contract. The release is scoped as a benchmarking suite and admitted evidence, not a new agent policy, model leaderboard, backend comparison, or autonomous SWE-bench solver.

Abstract

LLM Agent Verification

Explore similar work

An Executable Benchmarking Suite for Tool-Using Agents

VerifierBench: Benchmarking the Generation of Executable Verifiers for LLM Agents

Evidence-First Agentic Verification