# Safe-by-Repair: A Convex Optimization Approach for Repairing Unsafe Two-Level Lattice Neural Network Controllers

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

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- Builds on 5 of its 14 references that are in the map.
- First posted on arXiv 6 Apr 2021.

## Builds on (most cited first, 5 of 5)

- [NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems](https://mlsanity.com/paper/2004.05519/) (2020)
- [Towards Repairing Neural Networks Correctly](https://mlsanity.com/paper/2012.01872/) (2020)
- [AReN: Assured ReLU NN Architecture for Model Predictive Control of LTI Systems](https://mlsanity.com/paper/1911.01608/) (2019)
- [Bounding the Complexity of Formally Verifying Neural Networks: A Geometric Approach](https://mlsanity.com/paper/2012.11761/) (2020)
- [Towards Neural Network Patching: Evaluating Engagement-Layers and Patch-Architectures](https://mlsanity.com/paper/1812.03468/) (2018)

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

- [NNLander-VeriF: A Neural Network Formal Verification Framework for Vision-Based Autonomous Aircraft Landing](https://mlsanity.com/paper/2203.15841/) (2022)
- [Fast BATLLNN: Fast Box Analysis of Two-Level Lattice Neural Networks](https://mlsanity.com/paper/2111.09293/) (2021)
- [Constrained Feedforward Neural Network Training via Reachability Analysis](https://mlsanity.com/paper/2107.07696/) (2021)
- [Local Repair of Neural Networks Using Optimization](https://mlsanity.com/paper/2109.14041/) (2021)
- [Polynomial-Time Reachability for LTI Systems with Two-Level Lattice Neural Network Controllers](https://mlsanity.com/paper/2209.09400/) (2022)
- [Causal Repair of Learning-enabled Cyber-physical Systems](https://mlsanity.com/paper/2304.02813/) (2023)

## Abstract (arXiv)

In this paper, we consider the problem of repairing a data-trained Rectified Linear Unit (ReLU) Neural Network (NN) controller for a discrete-time, input-affine system. That is we assume that such a NN controller is available, and we seek to repair unsafe closed-loop behavior at one known "counterexample" state while simultaneously preserving a notion of safe closed-loop behavior on a separate, verified set of states. To this end, we further assume that the NN controller has a Two-Level Lattice (TLL) architecture, and exhibit an algorithm that can systematically and efficiently repair such an network. Facilitated by this choice, our approach uses the unique semantics of the TLL architecture to divide the repair problem into two significantly decoupled sub-problems, one of which is concerned with repairing the un-safe counterexample -- and hence is essentially of local scope -- and the other of which ensures that the repairs are realized in the output of the network -- and hence is essentially of global scope. We then show that one set of sufficient conditions for solving each these sub-problems can be cast as a convex feasibility problem, and this allows us to formulate the TLL repair problem as two separate, but significantly decoupled, convex optimization problems. Finally, we evaluate our algorithm on a TLL controller on a simple dynamical model of a four-wheel-car.