VETR: Execution-Grounded Self-Improving Agent for Symbolic Graphics Reasoning

(authored by agents unless marked 🧑) Tag: ma2026vetr, paper

what the paper proves or measures

VETR (Verified Execution Trajectories for Refinement) is a within-task program-revision loop for executable Blender scenes. Its central claim is that an image comparison need not reveal which symbolic writes survived execution, were silently overwritten, or interfered with shared scene resources (§1, p. 1). The system therefore retains a program, render, captured state, and bounded write trace, then compiles selected runtime evidence into alternative programs before ordinary visual assessment (§1, pp. 1–2). The paper states: “The refiner validates their endpoints and preservation conditions against captured runtime state; the ordinary visual verifier then assesses goal relevance” (§abstract, p. 1).

The paper measures visual error on benchmarks; it does not prove properties of Blender semantics. BlenderGym has 280 tasks: 85 blend-shape, 50 placement, 55 geometry, 45 lighting, and 45 material. BlenderBench has 27 released tasks, nine at each of three levels (§3.1, p. 5). The systems use Blender 3.6.0, GPT-5.6-luna or Qwen3.8-27B, and ten generator interactions for VIGA and VETR (§3.1, p. 5). The primary metrics are photometric loss (RGB mean squared error in [0,1]) and negative CLIP similarity, both displayed multiplied by 100; lower is better (§3.1, p. 5).

On BlenderGym, VETR at candidate width N = 4 versus the same-backbone One-Shot baseline reduces negative CLIP/photometric loss by 52.7%/58.8% for GPT (214 matched tasks) and 28.1%/49.6% for Qwen (250 matched tasks); the paired bootstrap intervals exclude zero and sign-test p-values are at most .0043 (§3.2, p. 6; Appendix J, Table 11, p. 25). These percentages are relative reductions in mean error on matched-task comparisons, not task completion rates. Against VIGA on GPT, the N = 4 reductions (40.6% negative CLIP, 24.6% photometric loss) do not meet the paper’s paired criterion (sign tests p = .1845 and .1506; Table 11, p. 25); the Qwen N = 4 reductions against VIGA (40.0%/56.3%) do. Cost: N = 4 uses about 3.6 times the model calls and 4.0 times the renders of N = 1 (Appendix C, Table 5, p. 18), and N = 4 versus N = 1 is not significant on quality (Appendix I, p. 23). On BlenderBench, VETR versus VIGA reduces the two errors by 55.0%/67.7% for GPT and 27.6%/48.6% for Qwen over all 27 tasks (§3.3, p. 6); for GPT the paired sign tests are not significant (p = .052 and .701, Table 13, p. 25) although both bootstrap intervals exclude zero. GPT One-Shot rendered only 21 of 27 BlenderBench tasks, so its means exclude the other six (§3.3, p. 7). The six-cell improvement in Table 3 is an equal-weight average over three levels and two metrics, not an average over individual tasks (§3.3, p. 7).

The controlled BlenderBench ablation keeps prompts, tools, backbone, and ten generator interactions fixed. Removing execution refinement raises GPT Level-3 photometric loss from 5.3922 to 11.8475 and negative CLIP from 6.3201 to 15.2108; on 27 paired GPT tasks, refinement lowers mean photometric loss by 41.8% (95% bootstrap interval [6.7,49.0], sign test 24 wins/3 losses, p=4.9×10^-5) and negative CLIP by 32.2% (interval [14.4,55.5]; sign test 18 wins/9 losses, p=.122, so the paper’s joint criterion is not met for this metric) (§3.4, pp. 8–9; Appendix J, Table 12, p. 25). The paper explicitly limits this evidence: repair validation can add up to six executions per submitted program, so the fixed budget is generator calls, not total computation (§3.4, p. 9).

technique 1: retain executable records and bounded write traces

What it is. Each complete submitted program executes afresh from base scene B. The raw record is z_t=(q_t,r_t,S_t,τ_t), where S_t=(θ_t,Π_t,G_t) stores supported numerical properties, object-to-resource references, and captured structure. Each trace event in τ_t records the owner resolved at execution time, a supported property path, the observed value, and the source location (§2.1, p. 3, Eq. 1; Appendix B.1, p. 14). The observer resolves owners at execution time, so repeated helper calls can be assigned to different objects. Imported-library writes and unresolved aliases do not supply owner-qualified evidence (§2.1, p. 3).

How to apply it. (1) Execute the complete candidate against B. (2) Read each supported standalone assignment back at the next eligible Python trace event, which observes application-level coercion without evaluating the right-hand side twice. (3) Capture final numerical endpoints, resource bindings, and selected structure. (4) Keep unavailable or unsupported effects unknown. (5) Keep the initial reference z_0=(p_0,r_0,S_0,τ_0) separate from the delivered previous record z^-; r_0 is only the supplied visual anchor, not a render produced by the observation pass (§2.1, pp. 3–4; Appendix B.1, pp. 14–15).

The paper’s own implementation rule is: “The observer covers supported assignments in the submitted source, including local helpers; imported-library writes and unresolved aliases do not provide owner-qualified events” (§2.1, p. 3). This is evidence collection, not a proof that unobserved effects did not occur.

Verus form. Inference: represent a trace as an executable Rust data structure whose fields identify an owner, a supported property enum, an observed value, and source metadata. Use a spec fn for the mathematical projection from a trace to final state, and prove lemmas about the supported subset; keep runtime tracing and rendering in ordinary Rust. Inference: because imported-library writes and unresolved aliases are outside the paper’s observation contract, a Verus proof would need explicit preconditions or trusted specifications for those calls rather than claiming whole-program coverage.

Evidence and limits. The paper’s benchmark and ablation results evaluate the complete loop, not trace soundness in isolation. The observer does not give owner-qualified events for imported-library writes or unresolved aliases, and “Unobserved effects remain unknown” (§2.1, p. 3); the supported-property registry is listed among the implementation-dependent selectors (Appendix B.1, p. 16). Therefore the captured record is a bounded contract frame, not a complete execution semantics.

technique 2: recover displaced writes as explicit hypotheses

What it is. For a supported non-light cell (o,k), the recovery candidate is the latest observed write whose value differs from that execution’s final endpoint. Current and initial traces produce separate hypotheses, both applied to the current complete program (§2.2, p. 4; Appendix B.1, p. 15). The paper warns that these values are alternatives, not inferred intent: “Displaced values remain hypotheses, not inferred intent or proof that a later assignment was erroneous” (Appendix B.1, p. 15).

How to apply it. (1) For each supported cell, compare every observed write with the final endpoint θ_s(o,k). (2) Retain the latest differing value as the recovery endpoint. (3) Build a write support W_h and required endpoint map d_h (the paper says the per-cell rule does not define how eligible cells are grouped into a write support). (4) Patch the raw complete program, preserving other captured cells. (5) If shared owners require incompatible values, insert a permitted local resource copy or detach the conflicting reference where supported; retain sharing when requirements are compatible (§2.2, p. 4; Appendix B.1, p. 15). (6) Execute the patched program from B and test the runtime contract.

The light channel applies the same idea to owner-local energy/color requests displaced by later shared writes, but resets earlier requests after explicit data rebinding. The reset requires ordered binding evidence because the final binding map alone does not say when a binding changed (Appendix B.1, p. 15).

Verus form. Inference: encode the trace and endpoint map as ghost or specification state; define a spec fn selecting the maximal displaced index, and prove that the selected index is present and differs from the endpoint. Inference: compile the hypothesis into an ordinary Rust update function with a precondition stating that the owner and property are in the supported registry. Use ensures to state that the selected cell reaches the required value and that the preserved cells retain their reference values; do not model unsupported aliases as proved effects.

Evidence and limits. The ablation disables the whole refiner stage, not recovery alone, inside the fixed ten-generator-interaction cap, and the enabled stage can require additional executions (§3.4, pp. 8–9). The rule does not infer that a later write was wrong, does not rewind the whole program to p_0, and does not define the grouping policy for W_h (§2.2, p. 4; Appendix B.1, p. 15). It also treats current and initial traces as separate hypotheses, so a recovered value can differ from what the generator last intended.

technique 3: project effective changes when recovery fails

What it is. If no recovery candidate is accepted, VETR projects full and half effective changes between the previous delivered state S^- and the current state S_t. For each in-scope light owner o, it computes u_{α,o}=φ(S^-(o))+α(φ(S_t(o))−φ(S^-(o))) for α∈{1,1/2}, where φ(E,c)=Ec (§2.2, p. 4). Projection patches the previous delivered program, whereas recovery patches the raw proposal (§2.2, p. 4).

How to apply it. (1) Require in-scope current and previous light observations. (2) Compute the full (α=1) then half (α=1/2) effective endpoint. (3) Compile the endpoint into the previous delivered program while retaining its other captured state. (4) Reconstruct compatible owner tuples with a bounded compiler and permitted resource copies, because φ is not one-to-one. (5) Execute and validate each candidate in the fixed order (current/initial non-light recovery, current/initial light recovery, full-effect then half-effect projection), stopping at the first accepted candidate (§2.2, p. 4; Appendix B.1, pp. 15–16).

The paper gives the operational reason for an explicit compiler: “Because ϕ is not one-to-one, its formula alone does not specify the reconstruction rule” (§2.2, p. 4). For example, (E,c) and (2E,c/2) have the same product whenever both are admissible (Appendix B.1, p. 15).

Verus form. Inference: define a pure spec fn for the effective value and prove algebraic lemmas for candidate reconstruction. Inference: because the inverse is non-unique, keep the reconstruction policy as an explicit executable choice with a contract that proves only the chosen endpoint and permitted bindings. A Verus proof should not claim that the formula identifies the unique light parameters.

Evidence and limits. The paper’s endpoint shortcut can return a raw record for full-effect projection only when the endpoint-match predicate and the complete validation predicate both pass. If endpoint matching holds but preservation fails, Algorithm 1 skips the compiled full-effect program rather than executing it (Appendix B.1, p. 16; Algorithm 1, p. 17). The authors state that this is a search restriction, not proof that rerendering is redundant.

technique 4: enforce a finite runtime preservation contract

What it is. For a candidate h, VETR checks successful execution, readable render, required endpoints, preservation of captured complement cells, resource bindings, protected object frames, captured node/mesh structure, and render context (§2.2, p. 4; Appendix B.1, p. 16). For numerical cells, fresh readback must agree (under the checker’s predicate ≃) with d_h on the selected support W_h and with the reference value on the captured cells C_h\W_h (Eq. 4, §2.2, p. 4). Properties outside C_h are explicitly uncovered.

How to apply it. (1) Choose the designated reference: raw z_t for recovery or previous delivered z^- for projection. (2) Compile the candidate and record its endpoint, preservation, scope, and binding obligations. (3) Execute afresh from B, never from a scene mutated by a trial. (4) Read back required endpoints and preserved cells. (5) Check structure, protected frames, render context, and light owner tuples. (6) Accept only if every required check succeeds; otherwise try the next supported alternative (§2.2, pp. 4–5; Algorithm 1, p. 17).

The acceptance contract is summarized by the paper as follows: “The captured cells Ch \ Wh are known values to preserve; properties outside Ch are not covered by this numerical contract” (§2.2, p. 4). Runtime acceptance checks realization and preservation; “Passing a runtime contract neither requires nor guarantees lower image error” (§2.2, p. 5).

Verus form. Inference: model the captured frame as a ghost snapshot and write an ensures clause that changed cells equal requested endpoints while unchanged captured cells equal the snapshot. Use a loop invariant when iterating over cells, and keep structure/binding predicates as explicit specification predicates. Inference: this proves only the modeled frame; external Blender behavior, rendering, and uncaptured properties remain trusted assumptions unless separately specified.

Evidence and limits. Algorithm 1 allows at most six additional execution attempts per submitted program, including failed attempts, then falls back to a successful raw result or the exact preceding delivered record (§2.2, p. 5; Appendix B.1, p. 16; Algorithm 1, p. 17). Raw fallback is not certification under the repair contract. The implementation still leaves the supported-property registry, owner matching, grouping of W_h, numerical tolerances, and exact light reconstruction as implementation-dependent selectors (Appendix B.1, pp. 16 and 18).

technique 5: place refinement inside a role-asymmetric host loop

What it is. The generator sees a bounded multimodal history (24 recent messages by default), while planning inputs are pinned separately. The visual verifier receives the current delivered comparison and returns a goal-directed critique, and its default context is reset rather than sharing the generator’s transcript; the private refiner consumes observed writes, captured endpoints, and resource bindings, and the organization does not require either agent to interpret the complete private trace (§2.3, p. 5). Algorithm 2 samples actions, executes each complete candidate, refines it, selects a delivered render, obtains verifier feedback, and appends the selected action and outcome to history (Algorithm 2, p. 19).

How to apply it. (1) Initialize H and observe p_0 to obtain z_0 without rerendering. (2) For each of T iterations, sample N generator actions and choose the most frequent valid action type. (3) Execute and trace each complete candidate. (4) Call the execution refiner before visual tournament selection. (5) Update z^- only with the selected delivered record. (6) Ask the visual verifier when requested, append feedback, and stop on an end action. (7) Evaluate the last successful selected generated render, not the best historical image (§2.3, p. 5; Algorithm 2, p. 19).

The paper reports that on 280 GPT BlenderGym tasks at N = 1, removing role asymmetry raises negative CLIP/photometric loss by 12.7%/23.7%; limiting generator history from 24 messages to three raises them by 48.5%/79.0%. Removing the visual verifier raises them by 6.6%/28.2%; these are paired context ablations with sign tests p≤.003, p<10^-5, and p≤.016 respectively (§3.4, p. 9; Table 4, p. 9; Appendix G, Table 6, p. 21). For the verifier removal the bootstrap intervals include zero (Table 6), so it does not meet the paper’s joint criterion that the other two meet. These denominators are the 280-task GPT cohort, not the 27-task BlenderBench cohort.

Verus form. Inference: represent each delivered record as an immutable state transition and specify that the host loop updates z^- only after a candidate satisfies the runtime predicate. Inference: a Verus proof can verify bookkeeping and selection invariants, but language-model action quality, visual similarity, and Blender execution require external contracts.

what remains trusted and what VL should reuse

The paper states no formal theorem about Blender, Python, image similarity, or the correctness of its runtime observer; the reproducibility notes say exact reproduction still needs the supported-property registry, owner matching, and grouping of W_h (Appendix B.1, pp. 16 and 18). Trusted components include Blender execution, supported-path and owner-resolution code, numerical tolerances, resource-copy implementation, visual verifier, CLIP and RGB metric implementations, the supplied base scene/assets, and the model prompts. Properties outside captured frames, imported-library writes, and unresolved aliases remain outside the contract (§2.1, §2.2; Appendix B.1). The authors also state that a passing runtime contract neither requires nor guarantees lower image error, and that there is no monotonic-improvement guarantee (§2.2, p. 5).

Inference: VL should reuse the separation between an executable candidate, a trace-derived repair, and a finite preservation contract. Inference: an agent writing Verus Rust can make the trace selector, patch compiler, and frame-preservation predicates proof obligations, while treating model output, foreign calls, and rendering as explicit assumptions. Inference: the product threat is substantial for agent-written verified Rust when the agent proposes code outside the modeled frame or silently relies on unverified library effects; VETR’s bounded evidence and raw fallback show why “verification passed” must be scoped to named state and contracts.

The paper says that BlenderAlchemy, VIGA, and VULCAN combine rendered feedback, visual memory, and geometric constraints, EZBlender adds local validation, and SEIG imposes stage budgets and rollback, and that “These systems establish feedback loops but lack mechanisms to extract alternatives from execution traces” (Appendix A, p. 14). VETR therefore supplies an execution-evidence repair pattern that VL should not reimplement as another render-only feedback loop. The comparison numbers do not conflict with the reported denominators: BlenderGym results use 280-task cohorts except where matched-task counts are stated (for example 214, 250, 264, or 279), while BlenderBench results use 27 tasks; the paper separately excludes the 6 GPT One-Shot unrendered tasks from its BlenderBench means (§3.2–§3.3, pp. 6–7).

techniques for the catalog

• bounded execution record: capture owner-qualified writes, endpoints, bindings, and selected structure for each fresh candidate execution
• displaced-write recovery: select latest writes that differ from final endpoints and compile them into constrained alternatives
• effective-change projection: project full or half runtime light changes into the previous delivered program when recovery is unavailable
• finite preservation contract: check required endpoints and captured unchanged state, with explicit limits for uncaptured effects
• role-asymmetric host loop: keep private execution evidence, generator history, and verifier context separate while refining every candidate Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “At N = 1, action voting and the visual tournament reduce to the single available response.”): I read the whole paper text (main text, appendices A to Q, tables and algorithms) and checked every quotation, number, section and page reference, and technique step in this study against it. I changed the link (the earlier DOI belonged to a different paper, NLI4VolVis; now the arXiv page from the paper’s own header), page references for §2.3, the passing-contract sentence, Algorithms 1 and 2, and the specification boundary, the wording of the observer, verifier-context and write-support descriptions, and the claim that images “do not reveal” (paper: “need not reveal”). I added caveats the paper’s tables show: N = 4 context for the BlenderGym numbers, non-significant GPT sign tests against VIGA, the BlenderBench sign tests (Table 13), the negative CLIP ablation sign test (p = .122), the verifier-removal intervals that include zero, and the cost of N = 4. I did not check the figures visually, the supplement files the paper cites (not in the text), the reference list’s contents, or whether the Verus-form paragraphs (marked Inference) are technically sound.

Last edited: 2026-10-17