Replay-Gated Neural Execution: Decoupling Persistent Behavioral Specifications from Neural Realizations in Frozen Language Models

Xianliang Zeng; Zhanzhan Zhao

cs.CLSep 5, 2026

Replay-Gated Neural Execution: Decoupling Persistent Behavioral Specifications from Neural Realizations in Frozen Language Models

Authors: Xianliang Zeng, Zhanzhan Zhao

Organizations: The Chinese University of Hong Kong, Shenzhen Shenzhen, China

Abstract

Input-conditioned neural interventions raise a runtime question: what persists when one behavioral specification admits multiple actions whose validity depends on execution state? We introduce replay-gated neural execution, separating five objects: a persistent behavioral predicate, its state-indexed certified realization set, a transient action witness, a budget-limited finder, and execution authorization. Candidates undergo isolated FP32/BF16 replay of the frozen model; commitment additionally requires a valid run audit. Experiments on Qwen3-0.6B and SmolLM2-360M-Instruct establish distinct failure modes for these objects. Independent initializations yield distinct certified actions in all 24 tested fixed-state cells. Unchanged SmolLM2 witnesses remain certified in all 128 native states but only 66 of 384 off-diagonal transfers. All 767 archived Qwen witnesses replay successfully, yet a budget-limited finder misses one known-realizable cell in all three prespecified runs. Of 1,141 replay-submitted candidates, 174 fail item certification. A frozen three-tier cascade uses these boundaries to reject uncertified proposals and escalate audit-valid search misses. On 256 previously sealed Qwen Fresh requests, 221 first certify at the lowest-cost tier and all 256 receive audited authorization, with no observed bypass. Relative to frozen full search, the median singleton search-and-certification cost ratio is 0.1055 and P95 is 1.3485, including failed tiers. Within the studied behavioral family on two small models, these results support state-indexed, set-valued execution semantics: specifications persist, search proposes witnesses, and replay certification plus run audit grants execution authority.

Figures & tables

Panel of Figure 1 — Figure 1: Authority-separated neural execution. A semantic target $U$ guides budgeted search for a candidate $a$ . ReplayCert tests that candidate by isolated FP32/BF16 replay of the frozen model from the original state. Execution requires both item certification and a passing run audit. The Qwen schematic shows nine declared residual-write slots. Audit-valid misses escalate or abstain; integrity failures stop (Figure 3 ).

Tier	Candidate generation	Update budget	Visible information	Escalation or termination
Tier1	Protocol-visible $K=8$ pullback warm start followed by a short full-space certified solve	$\leq 32$	$U,o$ , and protocol-permitted $z_{t}$	Escalate after an audit-valid search miss; fail closed on an invalid run
Tier2	Augmented curvature and relinearization	$\leq 48$	Same frozen interface	Escalate after an audit-valid search miss; fail closed on an invalid run
Tier3	Singleton WitnessSearch matching the full baseline	Frozen full lifecycle	Same frozen interface	Abstain after audit-valid search exhaustion; fail closed on an invalid run

Table 1: Frozen cascade structure. Exact internal phase lengths for Tier3 are listed in the appendix.

Cohort	Size	Purpose
Reachability Public	$4\times 64$	Physical reachability and cross-precision gating
Reference Stability	$12\times 64=768$ (767 reference + 1 abstention)	Witness replay and difficult-cell rediscovery
CascadePilot	$4\times 64$	One-time qualification and cost gate
Frozen Fresh	$4\times 64$	New-context evaluation of the frozen policy
Unseen Utility	Sealed	Outside the scope of this paper

Table 2: Qwen3 experimental cohorts and their roles.

Panel of Figure 2 — Figure 2: SmolLM2 cross-state transfer of unchanged witnesses. (a) Rows are source contexts and columns are target contexts, with 32 Utilities per source. XML: XML notice; DB Row: database row; Log: log excerpt; Chat: chat transcript. All $128/128$ native replays certify, versus $66/384$ off-diagonal transfers. (b) Each gate is evaluated on all 384 off-diagonal transfers; bars are not cumulative filtering stages. Physical legality persists, while Top-1 and robust-margin qualification change across contexts.

Panel of Figure 3 — Figure 3: Proposal, certification, and authorization. (a) Audited Qwen and SmolLM2 events, with mutually exclusive rejection counts (Appendix C ). (b) Audit-valid rejections escalate; selected certified actions require final replay and run audit before commitment. All 256 requests commit, with zero observed authorization bypasses. Node sizes are schematic.

Figure 4: Frozen Fresh routing at matched granularity. Rows align the 64 Utility requests in each context with their Tier 1/2/3 totals. Context 0 accounts for 28 of the 35 requests that escalate; all 256 requests ultimately certify. Historical cohort aggregates remain in Table 5 .

Active $U$ ( $m$ )	$1-\operatorname{med}(r_{i})$	LCB95	$\operatorname{P95}(r_{i})$	Paired-replay-equivalent cost reduction
1	$89.45\%$	$88.98\%$	1.3485	$85.59\%$
2	$91.37\%$	$90.90\%$	1.0973	$88.13\%$
4	$92.91\%$	$92.28\%$	0.9434	$90.54\%$
8	$93.32\%$	$92.42\%$	0.9037	$91.44\%$
64	$88.23\%$	$84.24\%$	0.6479	$86.44\%$

Table 3: Frozen Fresh normalized search-and-certification cost. LCB95 is the protocol-defined 95% bootstrap lower bound over frozen cyclic windows; it is not an i.i.d. population interval.

Appendix figures & tables5 assets

Supplementary material from the paper’s appendix.

Appendix

Metric	Frozen definition
Top-1	Target ranks first among all 64 candidates, evaluated separately in FP32 and BF16
Effect peak	Target-score effect is maximal relative to the zero action
Robust margin	Target exceeds the runner-up by at least $0.2$ at each precision
Exact zero	Empty Utility or abstention keeps the hard write path exactly zero
Permutation	Equivariance error under the frozen candidate-list transformation family is at most $10^{-6}$ ; this does not refer to search-generation order
Cohort P99	Nearest-rank/upward quantile over committed actions; threshold $\leq 0.018$ , separate from item certification

Appendix

Table 4: Frozen metric and statistical definitions.

Evidence block	Cohort	Frozen result	Role in the claim
Protocol H1: reachability	$4\times 64$	$256/256$ ; P99 $\approx.01675$ ; max $\approx.01738$	Port reachability
Protocol H2: non-uniqueness	16 cells $\times$ 8 initializations	16/16 each have 8 distinct certified solutions; 448 pairs; relative $\ell_{2}$ min $0.0225340$ , max $1.1948683$	Actions are non-unique at fixed cell
Protocol H3: Reference Stage A	767 cells	$767/767$ ; minimum margins $.20184/.20464$	Frozen-witness validity
Protocol H3: Reference Stage B	23 preselected difficult cells $\times 3$	22 cells $3/3$ ; one cell $0/3$	Existence counterexample; no population-rate estimate
Retrospective cascade	767 cells	$767/767$ versus full solver $766/767$ ; $709/33/25$	Full solver is not a realizability criterion
Protocol H4: CascadePilot	$4\times 64$	$256/256$ ; $256/0/0$ ; no authorization bypass	Tier1 sufficient on Pilot

Appendix

Table 5: Frozen evidence ledger and the role of each block.

Figure 5: Certified non-uniqueness and finite-search failure. (a) For each fixed cell, a line spans the minimum to maximum of 28 pairwise distances among eight certified restarts; a filled dot marks the median and an open dot the minimum. These are descriptive ranges, not confidence intervals. All minima are positive. (b) A stored witness certifies at

(\text{context }9,U37)

, while all three budget-limited rediscovery runs abstain. The 23 difficult cells were selected before execution.

Figure 6: Singleton lifecycle cost by first-certifying tier on Qwen Frozen Fresh. Each dot is one request; vertical offsets separate overlapping dots, and parenthesized counts sum to 256. Costs include failed tiers. The dashed line marks full-solver cost: requests to its left are cheaper, while the Tier 3 tail extends beyond parity.

Figure 7: Window-level cost on Qwen Frozen Fresh. (a) Median cost reductions; downward whiskers show the protocol-defined 95% bootstrap lower bounds for normalized cost. (b) P95 cascade/full ratio, with parity at one. Amortizing shared acquisition brings the tail below parity from

m=4

onward; per-request search is unchanged. Window sizes are ordered conditions.

Runtime Enforcement for AI Agents

Runtime enforcement for AI agents checks and constrains actions as they execute, helping prevent unsafe or unauthorized effects.

See all 279 papers

Proof of Execution: Runtime Verification for Governed AI Agent Actions
Apr 26, 2026James Rhodes, George KangAI Agent Security Formal Verification
AlphaBitCore, Inc.
ChronoState: Hidden Elapsed-Time Conditioning for Temporal-State Action Selection in Frozen-Backbone Language Models
Aug 10, 2026Sam Siavoshian, Omar Ramadan, Amir K. Saeed +3Temporal Reasoning in Language Models Language Modeling
Independent Researcher, California, USA · Johns Hopkins University, Whiting School of Engineering, Baltimore, MD, USA
Certified Speculative Execution for Untrusted AI Agents
Jun 30, 2026Chenyu Zhou, Qiliang Jiang, Shuning Wu +1AI Agent Reliability Constrained RL
School of Engineering, Institute of Science Tokyo, Japan · College of Control Science and Engineering, Zhejiang University, China · Department of Electrical and Computer Engineering, National University of Singapore, Singapore

Apr 26, 2026J/K move · Enter open · S save

Proof of Execution: Runtime Verification for Governed AI Agent Actions

James Rhodes, George Kang

AlphaBitCore, Inc.

AI Agent Security Formal Verification Runtime Enforcement for AI Agents AI Agent Governance Tamper-Evident Logging Runtime Verification

Open paper AskPDF arXiv

Agent systems increasingly execute rather than advise. When an AI agent queries regulated data, invokes effectful tools, and mutates persistent state, correctness is not captured by whether a terminal output looks plausible. The operative questions are whether each step was authorized under a contract, whether the recorded history is tamper-evident, and whether the trajectory can be reconstructed deterministically. We formalize this as runtime proof of execution. An execution is a triple

x = (C, T, R)

: a contract

C

, an Execution Causal Event Stream (ECES)

T

, and a replay context

R

. A well-formedness predicate and five validator-checkable invariants form the PoE validity predicate. Five semantic guarantees describe authorization, path compliance, null effect on deny, history integrity, and replayability. We prove soundness under explicit cryptographic and deployment assumptions: any PPT adversary that produces a PoE-valid execution violating a semantic guarantee yields a signature forgery, a hash collision, or a quantified deployment-failure event. The Prime Execution Model (PEM) separates planning, enforcement, effect, and recordkeeping into distinct authority planes; a lemma reduces trace completeness to Effector-exclusive credentialing. An Execution Attestation Certificate is issued only when PoE = 1. In a single-node TypeScript prototype, PoE adds approximately 2.7 ms on a minimal flow and 4.4% overhead on concurrent batch workloads; a standard eight-event trace compresses to approximately 1.1 KB; injected Gateway-bypass and trace-mutation attacks are rejected. PoE does not replace consensus, TEEs, or zkVMs; it binds authorization, effect, history, and replay into a single runtime-checkable object so that governed execution becomes attestable under contract.

Abstract

Runtime Enforcement for AI Agents

Explore similar work

Proof of Execution: Runtime Verification for Governed AI Agent Actions

ChronoState: Hidden Elapsed-Time Conditioning for Temporal-State Action Selection in Frozen-Backbone Language Models

Certified Speculative Execution for Untrusted AI Agents