v0.7.2 (release history) ·
The book: Verified Deep Learning with Lean 4
(PDF) — the interactive proof blueprint is the book: every theorem
clickable, from the pdiv primitives to the whole-network backward passes.
Lean 4 as a specification language for neural networks. Declare the architecture in Lean, render one StableHLO graph — forward, loss, backward and optimizer fused — from proofs that the backward is the Jacobian-transpose of the forward, hand the graph to a trusted lowerer, train end to end. No Python at run time and no autograd library: the gradients are derived at codegen time, in Lean, and machine-checked over the reals.
Companion code for Verified Deep Learning with Lean 4, forthcoming from Apress (Springer Nature)
as the follow-up to Convolutional Neural Networks with Swift for TensorFlow (2021).
Current version v0.7.2 (release history) ·
Four commands, one per scale, in the order the book meets the nets, then the demos. The numbers are the book's, from the verified XLA path on one RTX 4060 Ti unless the row says otherwise; the two Imagenette side quests the book does not quote (ResNet-50, MobileNetV4) are medians of five seeds. Setup is the book's Getting started, one track per tier; the short form is
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh # Lean 4
python3 -m venv .venv && . .venv/bin/activate && pip install jax-cuda12-pjrt # the XLA plugin only (jax-rocm7-pjrt on AMD)
gcc -fPIC -O2 -shared ffi/pjrt_ffi.c -ldl -o ffi/libpjrt_ffi.so # the shim; needs nothing but libc
lake exe cache get && ./scripts/datasets/download_mnist.sh && lake run mnist # Mathlib oleans, MNIST, tier 1| tier | command | trains | the number | chapter |
|---|---|---|---|---|
| 1 | lake run mnist |
linear, MLP and CNN on MNIST, 12 epochs each (~1 min) | 92.10 · 97.81 · 98.77 % | 1 · 2 · 3 |
| 2 | lake run cifar |
the wide 8-conv net on CIFAR-10: SGD / momentum / AdamW × no-BN / BN, 40 epochs at a constant lr (~5 min) | 76.3 % — BN + momentum, median of five | 4 |
| 3 | lake run imagenette |
seven nets on Imagenette at 224², 80 epochs AdamW, book order (~6 h) | R34 89.99 (mean of five seeds) · R50 89.71 · MNv2 89.25 · MNv4-Conv-M 86.24 · B0 90.04 · ConvNeXt-T 82.27 · ViT-Tiny 68.74 % | 5 · 6 · 7 · 8 · 9 |
| 4 | lake run imagenet |
the same nets on ImageNet-1k at the paper recipes, 4× 3060 / 4060 Ti, weeks of wall-clock; bare it prints the plan and every row's estimate, start runs it |
R34 74.17 · R50 78.08 on RSB-A3 and 77.09 on the 2018 recipe · MNv2 71.12 · MNv4-Conv-M 76.68 (side quest) · B0 76.88 · ConvNeXt-T 81.30 · ViT-Tiny 72.42 % on the verified path, none more than 0.51 from its JAX reference | Track 4 |
The demos ride on the chapter nets, in the order Chapter 10 meets them — recognition, then beyond it, then the games; demos/README.md has the command, the figure and the reasoning for each.
| demo | command | the number | book |
|---|---|---|---|
| object detection | lake exe yolov1-visdrone-fpn |
VisDrone [email protected] 0.2363 — ResNet-34 + FPN at 448 | 10.2.2 |
| industrial inspection | lake exe yolov1-neudet-fpn (and yolov1-neudet448) |
NEU-DET [email protected] 0.623 with the VisDrone detector unchanged; the single 14×14 grid gets 0.607 here and 0.0391 on the drones | 10.2.3 |
| people watching | lake exe arasl-signs |
ArASL 98.62 % under the published random split, 77.94 % once each hand's frames stay together | 10.2.4 |
| agriculture | lake exe plant-leaf |
PlantVillage 99.57 % on lab leaves, 17.80 % on PlantDoc's field leaves — the CAM and an exact Shapley value say why | 10.2.5 |
| remote sensing | lake exe rs-bands |
thirteen Sentinel-2 bands as the knob: 97–98 % on EuroSAT whatever the net sees, but in the Amazon the ten-band net keeps 97.0 % where RGB drops to 87.4 (pasture recall 95 % against 74), and in the Cerrado every arm fails on the seven-class map | 10.2.6 |
| segmentation | lake exe unet-brats-r34, then brats-predict |
BraTS mIoU 0.741 — a ResNet-34 encoder under a UNet | 10.2.7 |
| language | lake exe tinygpt-shakespeare (also bigram-shakespeare) |
2.28 bits/char held-out | 10.3.1 |
| diffusion | lake exe mnist-ddpm-train, then mnist-ddpm-sample |
energy distance to MNIST 0.0067 at 50 network evaluations — ancestral DDIM, ahead of the deterministic sampler at 200 | 10.3.3 |
| physics | lake exe diffusion-2d muller_brown flow |
a flow-matching Boltzmann generator on Müller–Brown; reweighted by its own density it returns the exact well populations to the last digit | 10.3.4 |
| signal processing | lake exe gw-detect |
LIGO O3a strain: the chapter-4 CNN reaches half detection at network SNR 6.91 (false-alarm rate 10⁻²), where the matched filter needs 10.32 | 10.3.5 |
| beyond vision | lake exe nqs-ising gpt |
the transverse-field Ising ground state at N = 12: a GPT wavefunction within 3.3 × 10⁻⁶ of the exact energy | 10.3.6 |
| structure | lake exe distogram-casp train …, then predict and scripts/demos/casp16_fold.py |
CASP16: a 5.4M-parameter distogram ResNet on frozen ESM-2 3B folds 78 evaluation units to TM-score 0.646, against ESMFold's 0.778 on the same language model and the field's median model at 0.892 | 10.3.7 |
| blackjack | lake exe blackjack-dqn (blackjack-env is the environment and its exact instrument) |
Double DQN agrees with the exact blackjack policy on 188 of 200 decision states | 10.4.1 |
| Pong | lake exe pong-dqn mode=pixels k=4 (pong-env for the baselines) |
DQN from four frames on a Pong written in Lean: +15.5 points a game over three seeds, above its own six-number state twin's +13.5 and the scripted tracker's +11.2 | 10.4.2 |
| poker | lake exe deep-cfr-leduc (leduc-env for the exact instrument) |
Deep CFR on Leduc hold'em, scored by the exact best response: exploitability 0.11–0.23 chips a hand over three seeds and two readouts, against 2.37 for the uniform policy, 1.05 for an honest script and 0.0002 for CFR+ | 10.4.3 |
| tic-tac-toe | lake exe alphazero-ttt n=3 (ttt-env for the solved game) |
AlphaZero's network alone agrees with the solved game on 97.3 % of 3×3 and 99.4 % of 4×4 positions and never loses to a perfect player at either; at 5×5, four in a row, 87.4 % and unbeaten as X | 10.4.4 |
Everything else in the repository is the lab — the ablation and robustness exes, the tests, the Bestiary — the evidence behind these numbers, one level down.
Every layer's backward is proven to be the Jacobian-transpose of its forward over the exact reals
(Mathlib's fderiv), composed up to whole-network VJPs for ResNet-34, MobileNetV2,
EfficientNet-B0, ConvNeXt-T and ViT-Tiny, with zero project axioms. For every chapter net the committed
train-step render in verified_mlir/ is tied to those proofs at the denotational level: each
emitted parameter-update node denotes the certified descent step, and the tiers train on exactly those
bytes. What stays trusted is the ℝ→Float32 numerics, the per-op text printing, and the lowerer with its
runtime. The book's On Verification appendix is the full
argument, gap by gap; the dependency graph is the same
suite as a clickable DAG, and
LeanMlir/Proofs/README.md
is the file-level map, and the API docs open on the same map with every name linked.
Check them without a GPU:
lake exe cache get # Mathlib oleans, ~30 s
lake build ProofsMinimal # the smallest end-to-end tie, ~1 min
lake build Certs # every certificate CI checks (the long one)tests/comparator/run.sh re-runs Lean's kernel typechecker over the headline theorems
independently, and tests/comparator/Challenge.lean imports Mathlib and nothing else, so those
can be read and checked without reading a line of this project.
Training runs through XLA/PJRT, and every number above comes from it. IREE is the second trusted
lowerer: it is what the differential oracle lowers the Lean side through, so that agreement with the JAX
reference is evidence from two independent compilers, and each lake run tier has an
-iree twin.