Learning Oblique Abstractions for the Safety Verification of Oblique DT Policies

Deep Reinforcement Learning (DRL) has shown major success. In safety-critical systems, though, a question mark remains on the safety of policies learned by DRL. In this paper, we consider the verification of classical reach-avoid properties for DRL problems. Our approach is the following: i) Consider Oblique Decision Trees (ODTs) as policies, which are more efficient than axis-aligned DT policies, ii) Learn unions of polytopes as abstractions of the sets reached after $n$ steps for all $n$ till goal is reached (reach-avoid), or as an invariant (pure safety), iii) Verify these candidate abstractions or invariants formally. The main tools we leverage are neurosymbolic architectures encoding ODTs as differentiable neural networks. They have already been shown to generate small ODT policies as efficient as pure Deep RL for Cyber-Physical Systems. The novelty here is to equip them with dedicated loss functions, to learn abstractions and invariants in the form of unions of polytopes. We demonstrate our techniques on \em discrete actions, discrete time environments MountainCar and Quadrotor (reach-avoid) as well as CartPole (safety). The number of polytopes to verify the policy is reduced by 1-2 orders of magnitude compared with using axis-aligned polytopes.