This paper presents a formalized analysis of the sigmoid function and a fully mechanized proof of the Universal Approximation Theorem (UAT) in Isabelle/HOL, a higher-order logic theorem prover. The sigmoid function plays a fundamental role in neural networks; yet, its formal properties, such as differentiability, higher-order derivatives, and limit behavior, have not previously been comprehensively mechanized in a proof assistant. We present a rigorous formalization of the sigmoid function, proving its monotonicity, smoothness, and higher-order derivatives. We provide a constructive proof of the UAT, demonstrating that neural networks with sigmoidal activation functions can approximate any continuous function on a compact interval. Our work identifies and addresses gaps in Isabelle/HOL's formal proof libraries and introduces simpler methods for reasoning about the limits of real functions. By exploiting theorem proving for AI verification, our work enhances trust in neural networks and contributes to the broader goal of verified and trustworthy machine learning.

翻译：本文在Isabelle/HOL（一种高阶逻辑定理证明器）中提出了对Sigmoid函数的正式化分析以及通用逼近定理（UAT）的完全机械化证明。Sigmoid函数在神经网络中扮演着基础性角色；然而，其可微性、高阶导数及极限行为等正式性质此前尚未在证明助手中得到全面机械化处理。我们提出了Sigmoid函数的严格正式化，证明了其单调性、光滑性及高阶导数。我们提供了UAT的构造性证明，展示了具有Sigmoid激活函数的神经网络可以在紧致区间上逼近任意连续函数。我们的工作识别并解决了Isabelle/HOL正式证明库中的空白，并引入了更简洁的方法来推理实函数的极限。通过利用定理证明进行人工智能验证，我们的工作增强了对神经网络的信任，并为实现可验证且可信的机器学习这一更广泛目标做出了贡献。