Typed Component Algebras for Simulated Annealing and Markov-Chain Monte Carlo

Abstract

Simulated annealing (SA) and fixed-temperature Markov-chain Monte Carlo (MCMC) run the same Metropolis-Hastings kernel over a tempered objective, but the variants appear as separate monolithic drivers, so improving one ingredient requires rewriting and re-verifying a whole solver. The shared kernel becomes a typed algebra of five components (objective, cooling schedule, neighborhood, move kernel, and acceptance rule) whose four local composition laws the construction checks; a single Sampler step then runs any point of the algebra. A surrogate proposal, a fitted generalized-Langevin thermostat, a quasi-Monte Carlo polish, or a noise-aware acceptance rule is implemented once and becomes available to every classical, fast, generalized, Hamiltonian, or parallel-tempered driver that shares the interface. The same typing carries the correctness artifacts: SymPy-checked reductions of Generalized SA to its Boltzmann, fast, and Metropolis limits (the reductions surfaced a sign error that had stood in the visiting-distribution literature for three decades); a TLA+ specification model-checked for four safety and two liveness properties; and a three-channel finite-precision audit showing that fixing one channel of the acceptance path does not let float16 reproduce float64 basin selection. The implementation is the open-source Rust-and-Python package anneal, with an Array-API/DLPack device boundary and a portfolio optimizer whose only argument is a budget. On the CUTEst collection under a shared work-unit budget it reaches the best observed basin on more problems than a budget-matched CMA-ES restart heuristic, while carrying the almost-sure convergence and regret guarantees that heuristic lacks. Every reported number and figure regenerates from the reproducibility package with its pinned environment.