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
▶
How the proofs are written.
1.1
The theorems
1.2
Example: MNIST linear classifier
1.3
MLIR: Linear
1.4
What’s inside
.train
?
1.5
MLIR: Training Step
2
MNIST: 1D MLP
▶
2.1
The theorems
2.2
Example: MNIST MLP
2.3
Return on width
2.4
MLIR: Dense
3
MNIST: 2D CNN
▶
3.1
The theorems
3.2
Example: MNIST 2D CNN
3.3
MLIR: Convolution
4
CIFAR with BatchNorm
▶
4.1
The theorems
4.2
Example: training dynamics on CIFAR
4.3
MLIR: BatchNorm
5
ResNet-34
▶
5.1
The theorem
5.2
Example: ResNet-34 on Imagenette
5.3
MLIR: Residual
5.4
What’s in the production recipe?
5.5
Ablation: what each ingredient contributes
5.6
ImageNet recipe
5.7
Side quest: ResNet-50, RSB-A3 (100 epochs)
6
MobileNetV2
▶
6.1
The theorems
6.2
Example: MobileNet V2 on Imagenette
6.3
MLIR: Depthwise Convolution
6.4
ImageNet recipe
6.5
Side quest: MobileNet V4
7
EfficientNet
▶
7.1
The theorem
7.2
Example: EfficientNet-B0 on Imagenette
7.3
MLIR: Squeeze-and-Excitation
7.4
ImageNet recipe
7.5
Side quests
8
ConvNeXt
▶
8.1
The theorems
8.2
Example: ConvNeXt-T on Imagenette
8.3
MLIR: Layer Scale
8.4
ImageNet recipe
9
Vision Transformer
▶
9.1
Matrix-level machinery
9.2
Attention proofs
9.3
Example: ViT-Tiny on Imagenette
9.4
MLIR: Attention
9.5
ImageNet recipe
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
Choosing a lowerer
Common troubleshooting
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
Float32
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
How the proofs are written.
1.1
The theorems
1.2
Example: MNIST linear classifier
1.3
MLIR: Linear
1.4
What’s inside
.train
?
1.5
MLIR: Training Step
2
MNIST: 1D MLP
2.1
The theorems
2.2
Example: MNIST MLP
2.3
Return on width
2.4
MLIR: Dense
3
MNIST: 2D CNN
3.1
The theorems
3.2
Example: MNIST 2D CNN
3.3
MLIR: Convolution
4
CIFAR with BatchNorm
4.1
The theorems
4.2
Example: training dynamics on CIFAR
4.3
MLIR: BatchNorm
5
ResNet-34
5.1
The theorem
5.2
Example: ResNet-34 on Imagenette
5.3
MLIR: Residual
5.4
What’s in the production recipe?
5.5
Ablation: what each ingredient contributes
5.6
ImageNet recipe
5.7
Side quest: ResNet-50, RSB-A3 (100 epochs)
6
MobileNetV2
6.1
The theorems
6.2
Example: MobileNet V2 on Imagenette
6.3
MLIR: Depthwise Convolution
6.4
ImageNet recipe
6.5
Side quest: MobileNet V4
7
EfficientNet
7.1
The theorem
7.2
Example: EfficientNet-B0 on Imagenette
7.3
MLIR: Squeeze-and-Excitation
7.4
ImageNet recipe
7.5
Side quests
8
ConvNeXt
8.1
The theorems
8.2
Example: ConvNeXt-T on Imagenette
8.3
MLIR: Layer Scale
8.4
ImageNet recipe
9
Vision Transformer
9.1
Matrix-level machinery
9.2
Attention proofs
9.3
Example: ViT-Tiny on Imagenette
9.4
MLIR: Attention
9.5
ImageNet recipe
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
Choosing a lowerer
Common troubleshooting
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
Float32
Acknowledgments
Colophon