Formalizing Piecewise Affine Activation Functions of Neural Networks in
  Coq
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.
Andrei Aleksandrov, Kim Völlinger
# Formalizing Piecewise Affine Activation Functions of Neural Networks in Coq

###### 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 \(\mathcal{N}\) to a pwa function representing \(\mathcal{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.

Keywords:Piecewise Affine Function Neural Network Interactive Theorem Prover Coq Verification.

## 1 Introduction

The growing importance of neural networks motivates the search of verification techniques for them. Verification with _automatic_ theorem provers is vastly under study, usually targeting feedforward networks with _piecewise affine_ (pwa) activation functions since the verification problem can be then encoded as an SMT or MILP problem. In contrast, few attempts exist on investigating _interactive_ provers. Setting them up for this task though offers not only a fallback option when automated proving fails but also insight on the verification process.

That is why in this paper, we work towards this goal by presenting the first formalization of pwa activation functions for an interactive theorem prover tailored to verifying neural networks with Coq. We constructively define pwa functions using the polyhedral subdivision of a pwa function [25] since many algorithms working on polyhedra are known [26] with some tailored to reasoning about reachability properties of neural networks [30]. Motivated by verification, we restrict pwa functions by a polyhedron's constraint to be _non-strict_ in order to suit linear programming [29] and by employing _finitely_ many polyhedra to fit
SMT/MILP solvers [11, 29]. We use reals supported by the library Coquelicot to enable reasoning about gradients and matrices with Coq's standard library providing the tactic lra - a decision procedure for linear real arithmetic. As a proof-of-concept, we construct the activation function ReLU- one of the most popular in industry [20] and formal verification [8]. Furthermore, we devise a sequential Coq model of feedforward neural networks integrating pwa activation layers. Most importantly, we present a verified transformation from a neural network \(\mathcal{N}\) to a pwa function \(f_{\mathcal{N}}\) representing \(\mathcal{N}\) with the main benefit being again encodings for proof automation. To this end, we introduce two verified binary operations on pwa functions - usual function composition and an operator to construct a pwa function for each layer. In particular, we provide the following contributions with the corresponding Coq code available on GitHub1:

Footnote 1: At [https://github.com/verinncq/formalizing-pwa](https://github.com/verinncq/formalizing-pwa) with matrix_extensions.v (Section 2), piecewise_affine.v (Section 3.1), neuron_functions.v (Section 3.2), neural_networks.v (Section 4.1 and 4.4) and pwa_operations.v (Section 4.2 and 4.3).

1. a formalization of pwa functions based on polyhedral subdivision tailored to verification of neural networks (Section 3),
2. a construction of the popular activation function ReLU (Section 3),
3. a sequential model for feedforward neural networks with parameterized layers (Section 4),
4. composition for pwa functions and an operator for constructing higher dimensional pwa functions out of lower dimensional ones (Section 4), and
5. a verified transformation from a feedforward neural network with pwa activation to a single pwa function representing the network (Section 4).

Related Work.A variety of work on using automatic theorem provers to verify neural networks exists with the vast majority targeting feedforward neural networks with pwa activation functions [6, 8, 12, 15, 18, 19, 24]. In comparison, little has been done regarding interactive theorem provers with some mechanized results from machine learning [2, 22], a result on verified training in Lean[27] and, relevant to this paper, pioneering work on verifying networks in Isabelle[7] and in Coq[3]. Apart from [7] targeting Isabelle instead of Coq, both network models are not generalized by entailing a formalization of pwa functions and in addition they do not offer a model of the network as a (pwa) function - both contributions of this paper.

## 2 Preliminaries

We clarify notations and definitions important to this paper. We write \(dom(f)\) for a function's domain, \(dim(f)\) for the dimension of \(dom(f)\) and \((f\circ g)(x)\) for function composition. For a matrix \(M\), \(M^{T}\) is the transposed matrix. We consider block matrices. To clarify notation, consider a block matrix made out of matrices \(M_{1},...,M_{4}\):

\[\begin{bmatrix}M_{1}&M_{2}\\ \hline M_{3}&M_{4}\end{bmatrix}\]
### Piecewise Affine Topology

We give the important definitions regarding pwa functions [23, 25, 32].

Definition 1 (Linear Constraint): For some \(c\in\mathbb{R}^{n},b\in\mathbb{R}\), a _linear constraint_ is an inequality of form \(c^{T}x\leq b\) for any \(x\in\mathbb{R}^{n}\).

Definition 2 (Polyhedron2): A _polyhedron_\(P\) is the intersection of finitely many halfspaces, meaning \(P:=\{x\in\mathbb{R}^{n}|c_{1}^{T}x\leq b_{1}\wedge...\wedge c_{m}^{T}x\leq b_{ m}\}\) with \(c_{i},b_{i}\in\mathbb{R}^{n},b_{i}\in\mathbb{R}\) and \(i\in\{1,...,m\}\).

Footnote 2: In the literature often referred to as a convex, closed polyhedron.

We denote the constraints of \(P\) as \(\mathcal{C}(P):=\{(c_{1}^{T}x\leq b_{1}),...,(c_{m}^{T}x\leq b_{m})\}\) for readability even though a constraint is given by \(c_{i}\) and \(b_{i}\) while \(x\) is arbitrary.

Definition 3 (Affine Function3): A function \(f:\mathbb{R}^{m}\rightarrow\mathbb{R}^{n}\) is called _affine_ if there exists \(M\in\mathbb{R}^{n\times m}\) and \(b\in\mathbb{R}^{n}\) such that for all \(x\in\mathbb{R}^{m}\) holds: \(f(x)=Mx+b\).

Definition 4 (Polyhedral Subdivision): A _polyhedral subdivision_\(S\subseteq\mathbb{R}^{n}\) is a finite set of polyhedra \(\mathbf{P}:=\{P_{1},\ldots,P_{m}\}\) such that (1) \(S=\bigcup_{i=1}^{m}P_{i}\) and (2) for all \(P_{i},P_{j}\in\mathbf{P},x\in P_{i}\cap P_{j}\), and for all \(\epsilon>0\) there exists \(x^{\prime}\) such that \(|x-x^{\prime}|<\epsilon\), and \(x^{\prime}\notin P_{i}\cap P_{j}\).

Definition 5 (Piecewise Affine Function): A continuous function \(f:D\subseteq\mathbb{R}^{m}\rightarrow\mathbb{R}^{n}\) is _piecewise-affine_ if there is a polyhedral subdivision \(\mathbf{P}=\{P_{1},\ldots,P_{l}\}\) of \(D\) and a set of affine functions \(\{f_{1},\ldots,f_{l}\}\) such that for all \(x\in D\) holds \(f(x)=f_{i}(x)\) if \(x\in P_{i}\).

### Neural Networks

Neural networks approximate functions by learning from sample points during training [9] with arbitrary precision [10, 14, 16]. A feedforward neural network is a directed acyclic graph with the edges having weights and the vertices (neurons) having biases and being structured in layers. Each layer applies a generic affine function for summation and an activation function (possibly a pwa function). In many machine learning frameworks (e.g. PyTorch), these functions are modelled as separate layers followed up by each other. We adopt this structure in our Coq model with a _linear layer_ implementing the generic affine function. Every network has an input and an output layer with optional hidden layers in between.
### Interactive Theorem Prover Coq & Library Coquelicot

We use the interactive theorem prover Coq[28] providing a non-turing-complete functional programming language extractable to selected functional programming languages and a proof development system - a popular choice for formal verification of programs and formalization of mathematical foundations. Additionally, we use the real analysis library Coquelicot[5] offering derivatives, integrals, and matrices compatible with Coq's standard library.

Extensions in Coq: Column Vectors & Block Matrices.For this paper, we formalized column vectors and block matrices on top of Coquelicot. A column vector colvec is identified with matrices and equipped with a dot product dot on vectors and some additional lemmas to simplify proofs. Additionally, we formalized several notions for Coquelicot's matrix type. We provide multiplication of a matrix with a scalar scalar_mult and transposition transpose of matrices. We provide operations on different shapes of matrices and vectors such as a right-to-left construction of block diagonal matrices block_diag_matrix, a specialization thereof on vectors colvec_concat and extensions of vectors with zeroes on the bottom extend_colvec_at_bottom or top extend_colvec_on_top, denoted as follows: \(\begin{bmatrix}M_{1}&0\\ \hline 0&M_{2}\end{bmatrix},\begin{bmatrix}\vec{v}_{1}\\ \hline\vec{v}_{2}\end{bmatrix},\begin{bmatrix}\vec{v}\\ \hline\vec{0}\end{bmatrix},\text{ and }\begin{bmatrix}\vec{0}\\ \hline\vec{v}\end{bmatrix}.\) Moreover, we proved lemmas relating all new operations with each other and the existing matrix operations.

## 3 Formalization of Piecewise Affine Functions in Coq

We formalize pwa functions tailored to neural network verification with pwa activation. As a proof-of-concept, we construct the activation function Rectified Linear Unit (ReLU) - one of the most popular activation functions in industry [20] and formal verification [8].

### Inductive Definition of PWA Functions

We define a linear constraint with a dimension _dim_ and parameters, vector \(c\in\mathbb{R}^{dim}\) and scalar \(b\in\mathbb{R}\), being satisfied for a vector \(x\in\mathbb{R}^{dim}\) if \(c\cdot x\leq b\):

```
InductiveLinearConstraint(dim:nat):Type:= |Constraint(c:colvecdim)(b:R). Definitionsatisfies_lc{dim:nat}(x:colvecdim)(l:LinearConstraintdim) :Prop:=matchlwith|Constraintcb\(\Rightarrow\)dotcx<=bend.
```

We define a polehydron as a finite set of linear constraints together with a predicate stating that a point lies in a polyhedron:

```
InductiveConvexPolyhedron(dim:nat):Type:= |Polyhedron(constraints:list(LinearConstraintdim)).
```
```
Definitionin_convex_polyhedron{dim:nat}(x:colvecdim)(p: ConvexPolyhedrondim):= matchpwith|Polyhedronlcs=> forallconstraint,Inconstraintlcs-satisfies_lcxconstraintend.
```

Finally, we define a pwa function as a record composed of the fields body holding the polyhedral subdivision for piecewise construction of the function, and prop for the property univalence (i.e. all "pieces" together yield a function).

```
RecordPWAF(in_dimout_dim:nat):Type:=mkPLF{ body:list(ConvexPolyhedronin_dim*((matrixout_dimin_dim)*colvecout_dim)); prop:pwaf_univalencebody;}.
```

Piecewise ConstructionWe construct a pwa function \(f\) by a list of polyhedra, matrices and vectors with a triple \((P,M,b)\) defining a "piece" of \(f\) by an affine function with \(f(x)=Mx+b\) if \(x\in P\). For evaluation, we search a polyhedron containing \(x\) and compute the affine function:

```
Fixpointpwaf_eval_helper{in_dimout_dim:nat} (body:list(ConvexPolyhedronin_dim*((matrix(T:=R)out_dimin_dim)*colvecout_dim)))(x:colvecin_dim) :option(ConvexPolyhedronin_dim*((matrixout_dimin_dim)*colvecout_dim)):= matchbodywith |nil->None |body_el::next-> matchbody_elwith |(polyh,(M,b))-> matchpolyhedron_evalxpolyhwith |true->Some(body_el) false->pwaf_eval_helpernext-> endend.
```

To handle the edge case where no such polyhedron is found (i.e. \(x\notin dom(f)\)), we use a wrapper function pwaf_eval. For the purpose of proving, we define a predicate in_pwaf_domain for the existence of such a polyhedron and a predicate is_pwaf_value for a stating the function is evaluated to a certain value.

UnivalenceWe enforce the construction to be a function by stating univalence, in this case all pairs of polyhedra having coinciding affine functions in their intersection, requiring a proof for each instance of type PWAF:
Class of Formalized PWA FunctionsMotivated by pwa activation functions in the context of neural network verification, our pwa functions are restricted by

1. all linear constraints being _non-strict_, and
2. being defined over a union of _finitely_ many polyhedra.

Restriction (1) is motivated by linear programming usually dealing with non-strict constraints [29], and restriction (2) by MILP/SMT solvers commonly accepting finitely many variables [11, 29]. Since we use that every continuous pwa function on \(\mathbb{R}^{n}\) admits a polyhedral subdivision of the domain [25], all continuous pwa functions with a finite subdivision can be encoded.

For pwa functions not belonging to this class, consider any discontinuous pwa function since discontinuity violates restriction (1), and any periodic pwa function as excluded by restriction (2) due to having infinitely many "pieces".

Choice of FormalizationWe use real numbers (instead of e.g. rationals or floats) to enable Coquelicot's reasoning about derivatives interesting for neural networks' gradients. Coquelicot builds up on the reals of Coq's standard library allowing the use of Coq's tactic lra - a Coq-native decision procedure for linear real arithmetic.

Moreover, we use inductive types since they come with an induction principle and therefore ease proving. In addition, the type list (e.g. used for the definition of pwa functions) enjoys extensive support in Coq. For example, pwaf_univalence is stated using the list predicate ForAllPairs and proofs intensively involve lemmas from Coq's standard library.

A constructive definition using the polyhedral subdivision is interesting since many efficient algorithms are known that work on polyhedra [26] with even algorithms tailored to neural network verification around [30]. We expect that such algorithms are implementable in an idiomatic functional style using our model. Furthermore, we anticipate easy-to-implement encodings for proof automation.

### Example: Rectified Linear Unit Activation Function

We construct ReLU as a pwa function defined by two "pieces" each of which being a linear function. The function is defined as:

\[\textsc{ReLU}(x):=\begin{cases}0,&x<0\\ x,&x\geq 0\end{cases}\]
Piecewise Construction.The intervals, \((-\infty,0)\) and \([0,\infty)\), each correspond to a polyhedron in \(\mathbb{R}\) defined by a single constraint4: \(P_{left}:=\{x\in\mathbb{R}^{1}|[1]\cdot x<=0\}\) and \(P_{right}:=\{x\in\mathbb{R}^{1}|[-1]\cdot x<=0\}\). We define these polyhedra as follows:5

Footnote 4: Matrices involved are one-dimensional vectors since ReLU is one-dimensional. For technical reasons, in Coq, the spaces \(\mathbb{R}\) and \(\mathbb{R}^{1}\) differ with the latter working on one-dimensional vectors instead on scalars.

DefinitionReLU1d_polyhedra_left := Polyhedron 1 [Constraint 1 None 0]. DefinitionReLU1d_polyhedra_right := Polyhedron 1 [Constraint 1 (scalar_mult (-1) None 0)].

ReLU's construction list contains these polyhedra each associated with a matrix and vector, in these cases \(([0],[0])\) and \(([1],[0])\), for the affine functions:

DefinitionReLU1d_body: list (ConvexPolyhedron 1 * (matrix (T:=R) 1 1 * \(\text{\sc{colvec 1}})\)) := [(ReLU1d_polyhedra_left, (Mzero, null_vector 1)); (ReLU1d_polyhedra_right, (Mone, null_vector 1))].

Univalence.Note that while ReLU's intervals are distinct, the according polyhedra with non-strict constraints are not. To ensure the construction to be a function, we prove univalence by proving that only \([0]\in(P_{left}\cap P_{right})\):

LemmaRelU1d_polyhedra_intersect_0:

forall x, in_convex_polyhedron x ReLU1d_polyhedra_left \(\wedge\)

in_convex_polyhedron x ReLU1d_polyhedra_right \(\rightarrow\) x = null_vector 1.

Finally, we ensure for each polyhedra pair holds \([1]\cdot[0]+[0]=[0]\cdot[0]+[0]\), and instantiate a PWAF by DefinitionReLU1dPWAF := mkPLF 1 1 ReLU1d_body ReLU1d_pwaf_univalence.

On the Construction of pwaFunctions.Analogously to the ReLU example, other activation functions sharing its features of being one-dimensional and consisting of a few polyhedra can be constructed similarly. We can construct a multi-dimensional version out of a one-dimensional function as we will illustrate for ReLU in Section 4.3. Activation functions that require more effort to construct are for example different types of pooling [9], mostly due to a non-trivial polyhedra structure and inherent multi-dimensionality. This effort motivates future development of more support in constructing pwa functions with the goal to compile a library of layer types.
## 4 Verified Transformation of a Neural Network to a Pwa Function

We present our main contribution: a formally verified transformation of a feedforward neural network with pwa activations into a single pwa function. First, we introduce a Coq model for feedforward neural networks (Section 4.1). We follow up with two verified binary operations on pwa functions at the heart of the transformation, _composition_ (Section 4.2) and _concatenation_ (Section 4.3), and finish with the verified transformation (Section 4.4).

### Neural Network Model in Coq

We define a neural network _NNSequential_ as a list-like structure containing layers parameterized on the type of activation, and the input's, output's and hidden layer's dimensions with dependent types preventing dimension mismatch:

```
InductiveNNSequential{input_dimoutput_dim:nat}:= |NNOOutput:NNSequential |NNplainLayer{hidden_dim:nat}: (colvecinput_dim\(\rightarrow\)colvechidden_dim) \(\rightarrow\)NNSequential(input_dim:=hidden_dim)(output_dim:=output_dim) \(\rightarrow\)NNSequential |NNPVALayer{hidden_dim:nat}: PMAFinput_dimhidden_dim \(\rightarrow\)NNSequential(input_dim:=hidden_dim)(output_dim:=output_dim) \(\rightarrow\)NNSequential |NNUnknownLayer{hidden_dim:nat}: NNSequential(input_dim:=hidden_dim)(output_dim:=output_dim) \(\rightarrow\)NNSequential.
```

The network model has four layer types: NNOutput as the last layer propagates input values to the output; NNPlainLayer is a layer allowing any function in Coq defined on real vectors; NNPVALayer is a pwa activation layer - the primary target of our transformation; and NNUnknownLayer is a stub for a layer with an unknown function.

Informally speaking, the semantics of our model is as follows: for a layer NNOutput the identity function6 is evaluated, for NNPlainLayer the passed function, for NNPVALayer the passed pwa function, and for NNUnknownLayer a failure is raised. Thus, the _NNSequential_ type does not prescribe any specific functions of layers but expects them as parameters.

Footnote 6: We use the customized identity function _flex_dim_copy_.

An Example of a Neural Network.In order to give an example, we define specific layers for a network, in this case the pwa layers Linear and ReLU:
_From a Trained Neural Network into the World of Coq._ As illustrated, we can construct feedforward neural networks in Coq. Another option is to convert a neuronal network trained outside of Coq into an instance of the model. In [3] a python script is used for conversion from PyTorch to their Coq model without any correctness guarantees, while in [7] an import mechanism from TensorFlow into Isabelle is used, where correctness of the import has to be established for each instance of their model. We are working with a converter expecting a neural network in the ONNX format (i.e. a format for neural network exchange supported by most frameworks) [4] to produce an according instance in our Coq model [13].7 This converter is mostly written within Coq with its core functionality being verified.

Footnote 7: A bachlor thesis supervised by one of the authors and scheduled for publication.

Choice of Model._ While feedforward neural networks are often modeled as directed acyclic graphs [17, 1], in the widely used machine learning frameworks TensorFlow and PyTorch a sequential model of layers is employed as well. Our model corresponds to the latter, and is inspired by the, to our knowledge, only published neural network model in Coq (having been used for generalization proofs) [3]. Our model though is more generic by having parameterized layers instead of being restricted to ReLU activation. Moreover, while their model works with customized floats, we decided for reals in order to support Coquelicot's real analysis as discussed in Section 3.

A graph-based model carries the potential to be extended to other types of neural networks such as recurrent networks featuring loops in the length of the input. For the reason of being generic, ONNX employs a graph-based model. Hence, an even more generic graph-based Coq model is in principle desirable but it also adds complexity. In [7] the focus is on a sequential model which the authors showed to be superior to a graph-based model for the purpose of verification. Hence, we expect that the need for a sequential Coq model for _feedforward_ networks will stay even in the existence of a graph-based model.
### Composition of PWA functions

Besides composition being a general purpose binary operation closed over pwa functions [25], it is needed in our transformation to compose pwa layers. Since for pwa functions \(f:\mathbb{R}^{l}\rightarrow\mathbb{R}^{n}\) and \(g:\mathbb{R}^{m}\rightarrow\mathbb{R}^{l}\) their composition \(z=f\circ g\) is a pwa function, composition in Coq produces an instance of type PWAF requiring a construction and a proof of univalence:

```
Definitionpwaf_compose{in_dimhidden_dimout_dim:nat} (f:PWAFhidden_dim out_dim) (g:PWAF in_dim hidden_dim) :PWAF in_dim out_dim (pwaf_compose_bodyfg) (pwaf_compose_univalencefg).
```

#### 4.2.1 Piecewise Construction of Composition.

Assume a pwa function \(f\) defined on the polyhedra set \(\mathbf{P}^{f}=\{P_{1}^{f},\ldots,P_{k}^{f}\}\) with affine functions given by the parameter set \(\mathbf{A}^{f}=\{(M_{1}^{f},b_{1}^{f}),\ldots,(M_{K}^{f},b_{k}^{f})\}\). Analogously, \(g\) is given by \(\mathbf{P}^{g}\) and \(\mathbf{A}^{g}\). For computing a composed function \(z=f\circ g\) at any \(x\in\mathbb{R}^{m}\), we need a polyhedron \(P_{j}^{g}\in\mathbf{P}^{g}\) such that \(x\in P_{j}^{g}\) to compute \(g(x)=M_{j}^{g}x+b_{j}^{g}\) with \((M_{j}^{g},b_{j}^{g})\in\mathbf{A}^{g}\). Following, we need a polyhedron \(P_{i}^{f}\in\mathbf{P}^{f}\) with \(g(x)\in P_{i}^{f}\) to finally compute \(z(x)=M_{i}^{f}g(x)+b_{i}^{f}\) with \((M_{i}^{f},b_{i}^{f})\in\mathbf{A}^{f}\).

We have to reckon on function composition on the level of polyhedra sets to construct \(z\)'s polyhedra set \(\mathbf{P}^{z}\). For each pair \(P_{i}^{f}\in\mathbf{P}^{f}\), \(P_{j}^{g}\in\mathbf{P}^{g}\), we create a polyhedron \(P_{i,j}^{z}\in\mathbf{P}^{z}\) such that \(x\in P_{i,j}^{z}\) iff \(x\in P_{j}^{g}\) and \(M_{j}^{g}x+b_{j}^{g}\in P_{i}^{f}\) with \((M_{j}^{g},b_{j}^{g})\in\mathbf{A}^{g}\). Consequently, \(\mathcal{C}(P_{j}^{g})\subseteq\mathcal{C}(P_{i,j}^{z})\) while the constraints of \(P_{i}^{f}\) have to be modified. For \((c_{i}\cdot x\leq b_{i})\in\mathcal{C}(P_{i}^{f})\) we have the modified constraint \(((c_{i}^{T}M_{j}^{g})\cdot x\leq b_{i}-c_{i}\cdot b_{j}^{g})\in\mathcal{C}(P_{ i,j}^{z})\). We construct a polyhedra set accordingly in Coq including empty polyhedra in case no qualifying pair of polyhedra exists:

```
Fixpointcompose_polyhedra_helper{in_dimhidden_dim:nat} (M:matrixhidden_dimin_dim)(b:colvechidden_dim) (l_f:list(LinearConstrainthidden_dim)):= matchl_fwith |[]\(\Rightarrow\)[] |(Constraintcb2)::tail\(\Rightarrow\) Constraintin_dim (transpose(Mmult(transposec)M))(b2-(dotcb1)):: compose_polyhedra_helperMb1tail end.
```

Definitioncompose_polyhedra{in_dimhidden_dim:nat} (p_g:ConvexPolyhedronin_dim) (M:matrixhidden_dimin_dim)(b:colvechidden_dim) (p_f:ConvexPolyhedronhidden_dim):= matchp_gwith|Polyhedronl1 \(\Rightarrow\) matchp_fwith|Polyhedronl2 \(\Rightarrow\) Polyhedronin_dim(l1++compose_polyhedra_helperMb12)
Further, each \((M^{z}_{i,j},b^{z}_{i,j})\in\mathbf{A}^{z}\) is defined as \((M^{f}_{j}M^{g}_{i},M^{f}_{j}b^{g}_{i}+b^{f}_{j})\) as a result of usual composition of two affine functions:

```
Definitioncompose_affine_functions{in_dimhidden_dimout_dim:nat} (M_f:matrix(T:=R)out_dimhidden_dim)(b_f:colvecout_dim) (M_g:matrix(T:=R)hidden_dimin_dim)(b_g:colvechidden_dim):= (MmultM_fM_g,Mplus(MmultM_fb_g)b_f).
```

Univalence of Composition.Due to the level of details, the Coq proof for the composed function \(z\) satisfying univalence is not included in this paper (see Theorem pwaf_compat_univalence).

Composition Correctness.For establishing the correctness of the composition, we proved the following theorem:

```
Theorempwaf_compose_correct: forallin_dimhid_dimout_dimxf_xg_x (f:PWAFhid_dimout_dim)(g:PWAFin_dimhid_dim), in_pwaf_domaingx\(\rightarrow\)is_pwaf_valuegxg_x\(\rightarrow\) in_pwaf_domainfg_x\(\rightarrow\)is_pwaf_valuefg_xf_x letfg:=pwaf_composefg in in_pwaf_domainfgx\(\wedge\)is_pwaf_valuefgxf_x.
```

For one of the lemmas (compose_polyhedra_subset_g) we proved that polyhedra of \(g\) are only getting smaller by composing \(g\) with \(f\) while the borders that are set by polyhedra of \(g\) being kept.

### Concatenation: Layers of Neural Networks as PWA Functions

While some neural networks come with each layer being _one_ multi-dimensional function, many neural networks feature layers where each neuron is assigned the same lower dimensional function independently then applied to each neuron's input. Motivated by the transformation of a neural network into a single pwa function, we introduce a binary operation _concatenation_ that constructs a single pwa function for each pwa layer of a neural network. Otherwise, concatenation is interesting due to constructing a multi-dimensional pwa function being challenging since a user has to define multiple polyhedra with a significant number of constraints. For illustration, we construct a multi-dimensional ReLU layer.

Concatenation of pwa functions has to yield an instance of type PWAF since being closed over pwa functions. Concatenation is defined as follows:

Definition 6 (Concatenation).: _Let \(f:\mathbb{R}^{m}\rightarrow\mathbb{R}^{n}\) and \(g:\mathbb{R}^{k}\rightarrow\mathbb{R}^{l}\). The concatenation \(\oplus\) is defined as:_

\[(f\oplus g)(\frac{\left[x^{f}\right]}{x^{g}}):=\left[\frac{f(x^{f})}{g(x^{g})}\right]\]
Piecewise Construction of Concatenation.Assume some \(f,g\), \(\mathbf{P}^{f},\mathbf{P}^{g},\mathbf{A}^{f}\) and \(\mathbf{A}^{g}\) as previously used, and \(z=f\oplus g\). The polyhedra set \(\mathbf{P}^{z}\) contains the pairwise joined polyhedra of \(\mathbf{P}^{f}\) and \(\mathbf{P}^{g}\) but with each constraint of a polyhedron lifted to the dimension of \(z\)'s domain. Consider a pair \(P_{i}^{f}\in\mathbf{P}^{f}\) and \(P_{j}^{g}\in\mathbf{P}^{g}\). For constraints \((c_{i}^{f}\cdot x^{f}\leq b_{i}^{f})\in\mathcal{C}(P_{i}^{f})\) and \((c_{j}^{g}\cdot x^{g}\leq b_{j}^{g})\in\mathcal{C}(P_{j}^{g})\) with \(\left[\frac{x^{f}}{x^{g}}\right]\in\mathbb{R}^{dim(f)+dim(g)}\), the following higher dimensional constraints are in \(\mathcal{C}(P_{i,j}^{z})\) with \(P_{i,j}^{z}\in\mathbf{P}^{z}\): \(\left[\frac{c_{i}^{f}}{0}\right]\cdot\left[\frac{x^{f}}{x^{g}}\right]\leq b_{i }^{f}\) and \(\left[\frac{0}{c_{j}^{g}}\right]\cdot\left[\frac{x^{f}}{x^{g}}\right]\leq b_{j }^{g}\). Thus, we get \(\left[\frac{x^{f}}{x^{g}}\right]\in P_{i,j}^{z}\) iff \(x^{f}\in P_{i}^{f}\) and \(x^{g}\in P_{j}^{g}\).

Hence, the concatenation requires the pairwise join of all polyhedra \(\mathbf{P}^{f}\) and \(\mathbf{P}^{g}\) each with their constraints lifted to the higher dimension of \(z\)'s domain:

```
Definitionconcat_polyhedra{in_dim1in_dim2:nat} (p_f:ConvexPolyhedronin_dim1)(p_g:ConvexPolyhedronin_dim2): ConvexPolyhedron(in_dim1+in_dim2):= matchp_fwith|Polyhedron11\(\Rightarrow\) matchp_gwith|Polyhedron12\(\Rightarrow\) Polyhedron(in_dim1+in_dim2) (extend_lincons_at_bottom11(in_dim1+in_dim2)++ extend_lincons_on_top12(in_dim1+in_dim2)) end.
```

The Coq code uses two functions for insertion of zeros similar to the dimension operations (see Section 2). The corresponding affine function of \(P_{i,j}^{z}\) is then:

\[(M_{i,j}^{z},b_{i,j}^{z}):=(\left[\begin{array}{c|c}M_{i}^{f}&0\\ \hline 0&M_{j}^{g}\end{array}\right],\left[\begin{array}{c|c}b_{i}^{f}\\ b_{j}^{g}\end{array}\right]).\]

Univalence of Concatenation.The technical proof of concatenation being univalent is outside of the scope of this paper (see pwaf_concat_univalence).

Concatenation Correctness.We proved the correctness of the concatenation:

```
Theorempwaf_concat_correct: forallin_dim1in_dim2out_dim1out_dim2x1x2f_x1g_x2 (f:PWAFin_dim1out_dim1)(g:PWAFin_dim2out_dim2), in_pwaf_domainfx1\(\rightarrow\)is_pwaf_valuefx1f_x1\(\rightarrow\) in_pwaf_domaingx2\(\rightarrow\)is_pwaf_valuegx2g_x2\(\rightarrow\) letfg:=pwaf_concatfgin letx:=colvec_concatx1x2in letfg_x:=colvec_concatf_x1g_x2in in_pwaf_domainfgx\(\wedge\)is_pwaf_valuefgxfg_x.
```

The proof relies on an extensive number of lemmas connecting matrix operations to block matrices and vector reshaping.
Example:ReLU Layer.Using concatenation, we construct a multi-dimensional ReLU layer using one-dimensional ReLU (see Section 4.1). To construct a ReLU layer \(\mathbb{R}^{n}\rightarrow\mathbb{R}^{n}\), we perform \(n\) concatenations of one-dimensional ReLU:

```
FixpointReLU_PWAF_helper(in_dim:nat):PWAFin_dimin_dim:= matchin_dimwith |0\(\Rightarrow\)OutputPWAF(in_dim:=0)(out_dim:=0) |Sn\(\Rightarrow\)pwaf_concatReLUdPWAF(ReLU_PWAF_helpern) end.
```

### Transforming a Neural Network into a Pwa Function

Building up on previous efforts, the transformation of a feedforward neural network with pwa activation functions into a single pwa function is straightforward. Using concatenation, we construct multi-dimensional pwa layers and then compose them to one pwa function representing the whole neural network. The transformation is illustrated conceptually in Figure 1.

The transformation in Coq simply fails when applied to hidden layers that are non-pwa:

```
Fixpointtransform_nn_to_pwaf{in_dimout_dim:nat} (nn:NNSequential(input_dim:=in_dim)(output_dim:=out_dim)) :option(PWAFin_dimout_dim):= matchnnwith |NNOutput\(\Rightarrow\)Some(OutputPWAF) |NNplainLayer\(\_\_\_\Rightarrow\)None |NNUnknownLayer\(\_\_\Rightarrow\)None |NNPWALayer\(\_\_\)pwafnext\(\Rightarrow\) matchtransform_nn_to_pwafnextwith |Somenext_pwaf\(\Rightarrow\)Some(pwaf_composenext_pwaf) |None\(\Rightarrow\)None end.
```

Correctness of Transformation.For this transformation, we have also proven the following theorem in Coq to establish its correctness:

```
Theoremtransform_nn_to_pwaf_correct: forallin_dimout_dim(x:colvecin_dim)(f_x:colvecout_dim)nn nn_pwaf, Somenn_pwaf=transform_nn_to_pwaf_correctnn\(\rightarrow\) in_pwaf_domainn_pwafx\(\rightarrow\) is_pwaf_valuenn_pwaf\(\_\)xf_x\(\leftrightarrow\)nn_evalnnx=Somef_x.
```

For a neural network \(\mathcal{N}\) and its transformed pwa function \(f_{\mathcal{N}}\), the theorem states that for all inputs \(x\in dom(f_{\mathcal{N}})\) holds \(f_{\mathcal{N}}(x)=\mathcal{N}(x)\). The proof of this theorem relies on several relatively simple properties of the composition. Note that for
\(dom(f_{\mathcal{N}})=\emptyset\) the theorem trivially holds, and in fact an additional proof is required for \(f_{\mathcal{N}}\)'s polyhedra being a subdivision of \(dom(\mathcal{N})\) (i.e. \(dom(f_{\mathcal{N}}(x))=dom(\mathcal{N}(x))\)).

On the Representation of a Neural Network as a pwa FunctionThe main benefit of having a pwa function obtained from neural network lies in the option to use simple-to-implement encodings of pwa functions for different solvers, e.g. Coq's tactic lra or MILP/SMT solvers. Hence, this representation paves the way for proof automation when stating theorems about the input-output relation of a network in Coq.

Furthermore, a representation as a pwa function moves the structural complexity of a neural network to the polyhedral subdivision of the pwa function. This is interesting since local search can be applied to the set of polyhedra for reasoning about reachability properties in neural networks [30]. Furthermore, one may estimate the size of a pwa function's polyhedral subdivision for different architectures of neural network [21].

Figure 1: Transformation of a feedforward network \(N\) with pwa activation functions into its representation as a pwa function \(F_{N}\) by concatenating neuron activation within each layer followed up by composing pwa layers.
## 5 Discussion

We were working towards neural network verification in Coq with a verified transformation from a network to a pwa function being the main contribution.

Summary.We presented the first formalization of pwa activation functions for an interactive theorem prover tailored to verifying neural networks with Coq. For our constructive formalization, we used a pwa function's polyhedral subdivision due to the numerous efficient algorithms working on polyhedra. Our class of pwa functions is on-purpose restricted to suit linear programming by using non-strict constraints and to fit SMT/MILP solvers by employing finitely many polyhedra. Using Coquelicot's reals, we enabled reasoning about gradients and support Coq's tactic lra. With ReLU, we constructed one of the most popular activation functions. We presented a verified transformation from a neural network to its representation as a pwa function enabling encodings for proof automation for theorems about the input-output relation. To this end, we devised a sequential model of neural networks, and introduced two verified binary operation on pwa functions - usual function composition together with an operator to construct a pwa function for each layer.

Future Work.Since the main benefit of having a pwa function obtained from neural network lies in the many available encodings [8, 12] targeting different solvers, we envision encodings for our network model. These encodings have to be adapted to the verification within Coq with our starting point being the tactic lra - a Coq-native decision procedure for linear real arithmetic.

Moreover, moving the structural complexity of a neural network to the polyhedral subdivision of a pwa function, opens up on investigating algorithms working on polyhedra for proof automation with our main candidate being local search on polyhedra for reasoning about reachability properties in neural networks [30].

Further, for our model of neural networks, we intend a library of pwa activation functions with proof automation to ease construction. We also plan on a generic graph-based model for neural networks in Coq but as argued, we expect the sequential model to stay the mean of choice for feedforward networks. Additionally, since tensors are used in machine learning to incorporate complex mathematical operations, we aim to integrate a formalization of tensors tailored to neural network verification.
