Formalizing Piecewise Affine Activation Functions of Neural Networks in Coq

TL;DR

This paper formalizes piecewise affine activation functions like ReLU within Coq, enabling verified neural network representations and proof automation for neural network verification tasks.

Contribution

It provides the first formalization of pwa activation functions in Coq, including a verified transformation from neural networks to pwa functions for verification purposes.

Findings

Successfully formalized ReLU in Coq.

Developed a verified transformation from neural networks to pwa functions.

Enabled proof automation using Coq tactics like lra.

Abstract

Verification of neural networks relies on activation functions being piecewise affine (pwa) -- enabling an encoding of the verification problem for theorem provers. In this paper, we present the first formalization of pwa activation functions for an interactive theorem prover tailored to verifying neural networks within Coq using the library Coquelicot for real analysis. As a proof-of-concept, we construct the popular pwa activation function ReLU. We integrate our formalization into a Coq model of neural networks, and devise a verified transformation from a neural network N to a pwa function representing N by composing pwa functions that we construct for each layer. This representation enables encodings for proof automation, e.g. Coq's tactic lra -- a decision procedure for linear real arithmetic. Further, our formalization paves the way for integrating Coq in frameworks of neural network verification as a fallback prover when automated proving fails.