eNNcode: Optimization-Based Analysis of Neural Networks

Abstract

The increasing use of neural networks (NNs) in high-stakes decision-making requires rigorous analysis to ensure safety, fairness, and explainability.

Formal verification tools for neural networks typically focus on determining the satisfiability of properties such as safety or fairness.

However, many fairness and explainability tasks go beyond satisfiability and instead rely on arbitrary optimization objectives.

To address such problems, neural networks are often encoded as mixed-integer linear optimization (MILO) problems with linear objectives.

In practice, these encodings are usually implemented in an ad-hoc manner, limiting comparability across works, reducing transparency, and increasing implementation effort.

We address this gap by introducing eNNcode, a user-friendly PyPI library that converts any piecewise-linear neural network in Open Neural Network Exchange (ONNX) format into a MILO instance.

The library supports arbitrary constraints on input and output nodes, as well as user-defined optimization objectives.

Our experiments show that eNNcode achieves performance comparable to existing libraries, despite its simplicity and ease of use.

Overall, eNNcode facilitates reproducible and standardized optimization-based analysis of neural networks.