Verified Deep Learning with Lean 4
Introduction
▶
What this book is about
The thesis
Who this book is for
Why now
Why image recognition
Why Lean
Let’s go
How this book is organized
▶
Roadmap: skip to your target architecture
For readers of the first book
Getting started
▶
Install
One command per tier
Foundations
▶
Mathlib’s
fderiv
Why VJPs, not Jacobians?
Inference and training
What the theorems cover, and what they leave to the run
1
The framework
▼
1
MNIST: linear classifier
2
MNIST: 1D MLP
3
MNIST: 2D CNN
4
CIFAR with BatchNorm
5
ResNet-34
6
MobileNetV2
7
EfficientNet
8
ConvNeXt
9
Vision Transformer
2
The bestiary
▶
10
The kit
11
The chapter nets at work
12
Beyond recognition
13
Game theory
Appendices
▶
A
Toolchain and platforms
B
On Verification
C
The ImageNet tier
D
Data availability
Acknowledgments
Colophon
Dependency graph
1 The framework
1
MNIST: linear classifier
1.1
Run it first
1.2
How it works
1.3
The theorems
1.4
Example: MNIST linear classifier
1.5
MLIR: Linear
1.6
What’s inside
.train
?
1.7
MLIR: Training Step
1.8
Recap
2
MNIST: 1D MLP
2.1
Run it first
2.2
The theorems
2.3
Example: MNIST MLP
2.4
MLIR: Dense
2.5
Recap
3
MNIST: 2D CNN
3.1
Run it first
3.2
The theorems
3.3
Example: MNIST 2D CNN
3.4
MLIR: Convolution
3.5
Recap
4
CIFAR with BatchNorm
4.1
Run it first
4.2
The theorems
4.3
Example: the eight-conv CNN on CIFAR-10
4.4
MLIR: BatchNorm
4.5
Recap
5
ResNet-34
5.1
Run it first
5.2
The theorems
5.3
Example: ResNet-34 on Imagenette
5.4
MLIR: Residual
5.5
The recipe
5.6
ImageNet recipe
5.7
Side quest: the A2 and A1 recipes
5.8
Recap
6
MobileNetV2
6.1
Run it first
6.2
The theorems
6.3
Example: MobileNet V2 on Imagenette
6.4
MLIR: Depthwise Convolution
6.5
ImageNet recipe
6.6
Side quest: MobileNet V4
6.7
Recap
7
EfficientNet
7.1
Run it first
7.2
The theorems
7.3
Example: EfficientNet-B0 on Imagenette
7.4
MLIR: Squeeze-and-Excitation
7.5
ImageNet recipe
7.6
Recap
8
ConvNeXt
8.1
Run it first
8.2
The theorems
8.3
Example: ConvNeXt-T on Imagenette
8.4
MLIR: Layer Scale
8.5
ImageNet recipe
8.6
Side quest: scaling to ConvNeXt-S and B
8.7
Recap
9
Vision Transformer
9.1
Run it first
9.2
The theorems
9.3
Example: ViT-Tiny on Imagenette
9.4
MLIR: Attention
9.5
ImageNet recipe
9.6
Side quest: scaling to ViT-S and B
9.7
Recap