Recursive World-Model Self-Repair in PDDL Domains: Verifier Coverage Is the Binding Constraint, and Under-Verified Loops Stall Rather Than Diverge
Abstract
We implement recursive self-improvement of a symbolic world model, an abstraction of the embodied verification problem: the agent holds a corrupted PDDL domain (4 seeded errors), plans, executes against ground-truth semantics, diagnoses the failure, edits its own model, and plans again. A repair can only be judged against the verifier the agent has, and real verifiers are neither absent nor complete, so we make verifier coverage an engineerable knob. We pre-registered a factorial evaluation: repairs are scored by a verifier seeing a stratified fraction c of the domain’s conditions, crossing c ∈ {0.2, 0.4, 0.6, 0.8, 1.0} with repair rounds k ∈ {0, 1, 2, 4} over 20 seeds and 3 IPC domains (60 seed-paired runs per cell, held-out instances). Two design rules follow. Coverage is the binding constraint: the pre-registered interaction holds: +0.530 (95% bootstrap CI [+0.447, +0.615]); success at k = 4 rises from 0.1733 at c = 0.2 to 0.900 at c = 1.0; it replicates in blocks (+0.56), gripper (+0.60) and logistics (+0.43); and the k = 0 negative control — the coverage main effect before any repair, not a success rate — is exactly 0.0000, raw success being identically 0.0133 at every coverage level. The failure mode is stagnation, not self-poisoning, so an under-verified loop should be instrumented for stalling rather than for runaway corruption: the mechanism we pre-registered is refuted by our own declared falsifier, which fired. Divergence events were 2 of 360 transitions at c ≤ 0.4 against 3 of 360 at c ≥ 0.8 (gap +0.0028 [−0.0056, +0.0111], covering zero and pointing the wrong way), while edit distance to truth falls in both bands (4.00 to 1.1833 at high coverage, 4.00 to 3.0167 at low). Strict-domination acceptance prevents macroscopic divergence by construction, so the loop stalls; in the unverified conditions local corruption is 7x more common at low coverage but never accumulates. At c ≤ 0.4, 0.6062 of repair rounds propose an edit and accept none, against 0.1437 at c ≥ 0.8. The design was fixed before any data existed, including an apparatus amendment made before the first run. The proposer is deterministic and search-based, not a language model: a local LLM proposer failed the pre-declared throughput pilot and appears only as an underpowered 8-seed arm.