Source-linked AI summary
Generator-Independent Runtime Assurance under Partial Observation
Guangxi Wan, Yongbo Xie, Yuqi Liu, Qingwei Dong, Qingxin Li, Hongfei Bai, Peng Zeng
TL;DR
The paper asks when runtime assurance can remain safe as black-box proposal generators change, given that per-candidate certification fails under selection. It develops setwise certification, partial-observation limits, and a sequential risk ledger, showing when safety is generator-independent and where statistical risk must be charged.
Problem
Per-candidate certification can fail under retry and best-of-k selection, so the paper asks when a runtime gate can support safety independently of the proposal generator.
Method
The paper analyzes simultaneous setwise soundness, a design-time certificate, partial-observation distinguishability, and a sequential risk ledger for runtime admission.
Results
Setwise soundness is necessary and sufficient for generator-independent admission soundness and, with the design-time certificate, sufficient for generator-independent contract safety.
Takeaways & Limitations
Safety can remain attached to the gate through arbitrary generator replacement when the certified triple is unchanged, while deterministic admission shifts statistical risk to state estimation.
Takeaways & Limitations
Theorem 1's contract-safety result is only sufficient, and the hard-safety disposition taxonomy is not exhaustive under chance-constrained or risk-budget semantics.
Abstract
from arXiv · showhide
Proposal-based controllers---learned policies, language-model planners, and other black-box \emph{generators}---are increasingly deployed behind runtime verification gates. We ask when the closed-loop safety guarantee decouples from the generator. The prevailing per-candidate certification pattern does not compose: under retry or best-of-$k$ selection a per-candidate false-admission level $α$ can inflate to $1-(1-α)^{k}$. Our main theorem shows that \emph{simultaneous setwise soundness}---certifying a set of admissible proposals containing no nonviable action---is necessary and sufficient for generator-independent \emph{admission soundness}, the worst case over all generators of executing a nonviable proposal equalling the probability of setwise failure; together with a design-time certificate and a no-bypass rule it is sufficient for \emph{contract safety}, with violation bound $Γ+\sum_t\varepsilon_t+η$ invariant under arbitrary, even adversarial, replacement of the generator. A second theorem bounds every admission mechanism under partial observation: for a fixed probing and admission policy, if two state hypotheses whose information laws lie within total-variation distance $δ$ require different safe decisions, then $\abar+β+δ\ge1$. A sequential risk ledger makes the guarantee implementable with time-uniform confidence tubes, and shows that deterministic admission computations concentrate all statistical risk in state estimation. Simplex-style runtime assurance and control-barrier-function filtering are recovered as degenerate cases.
1 Introduction
Runtime assurance aims to make safety depend on the verification gate rather than an evolving proposal generator, but per-candidate certification fails under selection. The paper identifies setwise certification as the generator-independent remedy and characterizes limits imposed by partial observation.
- Architecture: Runtime assurance places unverified generators behind gates that admit, modify, or reject proposals and transfer rejected actions to certified fallbacks.This architecture includes Simplex-style runtime assurance, shielding, and related safety-filtering patterns.
- Motivation: Per-candidate false-admission guarantees do not remain generator-level guarantees when retry or best-of-k selection is unrestricted.Selection changes the quantity realized by the closed loop from the quantity calibrated for each candidate.
- Contributions: Simultaneous setwise soundness certifies an admissible proposal set containing no nonviable action and is the exact object supporting generator-independent admission soundness.The result is necessary and sufficient for admission soundness, while contract-safety sufficiency additionally requires a design-time certificate.
- Implications: The safety guarantee attaches to the certified gate and remains valid under retraining, fine-tuning, or arbitrary generator replacement when the certified triple is unchanged.The generator may affect abstention frequency and task success, but not the stated safety bound.
- Contributions: Theorem 2 gives the partial-observation obstruction ¯α + β + δ ≥1 when nearby information laws correspond to state hypotheses requiring different safe decisions.The bound is model-free and applies to fixed probing and admission policies.
- Implementation: A sequential risk ledger separates estimation risk from admission-computation risk and makes deterministic admission computations contribute εt ≡0.The implementation uses conditional and horizon-uniform forms, with statistical risk concentrated in state estimation when admission is deterministic.
- Connections: Simplex-style runtime assurance and control-barrier-function filtering appear as degenerate or related instances of the setwise framework.Under partial observation, measurement-robust filtering remains subject to the impossibility bound.
- Related work: The framework connects its partial-observation converse to observability and selective-inference ideas while replacing exact indistinguishability with quantitative error levels.The paper emphasizes a model-free price δ for partial distinguishability.
2 Problem Formulation
The formulation models contracts, viability, observations, generators, and certified execution over a finite horizon. It explicitly separates verifier-observable information from latent physical history and states the certificate and measurability conditions used by the theorems.
- 2.1 Plant, contract, and viability: The state evolves as a controlled Markov process, while a contract violation occurs if φ(xt) = 1 at any time in the horizon.Actions may be proposals or engagements of a separately certified fallback mode.
- 2.1 Plant, contract, and viability: The viability map Aviable(x) contains proposal actions that preserve the contract and fallback feasibility at state x.Its computation and associated design-time certificates are outside the paper's scope.
- 2.2 Information structure: Ht contains verifier-observable history before admission, including observations, past actions, fallback engagements, certified sets, and verifier randomization.The verifier may choose probing excitations adaptively using this observable history.
- 2.2 Information structure: The latent state is generally Ft-measurable but not Ht-measurable, so verifier risk statements are conditioned on pre-computation information rather than full physical history.The distinction prevents conditioning realized outputs on information that already determines them.
- 2.2 Information structure: A verifier outputs an Ht-measurable certified set, with the empty set encoding abstention; deterministic verifiers use no fresh admission randomization.The certified set is the object passed to the execution rule.
- 2.3 Generators and the execution rule: Generators may inspect latent states, realized noise, and certified sets, coordinate across time, and thereby subsume retrying, best-of-k selection, distribution shift, and adversarial behavior.Uniform guarantees over this class are therefore stronger than guarantees for realistic generators.
- 2.3 Generators and the execution rule: The no-bypass assumption requires the executed action to pass through the certified set or fallback, with no other generator channel to the actuator.The certified set cannot depend on generator content beyond information already in the verifier history.
- 2.4 Certificate and regularity: Setwise failure records when the certified set contains a nonviable action, while admissible execution requires either a viable proposal or fallback engagement after a certified prefix.The design-time certificate then makes every admissible execution contract-safe on its certificate-valid event.
3 Generator–Guarantee Separation
Theorem 1 identifies simultaneous setwise soundness as the exact condition for generator-independent admission soundness, while contract safety additionally requires a design-time certificate and no-bypass rule. Under these safeguards, generator replacement affects performance but not the safety bound.
- Theorem 1(a): A level-ᾱ_t generator-independent bound on executed nonviable proposals holds if and only if the verifier is setwise sound at level ᾱ_t.The characterization takes the essential supremum over stage-t selectors with the past strategy fixed.
- Theorem 1(b): Setwise soundness, a design-time certificate, and no bypass compose across the horizon to yield generator-independent contract safety.The horizon result uses one-step setwise risk bounds together with the stated safeguards.
- Theorem 1(b): The resulting safety bound is unchanged under arbitrary, adversarial, or mid-run generator replacement.Replacement changes history distributions, but the conditional bounds remain uniform over generators and histories.
- Proof structure: Fallback engagements are treated as a certified recovery mode rather than proposals, keeping executed-proposal risk separate from design-time fallback safety.This separation makes the one-step identity unconditional because the generator can inject harm only through the proposal channel.
- Why safeguards matter: Per-candidate calibration can inflate under selection, because it measures individual admissions rather than the setwise event that every admitted proposal is viable.The example gives setwise failure probability 1 − (1 − α)^n despite per-candidate level α.
- Guarantee–performance split: The generator determines abstention and fallback frequency, not the safety guarantee, provided setwise soundness remains uniform over generator-supplied content.Direct actuator bypasses are excluded; without this channel restriction, the guarantee can fail.
4 Impossibility under Partial Observation
Theorem 2 establishes an informational obstruction to safe admission under partial observation: when distinct safe decisions correspond to nearby information laws, reliability and usefulness must trade off. The obstruction is mechanism-wide, while safety can still come from design-time exclusion or actions safe across all ambiguous states.
- Interpretation: The impossibility applies to every admission mechanism because the proof uses only information-law proximity and the two operational levels.It is not a limitation specific to a particular estimator or observation model.
- Theorem 2: For a fixed probing and admission policy, if two hypotheses require different safe decisions and their information laws are within total variation δ, then ᾱ + β + δ ≥ 1.Here ᾱ is statewise setwise risk, while 1 − β is required usefulness.
- Uniform version: When hypotheses are observationally equivalent, reliability and usefulness cannot both be high at any observation budget or under any policy.The uniform corollary gives ᾱπ + βπ ≥ 1 when δT = 0.
- Observation limits: In linear-Gaussian observations, adaptivity contributes at most a T factor and cannot create distinguishability absent from the observation maps.Theorem 2 itself is model-free and does not require linear or Gaussian observations.
- Interpretation: Partial distinguishability permits only a proportional relaxation: δ buys no more than its corresponding reduction in the incompatibility bound.The result does not prohibit safe operation when design-time reachability removes ambiguous unsafe hypotheses or when admitted actions are viable under every ambiguity.
5 Statistical Implementation
The statistical implementation uses confidence-reachable tubes and a sequential risk ledger to produce generator-uniform one-step bounds. Deterministic admission makes the admission computation risk-free, concentrating statistical uncertainty in state estimation.
- Confidence tubes: The implementation requires joint, time-uniform, and generator-uniform confidence guarantees for the state tube.Per-coordinate intervals do not provide joint coverage; confidence sequences provide a single horizon-wide Γ and tolerate adaptive monitoring and stopping.
- Set construction: The common admissible set contains proposals viable at every state remaining in the confidence tube.Intersecting the tube with the certified reachable set supplies the deterministic pruning component of the certificate.
- Risk ledger: The sequential ledger combines tube risk γt and admission-computation risk εt into one-step setwise bounds ᾱt = γt + εt.These bounds feed the horizon composition theorem uniformly over generators.
- Risk ledger: Pathwise containment of the certified proposal set in the common admissible set implies viability whenever the true state lies in the tube.The argument is generator-independent because it holds for every generator pathwise.
- Risk accounting: Conditioning must follow the decision cycle: tube validity is assessed before admission, while εt concerns admission computation under its own randomization.Conditioning εt on the post-admission history would make the statement vacuous.
- Deterministic admission: With deterministic, pre-admission containment checking, εt ≡ 0 and all statistical risk is concentrated in the state confidence tube.Containment checking, constraint tightening, and projection can discharge the admission requirement as a design obligation.
6 Consequences and Degenerate Cases
Observation quality affects conservatism rather than safety within this architecture, while unresolved ambiguity has three hard-semantics dispositions. Simplex and CBF filtering appear as special cases of the setwise framework.
- Conservatism: A tighter confidence tube weakly enlarges the certifiable proposal set and can reduce conservatism without weakening safety.The paper defers the quantitative relation between tube geometry, admissible-set erosion, and excitation design to companion work.
- Operational taxonomy: Under hard worst-case semantics, ambiguous hypotheses are handled by design-time pruning, actions viable across all unresolved hypotheses, or transfer to the certified fallback.These dispositions exhaust the set-based cases considered by the paper.
- Operational taxonomy: The operational taxonomy is not exhaustive under chance-constrained or risk-budget semantics that deliberately accept bounded risk.The scope limitation applies to the stated hard worst-case admission semantics.
- Degenerate cases: Simplex is recovered with one candidate per step, full-state observation, deterministic switching, and zero admission-computation risk.Under these conditions, the sequential proposition reduces to the classical guarantee P ≤ η.
- Degenerate cases: CBF-QP filtering is selection-robust under full-state, correct-model conditions because its constraint set acts as a certified admissible set.Under partial observation, the guarantee requires measurement-robust variants.
7 Discussion
The discussion positions setwise soundness as the condition that keeps admission guarantees independent of generator changes, while partial observation imposes an unavoidable risk–usefulness trade-off. It also delineates the theory’s architectural scope and assigns statistical risk primarily to estimation.
- Generator independence: Setwise soundness is necessary and sufficient for generator-independent admission soundness, and with a design-time certificate it also supports generator-independent contract safety.The generator may be retrained, fine-tuned, replaced, or adversarially retry proposals without a new safety argument when the certified triple remains unchanged.
- Generator independence: Per-candidate statistical screening is not a gate because unrestricted selection can invalidate its nominal generator-level error guarantee.The discussion identifies this as a warning about a certification pattern used for sampled actions.
- Partial observation: The admission layer faces an information-theoretic limit: hypotheses requiring different decisions cannot be reliably distinguished when their observation laws are too similar.The paper prices this ambiguity, prunes it at design time, or uses common-feasible proposal sets.
- Risk allocation: Deterministic admission computation contributes no statistical risk to the ledger; estimation governs Γ, while design-time verification governs η and pruning.This division concentrates the statistical burden in state estimation rather than runtime admission computation.
- Scope: The theory is architectural and bounded to a single-gate setting, while observation requirements, certifiability thresholds, adaptive excitation, and multi-gate coupling remain outside its scope.The paper also leaves the production of viable-action sets and design-time certificates unspecified.