An Inductive Synthesis Framework for Verifiable Reinforcement Learning

1 Introduction

• Neural-network complexity makes direct verification difficult, while common safety analyses omit deployment-environment effects, leaving effective verification an open problem.Source: §1 · p. 1
• The toolchain uses counterexample-guided inductive synthesis to find a simpler deterministic program that approximates a neural policy while satisfying safety constraints.The search is bounded by the control-system specification and deployment-context environment conditions.Source: §1 · pp. 1–2
• A verified program serves as a runtime shield, overriding neural actions that could lead to unsafe states while preserving the neural policy's performance.Verification uses an inductive invariant over the specified infinite-state transition system.Source: §1 · pp. 1–2
• Runtime assurance costs are typically only a few percent compared with running an unproven network without shield support.The paper reports experimental study across a wide range of cyber-physical control systems.Source: §1 · p. 2

2 Motivation and Overview

• The inverted pendulum illustrates a practical control system for which high assurance is desirable despite verification difficulty.The paper names Segway transporters and autonomous drones as representative systems.Source: §2 · p. 2

2.1 State Transition System

• The model uses angle and angular velocity as state, discrete-time transitions under continuous actions, and unsafe states to represent falling.The environment context can add constraints beyond the transition system, such as bounds on pendulum motion.Source: §2.1 · pp. 2–3

2.2 Synthesis, Verification and Shielding

• Synthesis seeks a deterministic program that remains close to its neural oracle while satisfying the environment’s logical safety property.The feasible program space is restricted to programs whose safety can be formally verified.Source: §2.2 · p. 3
• The search runs candidate programs in the environment, collects trajectories, and optimizes their proximity to oracle actions while favoring safety.The procedure samples program parameters iteratively.Source: §2.2 · p. 4
• Verification seeks an inductive invariant containing initial states, excluding unsafe states, and preserved by transitions; counterexamples guide resynthesis when verification fails.For the pendulum example, the discovered invariant separates reachable states from unsafe states.Source: §2.2 · p. 4
• At runtime, the shield lets the neural policy act within the verified boundary and substitutes the deterministic program’s safe action when a proposed transition leaves it.For changed environment constraints, the framework can synthesize and verify a new program and shield without retraining the original network from scratch.Source: §2.2 · pp. 4–5
• 41 unsafe-region entries were prevented, with only 414 of 5,000,000 neural decisions overridden (0.00828%) in the restricted pendulum environment.The evaluation covered 1,000 trajectories of 5,000 simulation steps each.Source: §2.2 · p. 5

3 Problem Setup

• The environment context C models real-valued state variables, continuous actions, initial and unsafe states, policy-dependent transitions, system dynamics, and reward.External disturbances are modeled as bounded nondeterministic values, with bounds assumed estimable at runtime using multivariate normal fitting.Source: §3 · pp. 5–6
• A neural control policy maps an environment state to an action, which changes the rate of change of state variables.The transition relation is parameterized by the deployed policy and represents all allowed state-to-state transitions.Source: §3 · p. 6
• The discrete-time model assumes a fixed time step and a constant action during each interval, and uses Euler’s method to approximate continuous dynamics.Higher-order methods such as Runge-Kutta can compensate when Euler’s method poorly approximates highly nonlinear dynamics.Source: §3 · p. 6
• Reinforcement learning seeks to maximize expected cumulative reward estimated from finite-length simulations of the transition system.The reward is collected along trajectories of the policy in the environment context.Source: §3 · p. 6
• Safety verification asks whether any trajectory from an initial state reaches an unsafe state, unlike reinforcement learning’s finite-length rollouts.The paper identifies the complexity of verifying a neural policy’s long-term safety within a nontrivial environment as a challenge.Source: §3 · p. 6

4.1 Synthesis

• Program sketches define deterministic policies, and synthesis searches for parameters that keep the policy close to the neural oracle while penalizing unsafe states.The search estimates this objective on sampled trajectories encountered in the environment.Source: §4.1 · pp. 6–7

4.2 Verification

• Verification seeks an inductive invariant that contains initial states, is preserved by transitions, and excludes unsafe states; polynomial barrier certificates are one supported form.The invariant is inferred over the synthesized program’s environment transition system.Source: §4.2 · pp. 7–8
• When verification cannot establish safety, CEGIS uses uncovered initial states as counterexamples to synthesize additional policies and invariants until the initial-state space is covered.If a candidate fails, the procedure can shrink the initial-state region considered for synthesis; the algorithm is sound but may not terminate.Source: §4.2 · pp. 8–9
• Theorem 4.2 establishes that the conditional program built from verified policy–invariant pairs is safe because their combined invariant makes unsafe states unreachable.The CEGIS output covers the initial state space with these pairs.Source: §4.2 · p. 9
• In the Duffing-oscillator example, two individually insufficient policies together cover the initial states and form a verified safe program.The combined invariant is φ1 ∨ φ2.Source: §4.2 · p. 9

4.3 Shielding

• At runtime, the shield predicts the next state and intervenes with the verified program when the neural policy would leave the invariant’s safety boundary.The intervention is intended to occur only when necessary.Source: §4.3 · pp. 9–10

5 Experimental Results

• The authors also extended the approach to synthesize deterministic programs that guarantee stability in supplementary material.Source: §5 · p. 10
• In the inverted-pendulum case, the neural controller made 60 unsafe decisions, all prevented by the synthesized program in 65 interventions over 1000 runs.Source: §5 · p. 10
• Direct reinforcement-learning or random-search training failed to find a safe linear pendulum controller under the added action constraint, while neural-oracle-guided synthesis found one.Source: §5 · p. 10
• Across benchmarks, shielded neural policies retained performance while maintaining safety; programmatic policies were less performant, sometimes by a factor of two or more.The table reports experimental results on program synthesis, verification, and shielding.Source: Table 1 · p. 11, §5 · p. 12
• The first five benchmarks had no observed safety violations or performance-affecting interventions, while violations in Quadcopter, Pendulum, and Cartpole were eliminated by shielding.Source: §5 · p. 11
• Oscillator required many interventions because its neural controller repeatedly approached the safety boundary; 74% of interventions prevented unsafe decisions, with the shield trading performance for safety.Source: §5 · pp. 11–12
• Higher-degree invariants generally reduce interventions but increase synthesis and verification time and overhead; a degree-8 Self-Driving shield incurred 26.85% overhead.Source: §5 · p. 12, Table 2 · p. 12
• After environment changes, shields were synthesized faster than retraining; the Cartpole shield took 239 seconds, and the adapted Pendulum shield took 581 seconds.For Cartpole, the changed environment increased pole length by 0.15 meters; the Pendulum mass increased by 0.3 kg.Source: §5 · pp. 12–13, Table 3 · p. 13

6 Related Work

• Unlike whitebox verification and testing that reason over network architecture and may ignore deployment environments, this framework learns a simpler program from the network as an oracle and verifies safety through shielding.Source: §6 · p. 13
• The framework can be incorporated into existing reinforcement-learning methods and can synthesize new shields for legacy models after reasonable environment changes without retraining.Source: §6 · p. 13
• Unlike interpretable-model approaches that verify generated outputs afterward, this method uses CEGIS to synthesize only safe programs and infer invariants that support guarantees for the original neural network.Source: §6 · p. 13
• The approach can synthesize conditional families of linear controllers, whereas a single linear controller was insufficient for safety in the authors’ benchmark experience.Source: §6 · p. 14
• Unlike finite-state shielding and reachability methods limited to about five dimensions, the framework learns symbolic shields for infinite-state systems and focuses on states a learned controller attempts to explore.Source: §6 · p. 14

• The toolchain verifies neural-network control policies within an environment formalized as an infinite-state transition system.Source: §7 · p. 14
• A counterexample-guided synthesis loop searches from a user-given sketch resembling a neural policy oracle for a deterministic program satisfying the safety specification.Source: §7 · p. 14
• At runtime, the deterministic program and learned inductive invariant shield the neural policy, correcting its action only when it can violate the invariant.Source: §7 · p. 14
• Experimental results indicate the approach can realize trustworthy reinforcement-learning systems with low overhead.Source: §7 · p. 14