The Rocq-NN-Roll Prover: Soundly Verifying Hyperproperties of Neural Networks in Rocq

<jats:title>Abstract</jats:title> <jats:p> Research on neural network verification has traditionally emphasized scalability. However, recent invalidations of formally verified results of neural networks highlight <jats:italic>soundness</jats:italic> as an equally important goal. Pursuing inherent soundness, we present <jats:italic>Rocq-NN-Roll</jats:italic> , the first <jats:italic>formally verified</jats:italic> prover for rational-valued piecewise-affine neural networks. Rocq-NN-Roll combines a network and its specification, including hyperproperties, into a piecewise-affine function and reduces the verification task to solving linear inequalities over the network’s polyhedral regions. Developed in Rocq, the prover also provides the first automated proof support for neural networks within any interactive theorem prover, highlighting their still underexplored role in this field. </jats:p>