PGD attack on the verified MNIST MLP. Trains the 784→512→512→10 ReLU MLP on the proof-rendered SGD step, then runs PGD through IREE 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 K proof-rendered steps (and once at the end) each weight Wᵢ is rescaled to ‖Wᵢ‖₂ ≤ 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 global L = ∏‖Wᵢ‖₂ down (L ≤ c³), 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 through IREE 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 spectral-norm product (specNormConvTapSum for convs × specNormW for denses; ReLU/maxpool 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 onto the spectral ball — every K proof-rendered steps (and once at the end) projectSpectral caps both the dense ‖Wᵢ‖₂ 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 (L ≤ cᵏ) 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 through IREE: 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.

PGD adversarial attack (Chapter 1 linear); see VerifiedNet.attackPgd.

PGD attack on the MLP (Chapter 2); see VerifiedNet.attackPgdMlp.

PGD attack on the CNN (Chapter 3); see VerifiedNet.attackPgdCnn.

Spectral-norm-constrained MLP training study; see VerifiedNet.attackPgdSpectralMlp.

Spectral-norm-constrained CNN training study; see VerifiedNet.attackPgdSpectralCnn.

PGD attack on the CIFAR-10 CNN (the deeper conv rung); see VerifiedNet.attackPgdCifar.

Spectral-norm-constrained CIFAR training study; see VerifiedNet.attackPgdSpectralCifar.