Formalized Hopfield Networks and Boltzmann Machines
cs.LG, cs.LO
Submitted: 2025-12-08
Updated: 2026-09-15
Comments: 20 pages, 3 figures, 2 tables. To appear in the proceedings of LPAR-26 (EPiC Series in Computing). v2: camera-ready version. Lean 4 development at https://github.com/mkaratarakis/HNBM
Code: https://github.com/mkaratarakis/HNBM
License: http://creativecommons.org/licenses/by/4.0/
The gist: Neural networks are widely used, yet their analysis and verification remain challenging.
Terminology
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.
Sources
Related papers
- Polynomial-Augmented Neural Networks (PANNs) with Weak Orthogonality Constraints for Enhanced Function and PDE Approximation
- AIRL-S: Unifying Reinforcement Learning and Search-Based Test-Time Scaling via Adversarial Inverse Reinforcement Learning
- Transformers as Bayesian In-Context Experimenters: Smoothness-Adaptive Efficient ATE Estimation
- Convergence issues in Relational Concept Analysis based on AOC-posets
- Beliefs Beyond Posteriors: Local-Consistency Optimisation for Bayesian Neural Networks
- Understanding Diffusion Models via Ratio-Based Function Approximation with SignReLU Networks