Heuristic Search for Global Optimization

This file provides heuristic search methods using fast floating-point arithmetic to find good candidate points for global optimization. These candidates are used to initialize rigorous branch-and-bound algorithms with tight upper bounds, enabling early pruning of the search space.

Main definitions

• FloatBox - Float representation of a Box for fast sampling
• PRNG - Simple pseudo-random number generator
• samplePoint - Generate a random point inside a box
• findBestCandidate - Monte Carlo search for minimum
• gridSearch - Uniform grid sampling

Design notes

The heuristic results are NOT verified. They are used only to guide the search:

1. Find a candidate point with low objective value
2. Certify this point using rigorous interval arithmetic
3. Use the certified upper bound to prune the branch-and-bound tree

This "oracle-guided" approach can prune 90%+ of the search space on typical problems.

Rational to Float conversion

def LeanCert.Engine.Search.ratToFloat (q : ℚ) : Float

Convert a rational to a Float (approximate)

Equations

• LeanCert.Engine.Search.ratToFloat q = LeanCert.Engine.Search.intToFloat✝ q.num / q.den.toFloat

Float representation of boxes

structure LeanCert.Engine.Search.FloatBox : Type

Float representation of a box for fast sampling

• centers : Array Float

  Center of each dimension

• radii : Array Float

  Half-width (radius) of each dimension

instance LeanCert.Engine.Search.instReprFloatBox : Repr FloatBox

Equations

• LeanCert.Engine.Search.instReprFloatBox = { reprPrec := LeanCert.Engine.Search.instReprFloatBox.repr }

def LeanCert.Engine.Search.instReprFloatBox.repr : FloatBox → ℕ → Std.Format

Equations

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

def LeanCert.Engine.Search.boxToFloatBox (B : Optimization.Box) : FloatBox

Convert a rational Box to float representation

Equations

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

def LeanCert.Engine.Search.FloatBox.dim (fb : FloatBox) : ℕ

Dimension of a float box

Equations

• fb.dim = fb.centers.size

Pseudo-Random Number Generator

structure LeanCert.Engine.Search.PRNG : Type

Simple Linear Congruential Generator (LCG) for reproducible randomness. Parameters from Numerical Recipes: a = 1664525, c = 1013904223, m = 2³²

• state : UInt64

def LeanCert.Engine.Search.instReprPRNG.repr : PRNG → ℕ → Std.Format

Equations

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

instance LeanCert.Engine.Search.instReprPRNG : Repr PRNG

Equations

• LeanCert.Engine.Search.instReprPRNG = { reprPrec := LeanCert.Engine.Search.instReprPRNG.repr }

def LeanCert.Engine.Search.PRNG.new (seed : ℕ := 12345) : PRNG

Create a PRNG with given seed

Equations

• LeanCert.Engine.Search.PRNG.new seed = { state := seed.toUInt64 }

def LeanCert.Engine.Search.PRNG.nextUnit (rng : PRNG) : Float × PRNG

Generate next random number in [0, 1) and updated PRNG

Equations

• rng.nextUnit = (((1664525 * rng.state + 1013904223) % 4294967296).toFloat / UInt64.toFloat 4294967296, { state := (1664525 * rng.state + 1013904223) % 4294967296 })

def LeanCert.Engine.Search.PRNG.next (rng : PRNG) : Float × PRNG

Generate next random number in [-1, 1] and updated PRNG

Equations

• rng.next = match rng.nextUnit with | (u, rng') => (2.0 * u - 1.0, rng')

def LeanCert.Engine.Search.PRNG.nextN (rng : PRNG) (n : ℕ) : Array Float × PRNG

Generate n random numbers in [-1, 1]

Equations

• rng.nextN n = LeanCert.Engine.Search.PRNG.nextN.loop n #[] rng

def LeanCert.Engine.Search.PRNG.nextN.loop (i : ℕ) (acc : Array Float) (r : PRNG) : Array Float × PRNG

Equations

• LeanCert.Engine.Search.PRNG.nextN.loop 0 acc r = (acc, r)
• LeanCert.Engine.Search.PRNG.nextN.loop k.succ acc r = match r.next with | (v, r') => LeanCert.Engine.Search.PRNG.nextN.loop k (acc.push v) r'

Sampling methods

def LeanCert.Engine.Search.samplePoint (fb : FloatBox) (rng : PRNG) : (ℕ → Float) × PRNG

Generate a random point inside a float box

Equations

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

def LeanCert.Engine.Search.samplePoints (fb : FloatBox) (rng : PRNG) (n : ℕ) : Array (ℕ → Float) × PRNG

Generate n random points inside a float box

Equations

• LeanCert.Engine.Search.samplePoints fb rng n = LeanCert.Engine.Search.samplePoints.loop fb n #[] rng

def LeanCert.Engine.Search.samplePoints.loop (fb : FloatBox) (i : ℕ) (acc : Array (ℕ → Float)) (r : PRNG) : Array (ℕ → Float) × PRNG

Equations

• LeanCert.Engine.Search.samplePoints.loop fb 0 acc r = (acc, r)
• LeanCert.Engine.Search.samplePoints.loop fb k.succ acc r = match LeanCert.Engine.Search.samplePoint fb r with | (pt, r') => LeanCert.Engine.Search.samplePoints.loop fb k (acc.push pt) r'

def LeanCert.Engine.Search.FloatBox.center (fb : FloatBox) : ℕ → Float

Get the center point of a float box

Equations

• fb.center i = fb.centers.getD i 0.0

Monte Carlo Minimization

def LeanCert.Engine.Search.findBestCandidate (e : Core.Expr) (B : Optimization.Box) (samples : ℕ := 100) (seed : ℕ := 12345) : (ℕ → Float) × Float

Heuristic Minimizer using Monte Carlo sampling. Samples n points using Float arithmetic and returns the best candidate found.

This is surprisingly effective for finding the "basin of attraction" of the global minimum, especially in high dimensions where grid search is infeasible.

Equations

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

def LeanCert.Engine.Search.findBestCandidate.loop (e : Core.Expr) (fb : FloatBox) (i : ℕ) (rng : PRNG) (bestVal : Float) (bestPt : ℕ → Float) : (ℕ → Float) × Float

Equations

• One or more equations did not get rendered due to their size.
• LeanCert.Engine.Search.findBestCandidate.loop e fb 0 rng bestVal bestPt = (bestPt, bestVal)

def LeanCert.Engine.Search.findTopCandidates (e : Core.Expr) (B : Optimization.Box) (samples : ℕ := 100) (k : ℕ := 5) (seed : ℕ := 12345) : Array ((ℕ → Float) × Float)

Find multiple good candidates (for multi-start local search). Returns the k best distinct points found during sampling.

Equations

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

def LeanCert.Engine.Search.findTopCandidates.collectSamples (e : Core.Expr) (fb : FloatBox) (i : ℕ) (rng : PRNG) (acc : Array ((ℕ → Float) × Float)) : Array ((ℕ → Float) × Float)

Equations

• One or more equations did not get rendered due to their size.
• LeanCert.Engine.Search.findTopCandidates.collectSamples e fb 0 rng acc = acc

Grid Search

def LeanCert.Engine.Search.gridSearch (e : Core.Expr) (B : Optimization.Box) (pointsPerDim : ℕ := 10) : (ℕ → Float) × Float

Uniform grid search over a box. Samples a regular grid with pointsPerDim points along each dimension. Total samples = pointsPerDim^dim, so use sparingly for high dimensions.

Equations

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

Combined Strategy

def LeanCert.Engine.Search.hybridSearch (e : Core.Expr) (B : Optimization.Box) (gridPoints : ℕ := 5) (mcSamples : ℕ := 50) (seed : ℕ := 12345) : (ℕ → Float) × Float

Hybrid search combining grid and Monte Carlo. First does a coarse grid search, then refines around the best point with Monte Carlo.

Equations

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