Formal Analysis of the Sigmoid Function and Formal Proof of the Universal Approximation Theorem
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866914178682322944 |
|---|---|
| author | Bryant, Dustin Woodcock, Jim Foster, Simon |
| author_facet | Bryant, Dustin Woodcock, Jim Foster, Simon |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2512_03635 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Formal Analysis of the Sigmoid Function and Formal Proof of the Universal Approximation Theorem Bryant, Dustin Woodcock, Jim Foster, Simon Logic in Computer Science Software Engineering 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. |
| title | Formal Analysis of the Sigmoid Function and Formal Proof of the Universal Approximation Theorem |
| topic | Logic in Computer Science Software Engineering |
| url | https://arxiv.org/abs/2512.03635 |