Formalized Hopfield Networks and Boltzmann Machines

TL;DR

This paper provides a formal mathematical framework for analyzing neural networks, specifically Hopfield networks and Boltzmann machines, using Lean 4 to prove convergence, correctness, and ergodicity.

Contribution

It introduces a formalization of neural networks in Lean 4, proving key properties like convergence, correctness of Hebbian learning, and ergodicity for stochastic models.

Findings

Proved convergence and correctness of Hebbian learning for orthogonal patterns.

Formalized the dynamics of Boltzmann machines and proved their ergodicity.

Established a new formalization of the Perron-Frobenius theorem for stochastic networks.

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.