TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.Verification.Monotonicity.Json

JSON acceptance implies real monotonicity #

The monotonicity_v1 format records an input_dim and a nonempty layers array. Linear layers have kind = "linear", a row-major weights array and a bias array; ReLU layers have kind = "relu". Parameters are exact integer or fraction strings, never rounded JSON numbers.

The decoder constructs shape-checked certificates using TorchLean tensors. Acceptance implies global real monotonicity of the decoded model, with no external transfer-soundness premise. This format does not import ONNX or certify the CROWN JSON formats. It says nothing about a different model that an external producer may claim the document represents.

source
def NN.Verification.Monotonicity.decodeLayer (n : ℕ) (j : Lean.Json) :
Except String ((m : ℕ) × Certificate [n] [m])

Read one vector layer, checking its input dimension.

Instances For
    source
    def NN.Verification.Monotonicity.decodeLayers (n : ℕ) :
    List Lean.Json → Except String ((m : ℕ) × Certificate [n] [m])

    Read a nonempty chain; each output dimension determines the next input dimension.

    Instances For
      source
      def NN.Verification.Monotonicity.decode (j : Lean.Json) :
      Except String ((n : ℕ) × (m : ℕ) × Certificate [n] [m])

      Decode exact parameters, rejecting malformed dimensions and unsupported operations.

      Instances For
        source
        def NN.Verification.Monotonicity.acceptsJson (j : Lean.Json) :
        Bool

        The executable JSON checker: malformed documents and failed weight checks reject.

        Instances For
          source
          theorem NN.Verification.Monotonicity.acceptsJson_sound (j : Lean.Json) (h : acceptsJson j = true) :
          ∃ (n : ℕ) (m : ℕ) (cert : Certificate [n] [m]), decode j = Except.ok ⟨n, ⟨m, cert⟩⟩ ∧ PreservesOrder cert.model.forward

          Every accepted JSON document denotes a globally monotone real TorchLean model.

          source
          def NN.Verification.Monotonicity.acceptsText (source : String) :
          Bool

          Parse and check a complete JSON document, rejecting syntax errors.

          Instances For
            source
            theorem NN.Verification.Monotonicity.acceptsText_sound (source : String) (h : acceptsText source = true) :
            ∃ (j : Lean.Json) (n : ℕ) (m : ℕ) (cert : Certificate [n] [m]), Lean.Json.parse source = Except.ok j ∧ decode j = Except.ok ⟨n, ⟨m, cert⟩⟩ ∧ PreservesOrder cert.model.forward

            Text acceptance establishes monotonicity of the model decoded from that text.