Formalized Hopfield Networks and Boltzmann Machines
Matteo Cipollina, Michail Karatarakis, Freek Wiedijk
cs.LG
Dec 8, 2025 · v1
TL;DR
Formalizes Hopfield networks and Boltzmann machines in Lean 4, proving convergence, Hebbian-learning correctness, and ergodicity.
Abstract
Neural networks are widely used, yet their analysis and verification remain challenging. In this work, we present a Lean 4 formalization of neural networks, covering both deterministic and stochastic models. We first formalize Hopfield networks, recurrent networks that store patterns as stable states. We prove convergence and the correctness of Hebbian learning, a training rule that updates network parameters to encode patterns, here limited to the case of pairwise-orthogonal patterns. We then consider stochastic networks, where updates are probabilistic and convergence is to a stationary distribution. As a canonical example, we formalize the dynamics of Boltzmann machines and prove their ergodicity, showing convergence to a unique stationary distribution using a new formalization of the Perron-Frobenius theorem.
Problem
Neural networks are widely used but their formal analysis and verification remain challenging. No prior work has formalized both deterministic recurrent networks and stochastic networks with convergence guarantees in a proof assistant.
Approach
The authors present a Lean 4 formalization covering Hopfield networks and Boltzmann machines. For Hopfield networks, they prove convergence and correctness of Hebbian learning (for pairwise-orthogonal patterns). For Boltzmann machines, they formalize stochastic dynamics and prove ergodicity using a new Lean 4 formalization of the Perron-Frobenius theorem, establishing convergence to a unique stationary distribution.
Results
The formalization covers both deterministic (Hopfield) and stochastic (Boltzmann) neural network models with machine-checked proofs of convergence. The Perron-Frobenius theorem is formalized in Lean 4 for the first time as part of this work, enabling the ergodicity proof for Boltzmann machines.
