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
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
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