Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Chun-Wei Kong, Sebastian Escobar, Ibon Gracia, Jay McMahon, Morteza Lahijanian

TL;DR

This work proposes two constraint-driven training frameworks with guarantees for supermartingale-based neural certificate construction and controller synthesis for SDEs, and introduces a partition-free, scenario-based training method that provides arbitrarily tight PAC 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.

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

TL;DR

This work proposes two constraint-driven training frameworks with guarantees for supermartingale-based neural certificate construction and controller synthesis for SDEs, and introduces a partition-free, scenario-based training method that provides arbitrarily tight PAC 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.
Paper Structure (36 sections, 4 theorems, 39 equations, 5 figures, 8 tables, 1 algorithm)

This paper contains 36 sections, 4 theorems, 39 equations, 5 figures, 8 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Related Work
  3. Problem Formulation
  4. Training with Hard Constraints
  5. Bound-Training for Hard Guarantees
  6. Bounding $\mathcal{G}[V_{\theta}]$
  7. Adaptive refinement and merging
  8. Hard-SAT Algorithm for Neural Certificate and Controller Synthesis
  9. Limitations of Hard-SAT Algorithm
  10. Scenario-based Training for PAC Guarantees
  11. Experiments
  12. Verification
  13. Joint controller-certificate synthesis
  14. Conclusion
  15. Derivation of analytical $\mathcal{G}[V]$
  16. ...and 21 more sections

Key Result

theorem 1

Consider System eq:sde under controller $\pi \in \Pi$, the corresponding infinitesimal generator and the sets $X$, $X_\mathrm{0}$, $X_\mathrm{g}$, and $X_\mathrm{u}$ in Definition def:ra_spec. If there exists a twice continuously differentiable function $V:X\rightarrow \mathbb{R}$ and scalar $\beta > 0$ such that then $V$ is called a reach-avoid certificate, guaranteeing it holds that $\mathrm{P

Figures (5)

  • Figure 1: 2D GBM synthesis: (a) $V_{\theta}$, (b) $\mathcal{G}[V_{\theta}]$, (c) trajectories (controlled vs. uncontrolled).
  • Figure 2: 2D GBM synthesis: (a) Cell partition at the end of warm-start training, before bound training; (b) Cell partition after 4000 epochs of bound training, shortly before achieving SAT.
  • Figure 3: Stochastic inverted pendulum synthesis: angle snapshots (left), phase-plane trajectories overlaid on $V_{\theta}$ (middle), and torque inputs (right), comparing controlled and uncontrolled rollouts.
  • Figure 4: Lorenz synthesis: 3D trajectories (left) and 2D projections on $V_{\theta}$ contours (right), controlled vs. uncontrolled.
  • Figure 5: XV15 aircraft synthesis: phase trajectories (left), longitudinal position (middle), and control inputs (right), comparing trim, sample-trained, and synthesized controllers.

Theorems & Definitions (11)

  • Definition 1: Reach-Avoid Probability
  • theorem 1: Reach-Avoid Certificate neustroev2025neural
  • Remark 1
  • Definition 2: Bound-based loss function
  • theorem 2: Constraint Satisfaction Guarantees
  • proof
  • theorem 3
  • Remark 2
  • theorem 4
  • proof
  • ...and 1 more