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.3).

  • 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), and 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, so 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), which is 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 carries the loading (parallel shard reads, JPEG decode, prefetch, all engineered to scale), and we inherit that performance work for free.

How the ImageNet numbers are validated. Every top-1 and top-5 in this book follows the validation protocol of timm’s “ResNet Strikes Back” work, which is the reference the ImageNet recipes are ported from, so that a number here and a number there are answers to the same question. Concretely, four things are matched, and each was checked against timm rather than assumed:

  • The denominator is all 50,000 validation images. This is worth stating because it moved: the loaders previously took drop_remainder=True on the validation split and scored \(49{,}920\), discarding \(80\) images. A top-1 over a different denominator is not an error bar, it is a different measurement.

  • The centre-crop ratio is read from timm’s own model configuration, not from a global default. resnet50.a1_in1k, a2_in1k and a3_in1k all resolve crop_pct \(= 0.95\); the \(2018\) torchvision weights (tv_in1k) resolve \(0.875\). Both values appear in this book, attached to the recipe each belongs to.

  • The field of view is identical. We decode a centred square of side \(\mathrm{crop\_ pct} \cdot \min (h,w)\) and resize it to the evaluation resolution; timm resizes the whole image so its shorter side is \(\mathrm{img\_ size}/\mathrm{crop\_ pct}\) and then centre-crops. The two orders end on the same pixels, and the ordering itself is measured at \(0.02\)–\(0.04\) points.

  • Top-5 is the true label’s rank, matching the reference’s own \(\sum \mathbb {1}[\ell _i {\gt} \ell _y] {\lt} 5\), and the train/test resolution split is the recipe’s (RSB-A3 trains at \(160\) and evaluates at \(224\)).

  • The resampler is timm’s. Validation resizes the whole image so its shorter side is \(\mathrm{img\_ size}/\mathrm{crop\_ pct}\) and only then centre-crops, which is timm’s order rather than the Google/TPU “Inception” crop-then-resize; and both that resize and the training RandomResizedCrop run antialiased, because PIL antialiases when downscaling and tf.image.resize does not by default. The two have to move together: a network partly fits the aliasing of the resampler it trained under, so matching only the evaluation side would be worse than matching neither. Antialiased tf.image.resize agrees with PIL to a mean \(|\Delta |\) of \(0.30\) of \(255\), flat across the whole range of downscale ratios ImageNet’s validation set spans.

Demo datasets. The demos/ trainers step past image classification into the three other task families in the book, which are detection, segmentation and language, and each pulls a dataset of its own:

  • MSD Task01 (BraTS) is the segmentation dataset. It is four-modality brain-tumour MRI, and the thin-class collapse is the whole problem rather than a nuisance (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.

  • TinyStories, Eldan & Li’s synthetic short-story corpus at \(\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).

  • VisDrone-DET2019 is where detection leaves the household frame entirely. It 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 a single \(7\times 7\) grid 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

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 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), and 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, and we also have 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, because 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, because 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, because 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, and skips iscrowd regions as COCO’s own evaluation does. It reads the list because COCO’s ids are not contiguous, and the obvious id - 1 remap mislabels 69 of the 80 classes without ever raising an error (id 13 is ‘stop sign’, which id - 1 calls ‘parking meter’). 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).