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
    instance LeanCert.Engine.instReprAffineConfig :
    Repr AffineConfig
    Equations
    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 LeanCert.Engine.instDecidableEqAffineConfig :
      DecidableEq 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 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.Engine.evalIntervalAffine (e : Core.Expr) (ρ : AffineEnv) (cfg : AffineConfig := { }) :
            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

              Convenience Functions #

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

              Evaluate and convert to 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
                      def LeanCert.Engine.evalDomainValidAffine (e : Core.Expr) (ρ : AffineEnv) (cfg : AffineConfig := { }) :
                      Prop

                      Domain validity for Affine evaluation. This is defined directly in terms of evalIntervalAffine 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 : ExprSupported e) (ρ : AffineEnv) (cfg : AffineConfig := { }) :
                        evalDomainValidAffine e ρ cfg

                        Domain validity is trivially true for ExprSupported 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) :
                        (evalIntervalAffine 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 = (evalIntervalAffine e ρ_affine cfg).coeffs.length) (hdom : evalDomainValidAffine e ρ_affine cfg) :
                        Core.Expr.eval ρ_real e ∈ (evalIntervalAffine 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.