Monotone Neural Barrier Certificates

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, 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.