aiqbench analysis
This paper provides a rigorous Lean 4 formalization of Hopfield networks and Boltzmann machines, mathematically proving their convergence properties and the correctness of Hebbian learning rules. By establishing ergodicity through a novel application of the Perron-Frobenius theorem, the work addresses critical gaps in verifying the theoretical foundations of these foundational neural architectures.
Formalized Hopfield Networks and Boltzmann Machines
arXiv:2512.07766v2 Announce Type: replace 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 \emph{unique} stationary distribution -- via a new formalization of the Perron--Frobenius theorem.
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 \emph{unique} stationary distribution -- via a new formalization of the Perron--Frobenius theorem.
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 this https URL
Machine Learning (cs.LG); Logic in Computer Science (cs.LO)
arXiv:2512.07766 [cs.LG]
(or arXiv:2512.07766v2 [cs.LG] for this version)
Full text under the publisher's open licence · 142 words
Related coverage
The General Theory of Localization Methods
arXiv · Sep 14, 2026
A Restricted Boltzmann Machine with Quantum-State Visible Units
arXiv · Sep 18, 2026
Safe-by-Design Learning via Energy-based Neural Networks
arXiv · Sep 30, 2026
Generative AI for Validating Physics Laws
arXiv · Aug 27, 2026