# Formal Control Synthesis for Stochastic Neural Network Dynamic Models

arXiv: https://arxiv.org/abs/2203.05903 · HTML: https://mlsanity.com/paper/2203.05903/

## Key facts

- Cited by 7 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 11 Mar 2022.

## Built on by (most cited first, 7 of 7)

- [Adversarial Robustness Certification for Bayesian Neural Networks](https://mlsanity.com/paper/2306.13614/) (2023)
- [Probabilistic Reach-Avoid for Bayesian Neural Networks](https://mlsanity.com/paper/2310.01951/) (2023)
- [Promises of Deep Kernel Learning for Control Synthesis](https://mlsanity.com/paper/2309.06569/) (2023)
- [Efficient Certified Training and Robustness Verification of Neural ODEs](https://mlsanity.com/paper/2303.05246/) (2023)
- [Data-Driven Abstractions via Binary-Tree Gaussian Processes for Formal Verification](https://mlsanity.com/paper/2407.21029/) (2024)
- [Learning-Based Shielding for Safe Autonomy under Unknown Dynamics](https://mlsanity.com/paper/2410.07359/) (2024)
- [Towards Global Neural Network Abstractions with Locally-Exact Reconstruction](https://mlsanity.com/paper/2210.12054/) (2022)

## Abstract (arXiv)

Neural networks (NNs) are emerging as powerful tools to represent the dynamics of control systems with complicated physics or black-box components. Due to complexity of NNs, however, existing methods are unable to synthesize complex behaviors with guarantees for NN dynamic models (NNDMs). This work introduces a control synthesis framework for stochastic NNDMs with performance guarantees. The focus is on specifications expressed in linear temporal logic interpreted over finite traces (LTLf), and the approach is based on finite abstraction. Specifically, we leverage recent techniques for convex relaxation of NNs to formally abstract a NNDM into an interval Markov decision process (IMDP). Then, a strategy that maximizes the probability of satisfying a given specification is synthesized over the IMDP and mapped back to the underlying NNDM. We show that the process of abstracting NNDMs to IMDPs reduces to a set of convex optimization problems, hence guaranteeing efficiency. We also present an adaptive refinement procedure that makes the framework scalable. On several case studies, we illustrate the our framework is able to provide non-trivial guarantees of correctness for NNDMs with architectures of up to 5 hidden layers and hundreds of neurons per layer.