Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Formal Analysis of the Sigmoid Function and Formal Proof of the Universal Approximation Theorem

Dustin Bryant, Jim Woodcock, Simon Foster

TL;DR

The paper tackles the problem of formalizing the expressive power of neural networks with sigmoidal activation by producing a fully mechanized, constructive proof of the Universal Approximation Theorem in Isabelle/HOL. It builds a reusable theory of the sigmoid, including a closed-form $n$-th derivative via Stirling numbers, and introduces a practical ε–N style limit framework to support rigorous real-analysis reasoning. The main contributions are a machine-checked UAT and an accompanying sigmoidal calculus that extends formal verification tools for AI, enabling executable witnesses and integration into verified AI pipelines. The work strengthens the foundations of trustworthy AI by bridging symbolic and subsymbolic methods and providing reusable formal libraries for future research.

Abstract

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.

Formal Analysis of the Sigmoid Function and Formal Proof of the Universal Approximation Theorem

TL;DR

The paper tackles the problem of formalizing the expressive power of neural networks with sigmoidal activation by producing a fully mechanized, constructive proof of the Universal Approximation Theorem in Isabelle/HOL. It builds a reusable theory of the sigmoid, including a closed-form -th derivative via Stirling numbers, and introduces a practical ε–N style limit framework to support rigorous real-analysis reasoning. The main contributions are a machine-checked UAT and an accompanying sigmoidal calculus that extends formal verification tools for AI, enabling executable witnesses and integration into verified AI pipelines. The work strengthens the foundations of trustworthy AI by bridging symbolic and subsymbolic methods and providing reusable formal libraries for future research.

Abstract

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.

Paper Structure

This paper contains 15 sections, 2 theorems, 8 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Contributions
  3. Significance: Why read this paper?
  4. Paper organization.
  5. Related Work
  6. Universal Approximation.
  7. Formal Methods and Verified ML.
  8. Activation Functions and Verified AI.
  9. Formalizing the Sigmoid Function
  10. Core Definition and Basic Properties
  11. Formal proof of sigma
  12. Limit Behaviors and Other Results
  13. A Formal Approach to Limits in Isabelle/HOL: Equivalence with the Classical ε–N Definition
  14. The Universal Approximation Theorem
  15. Conclusion

Key Result

lemma 1

Sigmoidal Uniform Approximation [Costarelli and Spigler] Let $x_0, x_1, \dots, x_N \in \mathbb{R}$, $N \in \mathbb{N}^+$, be fixed. For every $\varepsilon, h > 0$, there exists $\overline{w} := \overline{w}(\varepsilon, h) > 0$ such that for every $w \geq \overline{w}$ and $k = 0,1, \dots, N$, we ha

Figures (1)

  • Figure 1: Sigmoid Function

Theorems & Definitions (2)

  • lemma 1
  • theorem 1: Uniform Approximation by Sigmoidal Functions CostarelliS2013