Verified Deep Learning with Lean 4

A Data availability

Every dataset in this book is public, and every one except ImageNet is fetched by a script in the repository root that drops it under data/ where the trainers expect it. The table below lists each with its standard reference, homepage, and that fetch path. Four image datasets span the book’s whole range: MNIST and CIFAR-10 drive the verified-codegen chapters of Part 1 (§3, §4); Imagenette — a ten-class subset of ImageNet at \(224\times 224\) — is the ResNet-scale recipe (§5.2); and full ImageNet-1k backs the JAX-bridge runs of the larger architectures (ResNet-34, MobileNetV2, EfficientNet-B0, ConvNeXt-T, ViT-Ti).

Dataset

Abbrev.

Reference

Homepage

Path in repo

MNIST

MN

LeCun et al., 1998

yann.lecun.com/exdb/mnist

download_mnist.sh \(\to \) data/

CIFAR-10

CF10

Krizhevsky, 2009

cs.toronto.edu/ kriz/cifar.html

download_cifar.sh \(\to \) data/cifar-10/

Imagenette

IN10

Howard, 2019

github.com/fastai/imagenette

download_imagenette.sh \(\to \) data/imagenette/

ImageNet-1k

IN1K

Deng et al., 2009

image-net.org

TFDS \(\to \) JAX*

Dataset information: name, abbreviation, standard reference, homepage, and the repository script (with the on-disk path under data/) that fetches it. MNIST is pulled from the CVDF mirror (storage.googleapis.com/cvdf-datasets/mnist); the homepage above is the canonical reference. *ImageNet-1k is license-gated and not redistributable, so the repository ships no fetch script — see the build notes below.

Building the ImageNet-1k TFDS dataset. The image-net.org download is account-gated and slow; in practice the two LSVRC-2012 tarballs are most easily fetched from Academic Torrents (academictorrents.com/collection/imagenet): the training-set torrent (\(\sim \)138 GB) and the validation-set torrent (\(\sim \)6.3 GB), both Russakovsky et al. (2015). Each torrent is a single .tar: ILSVRC2012_img_train.tar is itself a tar of 1000 per-class tars (n01440764.tar, …) and ILSVRC2012_img_val.tar holds the 50,000 validation JPEGs. You never unpack them — TFDS reads the nested tars directly. Drop both files, as-is, into TFDS’s manual-download directory and let the standard builder do the rest:

# place the two tarballs (no extraction):
#   ~/tensorflow_datasets/downloads/manual/ILSVRC2012_img_train.tar
#   ~/tensorflow_datasets/downloads/manual/ILSVRC2012_img_val.tar
python -c "import tensorflow_datasets as tfds; \
           tfds.builder('imagenet2012').download_and_prepare()"

That validates, shuffles, and reshards into version 5.1.0 under ~/tensorflow_datasets/imagenet2012/5.1.0/: 1,281,167 training images across 1024 tfrecord shards (147.90 GB) and 50,000 validation images across 64 shards (6.74 GB) — the exact layout every ImageNet trainer in this book consumes. Budget disk accordingly: the raw tarballs (\(\sim \)144 GB) plus the 5.1.0 output (\(\sim \)155 GB) plus TFDS’s intermediate extraction mean you want roughly 500 GB of free space to prepare it in one pass. From there the JAX bridge does no image-loading of its own: it calls tfds.load(’imagenet2012’, split=…, data_dir=…) and streams through tfds.as_numpy, so TFDS’s tf.data pipeline — parallel shard reads, JPEG decode, prefetch, all engineered to scale — carries the loading, and we inherit that performance work for free.

Demo datasets. The demos/ trainers step past image classification into the three other task families in the book — detection, segmentation, and language — and each pulls a dataset of its own. Oxford-IIIT Pets backs both the UNet segmenter (unet-pets-train, via trimaps) and the YOLO detector (yolov1-pets-train-bootstrap, via head boxes tiled into \(2 \times 2\) mosaics); MSD Task01 (BraTS) carries segmentation to real medical imaging — four-modality brain-tumour MRI, where the thin-class collapse a Pets trimap merely tolerates becomes the entire problem (enhancing tumour is \(\sim \)0.5 % of voxels). Two trainers read it: unet-brats-train (a from-scratch UNet at native \(240 \times 240\)) and unet-brats-r34 (the ResNet-34 encoder of §10.2.3, which needs the \(224\) centre-cropped build since its stride-32 backbone does not divide 240); tiny Shakespeare — a single 1 MB character stream — is what the TinyGPT char-level transformer (tinygpt-shakespeare) trains on; and TinyStories — Eldan & Li’s synthetic short-story corpus, \(\sim \)2 GB — is its scaled-up sibling, byte-level-BPE tokenized to a deliberately small 4096-token vocabulary for the \(\sim \)8.5 M-parameter decoder-only GPT (tinystories). Detection then leaves the household frame entirely: VisDrone-DET2019 is drone-altitude imagery where the objects are the problem — a median box is \(20 \times 25\) px in the source frame, some 70 of them per image, so the single \(7\times 7\) grid that suffices for Pets head boxes collapses outright and the multi-scale FPN head of Definition 95 becomes necessary rather than decorative. MS-COCO 2017 is the standard detection benchmark alongside it, at the opposite end of the same axis (photographic scale, 80 classes, 118k training images); the repository ships its loader and the two standard subsets described below, though no trainer in this book consumes it yet. Same fetch-and-unpack story as the table above, with one extra step: each is tokenized or tiled into the trainer’s input format by the matching preprocess_*.py script before the first lake exe run.

Dataset

Abbrev.

Reference

Homepage

Path in repo

Oxford-IIIT Pets

Pets

Parkhi et al., 2012

robots.ox.ac.uk/ vgg/data/pets

download_pets.sh \(\to \) data/pets/

MSD Task01 (BraTS)

BraTS

Antonelli et al., 2022

medicaldecathlon.com

download_brats.sh \(\to \) data/brats/

tiny Shakespeare

TShk

Karpathy, 2015

github.com/karpathy/char-rnn

download_shakespeare.sh \(\to \) data/shakespeare/

TinyStories

TS

Eldan & Li, 2023

huggingface.co/datasets/roneneldan/TinyStories

download_tinystories.sh \(\to \) data/tinystories/

VisDrone-DET2019

VisD

Zhu et al., 2021

github.com/VisDrone/VisDrone-Dataset

download_visdrone.sh \(\to \) data/visdrone/

MS-COCO 2017

COCO

Lin et al., 2014

cocodataset.org

download_coco.sh \(\to \) data/coco/

The demo datasets, in the same columns as above. Each also has a preprocess_*.py step (e.g. preprocess_shakespeare.py builds train.bin/val.bin/vocab.txt) between download and training. For detection, preprocess_pets_mosaic.py tiles the Pets head boxes into class-balanced \(2 \times 2\) mosaics (data/pets_mosaic_bal/); the same download_pets.sh download feeds both the segmenter and the detector. For TinyStories, preprocess_tinystories.py trains a byte-level BPE tokenizer on a slice of the corpus and emits it in HuggingFace format (vocab.json/merges.txt) alongside the flat int32-LE token streams (train.bin/val.bin); the small vocabulary keeps the in-graph one-hot embedding and head matmuls cheap and the tokenizer auditable. The two detection sets follow the same pattern: preprocess_visdrone.py and preprocess_coco.py write the same three record formats — single-grid, single-scale anchor, and multi-scale FPN — so one set of Lean loaders and one codegen serve both. VisDrone’s official Google-Drive/Baidu links are large-file-flaky, so download_visdrone.sh pulls the byte-identical Ultralytics release-asset mirror over plain HTTPS; COCO’s own hosting needs no such workaround.

Building the BraTS dataset. BraTS 2021 proper (1,251 cases) is gated behind a free Synapse account and a signed research-use agreement, so no script can fetch it. The Medical Segmentation Decathlon’s Task01_BrainTumour is the same task from open storage: 484 labelled 4D volumes built from the BraTS 2016/2017 cases, the same four co-registered MRI modalities (FLAIR / T1w / T1gd / T2w) and the same glioma sub-regions, as a single 7.6 GB tarball over S3. Thus we have fewer volumes and numbers that are not comparable to a BraTS 2021 leaderboard — but this is also a real segmentation result on real medical data that a reader can reproduce.

Preprocessing details: preprocess_brats.py ships a dependency-free NIfTI-1 reader (numpy only) and two decisions that would silently ruin the numbers if done the obvious way: intensities are z-scored over brain voxels only (BraTS volumes are skull-stripped, so \(\sim \)83 % of each is exact zero and whole-volume statistics would crush the tissue contrast), and the train/val split is by patient, not by slice (adjacent axial slices of one brain are near-duplicates, so a slice-level split leaks memorized neighbours across the boundary). Volumes are quantized to uint8 over a \(\pm 5\sigma \) window and the C loader inverts it, matching the on-disk convention of every other dataset here.

The default build is \(240 \times 240\), BraTS’s native in-plane size, which suits a depth-4 UNet (\(240 = 16 \cdot 15\)). A stride-32 backbone needs a size divisible by 32, so unet-brats-r34 reads a second build made by preprocess_brats.py … –size 224 –seed 0 into data/brats224/. The same seed reproduces the same patient split and the same 14,415 / 2,569 slices. Note that –size crops rather than resizes: interpolating a label mask would invent classes that were never annotated, whereas a centre crop leaves intensities exact and the mask values untouched. It is also lossless here — the 8-pixel border it removes contains no brain voxels, these volumes being skull-stripped and centred. Reference: Antonelli et al., The Medical Segmentation Decathlon, Nature Communications 13, 4128 (2022), atop the underlying BraTS work (Menze et al. 2015, Bakas et al. 2017).

Building the COCO dataset. COCO is fetched from its own hosting — plain HTTPS, no account — as three zips: 19 GB of train2017 (118,287 images), 1 GB of val2017 (5,000), and 241 MB of annotations. Budget \(\sim \)45 GB to build in one pass; the zips and extracted trees can be deleted once the .bin files exist.

preprocess_coco.py derives its class map from the annotation file’s own categories list — COCO’s ids are not contiguous, and the obvious id - 1 remap mislabels 69 of the 80 classes (id 13 is ‘stop sign’; id - 1 calls it ‘parking meter’) without ever raising an error — and skips iscrowd regions, as COCO’s own evaluation does. References: Lin et al., Microsoft COCO: Common Objects in Context, ECCV (2014); Zhu et al., Detection and Tracking Meet Drones Challenge, IEEE TPAMI 43 (2021).