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

1. Problem Statement

The paper addresses the challenge of reach-avoid control for continuous-time, continuous-space stochastic systems governed by Stochastic Differential Equations (SDEs).

• Goal: Ensure that a system starting in an initial set ($X_0$) reaches a goal set ($X_g$) while avoiding an unsafe set ($X_u$) with a guaranteed probability ($P_{RA} \geq p_{RA}$).
• Theoretical Basis: The problem is framed using supermartingale theory. A "certificate" function $V(x)$ must satisfy specific inequalities (non-negativity, boundary conditions, and a negative infinitesimal generator condition) to mathematically guarantee the reach-avoid probability.
• Core Challenge: While Neural Networks (NNs) are expressive enough to approximate these certificate functions, enforcing the required hard constraints (inequalities holding over the entire continuous domain) during training is difficult. Existing methods either rely on soft penalties (no guarantees), post-training verification (scalability issues), or restrictive assumptions (e.g., linear dynamics).
• Objectives:
  1. Learn a neural certificate $V_\theta$ that satisfies hard constraints for a given controller.
  2. Jointly synthesize a neural controller $\pi_\theta$ and a certificate $V_\theta$ to guide the controller toward certifiable behavior.

2. Methodology

The authors propose two complementary training frameworks to enforce hard constraints directly during the learning process.

Approach A: Bound-Training (Hard-SAT)

This method provides deterministic, hard guarantees by discretizing the state space.

• Mechanism:
  • The domain is partitioned into cells ($Q$).
  • Using Interval Bound Propagation (IBP), the method computes rigorous upper and lower bounds for the certificate $V_\theta$ and its infinitesimal generator $G[V_\theta]$ over each cell.
  • A bound-based loss function is constructed. This loss aggregates the worst-case violations of the certificate inequalities across all cells.
  • Key Guarantee: If the loss reaches zero, the constraints are satisfied globally over the entire domain, not just at sampled points.
• Optimization Strategies:
  • Adaptive Refinement: Cells violating constraints are split to tighten bounds.
  • Merging: Cells that comfortably satisfy constraints are merged to prevent exponential growth in the number of partitions.
  • Joint Synthesis: The framework extends to joint training by backpropagating through a differentiable computation graph derived from the closed-loop SDE dynamics, updating both controller and certificate parameters simultaneously.
• Limitation: Scalability is limited by the "curse of dimensionality" due to state-space partitioning (practical up to ~5D).

Approach B: Scenario-Based Training (PAC Guarantees)

This method addresses high-dimensional systems where partitioning is infeasible, providing Probably Approximately Correct (PAC) guarantees.

• Mechanism:
  • Instead of partitioning, the method samples a finite set of states $\hat{X}$ from the domain.
  • It formulates a convex scenario optimization problem (specifically a Linear Program) focusing only on the last-layer weights of the neural certificate.
  • The constraints are enforced only on the sampled points.
• Theoretical Guarantee: Based on convex scenario theory, if the number of samples $N$ is sufficiently large ($N \propto \frac{1}{\epsilon} \log(1/\delta)$), the synthesized certificate satisfies the constraints everywhere except on a set of measure $\leq \epsilon$, with confidence $1-\delta$.
• Advantage: Sample complexity is independent of the state dimension, allowing scalability to 10D and beyond.

3. Key Contributions

1. Hard-SAT Framework: A novel bound-training approach that encodes hard constraints into NN training via domain discretization and interval arithmetic, guaranteeing global validity once the loss is zero.
2. Joint Synthesis: An extension of the bound-training framework to jointly learn neural controllers and certificates, using a unified loss that couples task performance with formal verification.
3. Scalable PAC Training: A partition-free, scenario-based training method that scales to high-dimensional SDEs (10D+) with arbitrarily tight PAC guarantees by optimizing only the last layer of the network.
4. Empirical Validation: Comprehensive benchmarks demonstrating superior scalability and performance compared to state-of-the-art methods (e.g., Neustroev et al., 2025).

4. Experimental Results

The authors evaluated their methods on several benchmarks, including Inverted Pendulums, Geometric Brownian Motion (GBM), Lorenz systems, and an XV-15 Tilt-Rotor aircraft.

• Verification (Problem 1):

  • Hard-SAT: Successfully verified systems up to 5D. It required significantly fewer partitions and less time than the state-of-the-art (Neustroev et al.) for 2D/3D systems and succeeded where others failed for higher dimensions.
  • Scenario-Based: Scaled effortlessly to 10D systems. With $N=10^6$ samples, it achieved $P_{RA} \approx 1$ with a violation measure $\epsilon$ as low as $10^{-4}$ at a confidence level of $1-10^{-9}$.
  • Ablation: Pre-training alone (soft constraints) failed to produce valid certificates; the final hard-constraint optimization step was essential.

• Joint Synthesis (Problem 2):

  • Successfully synthesized controllers for 2D, 3D, and complex 3D aircraft dynamics.
  • In all cases, the synthesized controllers achieved an empirical reach-avoid probability of 1.0 in Monte Carlo simulations.
  • The method guided the controller away from unsafe regions (e.g., preventing the pendulum from falling or the aircraft from stalling) more effectively than sample-trained baselines.

5. Significance and Impact

• Bridging the Gap: This work bridges the gap between the expressiveness of deep learning and the rigor of formal verification for stochastic systems. It moves beyond "soft" constraints that only work on training data to provide mathematical guarantees for safety-critical applications.
• Scalability: By introducing a scenario-based approach for high dimensions, the paper overcomes the primary bottleneck (curse of dimensionality) that has historically limited formal verification of neural controllers in stochastic environments.
• Practical Applicability: The ability to jointly synthesize controllers and certificates reduces the trial-and-error nature of safety-critical control design, offering a principled path to deploying neural controllers in real-world stochastic systems (e.g., autonomous aviation, robotics).
• Open Source: The authors provide code on GitHub, facilitating reproducibility and further research in certified neural control.