形式化的 Hopfield 网络与 Boltzmann 机
机器学习
2025-12-09 v1 计算机科学中的逻辑
摘要
神经网络虽被广泛应用，但其分析与验证仍具挑战性。本文提出一种基于 Lean 4 的神经网络形式化方法，涵盖确定性与随机模型。我们首先形式化 Hopfield 网络，即一种将模式存储为稳定状态的循环网络。我们证明了收敛性以及 Hebbian 学习的正确性——该训练规则通过更新网络参数来编码模式，此处限于成对正交模式的情形。随后我们考虑随机网络，其更新具有概率性且收敛至一个平稳分布。作为典型示例，我们形式化了 Boltzmann 机的动力学，并利用 Perron-Frobenius 定理的新形式化证明了其遍历性，展示了向唯一平稳分布的收敛。
引用
@article{arxiv.2512.07766,
title = {Formalized Hopfield Networks and Boltzmann Machines},
author = {Matteo Cipollina and Michail Karatarakis and Freek Wiedijk},
journal= {arXiv preprint arXiv:2512.07766},
year = {2025}
}