# Formalizing Piecewise Affine Activation Functions of Neural Networks in Coq

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

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Builds on 7 of its 35 references that are in the map.
- First posted on arXiv 30 Jan 2023.

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

- [On the Number of Linear Regions of Deep Neural Networks](https://mlsanity.com/paper/1402.1869/) (2014)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [Universal Function Approximation by Deep Neural Nets with Bounded Width and ReLU Activations](https://mlsanity.com/paper/1708.02691/) (2017)
- [Verification of Deep Convolutional Neural Networks Using ImageStars](https://mlsanity.com/paper/2004.05511/) (2020)
- [Reachable Polyhedral Marching (RPM): A Safety Verification Algorithm for Robotic Systems with Deep Neural Network Components](https://mlsanity.com/paper/2011.11609/) (2020)
- [Developing Bug-Free Machine Learning Systems With Formal Mathematics](https://mlsanity.com/paper/1706.08605/) (2017)

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

- [Neural Network Verification is a Programming Language Challenge](https://mlsanity.com/paper/2501.05867/) (2025)
- [TorchLean: Formalizing Neural Networks in Lean](https://mlsanity.com/paper/2602.22631/) (2026)
- [Formalized Hopfield Networks and Boltzmann Machines](https://mlsanity.com/paper/2512.07766/) (2025)
- [Benign Loss Landscapes Can Coexist with Worst-Case Hardness](https://mlsanity.com/paper/2609.13057/) (2026)

## Abstract (arXiv)

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.