Papers With

← All papers
First page of Formalized Hopfield Networks and Boltzmann Machines

Formalized Hopfield Networks and Boltzmann Machines

Matteo Cipollina, Michail Karatarakis, Freek Wiedijk

cs.LG Dec 8, 2025 · v2 cs.LO
formalization mathlib ml-theory probability
Read PDF arXiv abstract Code
TL;DR
Formalizes Hopfield networks, Boltzmann machines, and the Perron–Frobenius theorem in Lean 4 on top of Mathlib's graph theory and Markov kernels.
Abstract
Neural networks are widely used, yet their analysis and verification remain challenging. We present a Lean 4 formalization covering both deterministic and stochastic models. We first formalize Hopfield networks – recurrent networks that store patterns as stable states – and prove their convergence, and the correctness of Hebbian learning, the rule that updates parameters to encode patterns. We then turn to stochastic networks, whose probabilistic updates converge to a stationary distribution: we formalize the dynamics and learning of Boltzmann machines and prove their ergodicity – convergence to a unique stationary distribution – via a new formalization of the Perron–Frobenius theorem.
Problem

Neural network models and their learning dynamics lack machine-checked mathematical foundations, especially recurrent and stochastic models whose convergence properties are central to their theory.

Approach

A graph-based Lean 4 framework represents general neural networks, building on Mathlib's graph theory. Within it, Hopfield networks are defined with symmetric weights, threshold activations and no self-connections. Boltzmann machines are modeled as stochastic networks with Gibbs updates, using Mathlib's Markov kernel infrastructure. A new formalization of the Perron–Frobenius theorem supplies the convergence theory for stochastic matrices.

Results

The formalization proves convergence of Hopfield networks under asynchronous updates and correctness of Hebbian learning. It also proves ergodicity of Boltzmann machine dynamics, meaning convergence to a unique stationary distribution, which rests on what the authors describe as the first Lean 4 formalization of Perron–Frobenius. Most definitions are noncomputable.