Model Distillation Verification Example

This file demonstrates verified model distillation using LeanCert's interval arithmetic infrastructure.

The Scenario

In AI deployment, we often need to:

1. Train a large "Teacher" model for accuracy
2. Compress it into a smaller "Student" model for efficiency
3. Verify that the Student behaves similarly to the Teacher

LeanCert can formally prove that |Teacher(x) - Student(x)| ≤ ε for ALL inputs in a domain - not just sampled points, but a mathematical guarantee.

Example Networks

We define two simple 2→2→1 networks and verify their outputs differ by at most ε = 3 on the input domain [0, 1]².

Main Results

• distillationCheck_passes - The computable check returns true
• distillation_certificate - Formal proof of bounded difference

Network Definitions

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

Layer 1: 2 inputs → 2 outputs

Equations

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

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

Layer 2: 2 inputs → 1 output

Equations

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

def LeanCert.Examples.ML.Distillation.teacherNet : ML.Distillation.SequentialNet

The Teacher network

Equations

• LeanCert.Examples.ML.Distillation.teacherNet = { layers := [LeanCert.Examples.ML.Distillation.layer1, LeanCert.Examples.ML.Distillation.layer2] }

def LeanCert.Examples.ML.Distillation.studentNet : ML.Distillation.SequentialNet

The Student network

Equations

• LeanCert.Examples.ML.Distillation.studentNet = { layers := [LeanCert.Examples.ML.Distillation.layer1, LeanCert.Examples.ML.Distillation.layer2] }

Well-formedness Proofs

theorem LeanCert.Examples.ML.Distillation.layer1_wf : layer1.WellFormed

theorem LeanCert.Examples.ML.Distillation.layer2_wf : layer2.WellFormed

theorem LeanCert.Examples.ML.Distillation.teacherNet_wf : teacherNet.WellFormed 2

theorem LeanCert.Examples.ML.Distillation.studentNet_wf : studentNet.WellFormed 2

Input Domain

def LeanCert.Examples.ML.Distillation.mkInterval (lo hi : ℚ) (h : lo ≤ hi := by norm_num) (prec : ℤ := -53) : Core.IntervalDyadic

Create an interval from rational bounds

Equations

• LeanCert.Examples.ML.Distillation.mkInterval lo hi h prec = LeanCert.Core.IntervalDyadic.ofIntervalRat { lo := lo, hi := hi, le := h } prec

def LeanCert.Examples.ML.Distillation.inputDomain : Engine.IntervalVector

Input domain: [0, 1]²

Equations

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

Equivalence Check

def LeanCert.Examples.ML.Distillation.epsilon : ℚ

Tolerance for distillation verification

Equations

• LeanCert.Examples.ML.Distillation.epsilon = 3

def LeanCert.Examples.ML.Distillation.distillationCheck : Bool

The computable certificate

Equations

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

theorem LeanCert.Examples.ML.Distillation.distillationCheck_passes : distillationCheck = true

The check passes! This is verified by computation.

Helper Lemmas

theorem LeanCert.Examples.ML.Distillation.mem_mkInterval {x : ℝ} {lo hi : ℚ} (hle : lo ≤ hi) (hx : ↑lo ≤ x ∧ x ≤ ↑hi) (prec : ℤ) (hprec : prec ≤ 0 := by norm_num) : x ∈ mkInterval lo hi hle prec

Membership in mkInterval

The Distillation Certificate

theorem LeanCert.Examples.ML.Distillation.distillation_certificate (x y : ℝ) (hx : 0 ≤ x ∧ x ≤ 1) (hy : 0 ≤ y ∧ y ≤ 1) : List.length (teacherNet.forwardInterval inputDomain (-53)) = List.length (studentNet.forwardInterval inputDomain (-53)) ∧ ∀ (i : ℕ) (hi_t : i < List.length (teacherNet.forwardInterval inputDomain (-53))) (hi_s : i < List.length (studentNet.forwardInterval inputDomain (-53))), |(teacherNet.forwardReal [x, y])[i] - (studentNet.forwardReal [x, y])[i]| ≤ ↑epsilon

For ANY inputs (x, y) in [0, 1]², Teacher and Student outputs differ by at most ε = 3.

Interpretation

The theorem distillation_certificate proves that for ANY (x, y) ∈ [0, 1]²: |Teacher(x,y) - Student(x,y)| ≤ 3

This bound arises from interval arithmetic conservatism: the analysis computes bounds on Teacher and Student outputs independently, then subtracts them.

Applications

• Deployment Safety: Verify compressed models before deployment
• Regulatory Compliance: Provide machine-checked certificates
• CI/CD Integration: Automatically verify model equivalence in pipelines