Affine Multiplexing Networks: System Analysis, Learning, and Computation

TL;DR

This paper introduces affine multiplexing networks (AMNs), a new computational framework for analyzing complex systems with nonlinear feedback, enabling formal verification of properties like stability and robustness using SMT and optimization techniques.

Contribution

The paper presents a novel architecture called affine multiplexing networks that encode nonlinear systems into SMT and optimization problems for systematic analysis and verification.

Findings

Able to verify stability and robustness of nonlinear systems with neural networks.

Framework translates system properties into SMT, MIP, and convex optimization problems.

Demonstrates verification of closed-loop systems with neural network components.

Abstract

We introduce a novel architecture and computational framework for formal, automated analysis of systems with a broad set of nonlinearities in the feedback loop, such as neural networks, vision controllers, switched systems, and even simple programs. We call this computational structure an affine multiplexing network (AMN). The architecture is based on interconnections of two basic conceptual building blocks: multiplexers ($\mu$), and affine transformations ($\alpha$). When attached together appropriately, these building blocks translate to conjunctions and disjunctions of affine statements, resulting in an encoding of the network into satisfiability modulo theory (SMT), mixed integer programming, and sequential convex optimization solvers. We show how to formulate and verify system properties like stability and robustness, how to compute margins, and how to verify performance through a sequence of SMT queries. As illustration, we use the framework to verify closed loop, possibly nonlinear dynamical systems that contain neural networks in the loop, and hint at a number of extensions that can make AMNs a potent playground for interfacing between machine learning, control, convex and nonconvex optimization, and formal methods.