PGD attack on the verified MNIST MLP. Trains the 784→512→512→10 ReLU MLP on the proof-rendered SGD step, then runs PGD with genMlpPgdStep, a hand-typed StableHLO kernel that follows the formula of Proofs.mlpInputGrad (no theorem ties the kernel's text). The Lipschitz certificate is the product of the three layers' spectral norms, which is where the bound, and so the certificate, goes loose.

Spectral-norm-constrained training of the verified MNIST MLP. Trains the 784→512→512→10 net with projected SGD onto the spectral ball — after every projEvery proof-rendered steps (and once at the end) each weight Wᵢ is rescaled so its power-iteration ‖Wᵢ‖₂ estimate is ≤ c (projectSpectral) — then runs the same cert ≤ TRUE ≤ PGD sandwich. Sweeps a few caps c (plus an unconstrained baseline) so the table shows the trade: shrinking c pulls the certified L = ∏ᵢ Lᵢ (the Schatten-8 bounds, each somewhat above c) down, turning the vacuous product certificate non-vacuous — at the cost of clean accuracy. The empirical face of lipschitz_margin_certified_radius (LeanMlir/Proofs/Certificates/LipschitzCert/Basic.lean): smaller L ⇒ larger certified radius m/(√2·L). The training gradient comes from the proof-rendered train step; the projection is host-side weight rescaling, and the PGD kernel is the hand-typed genMlpPgdStep.

Generic conv-net PGD attack. Trains any packed conv net on its proof-rendered SGD step, then runs PGD with genKernel: a hand-typed StableHLO kernel that computes the input gradient dx (conv input-VJPs and maxpool select_and_scatter backs, following the backward ops of the net's <slug>_train_step.mlir); no theorem ties the kernel's text. Certificate = the conv-aware product of per-layer upper bounds (convLip for convs × denseLip for denses; ReLU and the disjoint 2×2 max-pools are 1-Lipschitz) — astronomically loose, the depth-cliff. genKernel and net.slug select the architecture (genCnnPgdStep/MNIST-CNN, genCifarPgdStep/CIFAR-CNN).

PGD attack on the verified MNIST CNN (the first conv rung).

PGD attack on the verified CIFAR-10 CNN (the deeper conv rung: 4 conv + 2 pool + 3 dense).

Spectral-norm-constrained training of the verified MNIST CNN. The CNN sibling of attackPgdSpectralMlp: projected SGD toward the spectral ball — every projEvery proof-rendered steps (and once at the end) projectSpectral caps the dense ‖Wᵢ‖₂ estimate and the conv tap-sum bound at c — then the cert ≤ TRUE ≤ PGD sandwich (PGD via genKernel, cert = the conv-aware product). Harder than the MLP: it's a k-layer product and the conv tap-sum is a loose bound, so projection over-penalizes the convs — the cert needs a tighter c (and pays more clean accuracy) than the MLP did, and certifies only at smaller radii. The honest "depth + loose conv-norm ⇒ certifying the conv net is harder." Generic over genKernel/net.slug (MNIST-CNN, CIFAR-CNN).

Spectral-norm-constrained training of the verified MNIST CNN.

Spectral-norm-constrained training of the verified CIFAR-10 CNN (7-layer product).

PGD adversarial attack on the verified linear classifier. Trains via the proof-rendered train step, then runs PGD: each PGD step's input gradient is computed on the GPU by genLinearPgdStep, a hand-typed StableHLO kernel that follows the formula dx = (softmax−onehot)·Wᵀ (no theorem ties the kernel's text). Reports clean vs L∞-PGD adversarial accuracy over an eps sweep.