論文の概要: Formal Analysis of the Sigmoid Function and Formal Proof of the Universal Approximation Theorem

• arxiv url: http://arxiv.org/abs/2512.03635v1
• Date: Wed, 03 Dec 2025 10:16:02 GMT
• ステータス: 情報取得中
• システム内更新日: 2025-12-04 12:09:11.94057
• Title: Formal Analysis of the Sigmoid Function and Formal Proof of the Universal Approximation Theorem
• Title（参考訳）: 普遍近似理論のシグモイド関数と形式証明の形式的解析
• Authors: Dustin Bryant, Jim Woodcock, Simon Foster,
• Abstract要約: 我々はシグモイド関数の形式化を示し、その単調性、滑らか性、高階微分を証明した。 本稿では、シグモダルアクティベーション関数を持つニューラルネットワークが、任意の連続関数をコンパクトな間隔で近似できることを示すユニバーサル近似定理の構成的証明を提案する。 我々の研究はニューラルネットワークの信頼性を高め、検証され信頼性の高い機械学習というより広い目標に貢献する。
• 参考スコア（独自算出の注目度）: 0.2599882743586163
• License:
• 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.
• Abstract（参考訳）: 本稿では、高階論理定理証明器であるIsabelle/HOLにおけるシグモイド関数の形式化解析と普遍近似定理(UAT)の完全機械化証明について述べる。 シグモイド関数はニューラルネットワークにおいて基本的な役割を担っているが、その形式的特性、例えば微分可能性、高次微分、極限挙動は、以前は証明アシスタントで包括的に機械化されていなかった。 我々はシグモイド関数の厳密な形式化を示し、その単調性、滑らか性、高階微分を証明した。 我々は、Sigmoidal activation関数を持つニューラルネットワークが、任意の連続関数をコンパクトな間隔で近似できることを示す、UATの構成的証明を提供する。 本研究は,Isabelle/HOLの形式的証明ライブラリのギャップを特定し,実際の関数の限界を推論するシンプルな手法を提案する。 AI検証のための定理証明を活用することで、ニューラルネットワークの信頼性を高め、検証と信頼性のある機械学習というより広範な目標に貢献する。

関連論文リスト

• ProofNet++: A Neuro-Symbolic System for Formal Proof Verification with Self-Correction [0.0]
  本稿では,自動定理証明を強化するニューロシンボリックフレームワークProofNet++を提案する。 ProofNet++は,従来のモデルよりも検証精度,正確性,形式的妥当性を著しく向上することを示す。
  論文  参考訳（メタデータ） (2025-05-30T05:44:34Z)
• DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning [67.93945726549289]
  DeepTheoremは、数学的推論を強化するために自然言語を活用する包括的な非公式な定理証明フレームワークである。 DeepTheoremには、121Kの高品質なIMOレベルの非公式な定理と証明からなる大規模なベンチマークデータセットが含まれている。 我々は、証明された定理の変種を利用して堅牢な数学的推論を動機付けることによって、非公式な定理証明に適した新しい強化学習戦略(RL-Zero)を考案する。
  論文  参考訳（メタデータ） (2025-05-29T17:59:39Z)
• Universal Approximation Theorem for Deep Q-Learning via FBSDE System [2.1756081703276]
  本稿では,Deep Q-Networks (DQN) のクラスに対する普遍近似理論を確立する。 関数空間上で作用するニューラル演算子として考えられたディープ残留ネットワークの層がベルマン作用素の作用を近似できることを示す。
  論文  参考訳（メタデータ） (2025-05-09T13:11:55Z)
• ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
  本稿では,LLMに様々な粒度で自動化手法を付加するProofAugを提案する。 本手法は,オープンソースのDeep-math-7bベースモデルとIsabelle証明アシスタントを用いて,MiniF2Fベンチマークで検証した。 また、ProofAugのLean 4バージョンを実装し、Kimina-Prover-seek-Distill-1.5Bのパス@1のパフォーマンスを44.3%から50.4%に改善します。
  論文  参考訳（メタデータ） (2025-01-30T12:37:06Z)
• Function Approximation with Randomly Initialized Neural Networks for Approximate Model Reference Adaptive Control [0.0]
  近年の研究では、ReLUのような特殊活性化関数に対して、ランダムなアクティベーションの線形結合によって高い精度が得られることが示されている。 本稿では, 直接積分表現が知られていないアクティベーションを用いて, 対象関数の積分表現を形成する手段を提供する。
  論文  参考訳（メタデータ） (2023-03-28T18:55:48Z)
• Formalizing Piecewise Affine Activation Functions of Neural Networks in Coq [0.0]
  本稿では,Coq内のニューラルネットワークの検証に適した対話型定理証明器として,pwaアクティベーション関数の最初の形式化を提案する。 概念実証として、一般的なpwaアクティベーション関数ReLUを構築する。 私たちのフォーマル化は、自動証明が失敗する際のフォールバック証明として、ニューラルネットワーク検証のフレームワークにCoqを統合するための道を開くものです。
  論文  参考訳（メタデータ） (2023-01-30T13:53:52Z)
• Provable General Function Class Representation Learning in Multitask Bandits and MDPs [58.624124220900306]
  マルチタスク表現学習は、サンプル効率を高めるために強化学習において一般的なアプローチである。 本研究では,解析結果を一般関数クラス表現に拡張する。 バンディットと線形MDPの一般関数クラスにおけるマルチタスク表現学習の利点を理論的に検証する。
  論文  参考訳（メタデータ） (2022-05-31T11:36:42Z)
• UNIPoint: Universally Approximating Point Processes Intensities [125.08205865536577]
  学習可能な関数のクラスが任意の有効な強度関数を普遍的に近似できることを示す。 ニューラルポイントプロセスモデルであるUNIPointを実装し,各イベントの基底関数の和をパラメータ化するために,リカレントニューラルネットワークを用いた。
  論文  参考訳（メタデータ） (2020-07-28T09:31:56Z)
• Formal Synthesis of Lyapunov Neural Networks [61.79595926825511]
  本稿では,リアプノフ関数の自動合成法を提案する。 我々は,数値学習者と記号検証器が相互作用して,確実に正しいリアプノフニューラルネットワークを構築する,反例誘導方式を採用する。 提案手法は,Lyapunov関数を他の手法よりも高速かつ広い空間領域で合成する。
  論文  参考訳（メタデータ） (2020-03-19T17:21:02Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。