Skip to content

Generator-Independent Runtime Assurance under Partial Observation

Sep 2026 · 1 citation · 23 references
Computer Science

TL;DR

This work shows that the closed-loop safety guarantee decouples from the generator is necessary and sufficient for generator-independent admission soundness, and bounds every admission mechanism under partial observation.

Abstract

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 $\alpha$ can inflate to $1-(1-\alpha)^{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 $\Gamma+\sum_t\varepsilon_t+\eta$ 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 $\delta$ require different safe decisions, then $\abar+\beta+\delta\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.

View source

Similar papers

#artificial intelligence Preprint Oct 2026

Certifying Almost-Sure Reachability in Unknown MDPs

{\em Specification-Guided Reinforcement Learning (RL)} has largely concerned itself with \emph{learning} an optimal policy against a formal specification in an unknown {\em Markov Decision Process (MDP)}. We take up the dual question. Given a policy already in hand, can one \emph{verify} that it is correct against a fo...

S. Akshay, Suguman Bansal, Gaurav Mahla · 0 citations
#artificial intelligence Review Oct 2026

SCOPE: Certified Theorem Proving with a Language Model as the Policy Planner

In proof assistants such as Lean, a generated proof must pass machine compilation checks, so evaluation needs no human scoring. Direct generation fails on multi-step numeric propositions: a proof is valid only if every content integer is correct, so the pass rate is bounded by the k-th power of the per-integer accuracy...

Han Zhou, Jia-Le Li · 0 citations
Preprint Sep 2026

Efficient Branch-and-Bound Testing and Verification of zkVMs

ZEBRA is a fully automated verification and bug-detection framework that reduces zkVM verification to a solution-set cardinality problem over a canonical trace space, where redundancies such as null-row padding and non-deterministic permutations are eliminated prior to counting.

Hideaki Takahashi, Suman Jana, Junfeng Yang · 0 citations
#artificial intelligence Preprint Sep 2026

AI Harness: Certification under Proposal-Conditioned Information for Foundation-Model Agents

The contribution is not a new fixed-point calculus, but a characterization of when proposal--history correlation at the model--tool boundary is necessary for certification, separating indefinite operational viability from finite worst-case verified progress.

Hai-Lin Zhong, Sheng-Xin Zhu · 0 citations

Related blog posts

We use cookies to run the site and, with your consent, for analytics and to show ads. See our Cookie Policy.