Paper deep dive

Training Needs Trustworthy Worlds: Verified Synthetic Web Environments for Agent Learning

Chenghao Zhang, Canran Xiao, SaiSai Hu, Dan Roth

Year: 2026Venue: arXiv preprintArea: cs.AIType: PreprintEmbeddings: 109

Intelligence

Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 95%

Last extracted: 8/25/2026, 7:39:39 AM

Summary

The paper introduces a framework for generating verified synthetic web environments to train web agents. It addresses the issue of unreliable, surface-level plausible environments by constructing structured scaffolds (pages, links, database records, state-change markers) that are verified and repaired for structural, semantic, consistency, and feasibility defects. This approach enables deterministic UI transitions and auditable backend updates, improving the feasible-task rate from 48.6% to 94.8% and enhancing PPO policy performance across domains like WebArena, WebShop, and MiniWoB++.

Entities (9)

MiniWoB · benchmark · 99%WebArena · benchmark · 99%WebShop · benchmark · 99%Verified Synthetic Web Environments · methodframework · 98%PPO · algorithm · 97%Chenghao Zhang · person · 95%University of Pennsylvania · organization · 95%State-Change Markers · component · 92%Feasible-Task Rate · metric · 90%

Relation Signals (7)

Verified Synthetic Web Environments → evaluatedon → WebShop

confidence 98% · improving transfer to WebShop

Verified Synthetic Web Environments → evaluatedon → WebArena

confidence 98% · improving transfer to WebArena

Verified Synthetic Web Environments → evaluatedon → MiniWoB

confidence 98% · improving transfer to MiniWoB++

Chenghao Zhang → affiliatedwith → University of Pennsylvania

confidence 95% · Chenghao Zhang1 ... 1 University of Pennsylvania

Verified Synthetic Web Environments → improves → Feasible-Task Rate

confidence 95% · our method reduces task-blocking defects and improves feasible-task rate from 48.6% to 94.8%

Verified Synthetic Web Environments → usedwith → PPO

confidence 93% · producing stronger PPO policies

State-Change Markers → enables → Verified Synthetic Web Environments

confidence 90% · persistent backend updates are invoked only through validated state-change markers

Cypher Suggestions (0)

No Cypher suggestions yet.

Abstract

Abstract:Web agents promise to automate complex digital workflows, but their training remains limited by synthetic environments that look plausible while hiding broken links, inconsistent states, or infeasible tasks. We address the gap between scalable environment generation and trustworthy agent learning by constructing synthetic web environments that are executable, auditable, and grounded in backend state. Our framework represents each generated website as a structured scaffold of pages, navigation links, database records, state-change markers, and task constraints, then verifies and repairs structural, semantic, consistency, and feasibility defects before policy training. During interaction, ordinary UI transitions are executed deterministically, while persistent backend updates are invoked only through validated state-change markers, enabling dense rewards compiled from verified task-progress predicates. Across 500 synthetic environments spanning six domains, our method reduces task-blocking defects and improves feasible-task rate from 48.6% to 94.8%, while producing stronger PPO policies and improving transfer to WebArena, WebShop, and MiniWoB++ without LLM calls at evaluation time. These results show that verified synthetic environments can serve as a scalable and reliable training substrate for compact web agents, shifting synthetic webagent learning from surface-level plausibility toward executable, state-grounded supervision.

PDF

Open source PDF →Open local PDF →

Trouble viewing inline? Open PDF directly →

Full Text

105,491 characters extracted from source content.

Expand or collapse full text

Training Needs Trustworthy Worlds: Verified Synthetic Web Environments for Agent Learning Chenghao Zhang1 Canran Xiao2 SaiSai Hu3 Dan Roth1 Abstract Web agents promise to automate complex digital workflows, but their training remains limited by synthetic environments that look plausible while hiding broken links, inconsistent states, or infeasible tasks. We address the gap between scalable environment generation and trustworthy agent learning by constructing synthetic web environments that are executable, auditable, and grounded in backend state. Our framework represents each generated website as a structured scaffold of pages, navigation links, database records, state-change markers, and task constraints, then verifies and repairs structural, semantic, consistency, and feasibility defects before policy training. During interaction, ordinary UI transitions are executed deterministically, while persistent backend updates are invoked only through validated state-change markers, enabling dense rewards compiled from verified task-progress predicates. Across 500 synthetic environments spanning six domains, our method reduces task-blocking defects and improves feasible-task rate from 48.6% to 94.8%, while producing stronger PPO policies and improving transfer to WebArena, WebShop, and MiniWoB++ without LLM calls at evaluation time. These results show that verified synthetic environments can serve as a scalable and reliable training substrate for compact web agents, shifting synthetic web-agent learning from surface-level plausibility toward executable, state-grounded supervision. †footnotetext: 1 University of Pennsylvania.†footnotetext: 2 Shenzhen Campus of Sun Yat-sen University.†footnotetext: 3 Pace University. 1 Introduction Autonomous web agents aim to complete user-specified tasks by perceiving graphical interfaces, selecting grounded actions, and manipulating persistent web states. This capability is increasingly important for automating digital workflows such as shopping, booking, form submission, customer-service operations, and enterprise knowledge work. Despite rapid progress in large language and multimodal agents, web interaction remains challenging because successful execution requires long-horizon planning, precise grounding in dynamic interfaces, and reliable reasoning over hidden backend states rather than only visible page content. Recent benchmarks and systems have substantially advanced web-agent research. Early platforms such as World of Bits and MiniWoB++ established reproducible browser-control tasks for reinforcement learning (Shi et al. 2017; Liu et al. 2018), while WebShop, Mind2Web, WebArena, VisualWebArena, WorkArena, and BrowserGym introduced more realistic tasks, websites, demonstrations, and evaluation protocols (Yao et al. 2023a; Deng et al. 2023; Zhou et al. 2024; Koh et al. 2024; Drouin et al. 2024; Chezelles et al. 2024). In parallel, LLM-based agents such as ReAct, WebVoyager, AgentOccam, Agent Q, and WebRL have improved reasoning, exploration, and learning from interaction traces (Yao et al. 2023b; He et al. 2024; Yang et al. 2024; Putta et al. 2024; Qi et al. 2024). These works demonstrate that web agents can benefit from richer environments and larger-scale interaction data. However, they also expose a central bottleneck: high-quality web-agent training requires many executable, stateful, and verifiable environments, yet realistic web environments are expensive to build, difficult to reset, and often limited in task coverage. A natural direction is to use LLMs to synthesize environments, tasks, or agent experiences. Prior work has shown that generated environments and synthetic trajectories can support agent learning in embodied and digital settings (Zala et al. 2024; Patel et al. 2024). Nevertheless, directly generated web environments are prone to a deeper reliability problem: locally plausible pages may still contain globally invalid workflows. For example, links may be unreachable, database values may contradict rendered content, required controls may be missing, and task success conditions may not correspond to any executable state transition. Such defects are especially harmful for reinforcement learning, because the agent may receive supervision from environments whose apparent failures are caused by scaffold errors rather than policy mistakes. Existing approaches do not fully resolve this high-level mismatch between plausible generation and executable, state-grounded interaction. Figure 1: Prior methods train on superficially plausible but inconsistent web interactions, while our approach verifies and repairs the environment to provide executable, state-grounded supervision for more effective agent policies. This paper asks: How can we construct synthetic web environments that are not only diverse and realistic, but also executable, auditable, and useful for training compact web agents? We address this question by shifting the object of generation from isolated pages or trajectories to verified environment scaffolds. As shown in Fig.1, our approach first represents a synthetic website as a structured environment with pages, navigation, data records, state-changing events, and task constraints; then it verifies and repairs the scaffold before policy learning; finally, it trains agents using rewards derived from backend-grounded task progress rather than from surface-level textual judgments. This design aims to make synthetic web interaction a reliable training substrate, where failures are attributable to the policy instead of hidden environment invalidity. Our contributions are summarized as follows: • We identify a core limitation of trajectory- or page-level generation: web-agent training depends on whether tasks are executable under consistent backend dynamics, not merely whether the generated interface appears plausible. • We propose a framework that canonicalizes, verifies, and repairs generated web scaffolds, producing environments with explicit navigation structure, database bindings, state-change events, and task constraints. • By deriving dense rewards from verified backend-state progress and executing ordinary interactions without LLM calls at evaluation time, our framework enables efficient reinforcement learning in synthetic web environments while preserving task-level auditability. 2 Related Work Web interaction benchmarks and web agents. Early work framed web interaction as language-conditioned control over semi-structured interfaces, from instruction following to reproducible environments such as World of Bits and MiniWoB++ (Branavan et al. 2009; Shi et al. 2017; Liu et al. 2018). Later benchmarks expanded realism and task diversity, including WebShop, Mind2Web, WebArena, VisualWebArena, WorkArena, and BrowserGym (Yao et al. 2023a; Deng et al. 2023; Zhou et al. 2024; Koh et al. 2024; Drouin et al. 2024; Chezelles et al. 2024). Recent agents such as WebVoyager and AgentOccam further show that improved observation and action design can benefit web navigation (He et al. 2024; Yang et al. 2024). However, these efforts mainly provide fixed benchmarks or agent-side improvements, rather than methods for automatically constructing large-scale, executable, stateful, and verifiably valid training environments. Our work instead generates checked web environments whose pages, data bindings, events, and task constraints are explicitly represented and verified before policy learning. Synthetic environments and agent experience generation. A complementary line of work uses LLMs to reduce the cost of interactive learning by generating environments, tasks, or trajectories. EnvGen uses LLMs to adaptively create training environments for embodied RL agents (Zala et al. 2024), while DreamGym synthesizes agent experiences through a learned reasoning-based environment model (Chen et al. 2025). For web agents, self-improvement methods synthesize or refine interaction data from agent rollouts, including model-generated web trajectories (Patel et al. 2024), search- and preference-based refinement in Agent Q (Putta et al. 2024), and self-evolving curriculum RL in WebRL (Qi et al. 2024). These methods show the promise of using generated interaction data, but the generated supervision is often trajectory-centric and may inherit invalid dynamics, inconsistent states, or unverifiable task completions. Our method instead treats the environment itself as the object of generation: raw scaffolds are canonicalized, verified, repaired, and instrumented with constrained state-change markers, so that rollouts are produced by an executable simulator rather than by unconstrained trajectory synthesis. Reward, verification, and policy learning for digital agents. Learning web agents is difficult because long-horizon tasks often provide sparse terminal feedback. Prior RL methods improved exploration with demonstrations and workflow constraints (Liu et al. 2018), while WebShop used programmatic matching functions to provide task-specific rewards (Yao et al. 2023a). More recent work studies automatic evaluators and process reward models for web or device-control agents, such as autonomous evaluator-guided refinement and Web-Shepherd’s step-level reward modeling (Pan et al. 2024; Chae et al. 2025). These approaches improve feedback quality but often rely on learned or LLM/VLM-based evaluators, which can be costly, miscalibrated, or disconnected from the true backend state. Our work takes a more environment-grounded route: task constraints are compiled into backend-state predicates that yield dense progress rewards, while invalid marker-triggered updates are rejected by construction. This enables standard PPO training (Schulman et al. 2017) of compact policies in checked synthetic environments, without requiring LLM calls during policy evaluation. 3 Preliminaries 3.1 Web Interaction and Environment Scaffold We model web interaction as a goal-conditioned sequential decision process. A task t∈Tt∈ T provides an instruction xtx_t and a programmatic completion constraint CtC_t evaluated on the environment state. Starting from s0∼ρts_0 _t, the agent observes a rendered interface, selects a DOM-grounded action, and triggers a state transition: ok=Render⁡(sk),ak∈A⁡(ok),sk+1=⁡(sk,ak).o_k=Render(s_k), a_k∈ A(o_k), s_k+1=T(s_k,a_k). (1) The terminal success signal is given by Ct(s)∈0,1C_t(s)∈\0,1\. This setting is difficult because the agent only observes the rendered interface rather than the full backend state, and successful completion often requires long-horizon navigation, form filling, and stateful updates. We represent a generated web environment as E=(P,L,D,T),E=(P,L,D,T), where P is the page set, L⊆P×PL P× P is the navigation graph, D is the database schema with initialized records, and T is the task set with verifiable constraints. Each page pi∈Pp_i∈ P contains a DOM tree τi _i and interactive elements IiI_i, whose action types and argument schemas ground high-level actions in executable UI operations. This representation separates two layers. The static scaffold defines pages, links, database bindings, interactive elements, and task constraints before execution. The dynamic layer specifies how actions update persistent records and session variables during interaction. This separation is necessary because one-shot LLM generation often produces interfaces that are locally plausible but globally invalid. We consider four scaffold defects: structural defects (ΔS)( _S), such as broken links or unreachable pages; semantic defects (ΔC)( _C), such as invalid field values or placeholder content; consistency defects (ΔX)( _X), such as contradictory entity attributes across pages; and feasibility defects (ΔT)( _T), where missing controls or workflow steps make a task unsatisfiable. 3.2 Motivating Diagnostics We run a lightweight diagnostic study on 500 raw LLM-generated environments from six domains, covering 6,842 generated tasks, and analyze 1,800 successful trajectories from scripted and human-assisted rollouts. For defect category c, let Nc(E)N_c(E) be its per-environment count. We measure its task-blocking effect as Bc(E)=1|T⁡(E)|∑t∈T⁡(E)[Blockc(E,t)=1],B_c(E)= 1|T(E)| _t∈ T(E)1\! [Block_c(E,t)=1 ], (2) where Blockc⁡(E,t)Block_c(E,t) indicates that task t is blocked by category c under bounded trace analysis. For a trajectory τ=(s0,a0,…,sH)τ=(s_0,a_0,…,s_H), we measure marker-trigger sparsity by M(τ)=1H∑k=0H−1[μ(pk,ak)≠∅],U(τ)=∑k=0H−1[μ(pk,ak)≠∅],M(τ)= 1H _k=0^H-11\! [μ(p_k,a_k)≠ ], U(τ)= _k=0^H-11\! [μ(p_k,a_k)≠ ], (3) where μ⁡(pk,ak)μ(p_k,a_k) returns the state-change marker triggered by action aka_k. Figure 2: Motivating diagnostics. (a) Raw LLM-generated environments contain frequent defects, with semantic and structural defects dominating the average total of 12.4 defects per environment. (b) Defect frequency and harmfulness differ: feasibility defects are less frequent but most likely to block task completion. (c) Marker-triggered updates are sparse across domains, indicating that most interactions are deterministic UI transitions. (d) The number of state-write calls remains small even for longer episodes. Figure 2 supports two design choices. First, raw scaffolds require verification because defect counts alone understate task-level harm: feasibility and structural defects are especially likely to block executable workflows. Second, runtime state updates are sparse: most steps are navigation, inspection, scrolling, or local input editing, while persistent backend writes occur only at a few marker-triggered events. These observations motivate verified static scaffolds and event-driven dynamic updates. Additional details on bounded trace analysis, defect attribution, marker statistics, and plotting protocol are provided in Appendix A.1. 3.3 Dynamic State and Event-Driven Updates The dynamic layer maintains the database instance and session state used for rendering and access control. Ordinary actions, such as navigation, scrolling, menu expansion, and local text entry, are executed deterministically. Only marked events, such as add-to-cart, submit-order, or update-profile, invoke a constrained state writer to propose a backend delta. The delta is committed only if it satisfies marker preconditions, schema constraints, and environment invariants. Thus, the simulator avoids calling a generative model at every step while keeping persistent state changes explicit, auditable, and aligned with the verified scaffold. 4 Method Given a domain-level website description, our method constructs an executable synthetic web environment for training compact web agents. The environment is first represented as a structured scaffold with pages, links, database records, state-change markers, and task constraints. We then verify and repair the scaffold before training, so that generated tasks correspond to reachable workflows instead of artifacts of one-shot generation. During interaction, the simulator executes ordinary UI transitions deterministically and invokes constrained state writes only when a verified marker is triggered. Task constraints are compiled into backend-grounded progress predicates, which provide dense rewards for PPO training while keeping the learned policy independent of LLM calls at evaluation time. Fig.3 shows the pipeline of our method. Figure 3: Pipeline of verified synthetic web-environment construction and policy training. The offline stage generates a scaffold from a site specification, canonicalizes it into pages, data, tasks, and markers, and verifies/repairs navigation, data consistency, and workflow feasibility. The online stage trains a compact policy in the checked environment, where deterministic transitions and marker-validated state updates provide state-grounded rewards for PPO. 4.1 Environment Representation and Marker Instrumentation A generated web environment must support three operations throughout training: rendering observations, executing actions, and checking task completion against ground-truth state. We therefore represent the environment as a structured object instead of a collection of independent HTML pages. This representation exposes the causal chain from backend records to rendered DOM nodes, from UI events to state updates, and from state changes to task progress. We represent an environment as ℰ=(,ℒ,,ℳ,),E=(P,L,D,M,Q), (4) where P is the page set, ℒ⊆×L ×P is the navigation graph, D is the database schema with initialized records, ℳM is the set of state-change markers, and Q is the task set. Each task t∈t contains an instruction xtx_t, an initial-state distribution ρt _t, and a completion constraint Ct:→0,1C_t:S→\0,1\ evaluated on simulator state. At step k, the simulator state, rendered observation, and executable action satisfy sk=(pk,bk,σk,hk),ok=Render⁡(pk,bk,σk),ak∈⁡(ok).s_k=(p_k,b_k, _k,h_k), o_k=Render(p_k,b_k, _k), a_k (o_k). (5) Here, pkp_k is the current page, bkb_k is the database instance, σk _k is the session state, hkh_k is the action history, and ⁡(ok)A(o_k) is the DOM-grounded candidate action set extracted from the current observation. The rendering function fills page templates using database bindings and session variables, making the observation a deterministic view of the underlying state. State-changing operations are specified by markers: m=(em,prem,Rm,Wm,Ωm).m=(e_m,pre_m,R_m,W_m, _m). (6) In Eq. (6), eme_m is the triggering UI element, prempre_m is a precondition over the current state and action, RmR_m and WmW_m are the permitted read and write fields, and Ωm _m is the operation signature. A marker therefore constrains which backend fields are accessed and modified when a UI event commits a persistent update. Additional parsing rules and marker schemas are given in Appendix A.2. 4.2 Verification-Guided Scaffold Construction One-shot LLM generation often produces locally plausible pages with globally invalid workflows. Broken links, inconsistent entity attributes, invalid database bindings, and infeasible tasks create misleading training signals. The verification stage detects these failures before policy learning; the repair stage modifies only the scaffold components implicated by accepted defect reports. Given a site description q, the generator produces raw scaffold artifacts ℰ~ E, including page templates, navigation links, database records, task instructions, and completion constraints. A canonical parser converts ℰ~ E into ℰ(0)E^(0), extracts DOM elements and database bindings, and builds the initial marker set. Deterministic checks handle reachability, link integrity, schema validity, DOM–database binding, and marker read–write consistency. These checks are specified in Appendix A.2. At repair iteration r, symbolic checks and semantic verifiers produce a defect set Δ(r)=Δsym(r)∪Δstr(r)∪Δsem(r)∪Δcons(r)∪Δfeas(r). ^(r)= _sym^(r)∪ _str^(r)∪ _sem^(r)∪ _cons^(r)∪ _feas^(r). (7) The five terms denote deterministic symbolic defects, structural defects, semantic content defects, cross-page consistency defects, and task feasibility defects. Each reported defect d is associated with a location, affected object, severity score, evidence, and verifier confidence. Reports with the same canonical key are merged. The aggregated confidence is conf⁡(d)=∑jωjcj(d)[d∈Δj(r)]∑jωj[d∈Δj(r)],conf(d)= _j _jc_j(d)1[d∈ _j^(r)] _j _j1[d∈ _j^(r)], (8) where j indexes verifiers, cj(d)c_j(d) is verifier j’s confidence for defect d, ωj _j is the reliability weight of verifier j, and [⋅]1[·] is the indicator function. Defect-triggered verifier coordination is used to re-check only defect categories that affect one another; the coordination protocol is described in Appendix A.3. Accepted defects are repaired in dependency order. We rank each defect by score⁡(d)=λ1sev(d)+λ2log⁡(1+dep⁡(d))+λ3scope(d)−λ4cost(d),score(d)= _1sev(d)+ _2 (1+dep(d))+ _3scope(d)- _4cost(d), (9) where sev⁡(d)sev(d) is severity, dep⁡(d)dep(d) is the number of downstream defects that depend on d, scope⁡(d)scope(d) counts affected pages and tasks, cost⁡(d)cost(d) estimates repair complexity, and λ1,…,λ4≥0 _1,…, _4≥ 0 are fixed scheduling weights. The repair operator updates the environment as ℰ(r+1)=ℛd⋆(ℰ(r))E^(r+1)=R_d (E^(r)), where d⋆d is the highest-scoring defect whose dependencies have been satisfied. Structural repair modifies links and required elements; semantic repair rewrites content while preserving database bindings; consistency repair propagates canonical database values; feasibility repair inserts missing workflow steps and marker signatures. The loop terminates when no accepted critical defect remains and each task has a bounded executable trace satisfying its completion constraint. Repair operators and termination checks are given in Appendix A.4. 4.3 Event-Driven Simulation A training simulator must be efficient and inspectable. Most web interactions, such as navigation, scrolling, local text entry, and client-side validation, follow deterministic rules. Persistent changes, such as form submission, entity creation, profile update, and permission change, require backend writes. We therefore execute deterministic transitions by default and restrict generative state updates to verified marker-triggered operations. Let μ⁡(pk,ak)μ(p_k,a_k) return the marker triggered by action aka_k on page pkp_k, and let ∅ denote no marker. The simulator transition is (sk+1,ϵk)=(Fdet(sk,ak),0),μ⁡(pk,ak)=∅,(Fmark(sk,ak,δk),[δk=⊥]),mk=μ⁡(pk,ak)≠∅.(s_k+1, _k)= cases(F_det(s_k,a_k),0),&μ(p_k,a_k)= ,\\ (F_mark(s_k,a_k, _k),1[ _k= ]),&m_k=μ(p_k,a_k)≠ . cases (10) Here, FdetF_det applies deterministic UI transitions, FmarkF_mark applies a validated backend update, δk _k is the state delta, and ϵk _k indicates a rejected transition. For a marker-triggered operation, a constrained state writer proposes a candidate delta using the current page, relevant database fragments, session state, action arguments, and marker signature. The candidate is accepted only after validation: δk=Validatemk(δ^k,sk,ak)∈mk(sk,ak)∪⊥. _k=Validate_m_k( δ_k;s_k,a_k) _m_k(s_k,a_k)∪\ \. (11) The feasible update set mk(sk,ak)U_m_k(s_k,a_k) contains deltas satisfying the marker precondition, permitted read–write fields, database schema, and environment invariants. If validation returns ⊥ , the simulator keeps the previous state and records a violation. This design makes every accepted persistent update traceable to a marker, a write set, and a validated state delta. The state writer interface and validation rules are detailed in Appendix A.5. 4.4 State-Grounded Reward and Policy Learning Terminal success alone gives sparse supervision for long-horizon web tasks. Since the checked environment exposes backend records and session variables, intermediate progress is computed from task constraints rather than from natural-language self-assessment. The reward therefore measures verified state progress and penalizes rejected transitions. For each task t, we compile its completion constraint CtC_t into progress predicates Φt=ϕt,1,…,ϕt,Mt _t=\ _t,1,…, _t,M_t\, where each ϕt,i:→0,1 _t,i:S→\0,1\ checks a necessary intermediate condition. These conditions include visiting required pages, satisfying form constraints, creating target entities, updating correct attributes, and matching rendered views with backend state. The predicates define a progress potential: Ψt(s)=1∑i=1Mtwi∑i=1Mtwiϕt,i(s), _t(s)= 1 _i=1^M_tw_i _i=1^M_tw_i _t,i(s), (12) where wi≥0w_i≥ 0 is the importance weight of predicate ϕt,i _t,i. The policy observes oko_k and xtx_t, while CtC_t, Φt _t, and backend state are used only by the environment to compute rewards. The step reward is rk=[Ct(sk+1)=1]+α(Ψt(sk+1)−Ψt(sk))−γϵk−η.r_k=1[C_t(s_k+1)=1]+α ( _t(s_k+1)- _t(s_k) )-γ _k-η. (13) The first term gives terminal success reward, the second term gives net verified progress, the third term penalizes rejected state transitions, and η is a step cost. The constants α,γ,η≥0α,γ,η≥ 0 are fixed. We train a compact policy πθ(ak∣ok,xt) _θ(a_k o_k,x_t) using standard clipped PPO over DOM-grounded candidate actions. During synthetic training rollouts, marker-triggered simulator updates may use the constrained state writer in Eq. (11); the learned policy itself performs action selection without LLM calls during evaluation. More details are provided in Appendix A.6. 5 Experiments We design experiments to answer three questions. First, does verification convert superficially plausible generated websites into executable training environments? Second, does training on verified environments improve compact policies beyond training on raw synthetic environments? Third, which components of the verification–repair–reward pipeline are responsible for the gains? We also discussed other questions regarding the mechanism of our method; see §C. 5.1 Experimental Setup Synthetic environment suite. We generate 500 synthetic web environments from domain-level site specifications across six domains: e-commerce, social media, banking, education, healthcare, and government. Each environment contains 15–30 pages, a navigation graph, database records, state-change markers, and a set of task instructions with programmatic completion constraints. Unless otherwise stated, we split environments by site specification into 350 training environments, 75 validation environments, and 75 held-out test environments, ensuring that held-out environments do not share page templates or task constraints with training environments. Policy and training. We train a compact DOM-grounded policy with fewer than 10M parameters using PPO. At each step, the policy receives the task instruction and the rendered DOM observation, scores the current candidate action set, and executes one DOM-grounded action. The policy never observes backend states, completion predicates, or verifier outputs. Unless otherwise stated, all policy results are averaged over three random seeds and reported with 95% confidence intervals. Environment-construction baselines. We compare our verified construction pipeline with five baselines. No Verification directly uses raw LLM-generated scaffolds. Rule-Based applies deterministic reachability, link, schema, and binding checks. Single-LLM uses one GPT-4 verifier prompted to detect all defect categories. Self-Consistency samples five independent verifier outputs and applies majority voting. AutoGen adapts a general-purpose multi-agent verification framework to the same environment scaffold. All methods start from the same scaffolds. Policy-training baselines. To isolate the effect of environment quality and reward design, we train the same compact PPO policy under different synthetic training conditions: raw environments with terminal rewards, raw environments with dense rewards, rule-checked environments with dense rewards, verified environments with terminal rewards, and our full verified environment with state-grounded dense rewards. For transfer evaluation, we also compare against GPT-4 direct prompting and GPT-4 with ReAct-style prompting under the same task interface. Metrics. For environment quality, we report average defects per environment (Def.), task-blocking defects per environment (Block Def.), the percentage of tasks with at least one bounded executable trace (Feasible), human task success rate (Human SR), state-invariant violation rate after marker-triggered updates (State Viol.), and average curation time per environment (Time). For policy learning, we report success rate (SR), average successful-episode length (Step), rejected marker-write rate (Reject), and sample efficiency. For simulation efficiency, we report LLM calls, token cost, latency, state fidelity, and training throughput. Figure 4: Verification–repair convergence. The repair loop rapidly removes defects and increases the fraction of tasks with bounded executable traces. The gains saturate after three to four iterations, supporting the use of targeted verification and repair rather than repeated full regeneration. 5.2 Main results RQ1: Does verification improve environment executability? Table 1 shows that raw LLM-generated environments are often invalid, with only 48.6% of tasks admitting bounded executable traces. Rule-based checks remove simple structural errors but miss task-blocking workflow defects and can reduce human success, while single-pass LLM verification still leaves many blocking defects. In contrast, our method achieves the fewest total and blocking defects, the highest feasible-task rate, the lowest state-violation rate, and lower curation time than self-consistency and AutoGen. Fig. 4 further shows that repair converges quickly: within three iterations, defects drop from 12.4 to 4.2 and feasible tasks rise from 48.6% to 90.7%, after which gains saturate. Method Def.↓ Block Def.↓ Feasible↑ Human SR↑ State Viol.↓ Time↓ No Verification 12.4 4.9 48.6% 36.9% 18.7% – Rule-Based 9.8 4.1 53.2% 27.2% 14.6% 0.5m Single-LLM 6.2 2.7 70.4% 54.3% 9.8% 12m Self-Consistency 5.8 2.1 79.6% 69.1% 7.2% 35m AutoGen 5.1 1.6 88.7% 89.2% 5.5% 28m Ours 3.3 0.7 94.8% 91.4% 2.8% 18m Table 1: Environment executability and fidelity. Verification should not merely reduce superficial defects; it should make generated tasks executable under consistent backend dynamics. Our method reduces both total defects and task-blocking defects. RQ2: Does verified synthetic training improve compact policies? We next evaluate whether verified environments improve downstream policy learning. Figure 5 compares PPO learning curves on held-out synthetic environments under different training substrates and reward signals. Training on raw environments gives weak performance because many failed episodes are caused by environment invalidity rather than policy errors. Dense rewards help on raw environments, but the gains remain limited because progress predicates can be noisy when the underlying scaffold is inconsistent. Verification alone improves learning under terminal rewards, while combining verified environments with state-grounded dense rewards produces the strongest learning curve and the best final success rate. Figure 5: Verified synthetic training improves compact policy learning. Raw environments provide noisy supervision, while verified environments make failures attributable to the policy. State-grounded dense rewards further accelerate learning and improve final success. RQ3: Which components matter? We ablate each major component using the same held-out environments and PPO setup. Fig. 6 reports environment quality, task executability, policy success, state violations, and curation cost, with colors indicating direction-corrected degradation. The feasibility verifier is most important for executable supervision, as removing it substantially reduces both feasible-task rate and PPO success. Marker validation mainly preserves backend fidelity by preventing state violations, while dense rewards primarily improve policy learning without changing environment quality. Together, these results show that reliable synthetic web training depends on three complementary ingredients: task-level feasibility verification, state-safe marker updates, and dense state-grounded rewards. Figure 6: Component ablation matrix. Rows remove individual components and columns report metrics with 95% confidence intervals. Colors denote direction-corrected degradation. Feasibility verification, marker validation, and dense rewards drive executability, state fidelity, and policy learning. 6 Conclusion We studied reinforcement learning for web agents from the perspective of environment reliability, arguing that synthetic websites must be executable, state-consistent, and auditable to provide useful supervision. We introduced a verified environment-construction framework that combines offline scaffold verification with event-driven state updates, enabling compact policies to learn from state-grounded synthetic interactions. Experiments show that task feasibility verification, marker-level validation, and dense backend-grounded rewards jointly improve environment executability and PPO performance. These findings highlight verified environments as a scalable training substrate, with future work extending this paradigm to richer multi-site and multimodal web workflows. References Branavan et al. [2009] S.R.K. Branavan, Harr Chen, Luke Zettlemoyer, and Regina Barzilay. Reinforcement learning for mapping instructions to actions. In Keh-Yih Su, Jian Su, Janyce Wiebe, and Haizhou Li, editors, Proceedings of the Joint Conference of the 47th Annual Meeting of the ACL and the 4th International Joint Conference on Natural Language Processing of the AFNLP, pages 82–90, Suntec, Singapore, August 2009. Association for Computational Linguistics. URL https://aclanthology.org/P09-1010/. Chae et al. [2025] Hyungjoo Chae, Sunghwan Kim, Junhee Cho, Seungone Kim, Seungjun Moon, Gyeom Hwangbo, Dongha Lim, Minjin Kim, Yeonjun Hwang, Minju Gwak, et al. Web-shepherd: Advancing prms for reinforcing web agents. arXiv preprint arXiv:2505.15277, 2025. Chen et al. [2025] Zhaorun Chen, Zhuokai Zhao, Kai Zhang, Bo Liu, Qi Qi, Yifan Wu, Tarun Kalluri, Sara Cao, Yuanhao Xiong, Haibo Tong, Huaxiu Yao, Hengduo Li, Jiacheng Zhu, Xian Li, Dawn Song, Bo Li, Jason Weston, and Dat Huynh. Scaling agent learning via experience synthesis, 2025. URL https://arxiv.org/abs/2511.03773. Chezelles et al. [2024] De Chezelles, Thibault Le Sellier, Sahar Omidi Shayegan, Lawrence Keunho Jang, Xing Han Lù, Ori Yoran, Dehan Kong, Frank F Xu, Siva Reddy, Quentin Cappart, et al. The browsergym ecosystem for web agent research. arXiv preprint arXiv:2412.05467, 2024. Deng et al. [2023] Xiang Deng, Yu Gu, Boyuan Zheng, Shijie Chen, Samuel Stevens, Boshi Wang, Huan Sun, and Yu Su. Mind2web: Towards a generalist agent for the web, 2023. URL https://arxiv.org/abs/2306.06070. Drouin et al. [2024] Alexandre Drouin, Maxime Gasse, Massimo Caccia, Issam H Laradji, Manuel Del Verme, Tom Marty, Léo Boisvert, Megh Thakkar, Quentin Cappart, David Vazquez, et al. Workarena: How capable are web agents at solving common knowledge work tasks? arXiv preprint arXiv:2403.07718, 2024. He et al. [2024] Hongliang He, Wenlin Yao, Kaixin Ma, Wenhao Yu, Yong Dai, Hongming Zhang, Zhenzhong Lan, and Dong Yu. Webvoyager: Building an end-to-end web agent with large multimodal models. In Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pages 6864–6890, 2024. Koh et al. [2024] Jing Yu Koh, Robert Lo, Lawrence Jang, Vikram Duvvur, Ming Lim, Po-Yu Huang, Graham Neubig, Shuyan Zhou, Russ Salakhutdinov, and Daniel Fried. Visualwebarena: Evaluating multimodal agents on realistic visual web tasks. In Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pages 881–905, 2024. Liu et al. [2018] Evan Zheran Liu, Kelvin Guu, Panupong Pasupat, Tianlin Shi, and Percy Liang. Reinforcement learning on web interfaces using workflow-guided exploration, 2018. URL https://arxiv.org/abs/1802.08802. Pan et al. [2024] Jiayi Pan, Yichi Zhang, Nicholas Tomlin, Yifei Zhou, Sergey Levine, and Alane Suhr. Autonomous evaluation and refinement of digital agents. arXiv preprint arXiv:2404.06474, 2024. Patel et al. [2024] Ajay Patel, Markus Hofmarcher, Claudiu Leoveanu-Condrei, Marius-Constantin Dinu, Chris Callison-Burch, and Sepp Hochreiter. Large language models can self-improve at web agent tasks, 2024. URL https://arxiv.org/abs/2405.20309. Putta et al. [2024] Pranav Putta, Edmund Mills, Naman Garg, Sumeet Motwani, Chelsea Finn, Divyansh Garg, and Rafael Rafailov. Agent q: Advanced reasoning and learning for autonomous ai agents. arXiv preprint arXiv:2408.07199, 2024. Qi et al. [2024] Zehan Qi, Xiao Liu, Iat Long Iong, Hanyu Lai, Xueqiao Sun, Wenyi Zhao, Yu Yang, Xinyue Yang, Jiadai Sun, Shuntian Yao, et al. Webrl: Training llm web agents via self-evolving online curriculum reinforcement learning. arXiv preprint arXiv:2411.02337, 2024. Schulman et al. [2017] John Schulman, Filip Wolski, Prafulla Dhariwal, Alec Radford, and Oleg Klimov. Proximal policy optimization algorithms, 2017. URL https://arxiv.org/abs/1707.06347. Shi et al. [2017] Tianlin Shi, Andrej Karpathy, Linxi Fan, Jonathan Hernandez, and Percy Liang. World of bits: An open-domain platform for web-based agents. In Doina Precup and Yee Whye Teh, editors, Proceedings of the 34th International Conference on Machine Learning, volume 70 of Proceedings of Machine Learning Research, pages 3135–3144. PMLR, 06–11 Aug 2017. URL https://proceedings.mlr.press/v70/shi17a.html. Yang et al. [2024] Ke Yang, Yao Liu, Sapana Chaudhary, Rasool Fakoor, Pratik Chaudhari, George Karypis, and Huzefa Rangwala. Agentoccam: A simple yet strong baseline for llm-based web agents. arXiv preprint arXiv:2410.13825, 2024. Yao et al. [2023a] Shunyu Yao, Howard Chen, John Yang, and Karthik Narasimhan. Webshop: Towards scalable real-world web interaction with grounded language agents, 2023a. URL https://arxiv.org/abs/2207.01206. Yao et al. [2023b] Shunyu Yao, Jeffrey Zhao, Dian Yu, Nan Du, Izhak Shafran, Karthik Narasimhan, and Yuan Cao. React: Synergizing reasoning and acting in language models, 2023b. URL https://arxiv.org/abs/2210.03629. Zala et al. [2024] Abhay Zala, Jaemin Cho, Han Lin, Jaehong Yoon, and Mohit Bansal. Envgen: Generating and adapting environments via llms for training embodied agents, 2024. URL https://arxiv.org/abs/2403.12014. Zhou et al. [2024] Shuyan Zhou, Frank F. Xu, Hao Zhu, Xuhui Zhou, Robert Lo, Abishek Sridhar, Xianyi Cheng, Tianyue Ou, Yonatan Bisk, Daniel Fried, Uri Alon, and Graham Neubig. Webarena: A realistic web environment for building autonomous agents, 2024. URL https://arxiv.org/abs/2307.13854. Appendix A Additional Technical Details A.1 Details of the Preliminary Diagnostics This subsection provides additional details for the motivating diagnostics in Section 3.2. The goal of these diagnostics is not to serve as the main evaluation, but to empirically justify two design choices: (i) one-shot generated scaffolds require offline verification, and (i) runtime state evolution can be handled by sparse event-driven updates rather than by calling a generative model at every step. A.1.1 Raw Environment Pool We construct a diagnostic pool of raw LLM-generated web environments before any verification or repair. Each environment is generated from a domain-level site specification and contains page templates, navigation links, database records, state-change candidates, and task specifications. The environments cover six representative domains: dom=e-commerce,social media,banking,education,healthcare,government.D_dom=\e-commerce,social media,banking,education,healthcare,government\. For each environment E, we record its page set P, navigation graph L, database schema D, initialized records, interactive elements, and task set T⁡(E)T(E). The diagnostic study reports statistics over 500 raw environments and 6,842 generated tasks. A.1.2 Defect Categories and Detection Criteria We use four defect categories. A detected defect is represented as d=⟨type,loc,obj,sev,ev⟩,d= ,loc,obj,sev,ev , where type∈ΔS,ΔC,ΔX,ΔTtype∈\ _S, _C, _X, _T\ is the defect category, locloc is the affected page, DOM node, database field, or task, objobj is the affected object, sev∈[0,1]sev∈[0,1] is the severity score, and evev is the supporting evidence. Category Typical failures Detection criterion Structural (ΔS)( _S) Broken links, orphaned pages, missing navigation elements The page graph is not connected from the entry page, a declared link has no target, or a required UI element is absent. Semantic (ΔC)( _C) Invalid prices, malformed dates, placeholder text, type mismatch A rendered value violates the declared schema, expected field type, or page-level content semantics. Consistency (ΔX)( _X) Conflicting prices, inconsistent user attributes, mismatched entity states The same entity attribute takes incompatible values across pages, views, or database bindings. Feasibility (ΔT)( _T) Missing buttons, inaccessible forms, incomplete workflow, unsatisfiable task No bounded executable trace can satisfy the task completion constraint under the current scaffold. Table 2: Defect categories and detection criteria used in the preliminary diagnostics. For each environment E, we count the number of detected defects in category c as Nc(E)=∑d∈Δ⁡(E)[type(d)=c],N_c(E)= _d∈ (E)1[type(d)=c], where Δ⁡(E) (E) is the full defect set of E. A.1.3 Bounded Trace Analysis To determine whether a task is executable, we perform bounded trace analysis. Given a task t, an initial state distribution ρt _t, and a completion constraint CtC_t, the analysis searches for an action sequence a1:H=(a1,…,aH)a_1:H=(a_1,…,a_H) such that s0∼ρt,sk+1=⁡(sk,ak),ak∈A⁡(ok),Ct(sH)=1,s_0 _t, s_k+1=T(s_k,a_k), a_k∈ A(o_k), C_t(s_H)=1, for some horizon H≤HmaxH≤ H_ . If such a trace exists, the task is considered executable under the current scaffold. Otherwise, the task is marked as blocked. This trace search is used only for diagnostics, not for policy training. Algorithm 1 Bounded Trace Analysis for Task Feasibility 0: Environment E, task t, initial states 0S_0, horizon HmaxH_ 0: Executable flag and blocking evidence 1: Initialize queue Q←(s0,[]):s0∈0Q←\(s_0,[]):s_0 _0\ 2: Initialize visited set ←∅V← 3: for h=0,…,Hmaxh=0,…,H_ do 4: Initialize next queue Q′←∅Q ← 5: for each (s,π)∈Q(s,π)∈ Q do 6: if Ct(s)=1C_t(s)=1 then 7: return (Executable,π,∅)( Executable,π, ) 8: end if 9: o←Render⁡(s)o (s) 10: Extract candidate actions A⁡(o)A(o) 11: for each a∈A⁡(o)a∈ A(o) do 12: Execute s′←⁡(s,a)s (s,a) 13: Record transition evidence ev⁡(s,a,s′)ev(s,a,s ) 14: if s′∉s then 15: Q′←Q′∪(s′,π∘a)Q ← Q ∪\(s ,π a)\ 16: ←∪s′V ∪\s \ 17: end if 18: end for 19: end for 20: Q←Q′Q← Q 21: end for 22: Extract blocking evidence from failed expansions 23: return (Blocked,∅,ev)( Blocked, ,ev) A.1.4 Blocking Attribution When a task is blocked, we attribute the failure to the earliest defect category that prevents progress along the attempted workflow. Let Reachh(E,t)Reach_h(E,t) denote the set of states reachable within h steps from the task initial state. A defect d is considered task-blocking if it invalidates all outgoing progress transitions from the current reachable frontier. We define Blockc⁡(E,t)=1Block_c(E,t)=1 if at least one defect of category c is responsible for blocking all bounded traces for task t. If multiple defect categories are implicated, we apply the following priority order based on causal proximity to execution: ΔT≻ΔS≻ΔX≻ΔC. _T _S _X _C. Feasibility defects are assigned first because they directly indicate missing workflow steps or inaccessible required controls. Structural defects are next because they prevent reaching necessary pages. Consistency and semantic defects are assigned when the task path exists but the required state or content is invalid. The task-blocking rate reported in the main text is Bc(E)=1|T⁡(E)|∑t∈T⁡(E)[Blockc(E,t)=1].B_c(E)= 1|T(E)| _t∈ T(E)1\! [Block_c(E,t)=1 ]. The global blocking rate for category c across environments is B¯c=1|ℰ|∑E∈ℰBc(E). B_c= 1|E| _E B_c(E). A.1.5 State-Change Markers and Runtime Statistics A state-change marker identifies a UI event that may modify persistent backend state. Each marker is represented as m=(em,prem,Rm,Wm,Ωm),m=(e_m,pre_m,R_m,W_m, _m), where eme_m is the triggering element, prempre_m is a precondition, RmR_m and WmW_m are the permitted read and write fields, and Ωm _m is the operation signature. Typical marker-triggered events include add-to-cart, submit-order, update-profile, create-post, and submit-application. For a successful trajectory τ=(s0,a0,s1,a1,…,sH),τ=(s_0,a_0,s_1,a_1,…,s_H), we compute the marker-trigger rate M(τ)=1H∑k=0H−1[μ(pk,ak)≠∅],M(τ)= 1H _k=0^H-11\! [μ(p_k,a_k)≠ ], and the number of runtime state-write calls U(τ)=∑k=0H−1[μ(pk,ak)≠∅].U(τ)= _k=0^H-11\! [μ(p_k,a_k)≠ ]. Here, μ⁡(pk,ak)μ(p_k,a_k) returns the marker triggered by action aka_k on page pkp_k, if such a marker exists. Deterministic UI actions, including navigation, scrolling, menu expansion, and local text entry, do not trigger persistent state writes. For marker-triggered operations, a candidate state delta δ^k δ_k is accepted only if it satisfies the marker precondition, schema constraints, and environment invariants: δk=Validatemk(δ^k,sk,ak)∈mk(sk,ak)∪⊥. _k=Validate_m_k( δ_k;s_k,a_k) _m_k(s_k,a_k)∪\ \. The accepted-delta rate is A⁡(τ)=∑k=0H−1[μ(pk,ak)≠∅][δk≠⊥]∑k=0H−1[μ(pk,ak)≠∅]+ϵ,A(τ)= _k=0^H-11\! [μ(p_k,a_k)≠ ]1\! [ _k≠ ] _k=0^H-11\! [μ(p_k,a_k)≠ ]+ε, where ϵε is a small constant used only to avoid division by zero for trajectories with no marker-triggered event. A.1.6 Confidence Intervals and Visualization Protocol For each scalar statistic z1,…,znz_1,…,z_n, we report the empirical mean and the normal-approximation 95% confidence interval: z¯=1n∑i=1nzi,CI95=1.96std⁡(z1,…,zn)n. z= 1n _i=1^nz_i, _95=1.96 std(z_1,…,z_n) n. In Fig. 2, each point corresponds to one environment or one trajectory, depending on the panel. Jitter is used only for visualization and does not affect the reported statistics. Panel (a) shows per-environment defect counts. Panel (b) shows task-blocking rates conditioned on detected defects. Panel (c) shows marker-trigger rates grouped by domain. Panel (d) shows the relationship between episode length and the number of runtime state-write calls, with the fitted line used only as a visual summary. These diagnostics are intended to motivate the method design. The main experimental evaluation in Section 5 separately measures environment quality, repair effectiveness, and downstream policy performance. A.2 Canonical Parsing and Symbolic Verification Raw scaffold artifacts. Given a site description q, the generator produces raw artifacts ℰ~=(~,ℒ~,~,~), E=( P, L, D, Q), where ~ P contains page templates, ℒ~ L contains declared links and menus, ~ D contains database schema and initialized records, and ~ Q contains task instructions with completion constraints. The parser converts these artifacts into the canonical scaffold ℰ(0)E^(0) by extracting DOM nodes, interactive elements, database bindings, and state-change markers. Page and binding representation. Each page p∈p is represented as p=(τp,ℐp,Γp),p=( _p,I_p, _p), where τp _p is a DOM template, ℐpI_p is the set of interactive elements, and Γp _p maps DOM variables to database fields. For an interactive element e∈ℐpe _p, the parser records its element type, admissible arguments, page-level effect, and marker association. Marker schema. A marker m=(em,prem,Rm,Wm,Ωm)m=(e_m,pre_m,R_m,W_m, _m) is attached to a persistent state-changing element. The precondition prempre_m specifies when the operation is valid. The sets RmR_m and WmW_m specify database fields that the operation reads and writes. The operation signature Ωm _m contains the operation name, target entity type, argument schema, output delta schema, and invariant checks. Symbolic checks. The symbolic verifier computes Δsym=Δreach∪Δlink∪Δschema∪Δbind∪Δmark. _sym= _reach∪ _link∪ _schema∪ _bind∪ _mark. The individual defect sets are Δreach _reach =p∈:p∉Reach⁡(phome,ℒ), =\p :p (p_home,L)\, Δlink _link =(pi,pj)∈ℒ:pj∉, =\(p_i,p_j) :p_j \, Δschema _schema =g:gviolates a type, key, range, or required-field constraint in, =\g:g\ violates a type, key, range, or required-field constraint in\ D\, Δbind _bind =(p,g):g∈Γp,field(g)∉Fields(), =\(p,g):g∈ _p,\;field(g) (D)\, Δmark _mark =m∈ℳ:Rm∪Wm⊈Fields⁡()orΩmhas an invalid argument schema. =\m :R_m∪ W_m (D)\ or\ _m\ has an invalid argument schema\. Here, phomep_home is the entry page, ReachReach returns reachable pages under the navigation graph, and Fields⁡()Fields(D) is the set of valid database fields. These deterministic checks are run before semantic verification and after each repair iteration on the affected subgraph. A.3 Semantic Verifiers and Defect-Triggered Coordination Verifier roles. We use four semantic verifiers: =str,sem,cons,feas.J=\str,sem,cons,feas\. The structural verifier checks layout coherence, missing required elements, and navigation anomalies beyond link existence. The semantic verifier checks content validity, content–type compatibility, placeholder text, and implausible values. The consistency verifier checks entity attributes across pages and rendered states. The feasibility verifier searches for bounded executable traces that satisfy task constraints. Structured defect report. Each verifier j∈j returns a set of reports j(ℰ(r))→Δj(r)=dj,1(r),…,dj,nj(r).A_j(E^(r))→ _j^(r)=\d_j,1^(r),…,d_j,n_j^(r)\. Each report has the schema d=⟨type,loc,obj,sev,ev,c⟩,d= ,loc,obj,sev,ev,c , where typetype is the defect category, locloc is the page, DOM node, database field, marker, or task where the defect occurs, objobj is the affected object, sev∈[0,1]sev∈[0,1] is severity, evev is supporting evidence, and c∈[0,1]c∈[0,1] is verifier confidence. Deduplication. Reports are merged by a canonical key κ⁡(d)=(type⁡(d),loc⁡(d),obj⁡(d)).κ(d)=(type(d),loc(d),obj(d)). All reports with the same key are grouped into one defect candidate. The main text defines the aggregated confidence in Eq. (8). Defect-triggered coordination. Verifier communication is routed by defect type: B⁡(type⁡(d))⊆,B(type(d)) , where B returns verifiers that need to re-check downstream effects of d. We use the following routing rules: B⁡(structural) B(structural) =feas, =\feas\, B⁡(semantic) B(semantic) =cons, =\cons\, B⁡(consistency) B(consistency) =feas, =\feas\, B⁡(feasibility) B(feasibility) =str,cons. =\str,cons\. For a defect d, the coordinator adds targeted requests Q←Q∪(d,j′):j′∈B⁡(type⁡(d)).Q← Q∪\(d,j ):j ∈ B(type(d))\. The receiving verifier checks only the affected pages, database fields, markers, and tasks referenced in the report evidence. Accepted defect set. A defect is accepted for repair when conf⁡(d)≥τcorsev⁡(d)≥τs,conf(d)≥ _c (d)≥ _s, where τc _c is the confidence threshold and τs _s is the severity threshold. This rule preserves high-severity single-verifier defects while filtering low-confidence reports. A.4 Repair Operators and Termination Dependency graph. Accepted defects form a dependency graph GΔ(r)=(Δacc(r),ℛΔ(r)),G_ ^(r)=( _acc^(r),R_ ^(r)), where (di,dj)∈ℛΔ(r)(d_i,d_j) _ ^(r) means that did_i must be repaired before djd_j. Dependencies are added when a database schema defect affects page rendering, when a marker defect affects task feasibility, and when a structural defect blocks access to pages used by semantic and consistency checks. Ready set. At iteration r, the ready set is Ready(r)=d∈Δacc(r):PredGΔ(d)⊆done(r),Ready^(r)=\d∈ _acc^(r):Pred_G_ (d) _done^(r)\, where PredGΔ(d)Pred_G_ (d) is the predecessor set of defect d, and done(r)S_done^(r) is the set of repaired defects. The selected defect is d⋆=arg⁡maxd∈Ready(r)⁡score⁡(d),d = _d ^(r)score(d), where score⁡(d)score(d) is defined in Eq. (9). Repair operators. The repair operator ℛd⋆R_d edits only objects referenced by the accepted report: ℰ(r+1)=ℛd⋆(ℰ(r)).E^(r+1)=R_d (E^(r)). We use the following repair families. • Structural repair. Adds missing pages, repairs invalid links, restores required navigation elements, and reconnects orphaned pages to the navigation graph. • Semantic repair. Rewrites invalid content while preserving database bindings and task-relevant entities. • Consistency repair. Selects a canonical value from the database and propagates it to all dependent DOM bindings. • Feasibility repair. Adds missing form fields, buttons, intermediate pages, marker signatures, and database writes required by a bounded task trace. • Marker repair. Corrects marker preconditions, argument schema, read–write sets, and invariant checks. Incremental re-verification. After repairing d⋆d , we re-check the affected subgraph ⁡(d⋆)=p:distℒ(p,loc⁡(d⋆))≤1∪Tasks⁡(d⋆)∪Markers⁡(d⋆),N(d )=\p:dist_L(p,loc(d ))≤ 1\ (d ) (d ), where distℒdist_L is graph distance in the navigation graph. This prevents each repair iteration from re-running all verifiers on the entire environment. Feasibility termination. For a task t, feasibility is accepted when the feasibility verifier finds a bounded executable trace π1:H=(a1,…,aH)such thatsk+1=F(sk,ak),ak∈(ok),Ct(sH)=1. _1:H=(a_1,…,a_H) that s_k+1=F(s_k,a_k),\;a_k (o_k),\;C_t(s_H)=1. The repair loop terminates when all accepted critical defects are resolved and every task has at least one such bounded trace. A.5 Event-Driven Simulator Details Deterministic transition. The deterministic transition FdetF_det handles navigation, local input editing, scroll state, menu expansion, client-side field validation, and page rendering. It does not modify persistent database records outside session-local variables. Candidate delta generation. For a marker-triggered action, the state writer receives zk=Pack⁡(pk,bk,Rm,σk,ak,Ωm),z_k=Pack(p_k,b_k,R_m, _k,a_k, _m), where bk,Rmb_k,R_m is the subset of database records referenced by the marker read set. The state writer outputs a candidate delta δ^k=Gψ(zk). δ_k=G_ψ(z_k). The output schema contains only field-level writes, session updates, and a short justification tied to Ωm _m. Full-page natural-language regeneration is not accepted as a state update. Feasible update set. For marker m, the feasible update set is m(sk,ak)=δ:prem(sk,ak)=1,RW(δ)⊆Rm∪Wm,bk⊕δ⊧,Inv(sk⊕δ)=1.U_m(s_k,a_k)= \δ:pre_m(s_k,a_k)=1,\;RW(δ) R_m∪ W_m,\;b_k δ ,\;Inv(s_k δ)=1 \. Here, RW⁡(δ)RW(δ) is the set of fields read and written by the delta, bk⊕δb_k δ is the database after applying the delta, and InvInv contains environment invariants including schema validity, entity identity consistency, permission constraints, and task-independent workflow constraints. Validation. The validation operator returns Validatem(δ^k,sk,ak)=δ^k,δ^k∈m(sk,ak),⊥,δ^k∉m(sk,ak).Validate_m( δ_k;s_k,a_k)= cases δ_k,& δ_k _m(s_k,a_k),\\ ,& δ_k _m(s_k,a_k). cases If the result is ⊥ , the simulator returns the original state, sets ϵk=1 _k=1, and exposes the rejected operation in the transition log. Otherwise, the simulator applies sk+1=sk⊕δks_k+1=s_k _k, re-renders the current page through RenderRender, and records the state delta for reward computation and debugging. A.6 Reward Compilation and PPO Training Predicate compilation. Each completion constraint CtC_t is decomposed into predicates Φt=ϕt,1,…,ϕt,Mt. _t=\ _t,1,…, _t,M_t\. Predicates are implemented as database queries, session-state checks, and DOM selectors. Examples include checking that a required page has been visited, a field has a valid value, a target entity has been created, an attribute has been updated correctly, and a rendered page reflects the backend value. Candidate action scoring. The policy receives the task instruction xtx_t, the rendered observation oko_k, and the candidate action set ⁡(ok)A(o_k). It scores each candidate action by ℓθ(a,ok,xt),a∈⁡(ok), _θ(a;o_k,x_t), a (o_k), and normalizes over the current candidate set: πθ(a∣ok,xt)=exp⁡(ℓθ(a,ok,xt))∑a′∈⁡(ok)exp⁡(ℓθ(a′,ok,xt)). _θ(a o_k,x_t)= ( _θ(a;o_k,x_t)) _a (o_k) ( _θ(a ;o_k,x_t)). Since sampling is restricted to ⁡(ok)A(o_k), invalid DOM actions do not appear in the policy distribution. Rejected transitions in the main reward arise from marker validation failures, not from selecting unavailable DOM elements. Trajectory collection. For each task t, PPO collects rollouts τ=(o0,a0,r0,o1,…,oH)τ=(o_0,a_0,r_0,o_1,…,o_H) by executing πθ _θ in the event-driven simulator. The environment computes rewards using Eq. (13); the policy does not observe the backend state, completion constraint, or progress predicates. Advantage estimation. We use generalized advantage estimation: A^k=∑ℓ=0H−k−1(ξλGAE)ℓδk+ℓV,δkV=rk+ξVθold(ok+1,xt)−Vθold(ok,xt), A_k= _ =0^H-k-1(ξ _GAE) δ^V_k+ , δ^V_k=r_k+ξ V_ _old(o_k+1,x_t)-V_ _old(o_k,x_t), where ξ is the RL discount factor, λGAE _GAE controls the bias–variance trade-off, and VθV_θ is the value function. PPO objective. The probability ratio is ρk(θ)=πθ(ak∣ok,xt)πθold(ak∣ok,xt). _k(θ)= _θ(a_k o_k,x_t) _ _old(a_k o_k,x_t). The policy is optimized with the clipped objective ℒPPO(θ)= _PPO(θ)= k[min⁡(ρk(θ)A^k,clip⁡(ρk(θ),1−ϵ,1+ϵ)A^k)] _k [ ( _k(θ) A_k,clip( _k(θ),1-ε,1+ε) A_k ) ] −cvk[(Vθ(ok,xt)−R^k)2]+chk[ℋ(πθ(⋅∣ok,xt))]. -c_vE_k [ (V_θ(o_k,x_t)- R_k )^2 ]+c_hE_k [H( _θ(· o_k,x_t)) ]. where ϵε is the clipping threshold, R^k R_k is the empirical return, cvc_v weights the value loss, chc_h weights the entropy bonus, and ℋH is policy entropy. Evaluation-time policy. At evaluation time, the learned policy uses only oko_k, xtx_t, and the DOM-grounded candidate actions ⁡(ok)A(o_k). It does not call the generation model, semantic verifiers, repair operators, or constrained state writer. A.7 Four agents design Four specialized LLM-based agents collaborate to detect complex defects requiring semantic understanding. Each agent is implemented as a GPT-4 instance with domain-specific system prompts and structured output schemas. Structure Validator (SV): Analyzes page layouts and navigation flows to identify structural anomalies beyond simple link checking. SV examines: (1) navigation consistency (breadcrumb accuracy, menu completeness), (2) page hierarchy adherence (category → subcategory → item), and (3) required element presence (search bars, footers, headers). Detection is based on embedding similarity using a fine-tuned sentence transformer to identify outlier page structures. Content Auditor (CA): Examines content for semantic validity using GPT-4’s world knowledge. CA detects: (1) placeholder text patterns (“Lorem ipsum”, “[TODO]”, “Example”), (2) content-metadata mismatches (product description contradicting title), (3) implausible content (negative prices, future birthdates), and (4) inappropriate content for page type (technical jargon on consumer pages). Consistency Checker (C): Cross-references data across pages using an entity database. For each entity e with attributes a1,…,ak\a_1,…,a_k\, C tracks all occurrences across pages and flags when ai(pj)≠ai(pk)a_i(p_j)≠ a_i(p_k) for any attribute. Semantic equivalence is handled via embedding similarity (threshold 0.92) for string attributes. Task Feasibility Analyzer (TFA): Traces task execution paths by simulating agent trajectories. For each task t∈t , TFA generates an action sequence using GPT-4 and verifies: (1) all required pages exist, (2) all form fields are accessible, (3) all buttons are clickable, and (4) the goal state is reachable. Type Example Detection Structural Link to /checkout returns 404 Graph + HTTP Semantic Price field shows “TBD” instead of $29.99 Schema + LLM Consistency Product $49 on list, $59 on detail Cross-page DB Feasibility “Add to cart” button not clickable Task simulation Table 3: Defect Examples and Detection Complexity A.7.1 Defect-Triggered Communication Protocol Rather than independent parallel execution, agents communicate through DTCP to enable cross-agent defect correlation. When agent AiA_i detects a defect d, it broadcasts a structured message to relevant agents: msg(d)=⟨type,location,severity,evidence⟩msg(d)= ,location,severity,evidence (14) Receiving agents use domain-specific rules to determine follow-up actions: • SV→TFASV→ TFA: Structural defects trigger task re-verification • CA→CCCA→ C: Semantic issues trigger consistency checks • CC→TFACC→ TFA: Data conflicts trigger feasibility re-analysis • TFA→SVTFA→ SV: Workflow gaps trigger navigation review A.8 Agent Configuration Details Structural Verification Agent The Structural Verification Agent (SA_S) employs the following prompt template: Figure 7: Structural Verification Agent Consistency Verification Agent The Consistency Verification Agent (CA_C) uses: Figure 8: Consistency Verification Agent Cross-Page Verification Agent The Cross-Page Verification Agent (XA_X) configuration: Figure 9: Cross-Page Verification Agent Task Flow Verification Agent The Task Flow Verification Agent (TA_T) prompt: Figure 10: Task Flow Verification Agent A.9 DTCP Protocol Specification Algorithm 2 presents the complete Defect-Triggered Communication Protocol. Algorithm 2 Defect-Triggered Communication Protocol (DTCP) 0: Agents S,C,X,T\A_S,A_C,A_X,A_T\, Environment ℰE, Thresholds τ1,τ2\ _1, _2\ 0: Aggregated defect reports Δ 1: Initialize message queue Q←∅Q← 2: Initialize defect set Δ←∅ ← 3: for each agent iA_i in parallel do 4: δi←i.Verify(ℰ) _i _i. Verify(E) 5: for each defect d∈δid∈ _i do 6: if d.confidence<τ1d.confidence< _1 then 7: Q.Push(RequestVerification(d,i))Q. Push( RequestVerification(d,A_i)) 8: else if d.affects_other_domaind.affects\_other\_domain then 9: Q.Push(NotifyRelated(d,i))Q. Push( NotifyRelated(d,A_i)) 10: end if 11: Δ←Δ∪d ← ∪\d\ 12: end for 13: end for 14: while Q≠∅Q≠ do 15: msg←Q.Pop()msg← Q. Pop() 16: j←GetTargetAgent(msg)A_j← GetTargetAgent(msg) 17: response←j.ProcessMessage(msg)response _j. ProcessMessage(msg) 18: if response.type=Confirmresponse.type= Confirm then 19: Δ[msg.defect].confidence+=τ2 [msg.defect].confidence += _2 20: else if response.type=Rejectresponse.type= Reject then 21: Δ.Remove(msg.defect) . Remove(msg.defect) 22: else if response.type=NewDefectresponse.type= NewDefect then 23: Δ←Δ∪response.defect ← ∪\response.defect\ 24: end if 25: end while 26: return Δ A.10 PWRS Algorithm Details The Priority-Weighted Repair Scheduling (PWRS) algorithm considers defect dependencies and repair costs. Algorithm 3 Priority-Weighted Repair Scheduling (PWRS) 0: Defects Δ , Dependency graph GdG_d, Weight function w 0: Ordered repair schedule S 1: S←[]S←[] 2: Compute priority scores: ∀d∈Δ:p⁡(d)=w⁡(d)⋅downstream(d,Gd)∀ d∈ :p(d)=w(d)·downstream(d,G_d) 3: Build dependency-aware priority queue PQPQ ordered by p⁡(d)p(d) 4: while PQ≠∅PQ≠ do 5: d←PQ.PopMax()d← PQ. PopMax() 6: if DependenciesSatisfied(d,S,Gd) DependenciesSatisfied(d,S,G_d) then 7: S.Append(d)S. Append(d) 8: Update downstream priorities in PQPQ 9: else 10: PQ.Push(d)PQ. Push(d) with reduced priority 11: end if 12: end while 13: return S Appendix B Experimental Details B.1 Implementation Details and Hyperparameters We implement the environment generator, canonical parser, symbolic verifiers, repair operators, event-driven simulator, and PPO training pipeline in Python. Each synthetic environment is stored as a structured scaffold containing page templates, navigation edges, database schemas and records, marker specifications, task instructions, and programmatic completion constraints. All baselines use the same raw scaffolds and train the same compact DOM-grounded policy unless otherwise stated. The policy contains fewer than 10M parameters and scores only DOM-grounded candidate actions extracted from the current rendered observation. We use Adam for optimization. Unless otherwise stated, PPO uses discount factor ξ=0.99ξ=0.99, GAE parameter λGAE=0.95 _GAE=0.95, clipping threshold 0.20.2, value-loss coefficient 0.50.5, entropy coefficient 0.010.01, learning rate 3×10−43× 10^-4, and gradient clipping threshold 0.50.5. Advantages are normalized within each PPO batch. The dense reward coefficients in Eq. (13) are fixed across domains and selected on the validation split: α=0.5α=0.5, γ=0.2γ=0.2, and η=0.01η=0.01. Here, α controls the contribution of verified progress shaping, γ penalizes rejected marker-triggered state updates, and η is a small per-step cost that discourages unnecessarily long trajectories. The maximum episode horizon is Hmax=40H_ =40. Each PPO update uses 40964096 rollout steps, minibatch size 512512, and 44 optimization epochs. We train each policy for 1.0×1061.0× 10^6 environment steps unless otherwise stated. For all reported policy experiments, we use the same train/validation/test environment split described in Section 5. Hyperparameters are selected using validation environments only and are then fixed for held-out synthetic evaluation and transfer evaluation. B.2 Compute Resources All experiments were run on a shared Linux compute cluster using CPU rollout workers and single-GPU training jobs. Each PPO training job used one NVIDIA A10G GPU with 24GB memory, 16 CPU cores, 64GB system RAM, and approximately 200GB local scratch storage for rollout logs and checkpoints. Synthetic environment generation and verification primarily used CPU workers plus LLM API calls, while PPO training used GPU workers for policy optimization and CPU workers for parallel environment rollout. A single PPO run for one training condition takes approximately 3.2 hours on one NVIDIA A10G GPU, corresponding to about 3.2 GPU-hours. The main learning-curve experiments use five training conditions and three random seeds, for a total of approximately 48 GPU-hours. The component ablation experiments use seven ablated variants and three random seeds, requiring approximately 67 GPU-hours. The additional diagnostic experiments, including defect-impact analysis, dense-reward alignment, simulator tradeoff analysis, and failure attribution, require approximately 35 GPU-hours in total. Transfer evaluation on WebArena, WebShop, and MiniWoB++ requires approximately 8 GPU-hours and 90 CPU-hours because the learned policy does not call an LLM at evaluation time. Environment construction uses 500 raw synthetic environments and invokes LLM-based verifiers only during offline scaffold verification and repair. For our full verification pipeline, the average curation time is 18 minutes per environment, as reported in Table 1. This corresponds to approximately 150 CPU-hours for the full synthetic environment suite, excluding parallelization overhead. The event-driven simulator cost and token usage are reported in Figure 11. Across all reported environment-construction runs, we used approximately 18 million LLM input/output tokens for scaffold generation, verification, and repair. Appendix C Additional Experimental Results C.1 Does the learned policy transfer beyond synthetic environments? The main experiments evaluate whether verification improves learning on held-out synthetic environments. We additionally test whether the learned policy transfers to external web-agent benchmarks under a unified DOM-grounded action interface. The goal of this experiment is not to claim that a small policy universally dominates frontier LLM agents under their native multimodal browser interfaces, but to test whether verified synthetic training produces reusable interaction skills when all methods are evaluated under the same observation and action protocol. Protocol. We evaluate on three external benchmarks: WebArena-compatible tasks, WebShop, and MiniWoB++. For WebArena, we use a DOM-compatible subset that does not require private credentials, file uploads, or visual-only information unavailable to the compact policy. Task goals are not rewritten, and benchmark success criteria are preserved. All evaluated methods receive the same textual task instruction and the same serialized DOM observation. All methods select from the same DOM-grounded action set, including click, type, select, and navigation actions. The compact policies do not call an LLM during evaluation. GPT-4 baselines use the same action interface and are evaluated with a fixed action budget. Benchmark # Tasks Observation Success Criterion WebArena-compatible 180 Serialized DOM + task Original programmatic evaluator WebShop 500 Product-page DOM + task Original purchase-match evaluator MiniWoB++ 560 DOM + task Original environment reward Table 4: Transfer-evaluation protocol. We use a unified DOM-grounded interface for all methods. WebArena results are reported on the DOM-compatible subset described in the text; WebShop and MiniWoB++ use their original success evaluators. Baselines. We compare against GPT-4 direct prompting, GPT-4 with ReAct-style prompting, a small policy trained by behavior cloning on synthetic trajectories, PPO trained on raw synthetic environments, PPO trained on verified environments with terminal rewards only, and our full method. GPT-4 baselines use temperature 00, a maximum of 20 actions per episode for WebArena-compatible tasks, and the same DOM action schema as the compact policy. For learned policies, no external benchmark fine-tuning is performed. Method WebArena SR↑ WebShop SR↑ MiniWoB++ SR↑ Eval LLM Calls↓ WebArena Step↓ GPT-4 Direct Prompting 10.6±2.110.6±2.1 32.5±2.732.5±2.7 41.2±2.941.2±2.9 17.517.5 17.5±0.617.5±0.6 GPT-4 ReAct 15.3±2.615.3±2.6 38.7±2.938.7±2.9 47.6±3.147.6±3.1 21.821.8 14.3±0.514.3±0.5 Small Policy, Synthetic BC 11.9±2.311.9±2.3 30.4±2.530.4±2.5 39.8±2.839.8±2.8 0.00.0 16.8±0.716.8±0.7 PPO on Raw Synthetic Env. 12.4±2.412.4±2.4 29.6±2.529.6±2.5 38.9±2.838.9±2.8 0.00.0 17.2±0.617.2±0.6 PPO on Verified Env. + Terminal 14.7±2.514.7±2.5 37.2±2.837.2±2.8 48.5±3.148.5±3.1 0.00.0 16.0±0.516.0±0.5 Ours 18.6±2.818.6 2.8 43.8±3.043.8 3.0 55.4±3.155.4 3.1 0.00.0 15.1±0.515.1 0.5 Table 5: Transfer beyond synthetic environments. All methods are evaluated under the same DOM-grounded observation and action interface. The compact policy trained in verified environments transfers better than policies trained on raw synthetic environments, while requiring no LLM calls at evaluation time. The comparison to GPT-4 baselines should be interpreted under this constrained DOM-only interface, not as a claim of general superiority under native multimodal browser use. Analysis. Verified synthetic training improves transfer on all three external benchmarks. Compared with PPO trained on raw synthetic environments, our full method improves success by 6.26.2 points on WebArena-compatible tasks, 14.214.2 points on WebShop, and 16.516.5 points on MiniWoB++. The largest gains appear on WebShop and MiniWoB++, where the external environments share more structural similarity with the synthetic training tasks. On WebArena-compatible tasks, the gains are smaller but still consistent, suggesting that verification improves general interaction skills rather than only fitting synthetic layouts. Importantly, the compact policy uses zero LLM calls at evaluation time. We therefore interpret these results as evidence that verified synthetic environments provide reusable supervision for efficient policies under a common DOM-grounded interface. C.2 Does event-driven simulation reduce cost while preserving state fidelity? A central design choice of our framework is to execute ordinary interface transitions deterministically and invoke constrained state writing only at sparse marker-triggered events. To understand whether this design improves the cost–fidelity tradeoff, we compare our simulator against three alternatives: (i) a Step-wise LLM simulator that queries an LLM for every transition, (i) a Deterministic-only simulator that never performs backend writes, and (i) an Unconstrained Marker LLM simulator that invokes an LLM only at markers but does not validate the proposed state deltas against marker schemas and invariants. Instead of reporting a separate table and a separate Pareto plot, Fig. 11 summarizes the full comparison in one figure. The left panel reports the mean and 95% confidence interval for six metrics: average LLM calls per episode (LLM Calls), token usage per episode (Tokens), end-to-end episode latency (Latency), state fidelity to the reference execution (State Fidelity), state-invariant violation rate after writes (State Viol.), and rollout throughput (Throughput). The right panel visualizes the rollout-level Pareto tradeoff between token cost and state fidelity, where faint points show individual rollout-batch observations and large markers show mean performance with 95% confidence intervals. Figure 11: Cost–fidelity tradeoff of simulators. Left: metric summary matrix. Each cell reports the mean and 95% confidence interval over rollout batches; color indicates metric-wise degradation after accounting for whether higher or lower is better. Right: rollout-level Pareto plot of token cost and state fidelity. Faint points denote individual rollout-batch observations; large markers denote simulator means with 95% confidence intervals, and marker size is proportional to rollout throughput. Our event-driven simulator lies near the practical Pareto frontier: it preserves fidelity close to step-wise LLM simulation while using far fewer tokens and achieving much higher throughput. Figure 11 shows that the step-wise LLM simulator achieves the highest state fidelity (97.1%97.1\%), but at a prohibitive cost: it requires 17.817.8 LLM calls and 22.422.4K tokens per episode, resulting in the highest latency and the lowest rollout throughput. At the other extreme, the deterministic-only simulator is extremely cheap and fast, but its fidelity drops to 71.5%71.5\%, indicating that removing backend writes entirely makes the environment too unrealistic for stateful web interaction. The unconstrained marker simulator improves efficiency by reducing the number of LLM calls to 2.32.3 and the token cost to 3.63.6K, but its lack of validation leads to a sharp increase in state violations (10.7%10.7\%) and substantially lower fidelity (88.2%88.2\%). Our event-driven simulator achieves a better balance. Compared with step-wise LLM simulation, it reduces token usage by 82.6%82.6\% (from 22.422.4K to 3.93.9K) while preserving nearly the same fidelity (96.3%96.3\% vs. 97.1%97.1\%), and improves rollout throughput by about 8.7×8.7× (from 210210 to 18201820 episodes per hour). Compared with the unconstrained marker simulator, our method retains a similar call budget but improves fidelity by 8.18.1 points and reduces state violations by more than 3.8×3.8×. These results suggest that sparse marker triggering alone is not sufficient. The key benefit comes from combining event-driven invocation with state-safe validation: the former removes unnecessary per-step generation cost, while the latter prevents low-cost simulation from drifting away from faithful backend dynamics. This is precisely the regime needed for scalable PPO training in synthetic web environments. C.3 Which defects most harm policy learning? The previous results show that verification improves environment executability and downstream PPO success. We next ask a more diagnostic question: which types of scaffold defects are most harmful for policy learning? This analysis is important because defect frequency alone may be misleading. A common semantic defect may be visually noticeable but harmless for learning, whereas a rare feasibility defect can corrupt the reward signal by making a task impossible under any policy. Setup. Starting from verified environments, we construct controlled defect-mixture variants by reintroducing localized defects into pages, database bindings, markers, and task workflows. For each variant, we train the same compact PPO policy under identical hyperparameters and measure the drop in held-out success rate relative to the fully verified environment: ΔSR(d)=SRverified−SRd, (d)=SR_verified-SR_d, where d denotes a defect subtype. For each subtype, we also measure its occurrence frequency, task-blocking rate, affected task fraction, and marker-write rejection rate. This produces a defect-level impact profile that connects environment errors to downstream learning degradation. Figure 12: Defect impact on policy learning. Each point denotes one defect subtype measured across domains and random seeds. The x-axis reports how often the defect occurs in raw scaffolds, while the y-axis reports the PPO success-rate drop after injecting that defect into otherwise verified environments. Marker size indicates task-blocking rate and color denotes defect category. Feasibility and structural defects occupy the upper-impact region despite being less frequent than semantic defects. This shows that the most damaging defects are those that invalidate executable workflows or corrupt backend-grounded progress, rather than those that merely affect surface plausibility. Figure 12 reveals a clear mismatch between defect frequency and learning harm. Semantic defects are the most frequent in raw scaffolds, but many of them have modest impact on PPO because they do not necessarily prevent state progress. In contrast, feasibility defects such as missing submit actions, inaccessible forms, and unsatisfiable completion constraints produce the largest success-rate drops. Structural defects are also highly damaging when they disconnect required pages or remove navigation paths. Marker defects occupy a second high-risk regime: they may not block navigation, but they corrupt backend updates and therefore make dense progress rewards unreliable. These results provide a more fine-grained explanation for the ablation trends in Section 5.2. The feasibility verifier is critical not because feasibility defects are the most common, but because each such defect creates a large amount of misleading negative experience for PPO. Similarly, marker validation matters because even sparse state-write errors can poison the reward signal. Therefore, verification should not be optimized only for reducing the total number of defects; it should prioritize defects with high task-blocking and reward-corrupting effects. C.4 Is dense reward aligned with terminal success? Dense rewards accelerate PPO training, but they are only useful if intermediate progress is aligned with final task completion. A poorly designed reward may encourage local progress without completing the user instruction, leading to reward hacking. We therefore evaluate whether our state-grounded dense reward is statistically calibrated with terminal success. Setup. For each held-out task, we collect rollouts from partially trained PPO checkpoints and record the final progress potential Ψt(sH) _t(s_H), cumulative dense reward RdenseR_dense, and terminal success Ct(sH)C_t(s_H). We compare three reward signals: Surface-Heuristic, which rewards visible UI changes such as clicks and form edits; LLM-Judge, which asks an LLM to score partial task completion from rendered observations; and State-Grounded, our reward computed from verified backend predicates. For each reward, we measure calibration between predicted progress and terminal success, the area under the ROC curve (AUROC), Spearman correlation, expected calibration error (ECE), and the high-progress failure rate: HPF=Pr⁡(Ct(sH)=0∣Ψt(sH)>0.8).HPF= (C_t(s_H)=0 _t(s_H)>0.8 ). A well-aligned reward should have high AUROC and Spearman correlation, low ECE, and low high-progress failure rate. Figure 13: Alignment between dense reward and terminal success. Left: calibration curves between final progress score and empirical terminal success. A well-aligned dense reward should lie close to the diagonal. Middle: success rate by progress decile. Our state-grounded progress produces a monotonic success-lift pattern, whereas surface and LLM-based rewards assign high progress to many unsuccessful rollouts. Right: reward-alignment summary across domains, including AUROC, Spearman correlation, expected calibration error, and high-progress failure rate. State-grounded dense reward is both more predictive and better calibrated with terminal success, indicating that PPO receives intermediate supervision consistent with the true task objective. Figure 13 shows that state-grounded dense reward is substantially better aligned with terminal success than surface-level or LLM-judged alternatives. The calibration curve of our reward stays close to the diagonal, suggesting that a progress score of 0.70.7, for example, corresponds to an approximately 70%70\% empirical chance of success. In contrast, Surface-Heuristic is over-optimistic: many trajectories receive high reward for clicking, typing, or navigating, even when backend constraints remain unsatisfied. LLM-Judge improves over surface heuristics but still overestimates progress in states where the rendered page looks plausible while hidden database fields are incorrect. The decile analysis further confirms this trend. For our state-grounded reward, terminal success increases almost monotonically with progress deciles, and the top decile has a much higher success rate than the bottom decile. The high-progress failure rate is also much lower for our method, showing that the reward is less vulnerable to reward hacking. These results support the central design choice of compiling task constraints into backend-state predicates: dense supervision should reward verified state progress, not merely plausible-looking interaction behavior. C.5 What are the failure modes of learned policies? Success rate alone does not reveal whether a failed rollout is caused by the policy or by an invalid training environment. This distinction is crucial for synthetic web-agent training. If an episode fails because the scaffold is broken, the task is infeasible, or the backend update is inconsistent, PPO receives misleading negative feedback. In contrast, if failure is caused by wrong navigation, wrong DOM grounding, or insufficient exploration, the failure is attributable to the learned policy and can be improved through training. Attribution protocol. For each failed rollout, we assign one primary failure label using a deterministic diagnostic order. First, we check whether the task admits a bounded executable trace under the current scaffold; if not, the failure is labeled as Environment Invalidity. Second, if the rollout triggers a marker-write rejection or produces a backend invariant violation, it is labeled as State-Update Violation. Third, if the rollout reaches high dense progress but fails the terminal constraint, it is labeled as Reward Mismatch. Remaining failures are attributed to the policy: Grounding Error when the policy selects a wrong DOM element or fills a wrong field, Planning Error when it visits valid pages in an invalid order or misses a required subgoal, and Timeout / Exploration when the rollout does not make sufficient progress before the horizon limit. Formally, for a failed trajectory τ=(s0,a0,…,sH)τ=(s_0,a_0,…,s_H), we assign Attr(τ)=Environment Invalidity,∄π1:H′s.t.Ct(sH′)=1,State-Update Violation,∑kϵk>0orInv(sH)=0,Reward Mismatch,Ψt(sH)>τψandCt(sH)=0,Grounding Error,∃k:ak∈⁡(ok)but targets an incorrect DOM element,Planning Error,∃i:ϕt,i(sH)=0for an unmet required subgoal,Timeout / Exploration,otherwise.Attr(τ)= cases Environment Invalidity,& _1:H \ s.t.\ C_t(s_H )=1,\\ State-Update Violation,& _k _k>0\ or\ Inv(s_H)=0,\\ Reward Mismatch,& _t(s_H)> _ψ\ and\ C_t(s_H)=0,\\ Grounding Error,&∃ k:a_k (o_k)\ but targets an incorrect DOM element,\\ Planning Error,&∃ i: _t,i(s_H)=0\ for an unmet required subgoal,\\ Timeout / Exploration,&otherwise. cases We use τψ=0.8 _ψ=0.8 in all experiments. Figure 14: Policy failure attribution. Left: outcome decomposition over all evaluated episodes. Raw synthetic environments contain many environment-induced failures, making PPO feedback noisy. Verification sharply reduces environment invalidity and state-update violations. Middle: failure attribution conditioned on failed episodes. After verification, most remaining failures become policy-attributable planning and grounding errors. Right: domain-level residual failures for our full method. Harder stateful domains such as banking and healthcare retain more planning and grounding failures, suggesting where future policy improvements are needed. Results. Figure 14 shows that raw synthetic environments produce a large fraction of non-policy failures. In particular, Environment Invalidity and State-Update Violation dominate the failure distribution when PPO is trained on raw scaffolds. This indicates that the policy is often penalized for tasks that are not executable or for backend transitions that are not faithfully simulated. Adding dense rewards to raw environments does not fully solve this problem; it can even introduce additional Reward Mismatch failures, because progress predicates are unreliable when the underlying scaffold is inconsistent. After verification and marker validation, the failure profile changes substantially. Environment-induced failures become rare, and most remaining failures are attributable to the policy itself. The full method therefore produces a cleaner training signal: failed episodes mostly correspond to wrong navigation, wrong element grounding, or insufficient long-horizon planning. This shift is important because these are learnable policy errors, whereas broken scaffolds and invalid backend updates are not. The domain-level analysis further shows that banking, healthcare, and government tasks retain more residual failures, mainly because they contain longer workflows and more state-dependent constraints. These results suggest that verified environments do not merely improve average success rate; they also make failure feedback more interpretable and more useful for policy optimization. C.6 Is executability improvement confirmed by an independent audit? The feasible-task metric in the main paper is computed by bounded trace analysis. Because this analysis is also used during repair, a natural concern is that the reported executability improvement may be partly induced by the verifier itself. We therefore perform an independent audit using two sources of validation that are not used by the repair loop. Setup. We sample 120 held-out environments and 720 tasks after applying each environment-construction method. We evaluate executability using: (i) the internal feasibility verifier used in the main experiments, (i) a held-out bounded trace analyzer with a separately implemented action enumerator and a different search ordering, and (i) author-audited replay on a randomly sampled subset of 240 tasks. The author audit is used only as a sanity check and is not used for model selection, repair, or hyperparameter tuning. We also report the false-feasible rate, defined as the percentage of tasks marked feasible by the internal verifier but judged infeasible by both the held-out analyzer and the author audit. Method Internal Feasible↑ Held-out Feasible↑ Author-Audited Exec.↑ False Feasible↓ Trace Agreement↑ No Verification 48.6±1.448.6±1.4 46.1±1.646.1±1.6 44.8±2.444.8±2.4 12.4±1.512.4±1.5 83.2±2.183.2±2.1 Rule-Based 53.2±1.553.2±1.5 51.4±1.751.4±1.7 49.6±2.649.6±2.6 10.7±1.410.7±1.4 84.9±1.984.9±1.9 Single-LLM 70.4±1.370.4±1.3 67.8±1.567.8±1.5 65.9±2.265.9±2.2 6.8±1.16.8±1.1 89.4±1.689.4±1.6 Self-Consistency 79.6±1.179.6±1.1 77.2±1.377.2±1.3 75.4±2.075.4±2.0 5.2±0.95.2±0.9 91.1±1.491.1±1.4 AutoGen 88.7±0.988.7±0.9 86.9±1.086.9±1.0 84.8±1.984.8±1.9 3.9±0.73.9±0.7 93.8±1.193.8±1.1 Ours 94.8±0.794.8 0.7 92.9±0.992.9 0.9 91.7±1.891.7 1.8 2.3±0.62.3 0.6 96.4±0.896.4 0.8 Table 6: Independent executability audit. The feasible-task improvement is confirmed by a held-out trace analyzer and author-audited replay. The low false-feasible rate indicates that our main feasible-task metric is not merely an artifact of the repair-time verifier. Analysis. The held-out analyzer and author audit preserve the same method ranking as the internal metric. Our method achieves 92.9%92.9\% held-out feasible tasks and 91.7%91.7\% author-audited executability, only slightly below the internal 94.8%94.8\% estimate. The false-feasible rate also drops from 12.4%12.4\% for raw environments to 2.3%2.3\% for our method. This suggests that the repair loop does not merely optimize for the internal feasibility checker; it produces workflows that remain executable under an independently implemented analyzer and manual replay. C.7 How reliable are the verifiers and repair operators? The verification stage is useful only if detected defects correspond to real environment errors and repairs do not introduce new inconsistencies. We therefore evaluate verifier reliability and repair reliability on an audited defect set. Setup. We sample 80 raw environments and construct an audited defect set by manually checking page graphs, database bindings, markers, and task workflows. The audit contains 1,286 labeled defects across symbolic, structural, semantic, consistency, feasibility, and marker categories. We evaluate each verification method by precision, recall, and F1 against this audited set. For accepted defects, we additionally measure repair success rate, defined as the fraction of repairs that remove the target defect without creating another critical defect, and false repair rate, defined as the fraction of repairs applied to audit-negative defect reports. Verifier Precision↑ Recall↑ F1↑ Repair Success↑ False Repair↓ Rule-Based 96.1±1.296.1±1.2 39.4±2.139.4±2.1 56.0±2.056.0±2.0 71.8±2.871.8±2.8 1.2±0.41.2±0.4 Single-LLM 78.4±2.078.4±2.0 66.7±2.466.7±2.4 72.1±2.272.1±2.2 74.3±2.674.3±2.6 8.9±1.18.9±1.1 Self-Consistency 83.1±1.883.1±1.8 73.6±2.273.6±2.2 78.1±2.078.1±2.0 80.2±2.480.2±2.4 6.1±0.96.1±0.9 AutoGen 86.7±1.686.7±1.6 79.5±2.079.5±2.0 82.9±1.882.9±1.8 84.6±2.184.6±2.1 4.8±0.84.8±0.8 Ours 91.5±1.491.5 1.4 87.2±1.787.2 1.7 89.3±1.589.3 1.5 90.8±1.890.8 1.8 2.7±0.62.7 0.6 Table 7: Verifier and repair reliability on an audited defect set. Rule-based checking is high precision but low recall. Single-pass LLM verification detects more defects but also produces more false repairs. Our coordinated verifier improves recall while keeping precision high and false repairs low. Category Precision↑ Recall↑ F1↑ Repair Success↑ Symbolic 97.497.4 93.193.1 95.295.2 96.596.5 Structural 91.291.2 86.786.7 88.988.9 90.590.5 Semantic 88.688.6 84.284.2 86.386.3 87.187.1 Consistency 90.490.4 85.585.5 87.987.9 88.388.3 Feasibility 87.887.8 91.691.6 89.789.7 92.192.1 Marker 92.392.3 88.988.9 90.690.6 93.493.4 Table 8: Category-level reliability of our verifier. Feasibility defects have slightly lower precision but higher recall, which is desirable because missed feasibility defects are especially harmful for policy learning. Analysis. The results explain why simple rule-based checking is insufficient: it rarely hallucinates defects, but it misses many semantic, consistency, and feasibility failures. Single-LLM verification improves recall but has a higher false repair rate, which can introduce unnecessary edits to otherwise valid scaffold components. Our method obtains the best F1 and repair success rate because defect-triggered coordination asks only the relevant verifier to re-check downstream effects, while priority-weighted repair scheduling avoids repairing low-confidence isolated reports before high-impact dependencies are resolved. The category-level results also support the design emphasis on feasibility and marker validation: these categories are detected with high recall and repaired with high success, reducing the chance that PPO receives misleading feedback from impossible tasks or invalid backend updates. C.8 Are the gains due to a larger LLM verification budget? Our verification pipeline uses LLM-based semantic verifiers, so a natural question is whether its advantage comes from better coordination or simply from a larger LLM budget. We therefore compare verification methods under measured LLM-call and token budgets. We also include an Ours-Token-Matched variant that uses the same average token budget as the Single-LLM verifier by running only one targeted coordination round and disabling optional low-severity re-checks. Method LLM Calls / Env.↓ Tokens / Env.↓ Time / Env.↓ Def.↓ Feasible↑ False Feasible↓ Rule-Based 0.00.0 0.00.0K 0.50.5m 9.89.8 53.253.2 10.710.7 Single-LLM 8.18.1 41.841.8K 12.012.0m 6.26.2 70.470.4 6.86.8 Self-Consistency 40.040.0 207.4207.4K 35.035.0m 5.85.8 79.679.6 5.25.2 AutoGen 29.429.4 154.2154.2K 28.028.0m 5.15.1 88.788.7 3.93.9 Ours-Token-Matched 8.38.3 42.542.5K 11.511.5m 4.74.7 87.487.4 3.43.4 Ours 22.622.6 116.4116.4K 18.018.0m 3.33.3 94.894.8 2.32.3 Table 9: LLM-budget comparison for environment verification. Our full method uses fewer tokens and less curation time than self-consistency and AutoGen while achieving higher executability. Even when matched to the Single-LLM token budget, our targeted coordination substantially improves feasible-task rate, suggesting that the gain is not merely due to spending more LLM calls. Analysis. Self-consistency spends the largest token budget because it repeatedly queries independent verifiers, but it does not explicitly route downstream checks to the defect categories most likely to be affected. AutoGen improves over self-consistency but remains more expensive than our full method. In contrast, our method uses targeted coordination and dependency-aware repair scheduling, which reduces redundant re-checks. The Ours-Token-Matched variant is particularly informative: with nearly the same token budget as Single-LLM, it improves feasible-task rate from 70.4%70.4\% to 87.4%87.4\%. This indicates that the main benefit comes from structured verifier coordination and repair scheduling, rather than from a larger LLM budget. C.9 Qualitative raw-to-verified case study We provide a representative example to illustrate how scaffold verification changes the learning signal. The raw environment is an e-commerce website with the task: “Buy a wireless mouse under $30 and place the order.” The raw pages look plausible, but the workflow is not executable because multiple scaffold components disagree. Defect Evidence in Raw Scaffold Repair Effect on Task Broken navigation Product page links to /cart, but the declared navigation graph has no reachable cart page. Add the missing cart route and reconnect it to the product and checkout pages. The bounded trace can reach the purchase workflow. Inconsistent price Product list shows the mouse as $24.99, while the detail page binds the same entity to $34.99. Propagate the canonical database value $24.99 to all rendered views. The price constraint in the task becomes evaluable and consistent. Missing backend transition The “Add to cart” button changes the visible page but does not update cart.items. Attach an add-to-cart marker with typed arguments and write set cart.items. Dense reward can credit verified cart insertion. Unsatisfiable completion constraint The completion predicate checks order.status=placed, but no checkout button writes this field. Add a place-order marker and validate the state delta against order schema invariants. Terminal success corresponds to an executable state transition. Table 10: Representative raw-to-verified repair example. The raw scaffold contains multiple locally plausible but globally task-blocking defects. Verification and repair convert the same task into an executable workflow with backend-grounded progress predicates. After repair, the shortest verified trace is: Home→SearchResults→ProductDetail→Cart→Checkout→Confirmation. Home→ SearchResults→ ProductDetail→ Cart→ Checkout→ Confirmation. The corresponding progress predicates check whether the target product has been visited, whether its canonical price satisfies the task constraint, whether the correct entity has been inserted into cart.items, whether the checkout form is valid, and whether the order state is updated to placed. In the raw environment, PPO failures on this task are not attributable to the policy because no policy can satisfy the completion constraint. In the verified environment, failed rollouts are attributable to policy errors such as selecting the wrong product, omitting checkout, or timing out before submitting the order. Appendix D Limitations The event-driven simulator reduces cost by invoking constrained state writing only at marker-triggered operations. This is effective when persistent state updates are sparse, as observed in our diagnostic study, but may be less efficient for applications where nearly every interaction changes backend state. Appendix E Broader Impacts and Safeguards This work may have positive impacts by making web-agent training more reproducible, auditable, and less dependent on brittle live websites or expensive manual environment construction. Verified synthetic environments can help researchers distinguish policy failures from environment invalidity and can reduce unnecessary LLM calls during evaluation. The same capability also has possible risks. More capable web agents could be misused for spam, unauthorized automation, credential abuse, synthetic phishing workflows, or other harmful web-scale actions if trained or deployed without safeguards. We can mitigate these risks in several ways. The proposed environments are sandboxed and use synthetic data rather than real user records. Persistent state changes are constrained by marker schemas, database invariants, and programmatic task constraints. Appendix F Declaration of LLM Usage LLMs are used to generate raw synthetic web scaffolds from domain-level site specifications, to support semantic verification of generated content and workflows, and to propose constrained state deltas for marker-triggered backend updates during synthetic training rollouts. In addition, LLMs are mainly used to help check for grammatical errors in writing.

Instant research discovery