Monotone Neural Barrier Certificates
Saber Jafarpour, Alireza Nadali, Ashutosh Trivedi, Majid Zamani

TL;DR
This paper introduces a neurosymbolic framework leveraging monotonicity in dynamical systems to efficiently verify safety and synthesize controllers using neural networks with formal guarantees, avoiding traditional high-complexity methods.
Contribution
It proposes a novel approach combining neural networks and symbolic reasoning for safety verification in high-dimensional monotone systems, exploiting monotonicity to reduce complexity.
Findings
Scalable safety verification from simulation data.
Effective synthesis of barrier certificates using monotone neural networks.
Formal safety guarantees without explicit system models.
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,…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
