TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.Verification.Monotonicity

Exact monotonicity certificates #

A certificate records linear and ReLU modules using exact rational parameters. Its interpretation uses the existing Spec.Module.Chain semantics over the reals. Checking nonnegative weights is a sufficient, incomplete test for global componentwise monotonicity. Biases are unrestricted.

This checks a universal real-valued hyperproperty, not a floating-point deployment guarantee or a CROWN certificate. It does not enumerate activation regions.

source
def NN.Verification.Monotonicity.PreservesOrder {α : Type} [TorchLean.Storage α] [LE α] {s t : Spec.Shape} (f : TorchLean.Tensor α s → TorchLean.Tensor α t) :
Prop

Componentwise order preservation for a tensor map.

Instances For
    source
    inductive NN.Verification.Monotonicity.Certificate :
    Spec.Shape → Spec.Shape → Type

    Serializable evidence for a composition of existing linear and ReLU modules.

    Instances For
      source
      noncomputable def NN.Verification.Monotonicity.realLayer {n m : ℕ} (layer : Spec.LinearSpec ℚ n m) :
      Spec.LinearSpec ℝ n m

      Interpret exact rational layer parameters as real numbers.

      Instances For
        source
        noncomputable def NN.Verification.Monotonicity.Certificate.model {s t : Spec.Shape} :
        Certificate s t → Spec.Module.Chain ℝ s t

        The certificate's model is an ordinary TorchLean mathematical module chain.

        Instances For
          source
          def NN.Verification.Monotonicity.Certificate.rationalModel {s t : Spec.Shape} :
          Certificate s t → Spec.Module.Chain ℚ s t

          Execute the same recorded linear/ReLU model using exact rational arithmetic.

          Instances For
            source
            def NN.Verification.Monotonicity.checkWeights {n m : ℕ} (weights : TorchLean.Tensor ℚ [m, n]) :
            Bool

            Exact executable nonnegativity check for a weight matrix.

            Instances For
              source
              def NN.Verification.Monotonicity.check {s t : Spec.Shape} :
              Certificate s t → Bool

              Accept only certificates whose linear modules have nonnegative weights.

              Instances For
                source
                theorem NN.Verification.Monotonicity.checkWeights_sound {n m : ℕ} {weights : TorchLean.Tensor ℚ [m, n]} (h : checkWeights weights = true) (i : Fin m) (j : Fin n) :
                0 ≤ Spec.get2 (TorchLean.Tensor.map (fun (q : ℚ) => ↑q) weights) i j

                A successful exact weight check supplies nonnegativity over the real interpretation.

                source
                theorem NN.Verification.Monotonicity.linear_preserves_order {α : Type} [TorchLean.Storage α] [CommRing α] [LinearOrder α] [IsStrictOrderedRing α] {n m : ℕ} (layer : Spec.LinearSpec α n m) (hw : ∀ (i : Fin m) (j : Fin n), 0 ≤ Spec.get2 layer.weights i j) :
                PreservesOrder (Spec.linearSpec layer)

                A linear module with nonnegative weights preserves componentwise real order.

                source
                theorem NN.Verification.Monotonicity.relu_preserves_order {α : Type} [TorchLean.Storage α] [LinearOrder α] [Zero α] (s : Spec.Shape) :
                PreservesOrder Activation.reluSpec

                ReLU preserves componentwise order at every tensor rank.

                source
                theorem NN.Verification.Monotonicity.check_sound {s t : Spec.Shape} (cert : Certificate s t) (h : check cert = true) :
                PreservesOrder cert.model.forward

                Acceptance proves global monotonicity of the recorded TorchLean model over real inputs.

                source
                theorem NN.Verification.Monotonicity.check_sound_rat {s t : Spec.Shape} (cert : Certificate s t) (h : check cert = true) :
                PreservesOrder cert.rationalModel.forward

                Acceptance also proves order preservation for the exact rational execution semantics.