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 the same UNet to real medical imaging (unet-brats-train) — 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); 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). 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/

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.

Building the BraTS dataset. Brain-tumour segmentation has two public faces, and the choice between them is a reproducibility decision. 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 — a demo whose first step is “go register on Synapse” is a demo readers do not run. 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 unauthenticated S3. That is what download_brats.sh fetches — and it splits the file into parallel ranged curls, since S3 throttles per connection, taking the download from \(\sim \)3 h single-stream to \(\sim \)12 min. The cost of the choice, stated plainly: 484 volumes rather than 1,251, and numbers that are not comparable to a BraTS 2021 leaderboard — this is a real segmentation result on real medical data that any reader can reproduce, not a challenge entry.

Two preprocessing details are load-bearing. preprocess_brats.py ships a dependency-free NIfTI-1 reader (numpy only): a pip install nibabel is a reader-hostile first step under PEP 668’s externally-managed-environment lock, so the \(\sim \)40-line header parser is cross-validated against nibabel 5.4.2 on nine cases (column-major, big-endian, scl_slope/scl_inter) instead. And the 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. 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).