Monotone Neural Barrier Certificates
Saber Jafarpour, Alireza Nadali, Ashutosh Trivedi, Majid Zamani
TL;DR
The paper addresses safety verification and safe control synthesis for high-dimensional discrete-time monotone systems with unknown dynamics. It introduces a neurosymbolic framework that learns barrier certificates as monotone neural networks and leverages monotonicity to reduce verification to boundary checks, using data from simulations. The method avoids explicit models, Lipschitz bounds, or semidefinite relaxations, delivering scalable, formally sound guarantees. This provides a practical path for deploying high-assurance control in complex systems where monotone structure is intrinsic.
Abstract
This report presents a neurosymbolic framework for safety verification and control synthesis in high-dimensional monotone dynamical systems without relying on explicit models or conservative Lipschitz bounds. The approach combines the expressiveness of neural networks with the rigor of symbolic reasoning via barrier certificates, functional analogs of inductive invariants that formally guarantee safety. Prior data-driven methods often treat dynamics as black-box models, relying on dense state-space discretization or Lipschitz overapproximations, leading to exponential sample complexity. In contrast, monotonicity--a pervasive structural property in many real-world systems--provides a symbolic scaffold that simplifies both learning and verification. Exploiting order preservation reduces verification to localized boundary checks, transforming a high-dimensional problem into a tractable, low-dimensional one. Barrier certificates are synthesized using monotone neural network architectures with embedded monotonicity constraints--trained via gradient-based optimization guided by barrier conditions. This enables scalable, formally sound verification directly from simulation data, bridging black-box learning and formal guarantees within a unified neurosymbolic framework.