用形式化方法验证霍普菲尔德与玻尔兹曼网络的收敛性与学习正确性
Formalized Hopfield Networks and Boltzmann Machines
- 在Lean 4中形式化构建神经网络模型，涵盖确定性与随机模型
- 证明了霍普菲尔德网络在正交模式下的学习正确性与收敛性
- 首次形式化证明玻尔兹曼机的遍历性及唯一稳态分布存在性
神经网络广泛应用，但其分析与验证仍具挑战。本文在Lean 4中对神经网络进行形式化，涵盖确定性与随机模型。首先形式化霍普菲尔德网络——一种将模式存储为稳定状态的递归网络，并证明其收敛性及赫布学习规则的正确性，该规则仅适用于成对正交模式。随后研究随机网络，其更新为概率性，收敛至稳态分布。以玻尔兹曼机为例，形式化其动态过程并证明其遍历性，通过新形式化的Perron-Frobenius定理，展示其收敛至唯一稳态分布。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。