Sigmoid函数的形式化分析与通用逼近定理的形式化证明
计算机科学中的逻辑
2025-12-04 v1 软件工程
摘要
本文在Isabelle/HOL高阶逻辑定理证明器中给出了Sigmoid函数的形式化分析以及通用逼近定理（UAT）的完全机械化证明。Sigmoid函数在神经网络中扮演基础角色；然而，其形式化性质，如可微性、高阶导数和极限行为，此前尚未在证明辅助工具中被全面机械化。我们给出了Sigmoid函数的严格形式化证明，证明了其单调性、光滑性和高阶导数。我们提供了UAT的构造性证明，证明了具有Sigmoid激活函数的神经网络可以在紧区间上逼近任意连续函数。我们的工作识别并弥补了Isabelle/HOL形式化证明库中的空白，并引入了关于实函数极限的更简单推理方法。通过利用定理证明进行AI验证，我们的工作增强了神经网络的可信度，并为实现经过验证且可信赖的机器学习这一更广泛目标做出了贡献。
引用
@article{arxiv.2512.03635,
title = {Formal Analysis of the Sigmoid Function and Formal Proof of the Universal Approximation Theorem},
author = {Dustin Bryant and Jim Woodcock and Simon Foster},
journal= {arXiv preprint arXiv:2512.03635},
year = {2025}
}
备注
1 figure