Mechanized Mathematics and Its Applications, Works in Progress

Multilayer Perceptron (Yamazaki H.,et al.)Regular Paper

階層型ニューラルネットワークの形式化について
On the Formalizations for Multilayer Perceptron
山崎 浩 1,* , 師玉 康成 2
Hiroshi Yamazaki1,* , Yasunari Shidama2
1 長野県工科短期大学校, 長野県上田市下之郷 813-8
1 Nagano Prefecture Institute of Technology. 813-8, Shimonogho Ueda, Nagano, Japan
2 長野県軽井沢町
2 Karuizawa, Nagano, Japan
1 yamazaki@cse.pit-nagano.ac.jp
2 shidama@cs.shinshu-u.ac.jp* Corresponding Author: yamazaki@cse.pit-nagano.ac.jp
Proof checked by Mizar Version: 8.1.10 and MML Version: 5.64.1388
Received: December 10, 2020. Accepted: April 30, 2021.

Abstract
In this paper, the hierarchical neural networks is formalized by ﬁnite sequence of
mappings. The input-output map of the this neural network is represented as a composite map of this ﬁnite sequence. The compactness of the set of these composite map
is proved by applying Ascoli-Arzela’s theorem.

1

はじめに
本稿では筆者らが作成している階層型ニューラルネットワークの形式化表現について

途中経過を報告する．この形式化による階層型ニューラルネットワークは有次元空間上の写像の有限列として表現される．また，このニューラルネットワークによる入出力の関係
は，それを定義する写像の有限列の直列的な合成関数として表現される．Rosenblatt のPerceptron [1] 以降，階層型ニューラルネットワークは 1986 年の Rumelhart [2] らの誤差逆伝搬法，最近の Deep Learning [3] の実用化など流行を繰り返してきた．人工知能研
究の重要な道具であり，工学的な有用性と共に，関数近似論でも興味深い課題を提供してきた．例えば Sprecher [4] および Hecht-Nielsen [5] は Kolmogorov の定理 [6](ヒルベルト

13 番問題の否定的解決) が 4 層のニューラルネットワークに適用できることを示した．また Funahashi [7] は Miyake-Irie [8] の結果を用いて，中間層の入出力関数がシグモイド関

MMA-WiP (2021), vol.3, no.4 - https://mizar-jp.org/journal/MMA-WiP/j2021.3.4 - ISSN 2434-5458 (Online)

1/12

Mechanized Mathematics and Its Applications, Works in Progress

Multilayer Perceptron (Yamazaki H.,et al.)数である 3 層ニューラルネットワークによってコンパクトな台を持つ任意の連続関数が近似できることを示した．最近では Deep Learning で中間層を増やすことにより何故学習
効果が上がるのかなど重要な未解決課題が残されている．階層型ニューラルネットワーク
は Mizar Mathematical Library(以後 MML) でも系統的な形式化表現は未だなされていない．階層型ニューラルネットワークを形式化表現しようとする場合，その一つに有向グ
ラフを用いる方法が考えられる．グラフ理論に関する MML ではグラフの位相的な性質の抽象化・一般化が行われている [9–13]．
例えば Nakamura は [13] でそれを用いた Dijkstra’s Shortest Path Algorithm の精密な形式化を行っている．しかしながら非線形関数の近似の議論など，関数系の理論の形式化にこれらを用いることは容易ではない．このため，筆者らは階層型ニューラルネット
ワークに関しての関数系の理論の形式化に使いやすい方法を意図して，形式化を進めている．

2

階層型ニューラルネットワークの形式化

2.1

写像の有限列を用いた形式化表現

周知のように階層型ニューラルネットワークは, 入力信号を与える入力層, 出力信号を出す出力層, それらの中間に配置される複数の中間層によって構成されている. 本稿では各層をベクトル値を入出力する有限次元ベクトル空間上の写像とみなし, それらの複数の写像の有限列によってニューラルネットワークを形式化する方法を報告する. このニューラルネットワークによる入出力の関係は, それを定義する写像の有限列全部の合成写像として表現される.
第 i 番目の層はそれに連結する第 i − 1 番目の層から出力される実数ベクトルを入力とし, 第 i + 1 番目の層への入力となる実数ベクトルを出力する. これは入力ベクトルが属す
る有限次元実数ベクトル空間から出力ベクトルが属する有限次元実数ベクトル空間への写像として表現できる. この第 i 番目の層を表す写像を Ni で表現する. 第 i − 1 番目の層からの出力であり同時に, 第 i 番目の層への入力である実数ベクトルが属する実数ベクトル空間の次元を ki で表す. 入出力層及び中間層の総数を n 個とすれば, 上記の各層を表す長さ n の写像の有限列 {Ni }1≤i≤n と各関数 Ni の定義域・値域である実数ベクトル空間の次元を表す長さ n + 1 の自然数の有限列 {ki }1≤i≤n+1 が下記のように与えられる.

Ni : x ∈ Rki 7→ Ni (x) ∈ Rki+1

1≤i≤n

(1)

入力層が N1 , 出力層が NN であり,

Ni2≤i≤n−1(2)が中間層である．
それらを直列に合成した写像

Nn ◦ Nn−1 ◦ · · · ◦ N2 ◦ N1

(3)が階層型ニューラルネットワークの入出力の関係を表す写像であり, k1 次元実数ベクトル
空間 Rk1 から kn+1 次元実数ベクトル空間 Rkn+1 への写像である．

MMA-WiP (2021), vol.3, no.4 - https://mizar-jp.org/journal/MMA-WiP/j2021.3.4 - ISSN 2434-5458 (Online)

2/12

Mechanized Mathematics and Its Applications, Works in Progress

Multilayer Perceptron (Yamazaki H.,et al.)

図 1. 階層型ニューラルネットワーク
上記の性質をもった写像の有限列と各写像の定義域・値域の空間の次元数の有限列を
次のように, 述語 (predicate) と属性 (attrivute) で定義した.

Listing 1. NEURONS1:def 1 def 2
deﬁnition
let n be Nat,k be FinSequence of NAT,
N be FinSequence;
pred N is Multilayer perceptron with k,nmeans:: NEURONS1:def 1
len N = n & len N + 1 = len k&
for i be Nat st 1<=i & i < len k holds
N.i is Function of REAL−NS (k.i),REAL−NS (k.(i+1));
end;
deﬁnition
let N be FinSequence;
attr N is Multilayer perceptron likemeans:: NEURONS1:def 2
ex k be FinSequence of NAT
stlen N + 1 = len k&
for i be Nat st 1<=i & i < len k holds

MMA-WiP (2021), vol.3, no.4 - https://mizar-jp.org/journal/MMA-WiP/j2021.3.4 - ISSN 2434-5458 (Online)

3/12

Mechanized Mathematics and Its Applications, Works in Progress

Multilayer Perceptron (Yamazaki H.,et al.)N.i is Function of REAL−NS (k.i),REAL−NS (k.(i+1));
end;

NEURONS1 : def 1 は自然数 n, 自然数の有限列 k と有限列 N を引数 N, k, n にもつ述語を定義している．k, N の長さがそれぞれ n + 1，n であり,N の各要素 Ni 1 ≤ i ≤ nが ki 次元実数ベクトル空間 Rki から ki+1 次元実数ベクトル空間 Rki+1 への写像であるこkiとを表す述語である. ここで√∑ REAL − NS(k.i) は ki 次元の数ベクトル空間 R でユー
i=ki 2ki
クリッドノルム ||x|| =i=1 xi , x = (x1 , x2 , · · · , xki ) ∈ R によりノルムを定義した実ノルム空間を表している [14]．

NEURONS1 : def 2 は有限列 {Ni }1≤i≤n についてこれが写像の有限列であり, 隣あった写像どうしで共有する定義域, 値域の次元数を表す自然数の有限列 {ki }1≤i≤n+1 が存在することを示す属性である.
この属性をもった写像の有限列が存在することを示すのが以下の cluster 宣言であり,mode でこの属性をもった, 型変数を Multilayer perceptron という名前で定義した.

Listing 2. cluster and mode
registration
cluster Multilayer perceptron like for FinSequence;
end;
deﬁnitionmode Multilayer perceptron
is Multilayer perceptron like FinSequence;
end;

2.2

入出力の関係を表す合成写像と再帰的定義

前節で述べたように本稿では各層をベクトル値を入出力する有限次元ベクトル空間上の写像とみなし,(1) 式の写像の有限列によってニューラルネットワークを表現する. それらを直列に合成した (3) 式の写像

Nn ◦ Nn−1 ◦ · · · ◦ N2 ◦ N1
が階層型ニューラルネットワークの入出力の関係を表す写像であり, k1 次元実数ベクトル
空間 Rk1 から kn+1 次元実数ベクトル空間 Rkn+1 への写像である. この合成写像の定義を形式化するには, 以下のように遂次構成される写像の有限列 {pi }1≤i≤n を用いる.

p 1 = N1
p2 = N2 ◦ p1
p3 = N3 ◦ p2..
.
pn = Nn ◦ pn−1(4)

これを使って記述したものが以下 NEURONS1 : def 3 である.

MMA-WiP (2021), vol.3, no.4 - https://mizar-jp.org/journal/MMA-WiP/j2021.3.4 - ISSN 2434-5458 (Online)

4/12

Mechanized Mathematics and Its Applications, Works in Progress

Multilayer Perceptron (Yamazaki H.,et al.)Listing 3. NEURONS1:def 3
deﬁnition
let n be Nat,k be FinSequence of NAT,
N be FinSequence;
assume N is Multilayer perceptron with k,n;assume len N <> 0;
func OutPutFunc(N,k,n)−> Function of REAL−NS (k.1), REAL−NS (k.(n+1))
means:: NEURONS1:def 3
ex p be FinSequencestlen p = len N & p.1 = N.1& ( for i be Nat st 1 <= i & i <len N holds
ex NN be Function of REAL−NS (k.(i+1)),REAL−NS (k.(i+2)),
pp be Function of REAL−NS (k.1),REAL−NS (k.(i+1))
st NN=N.(i+1) & pp =p.i & p.(i+1) = NN∗pp )& it = p.(len N) ;end;

上記は任意に与えられた自然数 n, 自然数の有限列 k と長さ n の写像の有限列 N でNEURONS1 : def 1 で定義された述語 N is Multilayer perceptron with k, n が成り立つもの, すなわち, 階層型ニューラルネットワークを構成するものについて上記の合成による写像を以下のように引数 N, k, n をもった Functor OutPutFunc(N, k, n) で定義している. この Functor OutPutFunc(N, k, n) の定義の正当性 (与えられた N, k, nについて定義の条件を満たす Rk1 からへの写像が一意に存在すること) の証明には (4) 式で定義される写像の有限列 {pi }1≤i≤n の一意存在を証明すればよい. 以下にその方法を証明の記述一部を抜粋しながら説明する．
有限列 {pi }1≤i≤n の存在を証明するには再帰的定義を利用する.

MML では再帰的定義は公理図式 (scheme) として RECDEF 1 などに収録されている. 本稿の形式化では以下を用いている．

Listing 4. RECDEF 1:sch 4
scheme :: RECDEF 1:sch 4
FinRecExD{D() −> non empty set,A() −> Element of D(), N() −> Nat,P[object,object,object]}:
ex p being FinSequence of D() st len p = N() & (p.1 = A() or N() = 0) &for n st 1 <= n & n < N() holds P[n,p.n,p.(n+1)]
providedfor n being Nat st 1 <= n & n < N() for x being Elementof D() ex y being Element of D() st P[n,x,y];

上記の schemeRECDEF 1 : sch 4 では, 空でない集合 D の要素の有限列 {pi }1≤i≤nの再帰的構成手続きが書かれている．これを本稿の有限列 {pi }1≤i≤n に当てはめるには,の各要素 pi が写像であることから各 pi を全て含む何らかの写像の集合を導入する必要がある. しかしながら (1) 式に示したように

Ni : x ∈ Rki 7→ Ni (x) ∈ Rki+1

1≤i≤n

各 Ni の定義域，値域は Rki ,Rki+1 であり, 各 Ni に共通の定義域，値域ではない. こ

MMA-WiP (2021), vol.3, no.4 - https://mizar-jp.org/journal/MMA-WiP/j2021.3.4 - ISSN 2434-5458 (Online)

5/12

Mechanized Mathematics and Its Applications, Works in Progress

Multilayer Perceptron (Yamazaki H.,et al.)kのため先ず {R i }1≤i≤n の合弁集合

X=

i=n
∪

Rki

i=1

を導入し, 各 Ni の定義域，値域が全てこの合弁集合 X の部分集合になっている X の中から X の中への部分関数全部の集合 PFuncs(X, X) を用いる. この PFuncs(X, X) は

PARTFUN1 : def 3 に以下のように定義されている.
Listing 5. PARTFUN1:def 3
deﬁnition
let X,Y;func PFuncs(X,Y) −> set means:: PARTFUN1:def 3
x in it iﬀ ex f being Function st x = f & dom f c= X & rng f c= Y;
end;

この X と PFuncs(X, X) を用いて式 (4) の漸化式を表す述語を記述しているのが以下の部分である.

Listing 6. PFuncs
set
X0 = { the carrier of REAL−NS (k.i)
where i is Nat : 1<=i & i <=len N+1 } ;1<=1 & 1 <=len N +1 by NAT 1:11;
then
the carrier of REAL−NS (k.1) in X0 ;thenreconsider X =union X0 as non empty set by TARSKI:def 4;
defpred P1[ Nat , object , object ]means
ex pp be PartFunc of X,X,
NN be Function of REAL−NS (k.($1+1)),REAL−NS (k.($1+2))
st pp=$2 & NN= N.($1+1) & $3=NN∗pp;

さらに schemeRECDEF 1 : sch 4 を適用するために以下の補題を証明した.

Listing 7. Lemma A3
A3: for i being Nat st 1 <= i & i < len N holds
for x being Element of PFuncs(X,X)
ex y being Element of PFuncs(X,X) st P1[i,x,y]

この補題 A3 と schemeRECDEF 1 : sch 4 を用いて式 (4) で定義した写像の有限列{pi }1≤i≤n を導入した記述が以下の部分である.
Listing 8. Lemma A16
consider p being FinSequence of PFuncs(X,X)
such that
A14: len p = len N
andA15: p.1 = N1 or len N = 0
andA16:
for i being Nat st 1 <= i & i < len N holds P1[i,p . i,p . (i + 1)]
from RECDEF 1:sch 4(A3);

MMA-WiP (2021), vol.3, no.4 - https://mizar-jp.org/journal/MMA-WiP/j2021.3.4 - ISSN 2434-5458 (Online)

6/12

Mechanized Mathematics and Its Applications, Works in Progress

Multilayer Perceptron (Yamazaki H.,et al.)

このようにして導入した写像の有限列 {pi }1≤i≤n の一意性については MML に収録されている公理図式 (scheme)RECDEF 1 : sch7 を用いている．

Listing 9. RECDEF 1:sch 7
scheme :: RECDEF 1:sch 7
FinRecUn{A() −> object, N() −> Nat, F,G() −> FinSequence,P[object,object,object]}:
F() = G()
providedfor n st 1 <= n & n < N() for x,y1,y2 being set st P[n,x,y1] & P[n,x,y2] holds y1 = y2 andlen F() = N() & (F().1 = A() or N() = 0) & for n st 1 <= n & n < N()holds P[n,F().n,F().(n+1)] andlen G() = N() & (G().1 = A() or N() = 0) & for n st 1 <= n & n < N()holds P[n,G().n,G().(n+1)];

この scheme は漸化式による有限列の構成手続きについて初期値が同じであれば構成された有限列も同じであることを帰納法によって示すものである. この scheme を使って式 (4)で定義した写像の有限列 {pi }1≤i≤n の一意性を示した記述が以下である．

Listing 10. Uniquenessdefpred P1[Nat,object,object]means
ex NN be Function of REAL−NS (k.($1+1)),REAL−NS (k.($1+2)),
pp be Function of REAL−NS (k.1),REAL−NS (k.($1+1))
st NN=N.($1+1) & pp =$2 & $3 = NN∗pp ;A34: len p1 = len N & (p1.1 = N.1 or len N = 0)
& for i be Nat st 1 <= i & i < len N holds P1[i,p1.i,p1.(i+1)] by A32;
A35: len p2 = len N & (p2.1 = N.1 or len N = 0)
& for i be Nat st 1 <= i & i < len N
holds P1[i,p2.i,p2.(i+1)] by A33;
A36: for i being Nat st 1 <= i & i <len N holds
for x, y1, y2 being set st P1[i,x,y1] & P1[i,x,y2] holds y1 = y2 ;p1=p2 from RECDEF 1:sch 7(A36,A34,A35);
hence F1=F2 by A32,A33;

3階層型ニューラルネットワークの集合
前章で各層をベクトル値を入出力する関数とみなし,(1) 式

Ni : x ∈ Rki 7→ Ni (x) ∈ Rki+11≤i≤nの関数の有限列によってニューラルネットワークを形式化した. それらを直列に合成した(3) 式の写像
Nn ◦ Nn−1 ◦ · · · ◦ N2 ◦ N1
が階層型ニューラルネットワークの入出力の関係を表す写像であり, k1 次元実数ベクトル
空間 Rk1 から kn+1 次元実数ベクトル空間 Rkn+1 への写像である. 以下のように, 自然数

n と自然数の有限列 k に対して, 定義 NEURONS1 : def 1 の条件
N is Multilayer perceptron with k, n を満たす階層型ニューラルネットワークにつ

MMA-WiP (2021), vol.3, no.4 - https://mizar-jp.org/journal/MMA-WiP/j2021.3.4 - ISSN 2434-5458 (Online)

7/12

Mechanized Mathematics and Its Applications, Works in Progress

Multilayer Perceptron (Yamazaki H.,et al.)

いて NEURONS1 : def 3 で定義された階層型ニューラルネットワークの入出力の関係を表す写像 OutPutFunc(N, k, n) の全部の集合 NEURONS(n, k) を以下のように定義した.

Listing 11. NEURONS
deﬁnition
let n be Nat,k be FinSequence of NAT;
func
NEURONS(n,k) −> Subset of
Funcs(the carrier of REAL−NS (k.1),the carrier of REAL−NS (k.(n+1)))
equals:: NEURONS1:def 4{ F where F is Function of REAL−NS (k.1),REAL−NS (k.(n+1)): ex N be FinSequence
st N is Multilayer perceptron with k,n& F = OutPutFunc(N,k,n) } ;end;

次節でこの NEURONS(n, k) の部分集合に前回報告した Ascoli-Arzelá の定理を適用する.

4

有限次元空間における写像の集合についての Ascoli-Arzelá
の定理
筆者らは, 前回, 以下の形式化した Ascoli-Arzelá の定理を報告した.

Listing 12. ASCORI:19
theorem :: ASCORI:19
for M be non empty MetrSpace,S be non empty compact TopSpace,
T be NormedLinearTopSpace,
F be non empty Subset of
R NormSpace of ContinuousFunctions(S,T),
G be Subset of Funcs(the carrier of M, the carrier of T)
st S = TopSpaceMetr(M) & T is complete & G = F
holds
Cl(F) is compact
iﬀ( for x be Point of M holds G is equicontinuous at x )&for x be Point of S,
Fx be non empty Subset of (MetricSpaceNorm T)
st Fx = {f.x where f is Function of S,T :f in F }holds(MetricSpaceNorm T) | Cl(Fx) is compact;

上記の定理で写像の値域 T が有限次元空間の場合は有界閉集合は compact 集合になるため, 以下のように簡潔な命題になる.

Listing 13. NEURONS1:27
theorem :: NEURONS1:27
for M be non empty MetrSpace,S be non empty compact TopSpace,
T be NormedLinearTopSpace
st S = TopSpaceMetr(M) & T is complete & T is ﬁnite−dimensional

MMA-WiP (2021), vol.3, no.4 - https://mizar-jp.org/journal/MMA-WiP/j2021.3.4 - ISSN 2434-5458 (Online)

8/12

Mechanized Mathematics and Its Applications, Works in Progress

Multilayer Perceptron (Yamazaki H.,et al.)& dim (T) <> 0
holds
for G be Subset of Funcs(the carrier of M, the carrier of T),
H be non empty Subset of(MetricSpaceNorm R NormSpace of ContinuousFunctions(S,T))
st G = H
holds
Cl(H) is sequentially compactiﬀ
G is equibounded & G is equicontinuous;

前章で形式化した, 自然数 n と自然数の有限列 {ki }1≤i≤n+1 に対して,
定義 NEURONS1 : def 1 の条件 N is Multilayer perceptron with k, n を満たす
写像の有限列 {Ni }1≤i≤n について以下の条件を課す.

Listing 14. LayerFunc
deﬁnition
let X,Y be RealNormSpace ;let F be Function of X,Y ;let D,K be Real ;pred F is LayerFunc D,K means:: NEURONS1:def 5( for x,y be Point of X holds ||.F.x−F.y.|| <= D∗||.x−y.|| )&( for x be Point of X holds ||.F.x.|| <= K );end;
deﬁnition
let n be Nat;
let k be FinSequence of NAT;
let D,K be Real ;let N be FinSequence;
pred N is LayerFunc Seq D,K,k,nmeans:: NEURONS1:def 6
len N = n
& N is Multilayer perceptron with k,n& for i be Nat st 1<=i & i < len kholds
ex Ni be Function of REAL−NS (k.i),REAL−NS (k.(i+1))
st N.i = Ni & Ni is LayerFunc D,K;
end;

NEURONS1 : def 5 は, 前述の Ascoli-Arzeá の定理の同程度有界性 equibounded と同程度連続性 equicontinuous に対応する. NEURONS1 : def 6 は {Ni }1≤i≤n の各層を表す写像がその条件を満たすことを表している. (1) 式のニューラルネットワークを構成する各写像 Ni は具体的には, 例えば, x = (x1 , x2 , · · · , xki ) ∈ Rki に対して

Ni (x) = (y1 , y2 , · · · , yki+1 ) ∈ Rki+1
yj = ρa (h=k∑i

aj,h · xkh − θ) 1 ≤ j ≤ ki+1

(5)
(6)

h=1

という形をしている. ここで ρa はシグモイド関数と呼ばれ,

ρa (x) =1
1 + e−ax(7)などである.a はシグモイド関数 ρa の傾斜の最大値を決めるパラメータである.

{aj,h }1≤j≤ki+1 ,1≤h≤ki

MMA-WiP (2021), vol.3, no.4 - https://mizar-jp.org/journal/MMA-WiP/j2021.3.4 - ISSN 2434-5458 (Online)

9/12

Mechanized Mathematics and Its Applications, Works in Progress

Multilayer Perceptron (Yamazaki H.,et al.)は第 i 層から第 i + 1 層への結合係数と呼ばれる．

(7) 式のシグモイド関数はリプシッツ連続かつ有界であり, 対象とするニューラルネッ
トワーク全てのシグモイド関数 ρa のパラメータ a や結合係数 ai,j の絶対値に上限が存在すれば, 条件 NEURONS1 : def 5 NEURONS1 : def 6 は満たされる.
本稿ではこのような各写像 Ni の具体的な形には立ち入らず, 一般的な連続写像の場合について議論する.
これらの条件のもとに,NEURONS(n, k) の部分集合に Ascoli-Arzelá の定理を適用すると以下の命題が得られる．

Listing 15. NEURONS1:35
theorem :: NEURONS1:35
for n be Nat,k be FinSequence of NAT,
S be non empty compact strict TopSpace,
X be non empty Subset of (REAL−NS (k.1)),
T be NormedLinearTopSpacestS is SubSpace of (TopSpaceNorm (REAL−NS (k.1)))& the carrier of S = X& X is compact& T is complete & T is ﬁnite−dimensional& dim (T) <> 0
& REAL−NS (k.(n+1)) = the NORMSTR of T
holds
for G be non empty Subset of R NormSpace of ContinuousFunctions(S,T),
D,K be Realst0<D&0<K&
G c= { F|X where F is Function of REAL−NS (k.1),REAL−NS (k.(n+1)): ex N be non empty FinSequence
st N is LayerFunc Seq D,K,k,n& F = OutPutFunc(N,k,n) }holds
Cl(G) is compact;

以上のように, ニューラルネットワークの各層 Ni に条件を課すことを前提にニューラ
ルネットワークを表現する連続写像の集合 NEURONS(n, k) の閉部分集合が compact
集合であることが示される. これは,NEURONS(n, k) に属するニューラルネットワークに何らかの性能評価が与えられ，それがこの NEURONS(n, k) の部分集合上の実数値連続関数の場合, その評価関数の最大 (最小) 値とそれを与えるニューラルネットワークの存在を保証する. また, この部分集合内で結合係数の学習など何らか逐次アルゴリズムで,この部分集合内内の元の無限列が生成されるときに, その無限列の集積点の存在を保証す
る. このような意味で, 上記の compact 性は有用な性質である.

5

まとめ
本稿では階層型ニューラルネットワークの形式化について報告した. ニューラルネッ

トワークの入出力及び中間各層をベクトル値を入出力する有限次元ベクトル空間上の写像とみなし, それらの複数の写像の有限列によってニューラルネットワークを表現した. このニューラルネットワークによる入出力の関係は, それを定義する写像の有限列全部の合

MMA-WiP (2021), vol.3, no.4 - https://mizar-jp.org/journal/MMA-WiP/j2021.3.4 - ISSN 2434-5458 (Online)

10/12

Mechanized Mathematics and Its Applications, Works in Progress

Multilayer Perceptron (Yamazaki H.,et al.)

成写像として表現される. 前回報告した Ascoli-Arzelá の定理について写像の値域が有限次元空間の場合の命題を形式化し, ニューラルネットワークの入出力の関係を表す写像全部の集合についての comapct 性に関する命題を形式化した. しかしながら, 現時点の形式化は各層を表す写像についての具体的な形, 例えば, 結合係数やシグモイド関数などについての考察までには至っていない．Funahashi [7] が既に証明しているニューラルネット
ワークによる非線形関数の近似可能性定理などもまだ, 形式化がなされていない. さらには, 最近話題となっている Deep Learning について何故, 中間層を増やすことによって, 学
習精度が向上するのかという重要な課題についてもその課題の形式化にも至っておらず,
今後さらに形式化の研究が必要である. これらの形式化に興味を持たれた読者の積極的な参加を歓迎する.

参考文献[1] Rosenblatt F. The Perceptron: A Probabilistic Model for Information Storage andOrganization in the Brain. Psychological Review. 1958;65(6):386–408.
[2] Rumelhart DE, Hinton GE, Williams RJ.

Learning representations by back-propagating errors. Nature. 1986;323(6088):533–536.
[3] Schmidhuber J. Deep Learning in Neural Networks: An Overview. Neural Networks. 2015;323(61):85–117.
[4] Sprecher D. On the structure of continuous functions of sevral variables. Translations of American Mathematical Society. 1965;(115):340–355.
[5] Hecht-Neilsen R. Kolmogorov mapping neural network existence theorem. In:
IEEE First International Conference on Neural Networks. 3; 1987. p. 11–13.
[6] Kolmogorov A. On the representation of continuous function of many variables
by superposition of continuous function of one variable and addition. Doklady
Akadmeii Nauk SSSR. 1957;(144):679–681.
[7] Funahashi K. On the approximate realization of continuous mappings by nural
networks. Neural Networks. 1989;(2):183–192.
[8] Irie B, Miyake S. Capability of three-layered perceptron. In: IEEE International
Conference on Neural Networks. 1; 1988. p. 641–648.
[9] Hryniewiecki K. Graphs. Formalized Mathematics. 1991;2(3):365–370. Available
from: http://fm.mizar.org/1991-2/pdf2-3/graph_1.pdf.
[10] Nakamura Y, Rudnicki P.

Vertex Sequences Induced by Chains.

Formalized

Mathematics. 1996;5(3):297–304. Available from: http://fm.mizar.org/1996-5/
pdf5-3/graph_2.pdf.
[11] Nakamura Y, Rudnicki P.

Euler Circuits and Paths.

Formalized Mathemat-

ics. 1997;6(3):417–425. Available from: http://fm.mizar.org/1997-6/pdf6-3/
graph_3.pdf.

MMA-WiP (2021), vol.3, no.4 - https://mizar-jp.org/journal/MMA-WiP/j2021.3.4 - ISSN 2434-5458 (Online)

11/12

Mechanized Mathematics and Its Applications, Works in Progress

Multilayer Perceptron (Yamazaki H.,et al.)[12] Nakamura Y, Rudnicki P.
1998;7(2):189–192.

Oriented Chains.

Available from:

Formalized Mathematics.

http://fm.mizar.org/1998-7/pdf7-2/

graph_4.pdf.
[13] Chen JC, Nakamura Y. The Underlying Principle of Dijkstra’s Shortest Path
Algorithm. Formalized Mathematics. 2003;11(2):143–152. Available from: http://fm.mizar.org/2003-11/pdf11-2/graph_5.pdf.
[14] Endou N, Shidama Y. Completeness of the Real Euclidean Space. Formalized Mathematics. 2005;13(4):577–580. Available from: http://fm.mizar.org/2005-13/
pdf13-4/real_ns1.pdf.

Mizar article information
Works in Progress
COSP3

C(Ω) space and C0 (Ω) space

by Hiroshi Yamazaki and Yasunari Shidama
Summary: In this article, ﬁrst we give a deﬁnition of a functional space which isconstructed from all continuous functions deﬁned on a compact topological space. We
prove that this functional space is a Banach spacea. Next, we give a deﬁnition of afunction space which is constructed from all continuous functions with bounded support.
We also prove that this function space is a normed space.
ASCORI

Ascoli − Arzela′ s theorem

by Hiroshi Yamazaki and Yasunari Shidama
Summary: In this article, the Ascoli-Arzela’s theorem is formalized. First, we gave
deﬁnitions of equicontinuousness and equiboundedness of a set of continuous functions.
Next,we formalized the Ascoli-Arzela’s theorem by those deﬁntions , and proved thistheorem.
NERONS1 Formalizations for Multilayer perceptron
by Hiroshi Yamazaki and Yasunari Shidama
Summary:
In this article, the hierarchical neural networks (Multilayer perceptron) is formalizedby ﬁnite sequence of mappings. The input-output map of the this neural network isrepresented as a composite map of this ﬁnite sequence. The compactness of the set ofthese composite map is proved by applying Ascoli-Arzela’s theorem.

MMA-WiP (2021), vol.3, no.4 - https://mizar-jp.org/journal/MMA-WiP/j2021.3.4 - ISSN 2434-5458 (Online)

12/12