Learning State-Dependent Reach-Avoid Bounds with PAC Guarantees

Learned control policies can succeed on average yet fail from particular initial states. Existing reach-avoid certificates either require a model of the dynamics with Lipschitz bounds and a grid over the state space, or certify a single success probability. We introduce Reach-Avoid Probability Certification (RAPC), which learns a function $q(x)$ that lower-bounds the probability that a policy started at $x$ reaches a target before an unsafe set, and certifies it from simulator rollouts alone. With probability at least $1-\delta$ over learning and certification, a returned $q$ overstates the true success probability only on initial states of total probability at most $ϵ$, even when the policy and bound are updated adaptively. The key step links an unobservable event, an overstated bound at a start, to an observable one: a failed binomial confidence check on repeated rollouts from that start. Calibrating $q$ to these confidence limits gives a learner-independent lower bound on its acceptance probability and, for a fixed calibration pipeline, certifies $q$ without a separate validation batch. On a 12-dimensional Hopper environment and a PointGoal environment with 44-dimensional observations, RAPC certifies bounds in all ten seeds of each task. On a wider Hopper start distribution, the learned bound averages $0.82$ over ten seeds, against $0.51$ for the largest constant accepted by the same test. We release our code at https://anonymous.4open.science/r/iclr-pac-BBBD/.