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
Verified Deep Learning with Lean 4
Brett Koonce
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