Skip to content
Back
Theme
Verified Deep Learning with Lean 4
Brett Koonce
2 min read
Original article ↗
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
▶
Theorem and definition budget per chapter
Roadmap: skip to your target architecture
For readers of the first book
Foundations
▶
Mathlib’s
fderiv
Why VJPs, not Jacobians?
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
2
MNIST: 1D MLP
▶
2.1
Run it first
2.2
The theorems
2.3
Example: MNIST MLP
2.4
Return on width
2.5
MLIR: Dense
3
MNIST: 2D CNN
▶
3.1
Run it first
3.2
The theorems
3.3
Example: MNIST 2D CNN
3.4
MLIR: Convolution
4
CIFAR with BatchNorm
▶
4.1
Run it first
4.2
The theorems
4.3
Example: training dynamics on CIFAR
4.4
MLIR: BatchNorm
5
ResNet-34
▶
5.1
Run it first
5.2
The theorem
5.3
Example: ResNet-34 on Imagenette
5.4
MLIR: Residual
5.5
What’s in the production recipe?
5.6
Ablation: what each ingredient contributes
5.7
ImageNet recipe
5.8
ResNet-50 on ImageNet: the 2018 recipe and RSB-A3
5.9
Side quest: the A2 and A1 recipes
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
7
EfficientNet
▶
7.1
Run it first
7.2
The theorem
7.3
Example: EfficientNet-B0 on Imagenette
7.4
MLIR: Squeeze-and-Excitation
7.5
ImageNet recipe
7.6
Further reading
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
9
Vision Transformer
▶
9.1
Run it first
9.2
Matrix-level machinery
9.3
Attention proofs
9.4
Example: ViT-Tiny on Imagenette
9.5
MLIR: Attention
9.6
ImageNet recipe
9.7
Side quest: scaling to ViT-S and B
10
Bestiary of Architectures
▶
What “\(N\) new primitives” means.
10.1
Bestiary-only
Layer
primitives
10.2
Bestiary entries
A
Data availability
B
Getting started
▶
Track 1: Proofs only (no GPU needed)
Track 2: Native install (XLA/PJRT)
Track 3: One-command demo tiers
Track 4: ImageNet-1k runners
Common troubleshooting
The second lowerer
C
On Verification
▶
C.1
Proven: the math is right
C.2
By construction: the code is the math
C.3
Cross-checked
C.4
Finite precision
Acknowledgments
Colophon
Dependency graph