Checked Program Recovery from Execution Video: A Sound Oracle for Untrusted Generators

Checked Program Recovery from Execution Video: A Sound Oracle for Untrusted Generators Yuan Si and Jialu Zhang∗

arXiv:2607.00635v1 [cs.SE] 1 Jul 2026

University of Waterloo, Waterloo, Canada [email protected], [email protected]

Abstract—A growing class of tools recovers a program from observations of its behavior using an untrusted generator, a neural model or a search, that proposes candidates with no correctness guarantee. We study how to make such recovery trustworthy, in the concrete setting of recovering a runnable Scratch program from a recording of its execution. The recording shows what the program does but never its code; many programs produce the same video, so the source cannot be recovered, and the right target is a program that behaves the same as far as the camera can tell, made precise with a lens. The core is a two-tier validation oracle with a deliberate verdict asymmetry. A static checker proves lens-equivalence to a reference and issues a certificate that, granting the partial-order independence quotient adequate, never accepts a wrong program; a renderer can only refute or witness finite agreement, never certify. Around it, V ID 2P ROG reads each sprite’s motion, visibility, and timing from the video and a known-asset manifest and synthesizes a candidate sourcefree; a closed loop renders and runs recovery again for ground truth. Under the exact lens the oracle makes no false accept on 246 labeled differing pairs, including an adversarial battery built to trap its concurrency quotient; on inputs outside the vocabulary and on real projects it abstains or refutes, accepting none we test. In-vocabulary recoveries reproduce their source frame for frame and 80% earn a static certificate, while whole real projects, mostly outside the vocabulary, recover at 14%, a vocabulary-bound rate the system never inflates with a wrong answer. A frontier vision-language model recovers none of the matched programs single-shot, which oracle-in-the-loop repair lifts only to a few while the structured pipeline recovers all, the gap a sound checker makes for an untrusted generator.

I. I NTRODUCTION A twenty-second screen recording of a Scratch game carries enough information for a person to grasp what the program does, and a neural model or a structured search can be asked to turn that recording back into a runnable .sb3 file a learner could open and edit. The code never appears on screen; what the camera captures is the rendered output of an execution, sprites moving, costumes cycling, the stage redrawing thirty times a second. Reconstructing an executable program from this signal is the problem we study, and the difficulty that organizes the paper is not only producing a candidate but trusting it: a recovered program is the output of an untrusted generator that perceives and guesses, and matching a handful of frames is no proof it behaves like the original. Our answer is a sound checker that certifies a candidate or refuses it, and is never allowed to do the reverse. Corresponding author: Jialu Zhang.

Scratch is among the largest novice programming communities, with over a hundred million publicly shared projects, and learners produce far more recordings of running projects than they keep as editable source. A recording whose source is lost cannot be analyzed, tested, tutored, or remixed; recovering an editable program reopens it to every tool that reads source. This problem sits apart from the inverse problems software engineering knows. Binary decompilation reads instructions that encode the computation directly; here the instructions are gone and only their visible consequences remain, so control flow, internal state, and object identity are inferred from how appearance changes over time. The central difficulty is that many distinct programs produce the same video. A variable the program never renders, a branch the execution never takes, two independent scripts in either order: none of these leaves a trace a camera can see. Asking to recover the original source is therefore ill-posed. The question that is well-posed is whether a recovered program reproduces what was seen and behaves like the original on everything the camera could observe. We make this precise by treating a video as one realized point of a lossy observation map parameterized by a lens, a description of which execution facts are visible. The camera fixes the lens. The strongest claim any method can earn is observational equivalence under that lens, and a recovered candidate is validated under that lens by a two-tier oracle whose static tier alone mints an equivalence certificate. Two commitments shape the system. Equivalence is certified, never assumed: a static checker re-derives a candidate’s behavior from its .sb3 bytes and mints a certificate only when it proves equivalence to a reference, available wherever a reference exists, while a video alone yields the weaker render witness; a renderer can expose a divergence but never mint a positive verdict, because matching finitely many frames cannot establish agreement on the infinitely many executions a camera never witnessed. And the part a camera cannot recover is stated as a theorem: we construct five families of programs pairwise indistinguishable under the camera lens, a constructive lower bound on the non-recoverable residual. V ID 2P ROG is the untrusted generator these commitments guard: it perceives sprite tracks from pixels, fits structural motifs that explain the tracks, synthesizes a candidate program, and routes it through the validation oracle. The pipeline recovers the motion, visibility, and frame-counter control of a program; the sprite cast, costumes, and backdrop are supplied as a known-

obs Lvideo asset manifest, which is the lens under which recovery is posed. perceive Program Video Tracks When passive observation is insufficient, because a behavior is P frames gated on an input that never occurred, the system queries the original program as a black box, synthesizes the missing input, synthesize elicits the hidden behavior, and recovers the input condition. denoise Oracle Candidate Motif fit ≈Lvideo ? P̂ The forward renderer that produces videos also serves as a labeled-data generator and as the refutation engine, which certificate / yields a closed loop: render a program, recover the program refutation from the video, check the result. The recovery rate is then the metric and the task definition at once, and the benchmark Fig. 1. From program to video and back. Perception and synthesis propose needs no human annotation. a candidate from the video and asset manifest alone. The validation oracle, The oracle never accepts a wrong program: no false accept which reads the source withheld from recovery, then certifies statically where a reference is available, witnesses by replay against the frames otherwise, or on 246 labeled differing pairs or on an adversarial battery built refutes. to trap its concurrency quotient, and outside the vocabulary and on real projects it abstains or refutes. Within the vocabulary the generator is strong, every recovery reproducing its source for cross-renderer validation. frame for frame and 80% earning a static certificate, both II. OVERVIEW stable across ten seeds; whole real projects, mostly outside the Figure 1 traces one video through the system. A Scratch vocabulary, recover at 14%, the vocabulary-bound rate paid in full. Recovery holds from thirty frames per second down program drives a sprite rightward and hides it after a fixed to five and through a second renderer’s compressed video, an number of frames. The renderer produces a sequence of frames, active loop recovers key-gated behavior, and a frontier vision- the only input the recovery sees. Perception reads each frame, segments the sprite from the language model recovers none of the matched programs from frames, a perception gap the pipeline’s least-squares fit closes, background, and reports its centroid and visibility. The result while the oracle catches its errors and the pipeline recovers is a noisy track: the measured position drifts by a few pixels all. The in-vocabulary corpus fixes the synthesis ceiling and per frame around the true trajectory. A least-squares fit over the whole track absorbs this noise and returns an exact permakes perception the variable under test. frame displacement, which is why recovery from imperfect This paper makes four contributions. pixels is feasible. Synthesis searches for a small program whose • A two-tier validation oracle that makes untrusted generaforward simulation reproduces the denoised track, and it accepts tive program recovery trustworthy: by a verdict asymmetry a motif only when the simulation matches the track exactly. only its static tier mints a lens-equivalence certificate, The candidate is a runnable .sb3 file. sound relative to the compiled IR semantics and the In the benchmark the validation oracle decides acceptance: it stated independence-quotient adequacy assumption, while compiles the candidate and the withheld source and compares a renderer only refutes or witnesses finite agreement, never them under the camera lens. Here a subtlety appears that the certifies, yielding zero false accepts over 246 labeled rest of the paper builds on. Suppose the original keeps a private different pairs (Section V). counter it never displays. A recovered program without that • A formalization of video-based recovery as inversion of a counter renders an identical video. The two are equivalent lens-parameterized observation map, with an identifiability under the camera lens, because no camera could separate them, lower bound characterizing what a camera cannot recover and the oracle accepts the smaller program. Acceptance means (Sections III and IV). equivalence on what the lens observes, and the facts the lens • V ID 2P ROG , a source-free neuro-symbolic pipeline that hides are exactly the residual our identifiability result quantifies. recovers a program’s motion, visibility, and frame-counter This example is why the target is a class, not a program: a control from rendered pixels under a known-asset lens, method insisting on the original source would have to recover through verification-based motif synthesis and a black- the counter, impossible from the video, while one targeting box active-inference loop for input-gated behavior (Sec- the class succeeds whenever it returns any member the oracle tion VI). accepts. The shift from a point to a class makes the problem • A closed-loop, label-free benchmark and an evaluation well-posed, and the camera forces it. of soundness, recovery, discrimination, robustness, and a vision-language baseline, reported with confidence III. P ROBLEM F ORMALIZATION intervals (Section VIII). We fix the space P of loadable Scratch programs. Execution

The static tier implements a published lens-equivalence algorithm [1]; the contribution is the soundness discipline around it, the two-tier oracle and its verdict asymmetry, the lens formalization and identifiability bound, the pipeline, the closedloop benchmark, and FastRender, a deterministic renderer used

is a relation rather than a function, because the outcome depends on exogenous choices: an input timeline ι that lists green-flag, key, mouse, and broadcast events, a random seed r that pins the generator and the clock, and a legal schedule s that orders concurrent scripts and clones at tick boundaries.

Treating execution as a relation places the schedule on the what was seen and at least the refinement clause (ii) asks offsame footing as the input and the seed, which is why script trace; being a symmetric multiset equality it in fact delivers order is a non-identifiability family, and it forces the acceptance full ≈L , more than (ii) demands, though never source identity. criterion to quantify over schedules. Once the three choices IV. W HAT A C AMERA C ANNOT R ECOVER are fixed the trace is determined, written run(P, ι, r, s), and The observation map is not injective, and the ways it all nondeterminism lives in the choice of the triple, not inside collapses distinct programs are the structural reason recovery the step relation. A lens L names which facts of a trace are observable. Lenses targets a class. We make the collapse constructive. carry an order: L ⊑ L′ means L′ observes at least as much as Theorem 1 (Non-identifiability, lower bound). The kernel L, and the two relate by a projection π with obs L = π ◦ obs L′ . ≈ Lvideo contains at least five effectively constructible, indiA video is one realized observation under the camera lens vidually non-empty families of pairs (P, Q) with P ̸= Q Lvideo : per sprite per frame, (x, y, dir, costume, visible, size), and P ≈Lvideo Q: (i) never-rendered state, (ii) dead or effect-masked code, (iii) reordered independent statements, (iv) together with rendered monitor values when shown. Audio, reordered independent scripts, and (v) externally observed pen-buffer layout, and internal state fall outside it. On this order latent state. The five families are pairwise distinct (Table I). the camera lens sits between a final-state lens that sees only Each family carries a generator that turns any program the last configuration, which is coarser, and a complete lens into a distinct, camera-equivalent variant, with the equivalence that sees every internal effect, which is finer. Fixing the camera witnessed by a static proof for three families and by a render lens turns an open-ended request to recover the program into a for the two intrinsic ones. The first family inserts a variable precise request to recover a member of one equivalence class. declared but referenced by no block; it produces no transaction The order on lenses is realized by a projection we construct and no observable feature, so the feature multisets of the explicitly. The checker represents an observation as a multiset two programs are equal and the checker proves equivalence of feature tokens, each tagged by the lens axis that emits it. To statically. The second wraps a real block stack under a constantcoarsen from L′ to L, π deletes every token whose axis is on false guard, which the compiler folds away before comparison, in L′ and off in L. The factorization obs L = π ◦ obs L′ then or leaves a stack with no hat, which the compiler drops; the holds by construction, and the monotonicity it supports does surviving features coincide. The third reorders two writes not rest on any per-axis guard scattered through the checker. to distinct invisible variables, which the partial-order normal This is the one place we build the structure the theory needs, form maps to the same representative. The fourth swaps two so the recoverability frontier of Section IV is a property of the independent scripts, which become unordered facts that project construction, not a conjecture about the implementation. identically under the camera lens. The fifth writes a cloud Two programs are equivalent under L, written P ≈L Q, variable the program never displays, which the lens projects when they produce identical L-observations for every input, to nothing. Table I lists the families with the certificate that seed, and legal schedule, the lens-parametric equivalence discharges each and the finer lens, where one exists, at which introduced by [1] and decided by our oracle’s static tier. The the difference becomes observable. relation ≈L is the kernel of the observation map, and the The boundary of each generator is sharper than the family quotient P/ ≈L is the codomain of recovery: recovery targets name suggests, and we state it precisely. A variable that is an equivalence class, not a point. written and then read leaves a feature even when the camera A video witnesses one execution, so acceptance is weaker never renders it, so it is a kernel member the static checker than full equivalence and separates what was seen from what cannot certify, and its non-emptiness is witnessed by a render, was not. not a static proof; code after an unconditional stop, dead yet still compiled, routes to the render witness for the same reason. Definition 1 (Reference-validated acceptance). A candidate The split is by certificate, not by family: some collapses carry P̂ is accepted for a video v = obs L (run(P, ι, r, s)) when a static proof, and some are real but witnessable only by (i) obs L (run(P̂ , ι, r, s)) = v, equivalence on the witnessed replaying both programs, which grants no soundness credit execution, and (ii) on every unwitnessed input, seed, and and is reported as such. schedule, P̂ exhibits no L-observable that P could not, a The statement is a lower bound, and we mark its boundary. refinement off-trace. Two families, never-rendered state and external latent state, are Clause (i) is the trace witness, checkable from the video; invisible at every lens: the difference is the absence of a feature, clause (ii) names the source and is established only by the which no checker can positively mint, so they admit no refuter. static tier against a reference. A render witness checks clause The other three become observable at a finer lens, which makes (i) over sampled frames alone, a trace acceptance short of the them constructive in both directions. We do not claim the five off-trace refinement (ii) demands, so the two tiers earn different families exhaust the kernel; claiming exhaustion would require halves of the definition. By translation validation, narrowing a normal-form theorem, that every camera-equivalent pair is open nondeterminism is sound while adding an unproduced connected by moves drawn from these five families, which is observable is not, so a static certificate gives equivalence on likely false. A lower bound is the right form of the claim, and

TABLE I F IVE NON - IDENTIFIABILITY FAMILIES , THE CERTIFICATE THAT PROVES CAMERA - EQUIVALENCE , AND WHAT SEPARATES EACH , A FINER LENS OR

conflated fraction coarse

INTERVENTION WHERE ONE EXISTS

Family

Why a camera cannot see it

never-rendered state no block reads the variable dead / masked code folded by guard pruning statement order shared normal form script order disjoint, unordered facts external latent state no external resource shown

What separates it none flip guard step-trace lens causal lens none

it still delivers what the system needs, a constructive account of the residual that recovery targets a class to absorb. A recovery returns one program, and the class it represents is infinite, so the system has to choose a member. We fix the choice with a description-length prior. Among the loadable programs in a class, order by code size first and break ties by a canonical serialization, with a penalty on any block the lens cannot see. The penalty pushes the choice toward a program with no camera-invisible structure, a counter that is never displayed, for example, is dropped from the recovered program. Theorem 2 (Representative). For a lens L and this prior, the least-cost member of a class exists and is unique. Within the static tier’s canonical fragment, a static certificate witnesses it equivalent to the source under L when the source leaves no L-invisible feature the representative drops; for a source that drops one, a written-then-read but unrendered counter for instance, or for a pair outside that fragment, the recovery may remain render-witnessed only.

fine floor residual a camera cannot recover

lens fineness

Fig. 2. The recoverability frontier. The fraction of a corpus a lens conflates falls monotonically as the lens sharpens; the floor is the non-identifiable residual of Theorem 1.

a complete view separates. V. T HE VALIDATION O RACLE Validation rests on a checker that tests equivalence under a lens and never errs toward acceptance. The oracle grades a candidate in the benchmark and in any paired or regression setting; it is not part of source-free deployment, where the render tier alone applies. The oracle has two tiers with deliberately different authority. The first tier is static and needs two programs to compare. Following the algorithm of [1], which we implement, it attempts to prove lens-equivalence and returns unknown when it cannot: it compiles both programs to a canonical intermediate form, builds an alpha-renamed feature multiset per trigger, and quotients same-trigger effects by a partial-order normal form [2], [3] so that independent operations in either order compare equal. It mints a positive verdict only when the two multisets are equal, or when the abstract final-state signatures match under the final-state lens. Every field is re-derived from the compiled form of the candidate, and no value supplied by the producer enters the verdict. Any other outcome defaults to different or unknown, and unknown is never an acceptance.

Existence holds because the cost is integer-valued and the integers are well-ordered, so a least cost is attained without any compactness of the class. Uniqueness needs the tie-break well-founded and injective on programs: a cost level can hold infinitely many programs, and a merely total order on an infinite set need not have a least element, while length-thenlexicographic order on finite serializations does, and provided Theorem 3 (Static soundness, assumption-relative). If the the canonical serialization is injective on programs, a property static tier reports equivalent for P and Q under lens L, and we require of the .sb3 canonical form rather than prove, the partial-order independence quotient is adequate for the the least string names one program. The representative is the compiled semantics, then P ≈L Q. smallest program under this prior; a different prior selects a Proof sketch: the checker emits lens-tagged transactions different member, so we never call it canonical absolutely. from the compiled IR, and equality of the per-trigger multisets The target is then well-defined and certifiable in the supported after lens projection and alpha-renaming gives agreement on fragment whenever the source hides no such feature. every L-observable effect. The one remaining step is the The projection that relates lenses also gives a monotonicity stated assumption, that the partial-order quotient preserves we record as an internal check, not a result. If L ⊑ L′ through the execution-order independence of the compiled semantics a total projection π with obs L = π ◦ obs L′ , then ≈L′ ⊆ ≈L : (Section X). applying π to both sides of an equality preserves it, needing The second tier renders. It replays the candidate under the neither injectivity nor lattice structure. So the fraction of a schedule that produced the video and compares its per-frame corpus that collapses to a common class is monotone non- observations against the recorded frames, a check that needs increasing as the lens sharpens, and sweeping the lens from no reference program and so applies even when the source coarse to fine the curve cannot rise (Fig. 2). This holds by is lost. This tier refutes by reporting the first frame and field construction, so an inversion would signal a token-leak defect at which the two diverge, and it reports agreement over the in the lens-coarsening code, and our corpus shows none. The sampled frames, which we label probable equivalence. It does curve traces the territory the camera gives up: the coarse end not mint a certificate. The reason is a quantifier gap. measures how much a camera conflates, the fine end how much

Theorem 4 (Verdict asymmetry). A positive equivalence verdict is minted only by the static tier. A renderer in the loop refutes a candidate with a localized counterexample or reports agreement on finitely many frames; it never certifies equivalence.

render witness accepts a broader set, a recovery that reproduces the witnessed execution, and claims no more than that.

Refutation is monotone: one divergent frame falsifies a universal claim. Confirmation is not: agreement on a finite sample says nothing about the unwitnessed executions, of which there are infinitely many. Granting the renderer certifying power would let a candidate that happens to match the sampled frames pass while differing everywhere else. The asymmetry keeps the renderer useful as a refuter and powerless as a certifier. Two conditions make the refuter sound. Replay is deterministic, achieved by a tick-derived clock and a pinned schedule, and the oracle abstains to unknown when determinism fails. Refutation replays under the schedule that produced the video, so a divergence caused by legal schedule reordering, family (iv) of Theorem 1, is not mistaken for a real difference. The split gives a quality ladder finer than a single accept bit. The bottom rung is over-fit replay: a program that hard-codes the witnessed poses, passes the renderer over the witnessed window, and diverges the moment it extends, so it carries no certificate. The middle rung fits the rule behind the motion; the synthesizer emits only such rule-form programs, never a pose table, so the doubled-window replay is a consistency check, not a memorization test. The top rung is a statically certified program, proved equivalent for every input and schedule. Reporting which rung a recovery reaches makes the soundness claim legible. The static tier is sound but incomplete: on data-dependent control flow it returns unknown, not a proof, and a bounded search for a renaming that aligns two programs can leave a true equivalence unproven. Incompleteness is the right failure mode here, because unknown is never an acceptance and a missed proof costs coverage, not soundness. The error bar that matters is the unknown rate on programs that are equivalent yet syntactically distinct; it surfaces as the recoveries the static tier leaves render-witnessed rather than certified, the gap reported in Section VIII, not as a soundness failure. An identity roundtrip, where a recovery equals its source, proves trivially, so it is not the measurement we report. The soundness invariant ties the tiers together, relative to the compiled IR semantics and the partial-order independence relation the static tier quotients by, the one adequacy obligation we name in Section X. A positive verdict is minted only by the static tier and only from the compiled bytes of the candidate; the renderer either refutes or abstains; any crash in the checker or a failed determinism guard fails closed to refutation. The recorded certificate is the lens, the two feature multisets, the alpharenaming, and the equality verdict; a refuting render witness records the first divergent frame and field. Under this invariant a certified recovery is equivalent to its reference whenever the quotient of Theorem 3 is adequate, a static proof of equivalence a different program cannot produce, and Section VIII tests that adequacy directly with an adversarial battery that reorders dependent operations the quotient could wrongly commute. The

V ID 2P ROG turns a video into a checked candidate in three stages: perception reads tracks from pixels, synthesis fits a generalizing program to the tracks, and the oracle of Section V decides acceptance. A fourth stage, active inference, handles behavior that no passive video reveals.

VI. T HE R ECOVERY P IPELINE

A. Perception Each frame is a 480 × 360 image. A foreground mask separates sprites from the stage, connected components give candidate blobs, and each blob yields a centroid and a bounding box. Identity across frames follows from a one-to-one assignment between detected blobs and the known cast [4], [5], which keeps multiple sprites separated as long as they do not occlude. The position of a sprite is the centroid mapped to stage coordinates through a fixed offset between the centroid and the rotation center of the costume. We calibrate this offset once with a static grid sweep, which removes a constant bias and leaves the measured position exact to within a pixel across the central region of the stage. The offset between the centroid and the rotation center is a property of the costume shape, and calibrating it matters more than its size suggests. A grid sweep that renders a sprite at known positions exposed a constant bias of more than ten pixels that a hand-set offset had left in place, hidden under the oracle tolerance yet far from exact; correcting it from the sweep left the perceived position exact to a pixel across the central stage, a defect the benchmark surfaced only because it checks every recovery against ground truth. Two design choices bound what perception infers. The size, direction, and costume identity of a sprite are granted from the program under test, not inferred from a single blob, because a lone silhouette carries no reliable scale or orientation cue; a colorful or photographic backdrop is granted on the same footing and subtracted as a sprite-free render, which turns a non-white scene back into the white-stage case the mask expects. The boundary this draws is clean: the cast, costumes, sizes, directions, and backdrop form the asset manifest that fixes the lens, while position, visibility, timing, and the motion and frame-counter control behind them are what perception and synthesis recover from pixels, with event-gated behavior added by the active loop. The original source is neither supplied nor returned; the recovered program is a representative of its class. B. Verification-Based Synthesis Perception produces a noisy track, and synthesis must return a program, not a pose table. The vocabulary is a set of structural motifs: constant per-frame displacement, a single-segment glide that moves for a fixed number of frames and then stops, a single visibility transition that hides or shows the sprite at a frame, periodic costume cycling, and a clone family that spawns a fixed number of copies each running a shared behavior. A

Algorithm 1 Verification-based motif synthesis Input: track T over frames 0..N ; tolerances τ, ζ, η Output: program P̂ with S IM(P̂ , N )=T , else A BSTAIN 1: function S YNTHESIZE(T ) 2: for sprite s ∈ T do 3: M ←∅ 4: for axis a ∈ {x, y} do 5: d ← F IT L INE(s.a) 6: if d ̸= ⊥ then 7: M ← M ∪ { CHANGE B Y(a, d) } 8: else 9: g ← F IT G LIDE(s.a) 10: if g = ⊥ then return A BSTAIN 11: end if 12: M ← M ∪ {g} 13: end if 14: end for 15: M ← M ∪ { F IT V ISIBILITY(s), F IT C OSTUME(s) } 16: P̂s ← forever [ tick ++; M ] 17: if S IM(P̂s , N ) ̸= Ts then 18: return A BSTAIN ▷ verification gate 19: end if 20: end for 21: return A SSEMBLE({P̂s }) 22: end function 23: function F IT L INE(v) 24: (a, b) ← L EAST S QUARES(v) 25: if maxi |v[i] − (b + a i)| > τ then 26: return ⊥ 27: end if 28: if |a| < ζ then 29: return 0 30: else if |a − round(a)| < η then 31: return round(a) 32: end if 33: return a 34: end function

answer off the table at the cost of coverage. The choice to abstain aligns the synthesizer with the oracle. A best partial guess would only hand the oracle a program to refute, and a confident point estimate would risk matching a misperception, which the refinement clause forbids; abstention turns both failure modes into a sound non-answer the benchmark reports in full. The cost is real: an abstention is a program the system could not recover, and we report it in the denominator, so the recovery rate is a rate over all attempts and not over a filtered subset. Synthesis extends to clone families. A program that spawns a fixed number of clones, each running a shared behavior, appears in the trace as a growing set of identical sprites that share a name. Recovery reads the maximum clone count, the spawn interval, and the per-clone motion off the trace, and rebuilds the spawning loop and the clone body. The oracle compares clones by birth order, so a recovered family with the right count and the right per-clone behavior matches the source frame by frame. This closes the largest remaining gap in the vocabulary at the trace level, and we mark its boundary in Section X. C. Active Inference for Input-Gated Behavior

Active inference is an extension under a different access model, kept separate from passive recovery. A behavior gated on an input never appears in a passive recording. A sprite that ▷ sub-perceptible moves only while a key is held stays still under a plain greenflag run, and no perception, however accurate, can recover a ▷ integer behavior that never occurs. Recovery here leaves the passivevideo setting and takes black-box query access to the original program: the system supplies inputs and observes the rendered response, and never reads the source. This is the interactive setting of active learning, and its input differs: the original is program is a loop over a frame counter whose body applies a runnable build whose source is not in hand, a packaged or embedded build that runs but exposes no blocks. the fitted motifs. Algorithm 2 recovers the gate. It renders the program Algorithm 1 fits the motifs and emits the program. Two ideas make it sound and precise. The first is a verification gate: passively and, finding it static, holds each candidate key in the program built for a sprite is kept only when its forward turn and renders again, which is the synthesized experiment. simulation reproduces the track frame by frame (line 17), which A motion present only under a key reveals the gate, and the discards a motif that matches a prefix and then diverges and system emits “forever, if the key is pressed, apply the motion.” guarantees the emitted program reproduces what was seen. Confirmation is the careful step: the recovered program must The second is the line fit F IT L INE, which turns noisy pixels agree with the original under both the passive timeline and the into an exact integer rule. It takes the least-squares slope over active one. Passive agreement alone is met by a do-nothing the whole track, rejects the axis when the largest residual program, so the active timeline is the render witness that exceeds the perception tolerance, snaps a sub-perceptible slope confirms the condition and rules out the vacuous answer. to zero, and snaps a near-integer slope to that integer. A single This loop is the one place where the contribution is frame carries several pixels of error, yet the slope of a line irreducibly about acting on the program: the information about through sixty frames averages the error to a fraction of a pixel, a gated behavior exists only in the program’s response to an so an integer-displacement program is recovered exactly and input it did not receive, and producing that response requires not merely to within tolerance. A glide the line fit rejects is synthesizing the input. The choice of which input to try is recovered by splitting the steps into one contiguous moving an experiment-design question [6], [7], and a held key is the run and a static remainder, and visibility and costume recover experiment that most separates a gated program from a doa single transition and a verified period in the same style. nothing one. The territory is not marginal: a static census over When no motif explains a track, synthesis abstains instead real Scratch programs places roughly a third with input-gated of emitting a program it cannot justify, which keeps a wrong visible behavior, structurally blind to passive observation, with ▷ not linear

Algorithm 2 Active-inference gate recovery Input: renderable program P ; candidate keys K; oracle E Q Output: render-witnessed gated program P̂ , else A BSTAIN 1: function R ECOVER G ATE(P, K) 2: T0 ← R ENDER(P, ⟨ ⟩) ▷ no input 3: if M OVES(T0 ) then 4: return S YNTHESIZE(T0 ) ▷ not gated 5: end if 6: for key k ∈ K do 7: Tk ← R ENDER(P, HOLD(k)) ▷ synthesize input 8: δ ← G ATED D ELTA(T0 , Tk ) ▷ motion only under k 9: if δ ̸= 0 then 10: P̂ ← forever [ if PRESSED(k) then APPLY(δ) ] 11: if E Q(P, P̂ , ⟨ ⟩) ∧ E Q(P, P̂ , HOLD(k)) then 12: return P̂ ▷ agrees on both timelines 13: end if 14: end if 15: end for 16: return A BSTAIN 17: end function

an empty-program floor below ten percent, so the active loop’s double-check against the vacuous answer matters. Both algorithms share one soundness discipline. Synthesis emits a program only after its forward simulation reproduces the track, and active inference emits a gate only after the render witness confirms it under both timelines. Neither mints a certificate: the static lens-equivalence certificate is the only positive verdict the system mints, reserved for the static tier, which by the verdict asymmetry of Theorem 4 a renderer can never supply. What the algorithms produce is a candidate that reproduces the witnessed execution under the refinement clause of Definition 1; the static tier alone turns that into a certificate. VII. T HE C LOSED -L OOP B ENCHMARK Evaluating recovery usually needs a labeled corpus of videos paired with their source programs, which is expensive to build and easy to bias. The forward renderer removes the need. A generator emits a program, the renderer turns it into frames, V ID 2P ROG recovers a candidate from the frames with no access to the source, and the validation oracle then compares the recovery to that withheld source under Lvideo . The source is known because the loop produced it, so the ground truth is exact and free, and the recovery rate becomes both the metric and the definition of success. The source is an evaluation input only; recovery sees the frames and the asset manifest. An audit of the pipeline confirms the boundary: perception, denoising, and synthesis receive only the frames and the manifest, and the source reaches only the renderer that makes the video and the validation oracle. The loop also defines a difficulty knob. Holding a program fixed and sharpening the lens raises the bar for a recovery, by the lens-frontier monotonicity, and perturbing a recovered program tests the other direction, whether the checker rejects a program that is close but wrong. We build near-misses by changing a single displacement by one or shifting a transition by a few frames, which probes the checker against the most

adversarial inputs a recovery faces, programs that differ from the source by the smallest step the vocabulary allows. Three guards keep the metric from inflating. A recovery has three outcomes, recovered, refuted, and abstained, and we report all three over the full denominator, so an abstention is never silently dropped or counted as a success. The metric is a sound checker, not a proxy such as pixel similarity, so a high rate cannot be bought by a lenient comparison. A do-nothing program, a tempting vacuous answer for a video with little motion, is ruled out by the near-miss test and the requirement that a recovery reproduce the witnessed observables: an empty program reproduces nothing and is refuted. VIII. E VALUATION The corpus is procedurally generated inside the fragment the vocabulary covers, which fixes the synthesis ceiling and makes perception the variable under test; this isolates recovery-frompixels from synthesis coverage, reported separately in RQ6. Each program is deterministic under a pinned seed and clock. The generator draws each program from constant, boundedglide, and static motion along one axis, with small integer per-frame displacements, visibility and costume transitions at frames sampled over the clip, and one or two separable sprites; this space is broader than the canonical vocabulary of the synthesizer, so a non-canonical source must be recovered as a distinct lens-equivalent program rather than echoed, while a source already in canonical form is recovered exactly. The oracle runs at a position tolerance of 18 pixels for recovery from real pixels, which matches the perception noise floor, and at gold resolution for tests that probe the checker itself. Every rate carries a Wilson 95% confidence interval [8], the appropriate interval for proportions near one where a normal approximation understates uncertainty. We ask six questions. RQ1: does the pipeline recover programs from rendered video? RQ2: does the oracle reject programs that are close but wrong? RQ3: does recovery survive degraded video? RQ4: can the active loop recover inputgated behavior? RQ5: how does a commercial vision-language model compare? RQ6: is the certifier sound, and how far does synthesis reach? a) Perception Accuracy: After offset calibration, the perceived position of a sprite matches the truth to within a pixel across the central stage, and the assignment step keeps two sprites’ identities correct on every frame at the same accuracy. The remaining error is small, unbiased, and centered on the truth, the precondition the least-squares fit needs to average it away, so perception is not the bottleneck for in-vocabulary motion and the end-to-end rate reflects the vocabulary and the lens, not a perception ceiling. b) Recovery From Video (RQ1): The first block of Table II reports recovery under the render witness. Over 798 procedurally generated programs across ten seeds, every recovery reproduces its source frame for frame under the render witness: the recovered program replays in exact agreement with the original over the witnessed window and a window twice as long, with four refutations, no abstention, and no wrong

answer, the three benchmark outcomes reported over the full denominator. Single-sprite and multi-sprite recovery each reach 397 of 399 (99.5%, [98.2, 99.9]), the four misses refuted and never accepted. The multi-sprite programs place two sprites in separate horizontal bands with independent motion and visibility, which the assignment step keeps apart for the full run. The recovery reproduces the observed trajectory exactly: the least-squares fit drives the per-frame displacement to integer precision, so the witnessed motion is matched frame by frame and not merely within tolerance, which establishes that the perception-to-synthesis path carries enough information to reconstruct these programs from pixels under the known-asset lens. How strongly each recovery is certified is the finer question, and it separates the render witness from a static proof. By the verdict asymmetry of Theorem 4 the render witness refutes but never certifies, so a recovery it accepts sits on the middle rung of the quality ladder, a generalizing rule-form program; the over-fit bottom rung that freezes once the window extends is a baseline the synthesizer never emits, so the doubled-window agreement checks consistency, not memorization. The top rung is a static lens-equivalence certificate, and running the static tier on the recovered programs proves 80% of them equivalent to their source at every lens (635 of 794 across ten seeds, single-sprite 87.4% [83.8, 90.3], multi-sprite 72.5% [68.0, 76.7]). Treating each seed as the unit of analysis, the rate is 80.0% with a seed-level 95% interval of [76.9, 83.1] that brackets the pooled figure, so the headline tracks variance across corpora, not two lucky draws. The synthesizer earns the certificate by emitting canonical integer literals and initial poses, which makes an identifiable recovery byte-equal to its source. Without this canonicalization the same recoveries stay render-witnessed but only 15% carry a static proof. This rate measures how exactly the recovery matches the source, a structural comparison placing every certified recovery within a pixel of it, not the checker discriminating syntactically distinct programs, the content of RQ2 and RQ6. The residual that no canonicalization reaches is the recoverability frontier in miniature: a recovery that drops camera-invisible structure, the minimal representative of Theorem 2, or a bounded glide whose gating the witnessed trace underdetermines, matches its source frame for frame yet is statically distinct from a bulkier source. The system recovers the rule, not the trajectory. A full-vocabulary corpus with motion under occlusion makes this quantitative: 79 of 80 recover frame for frame but only 58 certify, the residual motion the occlusion makes non-identifiable. c) The Oracle Discriminates (RQ2): A recovery rate is meaningful only if the checker rejects programs that are close but wrong. We build near-misses by perturbing each program minimally, a single displacement off by one or a transition shifted by a few frames, and ask the oracle to reject them. At gold resolution the oracle rejects all 33 genuine near-misses with zero false accepts, which shows the checker discriminates structurally. At the perception tolerance the rejection rate is 26 of 33. The seven near-misses not refuted at the 18-pixel tolerance deviate, over their whole trajectory, by less than that

perception noise floor; under the exact camera lens, which sees position to the pixel, they are distinct, but the tolerant render witness the denoiser needs against real-pixel noise does not separate them. These seven are a perception-noise shortfall at the operating tolerance, not a soundness failure: the static certifier’s soundness is defined under the exact lens, where the gold-resolution result rejects all 33, and the tolerance floor shrinks as perception sharpens. The synthesis vocabulary is a knob under an invariant oracle. Extending it to two-segment motion and arbitrary show/hide sequences recovers 40 programs of two-speed motion, bounce, and multi-transition visibility that the single-segment vocabulary left uncertified, now 40 recovered and 39 certified with zero false accepts, the base corpus unchanged; a harder suite of 30 three- and four-segment motions stays beyond reach, abstained on in full, none wrong. d) Robustness (RQ3): Real recordings are compressed and slow. The second block of Table II reports two stresses. Framerate decimation keeps every k-th frame, simulating capture from 30 down to 5 frames per second; the denoiser fits displacement against the true tick of each surviving frame, so a sparse sample recovers the same per-tick motion as a dense one. Motion recovery stays at 20 of 20 across every rate down to 5 frames per second, where a two-second clip is eleven frames. A straight line is fixed by any two points, so continuous motion costs nothing under decimation, while a discrete event such as a hide localizes only to within one sampling interval. A colorful, per-frame-noisy backdrop, handled by background subtraction, also recovers 20 of 20, which shows perception is not tied to a white stage. Separately, encoding the frames as H.264 across the full quality range leaves the measured position within five to eight pixels, so compression preserves the coarse spatial structure recovery depends on. The strongest test is a genuine recording: each program is rendered through FastRender, a separate deterministic renderer we contribute with its own rasterizer, and its H.264 video is decoded back to frames; perception, now reading pixels a different engine produced, recovers all 40 losslessly and 39 of 40 under visible compression (CRF 28), one abstaining and none wrong. These stresses bound the gap to genuine recordings from several sides, and continuous motion survives all of them because its information is spread across frames; the one stated limit is that at five frames per second a discrete event is pinned only to within a sixth of a second, the resolution the observation rate allows. e) Active Inference (RQ4): The third block of Table II reports the input-gated case. Each of 16 programs is static under a passive run and moves only while a key is held. V ID 2P ROG queries the program as a black box, synthesizes the heldkey input, recovers the gate, and the oracle confirms that the recovered program reproduces both the passive and the active trace. All 16 are recovered, with passive and active agreement on every one. The double check matters: passive agreement alone is met by a do-nothing program, so requiring active agreement is what certifies the recovered condition. The static census we ran over 262 real Scratch programs places inputgated visible behavior at 31%, the prevalence the active loop

addresses when such a program reaches a viewer as a runnable quotient to commute everything turns all four into false accepts, build without source. so the real quotient’s zero accepts bound its inadequacy, not a f) Vision-Language Baseline (RQ5): A natural question weak battery. The zero rate over both stresses the soundness is whether a commercial model recovers programs directly invariant rather than proving it. A lens sweep from coarse from frames. We feed frames sampled at known ticks and the to fine records the fraction each lens conflates; the curve is sprite list to a vision-language model and ask, at temperature monotone non-increasing, a consistency check on the lenszero, for each sprite’s per-frame pixel displacement and any coarsening implementation, where an inversion would signal a visibility transition as a JSON specification, build a runnable token-leak defect. program from its answer through our reliable builder, and Coverage measures the other side, how far the synthesis route the result through the same oracle. Table III reports two vocabulary reaches when perception is perfect, which is the models, the open-weight MiniMax-M3 and Claude Sonnet 4.6, ceiling the in-fragment benchmark fixes. At gold perception the with exact versions, run dates, and frame sampling specified vocabulary synthesizes 88% of 987 sprites from real Scratch in the evaluation protocol; we read them as evidence that an projects. The clone family closes the largest remaining gap, untrusted generator errs confidently, not as a tuned competitor. and clone-family synthesis recovers 20 of 20 programs across On a matched set of the 40 single-sprite programs the pipeline clone counts from three to ten with the oracle matching clones recovers in full, Claude Sonnet 4.6 recovers 0 and MiniMax- by birth order. The residual the vocabulary does not yet name is M3 recovers 1, the oracle refuting every wrong answer with multi-segment motion and arbitrary costume content, recovered no false accept. The model reads qualitative behavior such by adding motifs under the same fit, together with control as a costume cycle but misreads the quantitative parameters, beyond the frame-counter form, data-dependent branching, eyeballing a displacement where the pipeline fits the rule over broadcasts, and bounded loops, which the static tier cannot every frame. The failure is perception, not synthesis: handed the certify and we leave open. The 88% ceiling and the 100% endperceived tracks as text, with no displacement left to eyeball, to-end rate measure different things: the 100% is perceptionthe same model recovers 29 of 40, and the oracle refutes the to-synthesis fidelity inside the supported vocabulary, not a 10 it still gets wrong while accepting none. The pipeline’s edge recovery rate for arbitrary Scratch programs, while the 88% is the least-squares fit on noisy pixels; the oracle catches a estimates how far that vocabulary reaches on an unrestricted wrong specification whoever produced it. real corpus under perfect perception. The verification gate This is where the sound checker earns its place. Any and the description-length prior are soundness and selection generative recovery, a model or a search, produces candidates disciplines, not tuned components, so the one ablation we without a guarantee; the oracle converts them into trustworthy report is canonicalization on or off. output by refuting the wrong ones and feeding the first h) Real Projects End-to-End: A complementary run takes divergence back for repair. We close that loop: the oracle returns the whole pipeline to real Scratch projects from the public to the model the first frame and field where the candidate’s site. On 30 projects rendered and recovered from pixels, replay diverges from the recording, with the value the recording recovery reaches 4 of the 29 that return a verdict, alongside 17 shows there, all observational, and the model revises. Over three abstentions, 8 refutations, one timeout, and no false accept. Real rounds this lifts Claude from 0 to 3 of 40, concrete evidence projects mostly use behavior outside the current vocabulary, so that the refutations are actionable, while the structured pipeline this 14% is a vocabulary-bound end-to-end rate, the per-sprite with the same checker reaches all 40. The model proposes, the coverage ceiling now paid in full on whole projects, with the oracle disposes, and a search, neural or symbolic, repairs; the no-wrong-answer guarantee intact on real data. checker is what makes any of them trustworthy. i) Reading the Table as a Whole: Across Table II, no row g) Soundness and Coverage (RQ6): Two measurements reports a wrong answer and the certifier never false-accepts; bound the system from the sound side. The certifier mints no recovery is bounded by the synthesis vocabulary and by what a false positive over 604 labeled program pairs, where a false passive camera can witness, not by perception or the certifier. positive is a positive equivalence verdict on a pair the ground IX. R ELATED W ORK truth marks different. Zero false accepts is the expected face Program synthesis from examples infers a program from of the verdict asymmetry of Theorem 4, a positive verdict requiring a static proof a different program cannot supply. A input-output pairs [9]–[14], with neural variants learning the false accept is possible only on a gold-different pair; of the 604 map from data [15]–[17], and programming by demonstration labeled pairs, 246 are gold-different under the full lens, the 33 generalizes a user’s actions into a script [18]–[20]. All read a near-misses the hardest, and the certifier false-accepts none. The clean, structured specification; our input is a rendered video, near-misses perturb visible axes, so a five-pair battery targets where object identity, control flow, and internal state are the quotient itself, reordering dependent operations whose order recovered before synthesis begins. Neural program induction changes a lens-observable: a write-write, a read-after-write and maps trajectories to programs [21]–[23] but supervises on a read-after-change across variables, an absolute-then-relative ground-truth programs and trusts the output; we supervise with move, and a list insertion. The static tier returns different on the a renderer and accept only under a sound check. four the lens observes, never equivalent, and commutes only Inverse graphics and scene de-rendering recover scene the independent control, a disjoint-variable write. Forcing the parameters or a scene-drawing program from images [24]–

TABLE II R ECOVERY, CERTIFICATION , AND DISCRIMINATION BY TASK , WITH W ILSON 95% CONFIDENCE INTERVALS Task

n

Pass

Render-witnessed trace match (Tier-2) single sprite, ten seeds 399 397 multi-sprite, ten seeds 399 397

Rate (95% CI) 99.5 [98.2, 99.9] 99.5 [98.2, 99.9]

Static lens-equivalence certificate (Tier-1) single sprite, ten seeds 397 347 87.4 [83.8, 90.3] multi-sprite, ten seeds 397 288 72.5 [68.0, 76.7] Discrimination (near-miss rejection) gold resolution 33 33 perception resolution 33 26

100.0 [89.6, 100] 78.8 [62.2, 89.3]

Robustness and active inference motion at 5 fps 20 colorful backdrop 20 active-inference gate 16 clone family (3–10) 20

100.0 [83.9, 100] 100.0 [83.9, 100] 100.0 [80.6, 100] 100.0 [83.9, 100]

20 20 16 20

TABLE III R ECOVERY ON A MATCHED SET OF 40 SINGLE - SPRITE PROGRAMS , THROUGH THE SAME BUILDER AND ORACLE : VISION - LANGUAGE MODELS SINGLE - SHOT FROM FRAMES , C LAUDE HANDED THE PERCEIVED TRACKS ( PERCEPTION - MATCHED ) AND WITH ORACLE - IN - THE - LOOP REPAIR (3 ROUNDS ), AND OUR STRUCTURED PIPELINE . N O METHOD EVER FALSE - ACCEPTS . System MiniMax-M3, single-shot Claude Sonnet 4.6, single-shot Claude Sonnet 4.6, perceived tracks Claude Sonnet 4.6 + oracle repair V ID 2P ROG, structured

Recovered (95% CI)

False acc.

1/40 (2.5%) [0.4,12.8] 0/40 (0%) [0.0,8.8] 29/40 (72.5%) [57.2,83.9] 3/40 (7.5%) [2.6,19.7] 40/40 (100%) [91.2,100]

0 0 0 0 0

[29]; that target is a parameter vector, while ours is the producing program, which re-executes and can be edited, making observational equivalence the criterion and a class, not a point, the codomain. Decompilation reconstructs source-level structure from a binary [30], and learned decompilers translate assembly to source or recover names [31]–[33], but the binary still encodes the computation; execution video retains only its visible effects, a strictly lossier signal, which is why a theorem about what cannot be recovered belongs in the problem statement. Extracting code from a screencast [34]–[36] assumes the code is on screen; in a running game it never is. Analysis and testing of Scratch programs read the source: tools assess code quality [37], generate tests [38], detect smells and bugs [39], [40], and characterize the public corpus [41], on a language designed for novices [42], [43]. We start one step earlier, from a recording with no source, and produce the source those tools consume, a front end to the Scratch analysis stack, answering under a stated lens the equivalence question they sidestep. Recent Scratch-specific systems increasingly exploit execution evidence, but they still start from source, a reference, or a controlled repair/evaluation setup. ViScratch combines code and gameplay video for feedback [44]; Stitch structures

feedback as step-by-step tutoring [45]; ScratchEval supplies executable repair benchmarks and metrics [46]; EcoScratch adapts multimodal repair effort using execution feedback [47]; Raven uses video-grounded evaluation for automated assessment [48]; ScratchWorld uses replay-verified Scratch transitions to evaluate executable world-model reasoning [49]; and ScratchLens supplies lens-parametric equivalence for comparing Scratch programs [1]. Zhang and collaborators also study automated feedback for competition-level code, LLM-based Python repair, time-limit-exceeded errors, mergeconflict resolution, CI-configuration correctness, and silent misconfiguration detection [50]–[55]. V ID 2P ROG is orthogonal: it treats the video itself as the only observable artifact and accepts a recovered program only after a sound oracle checks it under the chosen observation lens. The soundness discipline follows translation validation, which certifies equivalence of two programs instead of trusting the transformer [56]–[58], and program-equivalence checking more broadly [59], [60]. A validator compares two given programs; we first recover one from pixels, so a small trusted checker downstream of an untrusted producer follows proof-carrying code and verified compilation [61], [62], and forbidding the renderer from minting a verdict carries the no-false-accept guarantee, a discipline shared with program repair [63], [64]. X. D ISCUSSION AND T HREATS a) What the Certificates Rest On: The results separate by the strength of their backing: a passing run of the static tier (the algorithm of [1], which we implement) covers its soundness, three non-identifiability families, the representative, and the verdict asymmetry, while the rest rest on short mechanizable proofs (the representative’s uniqueness, the frontier monotonicity) or are definitional or undecidable (the two intrinsic families, the completeness bound). One obligation sits at the boundary, the adequacy hypothesis of Theorem 3: that the partial-order quotient matches the true execution relation, the one claim a green check does not establish. We carry it as a named residual, reachable by generalizing known footprint theorems. b) Generality: The recipe transfers to any domain with a sound lens-equivalence checker, and that checker is the hard part: Scratch has one because its execution model is small and its output well defined, while a general-purpose runtime needs a checker of comparable strength first. c) Threats to Validity: The recovery results use programs inside the fragment the vocabulary covers on controlled scenes, a deliberate scope that fixes the synthesis ceiling and isolates perception; recovery of an arbitrary real program is bounded by the vocabulary and by what passive observation reveals, both measured (end to end at 14% on real projects). Recovery assumes a known asset manifest; inferring arbitrary costume or backdrop content from pixels is out of scope. Perception is not tied to the forward model: re-rendering through FastRender, a separate rasterizer used for cross-renderer validation, and recovering from its decoded H.264 video gives 40 of 40 lossless

and 39 of 40 under visible compression, none wrong. That video is itself a rendered-execution recording through a real codec, so it answers external validity directly; what a desktop capture adds beyond it, window chrome and capture timing, the stage crop the lens already assumes removes and the frame-rate result bounds. d) Future Work: Three directions follow: growing the synthesis vocabulary, oscillation and three-plus-segment motion next; inferring costume and backdrop content from pixels to lift the known-asset assumption; and mechanizing the one obligation a positive verdict does not discharge. XI. C ONCLUSION Untrusted program recovery becomes trustworthy when a sound checker, not the generator, has the last word. We make it precise for execution video: success is observational equivalence under the camera lens, certified by a static tier and witnessed by a refute-only renderer, realized by V ID 2P ROG with motif synthesis and an active-inference loop. The oracle false-accepts nothing we test, 80% of recoveries certify, and a model’s confident errors are caught. The discipline extends to any generative recovery backed by a sound checker. R EFERENCES [1] Y. Si and J. Zhang, “ScratchLens: Lens-parametric behavioral equivalence for Scratch programs,” 2026, arXiv:2606.15817 [cs.PL]. [2] A. W. Mazurkiewicz, “Trace theory,” Advances in Petri Nets, LNCS 255, pp. 279–324, 1987. [3] C. Flanagan and P. Godefroid, “Dynamic partial-order reduction for model checking software,” in Proc. 32nd ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages (POPL), 2005, pp. 110–121. [4] H. W. Kuhn, “The hungarian method for the assignment problem,” Naval Research Logistics Quarterly, vol. 2, no. 1-2, pp. 83–97, 1955. [5] A. Bewley, Z. Ge, L. Ott, F. Ramos, and B. Upcroft, “Simple online and realtime tracking,” in IEEE Int. Conf. Image Processing (ICIP), 2016, pp. 3464–3468. [6] B. Settles, “Active learning literature survey,” University of WisconsinMadison, Tech. Rep. Computer Sciences Technical Report 1648, 2009. [7] D. Angluin, “Learning regular sets from queries and counterexamples,” Information and Computation, vol. 75, no. 2, pp. 87–106, 1987. [8] E. B. Wilson, “Probable inference, the law of succession, and statistical inference,” Journal of the American Statistical Association, vol. 22, no. 158, pp. 209–212, 1927. [9] S. Gulwani, “Automating string processing in spreadsheets using inputoutput examples,” in Proc. 38th ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages (POPL), 2011, pp. 317–330. [10] A. Solar-Lezama, “Program synthesis by sketching,” Ph.D. dissertation, University of California, Berkeley, 2008. [11] S. Gulwani, O. Polozov, and R. Singh, “Program synthesis,” Foundations and Trends in Programming Languages, vol. 4, no. 1-2, pp. 1–119, 2017. [12] R. Alur, R. Bodı́k, G. Juniwal, M. M. K. Martin, M. Raghothaman, S. A. Seshia, R. Singh, A. Solar-Lezama, E. Torlak, and A. Udupa, “Syntax-guided synthesis,” in Formal Methods in Computer-Aided Design (FMCAD), 2013, pp. 1–8. [13] J. K. Feser, S. Chaudhuri, and I. Dillig, “Synthesizing data structure transformations from input-output examples,” in Proc. ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI), 2015, pp. 229–239. [14] O. Polozov and S. Gulwani, “FlashMeta: A framework for inductive program synthesis,” in Proc. ACM SIGPLAN Int. Conf. Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2015, pp. 107–126. [15] M. Balog, A. L. Gaunt, M. Brockschmidt, S. Nowozin, and D. Tarlow, “DeepCoder: Learning to write programs,” in Int. Conf. Learning Representations (ICLR), 2017.

[16] J. Devlin, J. Uesato, S. Bhupatiraju, R. Singh, A. rahman Mohamed, and P. Kohli, “RobustFill: Neural program learning under noisy i/o,” in Int. Conf. Machine Learning (ICML), 2017, pp. 990–998. [17] K. Ellis, C. Wong, M. I. Nye, M. Sablé-Meyer, L. Morales, L. B. Hewitt, L. Cary, A. Solar-Lezama, and J. B. Tenenbaum, “DreamCoder: Bootstrapping inductive program synthesis with wake-sleep library learning,” in Proc. 42nd ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI), 2021, pp. 835–850. [18] A. Cypher, Ed., Watch What I Do: Programming by Demonstration. MIT Press, 1993. [19] H. Lieberman, Ed., Your Wish is My Command: Programming by Example. Morgan Kaufmann, 2001. [20] T. A. Lau, S. A. Wolfman, P. M. Domingos, and D. S. Weld, “Programming by demonstration using version space algebra,” Machine Learning, vol. 53, no. 1-2, pp. 111–156, 2003. [21] S.-H. Sun, H. Noh, S. Somasundaram, and J. J. Lim, “Neural program synthesis from diverse demonstration videos,” in Int. Conf. Machine Learning (ICML), 2018, pp. 4790–4799. [22] R. Bunel, M. J. Hausknecht, J. Devlin, R. Singh, and P. Kohli, “Leveraging grammar and reinforcement learning for neural program synthesis,” in Int. Conf. Learning Representations (ICLR), 2018. [23] X. Chen, C. Liu, and D. Song, “Execution-guided neural program synthesis,” in Int. Conf. Learning Representations (ICLR), 2019. [24] T. D. Kulkarni, W. F. Whitney, P. Kohli, and J. B. Tenenbaum, “Deep convolutional inverse graphics network,” in Advances in Neural Information Processing Systems (NeurIPS), 2015, pp. 2539–2547. [25] V. K. Mansinghka, T. D. Kulkarni, Y. N. Perov, and J. B. Tenenbaum, “Approximate bayesian image interpretation using generative probabilistic graphics programs,” in Advances in Neural Information Processing Systems (NeurIPS), 2013, pp. 1520–1528. [26] J. Wu, J. B. Tenenbaum, and P. Kohli, “Neural scene de-rendering,” in IEEE Conf. Computer Vision and Pattern Recognition (CVPR), 2017, pp. 7035–7043. [27] K. Yi, J. Wu, C. Gan, A. Torralba, P. Kohli, and J. B. Tenenbaum, “Neuralsymbolic VQA: Disentangling reasoning from vision and language understanding,” in Advances in Neural Information Processing Systems (NeurIPS), 2018, pp. 1039–1050. [28] K. Ellis, D. Ritchie, A. Solar-Lezama, and J. B. Tenenbaum, “Learning to infer graphics programs from hand-drawn images,” in Advances in Neural Information Processing Systems (NeurIPS), 2018, pp. 6062–6071. [29] Y. Tian, A. Luo, X. Sun, K. Ellis, W. T. Freeman, J. B. Tenenbaum, and J. Wu, “Learning to infer and execute 3d shape programs,” in Int. Conf. Learning Representations (ICLR), 2019. [30] D. Brumley, J. Lee, E. J. Schwartz, and M. Woo, “Native x86 decompilation using semantics-preserving structural analysis and iterative control-flow structuring,” in Proc. 22nd USENIX Security Symposium, 2013, pp. 353–368. [31] H. Tan, Q. Luo, J. Li, and Y. Zhang, “LLM4Decompile: Decompiling binary code with large language models,” arXiv preprint arXiv:2403.05286, 2024. [32] C. Fu, H. Chen, H. Liu, X. Chen, Y. Tian, F. Koushanfar, and J. Zhao, “Coda: An end-to-end neural program decompiler,” in Advances in Neural Information Processing Systems (NeurIPS), 2019, pp. 3703–3714. [33] J. Lacomis, P. Yin, E. J. Schwartz, M. Allamanis, C. L. Goues, G. Neubig, and B. Vasilescu, “DIRE: A neural approach to decompiled identifier naming,” in Proc. 34th IEEE/ACM Int. Conf. Automated Software Engineering (ASE), 2019, pp. 628–639. [34] S. Yadid and E. Yahav, “Extracting code from programming tutorial videos,” in Proc. ACM Int. Symp. New Ideas, New Paradigms, and Reflections on Programming and Software (Onward!), 2016, pp. 98–111. [35] L. Ponzanelli, G. Bavota, A. Mocci, M. D. Penta, R. Oliveto, M. Hasan, B. Russo, S. Haiduc, and M. Lanza, “Too long; didn’t watch! extracting relevant fragments from software development video tutorials,” in Proc. 38th Int. Conf. Software Engineering (ICSE), 2016, pp. 261–272. [36] L. Bao, Z. Xing, X. Xia, D. Lo, M. Wu, and X. Yang, “psc2code: Denoising code extraction from programming screencasts,” ACM Trans. Software Engineering and Methodology, vol. 29, no. 3, pp. 21:1–21:38, 2020. [37] J. Moreno-León and G. Robles, “Dr. scratch: A web tool to automatically evaluate scratch projects,” in Proc. Workshop in Primary and Secondary Computing Education (WiPSCE), 2015, pp. 132–133. [38] A. Stahlbauer, M. Kreis, and G. Fraser, “Testing scratch programs automatically,” in Proc. 27th ACM Joint European Software Engineering

Conf. and Symp. Foundations of Software Engineering (ESEC/FSE), 2019, pp. 165–175. [39] G. Fraser, U. Heuer, N. Körber, F. Obermüller, and E. Wasmeier, “LitterBox: A linter for scratch programs,” in Proc. 43rd Int. Conf. Software Engineering: Software Engineering Education and Training (ICSE-SEET), 2021, pp. 183–188. [40] B. Boe, C. Hill, M. Len, G. Dreschler, P. T. Conrad, and D. Franklin, “Hairball: Lint-inspired static analysis of scratch projects,” in Proc. 44th ACM Technical Symp. Computer Science Education (SIGCSE), 2013, pp. 215–220. [41] E. Aivaloglou and F. Hermans, “How kids code and how we know: An exploratory study on the scratch repository,” in Proc. ACM Conf. Int. Computing Education Research (ICER), 2016, pp. 53–61. [42] M. Resnick, J. Maloney, A. Monroy-Hernández, N. Rusk, E. Eastmond, K. Brennan, A. Millner, E. Rosenbaum, J. Silver, B. Silverman, and Y. Kafai, “Scratch: Programming for all,” Communications of the ACM, vol. 52, no. 11, pp. 60–67, 2009. [43] J. Maloney, M. Resnick, N. Rusk, B. Silverman, and E. Eastmond, “The scratch programming language and environment,” ACM Trans. Computing Education, vol. 10, no. 4, pp. 16:1–16:15, 2010. [44] Y. Si, D. Li, H. Shi, and J. Zhang, “ViScratch: Using large language models and gameplay videos for automated feedback in Scratch,” arXiv:2509.11065 [cs.SE], 2025. [45] Y. Si, K. Qi, D. Li, H. Shi, and J. Zhang, “Stitch: Step-by-step LLM guided tutoring for Scratch,” arXiv:2510.26634 [cs.SE], 2025. [46] Y. Si, S. Han, D. Li, H. Shi, and J. Zhang, “ScratchEval: A multimodal evaluation framework for LLMs in block-based programming,” arXiv:2602.00757 [cs.SE], 2026. [47] Y. Si, M. Wang, D. Li, H. Shi, and J. Zhang, “EcoScratch: Costeffective multimodal repair for Scratch using execution feedback,” arXiv:2603.29624 [cs.SE], 2026. [48] D. Li, D. Li, H. Shi, and J. Zhang, “Raven: Rethinking automated assessment for Scratch programs via video-grounded evaluation,” arXiv:2604.17820 [cs.SE], 2026. [49] Y. Lin and J. Zhang, “ScratchWorld: Evaluating if world models compute executable consequences,” arXiv:2606.31689 [cs.SE], 2026. [50] J. Zhang, D. Li, J. C. Kolesar, H. Shi, and R. Piskac, “Automated feedback generation for competition-level code,” in Proceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering, ser. ASE 2022. ACM, 2022, pp. 13:1–13:13. [51] J. Zhang, J. P. Cambronero, S. Gulwani, V. Le, R. Piskac, G. Soares, and G. Verbruggen, “PyDex: Repairing bugs in introductory python assignments using LLMs,” Proceedings of the ACM on Programming Languages, vol. 8, no. OOPSLA1, pp. 1100–1124, 2024. [52] J. Zhang, J. Gu, W. Zhang, J. P. Cambronero, J. C. Kolesar, R. Piskac, D. Li, and H. Shi, “A systematic study of time limit exceeded errors in online programming assignments,” arXiv:2510.14339 [cs.SE], 2025. [53] J. Zhang, T. Mytkowicz, M. Kaufman, R. Piskac, and S. K. Lahiri, “Using pre-trained language models to resolve textual and semantic merge conflicts,” in Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis, ser. ISSTA 2022. ACM, 2022, pp. 77–88. [54] M. Santolucito, J. Zhang, E. Zhai, J. Cito, and R. Piskac, “Learning CI configuration correctness for early build feedback,” in Proceedings of the 2022 IEEE International Conference on Software Analysis, Evolution and Reengineering, ser. SANER 2022. IEEE, 2022, pp. 1006–1017. [55] J. Zhang, R. Piskac, E. Zhai, and T. Xu, “Static detection of silent misconfigurations with deep interaction analysis,” Proceedings of the ACM on Programming Languages, vol. 5, no. OOPSLA, pp. 1–30, 2021. [56] A. Pnueli, M. Siegel, and E. Singerman, “Translation validation,” in Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 1998, pp. 151–166. [57] G. C. Necula, “Translation validation for an optimizing compiler,” in Proc. ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI), 2000, pp. 83–94. [58] N. P. Lopes, J. Lee, C.-K. Hur, Z. Liu, and J. Regehr, “Alive2: Bounded translation validation for LLVM,” in Proc. 42nd ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI), 2021, pp. 65–79. [59] R. Sharma, E. Schkufza, B. R. Churchill, and A. Aiken, “Data-driven equivalence checking,” in Proc. ACM SIGPLAN Int. Conf. ObjectOriented Programming, Systems, Languages, and Applications (OOPSLA), 2013, pp. 391–406.

[60] B. R. Churchill, O. Padon, R. Sharma, and A. Aiken, “Semantic program alignment for equivalence checking,” in Proc. 40th ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI), 2019, pp. 1027–1040. [61] G. C. Necula, “Proof-carrying code,” in Proc. 24th ACM SIGPLANSIGACT Symp. Principles of Programming Languages (POPL), 1997, pp. 106–119. [62] X. Leroy, “Formal verification of a realistic compiler,” Communications of the ACM, vol. 52, no. 7, pp. 107–115, 2009. [63] F. Long and M. C. Rinard, “Automatic patch generation by learning correct code,” in Proc. 43rd ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages (POPL), 2016, pp. 298–312. [64] S. Mechtaev, J. Yi, and A. Roychoudhury, “Angelix: Scalable multiline program patch synthesis via symbolic analysis,” in Proc. 38th Int. Conf. Software Engineering (ICSE), 2016, pp. 691–701.