Documentation

LeanCert.Examples.ML.SineApprox

Neural Network: sineNet #

This file demonstrates end-to-end verified ML:

  1. A neural network was trained in PyTorch to approximate sin(x)
  2. Weights were exported as exact rational numbers
  3. We formally verify output bounds using interval arithmetic

Key Point: Formal Verification vs Testing #

Unlike testing (which checks finitely many points), formal verification proves properties for ALL inputs in a region. This is a mathematical proof covering infinitely many inputs - not sampling.

Architecture #

Training Results #

Verification #

This file provides formal verification that the network output is bounded for all inputs in the specified domain.

source
def LeanCert.Examples.ML.SineApprox.sineNetLayer1Weights :
List (List ℚ)

Layer 1: 1 → 16

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def LeanCert.Examples.ML.SineApprox.sineNetLayer1Bias :
    List ℚ
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def LeanCert.Examples.ML.SineApprox.sineNetLayer1 :
      ML.Layer
      Equations
      Instances For
        source
        def LeanCert.Examples.ML.SineApprox.sineNetLayer2Weights :
        List (List ℚ)

        Layer 2: 16 → 1

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def LeanCert.Examples.ML.SineApprox.sineNetLayer2Bias :
          List ℚ
          Equations
          Instances For
            source
            def LeanCert.Examples.ML.SineApprox.sineNetLayer2 :
            ML.Layer
            Equations
            Instances For
              source
              def LeanCert.Examples.ML.SineApprox.sineNet :
              ML.TwoLayerNet

              The sineNet network

              Equations
              Instances For

                Well-formedness Proofs #

                source
                theorem LeanCert.Examples.ML.SineApprox.sineNetLayer1_wf :
                sineNetLayer1.WellFormed
                source
                theorem LeanCert.Examples.ML.SineApprox.sineNetLayer2_wf :
                sineNetLayer2.WellFormed
                source
                theorem LeanCert.Examples.ML.SineApprox.sineNet_wf :
                sineNet.WellFormed

                Input Domain and Output Bounds #

                source
                def LeanCert.Examples.ML.SineApprox.mkInterval (lo hi : ℚ) (h : lo ≤ hi := by norm_num) (prec : ℤ := -53) :
                Core.IntervalDyadic

                Helper to create dyadic interval

                Equations
                Instances For
                  source
                  def LeanCert.Examples.ML.SineApprox.sineNetInputDomain :
                  Engine.IntervalVector

                  Input domain

                  Equations
                  Instances For
                    source
                    def LeanCert.Examples.ML.SineApprox.sineNetOutputBounds :
                    Engine.IntervalVector

                    Computed output bounds for the entire input domain

                    Equations
                    Instances For

                      Main Verification Theorem #

                      source
                      theorem LeanCert.Examples.ML.SineApprox.mem_mkInterval {x : ℝ} {lo hi : ℚ} (hle : lo ≤ hi) (hx : ↑lo ≤ x ∧ x ≤ ↑hi) (prec : ℤ) (hprec : prec ≤ 0 := by norm_num) :
                      x ∈ mkInterval lo hi hle prec

                      Membership in mkInterval

                      source
                      theorem LeanCert.Examples.ML.SineApprox.output_bounded {x : ℝ} (hx : 0 ≤ x ∧ x ≤ 355 / 113) (i : ℕ) (hi : i < min sineNet.layer2.outputDim sineNet.layer2.bias.length) :
                      (sineNet.forwardReal [x])[i] ∈ sineNetOutputBounds[i]

                      Main Theorem: For any x in [0, π], the network output is bounded.

                      This is a formal verification certificate proving that the trained neural network's output lies within computed bounds for ALL inputs in the domain.

                      Unlike testing (which checks finitely many points), this is a mathematical proof covering infinitely many inputs.

                      What This Proves #

                      The theorem output_bounded establishes:

                      For every real number x with 0 ≤ x ≤ π: The neural network output is contained in the computed interval bounds.

                      This is verified by Lean's proof checker - a mathematical certainty, not empirical testing.

                      Applications #