Formal Analysis of the Sigmoid Function and Formal Proof of the Universal Approximation Theorem
By: Dustin Bryant, Jim Woodcock, Simon Foster
Potential Business Impact:
Proves computers can learn any task perfectly.
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.
Similar Papers
From Universal Approximation Theorem to Tropical Geometry of Multi-Layer Perceptrons
Machine Learning (Stat)
Teaches computers to draw shapes before learning.
Universal Approximation Theorem for Deep Q-Learning via FBSDE System
Machine Learning (CS)
Makes AI learn better by copying how problems are solved.
On the Mathematical Impossibility of Safe Universal Approximators
Machine Learning (CS)
Computers can't be perfectly controlled.