Float-Guided Global Optimization

This file provides "oracle-guided" global optimization that uses fast floating-point heuristics to initialize the rigorous branch-and-bound algorithm with tight bounds.

Algorithm Overview

The key insight: finding a good upper bound early allows aggressive pruning.

1. Heuristic Phase: Use Monte Carlo sampling with hardware floats to find a candidate point x_guess that likely minimizes f.

2. Certification Phase: Convert x_guess to a tiny rational interval and rigorously evaluate f(x_guess) using interval arithmetic to get a certified upper bound U.

3. Pruning Phase: Initialize branch-and-bound with upper bound U. Any box B with lower bound L > U is immediately pruned.

Performance Impact

For typical optimization problems, this approach can prune 90%+ of the search space on the first iteration, dramatically reducing total computation.

Main definitions

• certifyCandidate - Convert a float candidate to a certified upper bound
• globalMinimizeGuided - Guided minimization using float heuristics
• globalMaximizeGuided - Guided maximization using float heuristics

Design notes

The float results are NEVER trusted directly. They only guide where to look. All bounds returned are rigorously computed using interval arithmetic.

Configuration for guided optimization

structure LeanCert.Engine.Optimization.GuidedOptConfigextends LeanCert.Engine.Optimization.GlobalOptConfig : Type

Extended configuration for guided optimization

• maxIterations : ℕ
• tolerance : ℚ
• useMonotonicity : Bool
• taylorDepth : ℕ
• heuristicSamples : ℕ

  Number of Monte Carlo samples for heuristic search

• seed : ℕ

  Random seed for reproducibility

• useGridSearch : Bool

  Use grid search in addition to Monte Carlo (good for low dimensions)

• gridPointsPerDim : ℕ

  Grid points per dimension (only if useGridSearch = true and dim ≤ 3)

instance LeanCert.Engine.Optimization.instReprGuidedOptConfig : Repr GuidedOptConfig

Equations

• LeanCert.Engine.Optimization.instReprGuidedOptConfig = { reprPrec := LeanCert.Engine.Optimization.instReprGuidedOptConfig.repr }

def LeanCert.Engine.Optimization.instReprGuidedOptConfig.repr : GuidedOptConfig → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance LeanCert.Engine.Optimization.instInhabitedGuidedOptConfig : Inhabited GuidedOptConfig

Equations

• LeanCert.Engine.Optimization.instInhabitedGuidedOptConfig = { default := { } }

Float to Rational conversion

def LeanCert.Engine.Optimization.floatToRat (f : Float) : ℚ

Convert a Float to a rational approximation. Returns a rational that is close to the float value. Note: This is approximate; the certified interval evaluation handles precision.

Equations

• LeanCert.Engine.Optimization.floatToRat f = if (f.isNaN || f.isInf) = true then 0 else have scaled := f * 1000000.0; have rounded := scaled.round.toInt64.toInt; ↑rounded / 1000000

def LeanCert.Engine.Optimization.floatEnvToRatEnv (pt : ℕ → Float) (dim : ℕ) : IntervalEnv

Convert a float environment to a rational point interval environment. Each float coordinate becomes a small interval around the rational approximation. Uses a fixed width of 1/1000000 for simplicity.

Equations

• One or more equations did not get rendered due to their size.

def LeanCert.Engine.Optimization.floatEnvToRatEnvClamped (pt : ℕ → Float) (B : Box) (width : ℚ := 1 / 1000000) : IntervalEnv

Convert a float environment to interval environment within box bounds. Clamps coordinates to stay within the box.

Equations

• One or more equations did not get rendered due to their size.

Candidate certification

def LeanCert.Engine.Optimization.certifyCandidate (e : Core.Expr) (B : Box) (pt : ℕ → Float) (cfg : GlobalOptConfig) : Core.IntervalRat

Certify a float candidate by evaluating it rigorously. Returns an interval containing the true function value at (or near) the candidate.

Equations

• LeanCert.Engine.Optimization.certifyCandidate e B pt cfg = LeanCert.Engine.evalIntervalCore e (LeanCert.Engine.Optimization.floatEnvToRatEnvClamped pt B) { taylorDepth := cfg.taylorDepth }

def LeanCert.Engine.Optimization.certifyCandidateDiv (e : Core.Expr) (B : Box) (pt : ℕ → Float) (cfg : GlobalOptConfig) : Core.IntervalRat

Certify with division support.

Equations

• One or more equations did not get rendered due to their size.

Guided optimization

def LeanCert.Engine.Optimization.globalMinimizeGuided (e : Core.Expr) (B : Box) (cfg : GuidedOptConfig := { }) : GlobalResult

Global minimization with Float guidance.

Algorithm:

1. Evaluate the whole box to get initial bounds
2. Use Monte Carlo (and optionally grid search) to find a good candidate
3. Certify the candidate to get a rigorous upper bound
4. Initialize branch-and-bound with this upper bound for early pruning

Equations

• One or more equations did not get rendered due to their size.

def LeanCert.Engine.Optimization.globalMinimizeGuidedDiv (e : Core.Expr) (B : Box) (cfg : GuidedOptConfig := { }) : GlobalResult

Global minimization with Float guidance and division support.

Equations

• One or more equations did not get rendered due to their size.

def LeanCert.Engine.Optimization.globalMaximizeGuided (e : Core.Expr) (B : Box) (cfg : GuidedOptConfig := { }) : GlobalResult

Global maximization with Float guidance.

Equations

• One or more equations did not get rendered due to their size.

def LeanCert.Engine.Optimization.globalMaximizeGuidedDiv (e : Core.Expr) (B : Box) (cfg : GuidedOptConfig := { }) : GlobalResult

Global maximization with Float guidance and division support.

Equations

• One or more equations did not get rendered due to their size.

Convenience API

def LeanCert.Engine.Optimization.minimize (e : Core.Expr) (B : Box) (maxIters : ℕ := 1000) (tolerance : ℚ := 1 / 1000) : GlobalResult

Quick guided minimization with sensible defaults

Equations

• LeanCert.Engine.Optimization.minimize e B maxIters tolerance = LeanCert.Engine.Optimization.globalMinimizeGuided e B { maxIterations := maxIters, tolerance := tolerance }

def LeanCert.Engine.Optimization.maximize (e : Core.Expr) (B : Box) (maxIters : ℕ := 1000) (tolerance : ℚ := 1 / 1000) : GlobalResult

Quick guided maximization with sensible defaults

Equations

• LeanCert.Engine.Optimization.maximize e B maxIters tolerance = LeanCert.Engine.Optimization.globalMaximizeGuided e B { maxIterations := maxIters, tolerance := tolerance }

Result inspection

def LeanCert.Engine.Optimization.GlobalResult.minInterval (r : GlobalResult) : Option Core.IntervalRat

Get the certified minimum interval from a result. Note: Returns none if lo > hi (should not happen for valid results).

Equations

• r.minInterval = if hle : r.bound.lo ≤ r.bound.hi then some { lo := r.bound.lo, hi := r.bound.hi, le := hle } else none

def LeanCert.Engine.Optimization.GlobalResult.hasConverged (r : GlobalResult) (tol : ℚ := 1 / 1000) : Bool

Check if the optimization has converged (gap is small)

Equations

• r.hasConverged tol = decide (r.bound.hi - r.bound.lo ≤ tol)

def LeanCert.Engine.Optimization.GlobalResult.gap (r : GlobalResult) : ℚ

Get the optimality gap

Equations

• r.gap = r.bound.hi - r.bound.lo