Neural Network Verification Example

This file demonstrates verified neural network robustness using LeanCert's interval arithmetic infrastructure.

Example: Verifying a 2→2→1 Network

We define a small neural network and prove that for inputs in a bounded region, the output remains within specified bounds. This is the foundation for certified adversarial robustness.

Main results

• exampleNet - A simple 2→2→1 ReLU network
• robustness_certificate - Proof that output stays bounded for bounded inputs

Network Definition

def LeanCert.Examples.NeuralNet.layer1 : ML.Layer

First layer: 2 inputs → 2 outputs W1 = [[1, -1], [1, 1]], b1 = [0, 0] This computes [x - y, x + y]

Equations

• LeanCert.Examples.NeuralNet.layer1 = { weights := [[1, -1], [1, 1]], bias := [0, 0] }

def LeanCert.Examples.NeuralNet.layer2 : ML.Layer

Second layer: 2 inputs → 1 output W2 = [[1, 1]], b2 = [0] This computes (x - y) + (x + y) = 2x after ReLU

Equations

• LeanCert.Examples.NeuralNet.layer2 = { weights := [[1, 1]], bias := [0] }

def LeanCert.Examples.NeuralNet.exampleNet : ML.TwoLayerNet

The example two-layer network

Equations

• LeanCert.Examples.NeuralNet.exampleNet = { layer1 := LeanCert.Examples.NeuralNet.layer1, layer2 := LeanCert.Examples.NeuralNet.layer2 }

Well-formedness Proofs

theorem LeanCert.Examples.NeuralNet.layer1_wf : layer1.WellFormed

theorem LeanCert.Examples.NeuralNet.layer2_wf : layer2.WellFormed

theorem LeanCert.Examples.NeuralNet.exampleNet_wf : exampleNet.WellFormed

Input Region Definition

def LeanCert.Examples.NeuralNet.intervalAround (center eps : ℚ) (heps : 0 ≤ eps := by norm_num) (prec : ℤ := -53) : Core.IntervalDyadic

Create an interval around a center point with radius ε

Equations

• LeanCert.Examples.NeuralNet.intervalAround center eps heps prec = LeanCert.Core.IntervalDyadic.ofIntervalRat { lo := center - eps, hi := center + eps, le := ⋯ } prec

def LeanCert.Examples.NeuralNet.inputRegion : Engine.IntervalVector

Input region: x ∈ [0.4, 0.6], y ∈ [0.4, 0.6] This represents inputs near (0.5, 0.5) with perturbation ε = 0.1

Equations

• One or more equations did not get rendered due to their size.

Verification

def LeanCert.Examples.NeuralNet.outputInterval : Engine.IntervalVector

Compute the output interval for the example network

Equations

• LeanCert.Examples.NeuralNet.outputInterval = LeanCert.Examples.NeuralNet.exampleNet.forwardInterval LeanCert.Examples.NeuralNet.inputRegion

Robustness Certificate

theorem LeanCert.Examples.NeuralNet.mem_intervalAround {x : ℝ} {center eps : ℚ} (heps : 0 < eps) (hx : |x - ↑center| ≤ ↑eps) (prec : ℤ) (hprec : prec ≤ 0 := by norm_num) : x ∈ intervalAround center eps ⋯ prec

Helper: membership in intervalAround

theorem LeanCert.Examples.NeuralNet.robustness_certificate {x y : ℝ} (hx : |x - ↑(1 / 2)| ≤ ↑(1 / 10)) (hy : |y - ↑(1 / 2)| ≤ ↑(1 / 10)) (i : ℕ) (hi : i < min exampleNet.layer2.outputDim exampleNet.layer2.bias.length) : (exampleNet.forwardReal [x, y])[i] ∈ outputInterval[i]

Main robustness theorem: For any real input (x, y) within ε=0.1 of (0.5, 0.5), the network output is contained in the computed output interval.

This is a verified robustness certificate: it proves that small perturbations to the input cannot cause the output to leave the computed bounds.

Interpretation

The theorem robustness_certificate proves that for ANY real values x, y satisfying |x - 0.5| ≤ 0.1 and |y - 0.5| ≤ 0.1, the network output is guaranteed to be within the computed bounds.

This is a formal verification of robustness - not just an empirical test, but a mathematical proof that holds for ALL inputs in the region.

Applications:

• Certified defense against adversarial examples
• Safety verification for neural network controllers
• Proving bounds on neural network outputs for formal verification