TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.MLTheory.Proofs.Verification.Robustness.MlpRobustness

MLP robustness: basic analytic lemmas #

This file proves L2 Lipschitz bounds for spec-level linear layers and two-layer ReLU MLPs, with the Frobenius norm of each weight matrix as the layer constant. The general tensor-norm facts come from NN.Proofs.Analysis.Lipschitz.

References #

source
noncomputable def NN.MLTheory.Proofs.linearLayerFrobeniusBound {inDim outDim : ℕ} (layer : Spec.LinearSpec ℝ inDim outDim) :
ℝ

Frobenius-norm Lipschitz bound for a linear layer's weight matrix.

Instances For
    source
    theorem NN.MLTheory.Proofs.linearLayerFrobeniusBound_nonneg {inDim outDim : ℕ} (layer : Spec.LinearSpec ℝ inDim outDim) :
    0 ≤ linearLayerFrobeniusBound layer

    The Frobenius constant is nonnegative.

    source
    theorem NN.MLTheory.Proofs.linearLayerFrobeniusBound_pos {inDim outDim : ℕ} (layer : Spec.LinearSpec ℝ inDim outDim) (h_weights_nonzero : layer.weights ≠ TorchLean.Tensor.full [outDim, inDim] 0) :
    0 < linearLayerFrobeniusBound layer

    The Frobenius constant is positive for a nonzero weight matrix.

    source
    theorem NN.MLTheory.Proofs.linear_layer_lipschitz_bound {inDim outDim : ℕ} (layer : Spec.LinearSpec ℝ inDim outDim) (x y : TorchLean.Tensor ℝ [inDim]) :
    Proofs.tensorL2Dist (Spec.linearSpec layer x) (Spec.linearSpec layer y) ≤ linearLayerFrobeniusBound layer * Proofs.tensorL2Dist x y

    A linear layer is Lipschitz in L2 with the Frobenius norm of its weights as a valid, possibly loose, constant. The bias cancels in the difference of two outputs.

    source
    theorem NN.MLTheory.Proofs.relu_activation_lipschitz {n : ℕ} (x y : TorchLean.Tensor ℝ [n]) :
    Proofs.tensorL2Dist (Activation.reluSpec x) (Activation.reluSpec y) ≤ Proofs.tensorL2Dist x y

    ReLU is 1-Lipschitz in the L2 distance, so activations never amplify an input perturbation.

    source
    theorem NN.MLTheory.Proofs.mlp_lipschitz_frobenius {inDim hidDim outDim : ℕ} (l1 : Spec.LinearSpec ℝ inDim hidDim) (l2 : Spec.LinearSpec ℝ hidDim outDim) (x y : TorchLean.Tensor ℝ [inDim]) :
    Proofs.tensorL2Dist (Examples.mlpForward l1 l2 x) (Examples.mlpForward l1 l2 y) ≤ linearLayerFrobeniusBound l2 * linearLayerFrobeniusBound l1 * Proofs.tensorL2Dist x y

    A two-layer ReLU MLP is Lipschitz in L2, with the product of the two Frobenius constants.

    The constant is the naive product of layer norms, which is what makes it cheap: it needs no information about the input region. That is also why it is loose compared to the CROWN bounds in NN.MLTheory.CROWN, and the contrast is the reason both developments are kept.

    source
    theorem NN.MLTheory.Proofs.mlp_is_lipschitz_continuous_l2 {inDim hidDim outDim : ℕ} (l1 : Spec.LinearSpec ℝ inDim hidDim) (l2 : Spec.LinearSpec ℝ hidDim outDim) (h1_nonzero : l1.weights ≠ TorchLean.Tensor.full [hidDim, inDim] 0) (h2_nonzero : l2.weights ≠ TorchLean.Tensor.full [outDim, hidDim] 0) :
    ∃ L > 0, Robustness.Spec.IsLipschitzContinuous (fun (x : TorchLean.Tensor ℝ [inDim]) => Examples.mlpForward l1 l2 x) (fun {s : Spec.Shape} => Proofs.tensorL2Norm) (fun {s : Spec.Shape} => Proofs.tensorL2Norm) L

    Repackage mlp_lipschitz_frobenius as a robustness-spec IsLipschitzContinuous fact with a positive constant. The nonzero-weight hypotheses only make the Frobenius product positive.

    This is the form expected by the certified-robustness lemmas in NN.MLTheory.Proofs.Verification.Robustness.LipschitzCertified.