Verified Deep Learning with Lean 4
1
Introduction
▶
What this book is about
The thesis
Who this book is for
Why now
Why image recognition
Why Lean
How to read this book
How this book is organized
A note on the proofs
Let’s go
2
Tensor: Calculus Foundations
3
MLP: Dense Layer
4
CNN: Convolution and Pooling
5
BatchNorm: the hard one
6
Residual: Skip Connections
7
Depthwise Convolution
8
Squeeze-and-Excitation
9
LayerNorm and GELU
10
Attention and the ViT finale
11
Bestiary of Architectures
▶
11.1
Bestiary-only
Layer
primitives
11.2
Bestiary entries
▶
11.2.1
Vision classifiers — Part 1’s primitives at scale
11.2.2
Object detection
11.2.3
Semantic segmentation
11.2.4
Image generation
11.2.5
Reinforcement learning
11.2.6
Beyond vision
A
Axioms at a glance
Dependency graph
9 LayerNorm and GELU
Axiom
55
GELU scalar function
✓
#
L∃∀N
Lean declarations
Axiom
56
GELU scalar derivative
✓
#
L∃∀N
Lean declarations
Axiom
57
GELU Jacobian
✓
#
Uses
Axiom 1
Axiom 56
L∃∀N
Lean declarations
Diagonal activation Jacobian.
Theorem
58
LayerNorm VJP
✓
#
Uses
Theorem 48
L∃∀N
Lean declarations
Proofs.layerNorm_has_vjp
LayerNorm = BatchNorm on a different axis; same primitive.
Theorem
59
GELU VJP
✓
#
Uses
Axiom 57
L∃∀N
Lean declarations
Proofs.gelu_has_vjp