Training with Hard Constraints: Learning Neural Certificates and Controllers for SDEs

TL;DR

This paper introduces two novel neural network training frameworks that ensure hard constraints for stochastic differential equations, enabling scalable and guaranteed synthesis of certificates and controllers for high-dimensional systems.

Contribution

It presents two constraint-driven training methods for neural certificates in SDEs, with guarantees and scalability to high-dimensional systems.

Findings

Bound-based method scales up to 5D, outperforming existing methods.

Scenario-based method scales to at least 10D with high-confidence guarantees.

Both methods provide formal guarantees for certificate constraint satisfaction.

Abstract

Due to their expressive power, neural networks (NNs) are promising templates for functional optimization problems, particularly for reach-avoid certificate generation for systems governed by stochastic differential equations (SDEs). However, ensuring hard-constraint satisfaction remains a major challenge. In this work, we propose two constraint-driven training frameworks with guarantees for supermartingale-based neural certificate construction and controller synthesis for SDEs. The first approach enforces certificate inequalities via domain discretization and a bound-based loss, guaranteeing global validity once the loss reaches zero. We show that this method also enables joint NN controller-certificate synthesis with hard guarantees. For high-dimensional systems where discretization becomes prohibitive, we introduce a partition-free, scenario-based training method that provides arbitrarily tight PAC guarantees for certificate constraint satisfaction. Benchmarks demonstrate scalability of the bound-based method up to 5D, outperforming the state of the art, and scalability of the scenario-based approach to at least 10D with high-confidence guarantees.