Documentation

LeanCert.Engine.IntervalEvalAffine

Affine Arithmetic Expression Evaluator #

This module provides expression evaluation using Affine Arithmetic (AA). Affine arithmetic tracks correlations between variables, solving the "dependency problem" that causes interval arithmetic to over-approximate.

Main definitions #

Performance #

For expressions with repeated variables:

Affine arithmetic gives 50-90% tighter bounds for many real-world expressions, especially in neural network verification where the same inputs flow through multiple paths.

Limitations #

Some transcendental functions (sin, cos, atan) fall back to interval arithmetic because affine approximations aren't yet implemented.

Configuration #

source
structure LeanCert.Engine.AffineConfig :
Type

Configuration for Affine evaluation.

  • taylorDepth - Number of Taylor terms for transcendental functions
  • maxNoiseSymbols - Maximum noise symbols before consolidation (0 = unlimited)
  • taylorDepth : ℕ

    Number of Taylor series terms for transcendental functions

  • maxNoiseSymbols : ℕ

    Max noise symbols before consolidation (0 = no limit)

Instances For
    source
    def LeanCert.Engine.instReprAffineConfig.repr :
    AffineConfig → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[instance_reducible]
      instance LeanCert.Engine.instReprAffineConfig :
      Repr AffineConfig
      Equations
      source
      def LeanCert.Engine.instDecidableEqAffineConfig.decEq (x✝ x✝¹ : AffineConfig) :
      Decidable (x✝ = x✝¹)
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[instance_reducible]
        instance LeanCert.Engine.instDecidableEqAffineConfig :
        DecidableEq AffineConfig
        Equations
        source
        @[instance_reducible]
        instance LeanCert.Engine.instInhabitedAffineConfig :
        Inhabited AffineConfig
        Equations

        Variable Environment #

        source
        @[reducible, inline]
        abbrev LeanCert.Engine.AffineEnv :
        Type

        Variable assignment as Affine forms

        Equations
        Instances For
          source
          def LeanCert.Engine.toAffineEnv (intervals : List Core.IntervalRat) :
          AffineEnv

          Create an affine environment from rational intervals.

          Each variable gets a unique noise symbol to track correlations.

          Equations
          Instances For

            Main Evaluator #

            source
            def LeanCert.Internal.Affine.evalUnchecked (e : Core.Expr) (ρ : Engine.AffineEnv) (cfg : Engine.AffineConfig := { }) :
            Engine.Affine.AffineForm

            Evaluate expression using Affine Arithmetic.

            This function recursively evaluates an expression, using:

            • Exact affine operations for linear functions (add, sub, neg, scale)
            • Controlled approximations for nonlinear functions (mul, sq)
            • Interval fallbacks for unsupported transcendentals (sin, cos, atan)

            The result is an AffineForm that can be converted to an interval via toInterval, typically giving tighter bounds than pure interval arithmetic.

            Equations
            Instances For
              source
              def LeanCert.Engine.evalIntervalAffine? (e : Core.Expr) (ρ : AffineEnv) (cfg : AffineConfig := { }) :
              Option Affine.AffineForm

              Strict affine evaluator.

              This variant returns none for operations that the legacy evaluator handles by returning default or a huge fallback interval. All expression constructors are implemented here; none means that a partial operation's domain could not be proved for the supplied interval.

              Equations
              Instances For
                source
                @[irreducible]
                def LeanCert.Engine.diagnoseEvalIntervalAffineFailure (e : Core.Expr) (ρ : AffineEnv) (cfg : AffineConfig := { }) :
                EvalError

                Diagnose the first strict affine evaluation failure.

                Equations
                Instances For
                  source
                  def LeanCert.Engine.evalIntervalAffineChecked (e : Core.Expr) (ρ : AffineEnv) (cfg : AffineConfig := { }) :
                  EvalResult Affine.AffineForm

                  Checked affine evaluator with structured domain errors.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    def LeanCert.Engine.evalAffineToInterval? (e : Core.Expr) (ρ : AffineEnv) (cfg : AffineConfig := { }) :
                    Option Core.IntervalRat

                    Strictly evaluate and convert to an interval.

                    Equations
                    Instances For
                      source
                      def LeanCert.Engine.checkUpperBoundAffine (e : Core.Expr) (ρ : AffineEnv) (bound : ℚ) (cfg : AffineConfig := { }) :
                      Bool

                      Check if expression is bounded above

                      Equations
                      Instances For
                        source
                        def LeanCert.Engine.checkLowerBoundAffine (e : Core.Expr) (ρ : AffineEnv) (bound : ℚ) (cfg : AffineConfig := { }) :
                        Bool

                        Check if expression is bounded below

                        Equations
                        Instances For

                          Correctness Theorem #

                          source
                          def LeanCert.Engine.envMemAffine (ρ_real : ℕ → ℝ) (ρ_affine : AffineEnv) (eps : Affine.AffineForm.NoiseAssignment) :
                          Prop

                          Environment membership: real value is represented by the affine form

                          Equations
                          Instances For
                            source
                            theorem LeanCert.Engine.evalIntervalAffine?_correct (e : Core.Expr) (ρ_real : ℕ → ℝ) (ρ_affine : AffineEnv) (eps : Affine.AffineForm.NoiseAssignment) (hvalid : Affine.AffineForm.validNoise eps) (hρ : envMemAffine ρ_real ρ_affine eps) (cfg : AffineConfig := { }) (result : Affine.AffineForm) (hsuccess : evalIntervalAffine? e ρ_affine cfg = some result) :
                            result.mem_affine eps (Core.Expr.eval ρ_real e)

                            A successful strict affine evaluation represents the true value.

                            Unlike the legacy total evaluator, success itself discharges every partial domain condition. Operations without a dedicated affine linearization use the proved interval fallback and therefore remain sound while losing correlation.

                            source
                            theorem LeanCert.Engine.evalIntervalAffineChecked_correct (e : Core.Expr) (ρ_real : ℕ → ℝ) (ρ_affine : AffineEnv) (eps : Affine.AffineForm.NoiseAssignment) (hvalid : Affine.AffineForm.validNoise eps) (hρ : envMemAffine ρ_real ρ_affine eps) (cfg : AffineConfig := { }) (result : Affine.AffineForm) (hsuccess : evalIntervalAffineChecked e ρ_affine cfg = Except.ok result) :
                            result.mem_affine eps (Core.Expr.eval ρ_real e)

                            Successful checked affine evaluation is sound for every expression.

                            source
                            def LeanCert.Engine.evalDomainValidAffine (e : Core.Expr) (ρ : AffineEnv) (cfg : AffineConfig := { }) :
                            Prop

                            Domain validity for Affine evaluation. This is defined directly in terms of LeanCert.Internal.Affine.evalUnchecked to ensure compatibility. For log, we require the argument's toInterval to have positive lower bound.

                            Equations
                            Instances For
                              source
                              theorem LeanCert.Engine.evalDomainValidAffine_of_ExprSupported {e : Core.Expr} (hsupp : ADSupported e) (ρ : AffineEnv) (cfg : AffineConfig := { }) :
                              evalDomainValidAffine e ρ cfg

                              Domain validity is trivially true for ADSupported expressions (which exclude log).

                              source
                              theorem LeanCert.Engine.evalIntervalAffine_correct (e : Core.Expr) (hsupp : ExprSupportedCore e) (ρ_real : ℕ → ℝ) (ρ_affine : AffineEnv) (eps : Affine.AffineForm.NoiseAssignment) (hvalid : Affine.AffineForm.validNoise eps) (hρ : envMemAffine ρ_real ρ_affine eps) (cfg : AffineConfig := { }) (hdom : evalDomainValidAffine e ρ_affine cfg) :
                              (Internal.Affine.evalUnchecked e ρ_affine cfg).mem_affine eps (Core.Expr.eval ρ_real e)

                              Correctness theorem for Affine interval evaluation.

                              If all input variables are represented by their affine forms (via noise assignment eps), then the real evaluation of the expression is represented by the affine result.

                              This proves soundness: the affine form always contains the true value.

                              Note: Requires valid noise assignment and domain validity for log. Some transcendental cases (sin, cos, pi) use interval fallback and have separate soundness via interval bounds.

                              source
                              theorem LeanCert.Engine.evalIntervalAffine_toInterval_correct (e : Core.Expr) (hsupp : ExprSupportedCore e) (ρ_real : ℕ → ℝ) (ρ_affine : AffineEnv) (eps : Affine.AffineForm.NoiseAssignment) (hvalid : Affine.AffineForm.validNoise eps) (hρ : envMemAffine ρ_real ρ_affine eps) (cfg : AffineConfig := { }) (hlen : List.length eps = (Internal.Affine.evalUnchecked e ρ_affine cfg).coeffs.length) (hdom : evalDomainValidAffine e ρ_affine cfg) :
                              Core.Expr.eval ρ_real e ∈ (Internal.Affine.evalUnchecked e ρ_affine cfg).toInterval

                              Corollary: The interval produced by toInterval contains the true value.

                              This is the key result for optimization: if we compute an affine form and convert to an interval, the interval is guaranteed to contain the true value.