BURNS computes sound underapproximate backward reachable sets for discrete-time nonlinear neural feedback loops using mixed-integer linear programming, enabling goal-reaching verification.
Verifying Inverse Model Neural Networks
1 Pith paper cite this work. Polarity classification is still indexing.
abstract
Inverse problems exist in a wide variety of physical domains from aerospace engineering to medical imaging. The goal is to infer the underlying state from a set of observations. When the forward model that produced the observations is nonlinear and stochastic, solving the inverse problem is very challenging. Neural networks are an appealing solution for solving inverse problems as they can be trained from noisy data and once trained are computationally efficient to run. However, inverse model neural networks do not have guarantees of correctness built-in, which makes them unreliable for use in safety and accuracy-critical contexts. In this work we introduce a method for verifying the correctness of inverse model neural networks. Our approach is to overapproximate a nonlinear, stochastic forward model with piecewise linear constraints and encode both the overapproximate forward model and the neural network inverse model as a mixed-integer program. We demonstrate this verification procedure on a real-world airplane fuel gauge case study. The ability to verify and consequently trust inverse model neural networks allows their use in a wide variety of contexts, from aerospace to medicine.
fields
cs.AI 1years
2025 1verdicts
CONDITIONAL 1representative citing papers
citing papers explorer
-
BURNS: Backward Underapproximate Reachability for Neural-Feedback-Loop Systems
BURNS computes sound underapproximate backward reachable sets for discrete-time nonlinear neural feedback loops using mixed-integer linear programming, enabling goal-reaching verification.