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
2 The bestiary
10
The kit
What “\(N\) new primitives” means.
10.1
Bestiary-only
Layer
primitives
11
The chapter nets at work
11.1
Vision classifiers
11.2
Object detection — demo: R34+FPN on VisDrone
11.3
Industrial inspection — demo: the same detector on NEU-DET steel defects
11.4
People watching — demo: Arabic sign-language letters on ArASL
11.5
Agriculture — demo: lab leaves to field leaves on PlantVillage and PlantDoc
11.6
Remote sensing — demo: which wavelengths travel, EuroSAT to the Amazon and the Cerrado
11.7
Semantic segmentation — demo: UNet on BraTS
12
Beyond recognition
12.1
Natural language processing — demo: TinyGPT on Shakespeare
12.2
Image generation
12.3
Diffusion — demo: DDPM on MNIST
12.4
Physics — demo: Boltzmann generator on Müller–Brown
12.5
Signal processing — demo: gravitational-wave detection on LIGO strain
12.6
Beyond vision — demo: neural quantum states on the Ising chain
12.7
Structure — demo: a distogram ResNet against the CASP16 field
13
Game theory
13.1
Pong — DQN from pixels against the six-number state
13.2
Poker — Deep CFR against the exact best response
13.3
Tic-tac-toe — AlphaZero against the solved game
13.4
Tic-tac-toe without the rules — MuZero against the solved game
13.5
The catalogue: the AlphaGo family and Deep CFR