Which Hypothese can be found with Inverse

知能情報システム特論
Introduction
山本章博
京都大学情報学研究科知能情報学専攻
http://www.iip.ist.i.kyoto-u.ac.jp/member/akihiro/
[email protected]
概要


定理証明とその機械学習とプログラム開発へ
の応用
離散データを対象とした機械学習のためのデ
ータ構造の基礎理論


構造体（木），文字列，テーブル，グラフ，…
連続値データからの機械学習が実数論を基盤にし
ているように
内容

定理自動証明



帰納論理





節論理
論理プログラミング
極限同定とMIS
正データ学習
反単一化
計算代数
仕様と検証
講義資料


http://www.iip.ist.i.kyoto-u.ac.jp/member/akihiro/
山本：帰納論理プログラミングの基礎理論とそ
の展開，コンピュータソフトウェア，5月号，2006
http://www.jstage.jst.go.jp/article/jssst/23/2/2_29/_pdf/-char/ja/
(参) S.H. Nienhuys-Cheng and R. de Wolf, Foundations of
Inductive Logic Programming”, Springer
演繹と帰納
帰納の例(関数)


単振子の周期 T は(振幅が小さけれ
ば)糸の長さ l の平方根に比例する
T l
具体的事実(観測データ)の収集
l
T

20
30
40
50
60
0.98 1.10 1.26 1.41 1.55
一般的法則の導出
一般的法則の探索・発想
 具体的事実を用いた検証

T=kl
帰納の例(形式言語)


M社のワープソフト用のファイルの拡張子
は .doc または .docx である
具体的事実(観測データ)の収集
帰納の例(形式言語つづき)

一般的法則の導出

一般的法則の探索・発想
S = 0+1+…+9+A+…+a+…+z として
E = S (S*).doc

具体的事実を用いた検証
帰納の例(数学的概念)



偶数とは 2 で割切れる自然数である
具体的な事実の観測(データの収集)
偶数である：22, 4, 16, 6, 184,…
偶数でない：7, 55, 13, 9, 1,…
法則の導出

一般的法則の探索・発想
S = { x | x は自然数かつ x mod 2 = 0 }

具体的事実を用いた検証
「帰納」を定める要素

対象


表現




個々の対象はある法則で表現されている
観測事実の表現方法


法則を導出したい対象を含むクラス
関数ならば、入出力の組
言語や概念ならば、データとその正負値
法則を探索・発想する方法
評価（帰納の正当性）
概念を対象とした帰納推論

(対象) 概念空間 C(H)



全体集合 U の部分集合のクラス
帰納推論したい概念を含む
(表現) 仮説空間 H


概念の表現全体の集合
個々の概念はある法則で表現されている
U
H
h1
h2
h
概念を対象とした帰納推論(2)

観測事実は全体集合U の要素と正負のラベ
ル付け


正負のラベルとは、帰納推論の対象となる概念の
特徴関数
CS(x) = 1  x  S
の値
許容性：個々の概念は一つ以上の仮説で表
現されている
計算機科学における概念定義方法

述語論理

数学的推論の形式化・機械化
S = { x | x は自然数かつ x mod 2 = 0 }
"x (even(x)  nat(x)  (x mod 2 = 0))
"x (even(x)  nat(x) mod(x,2,0))
"x even(x) x = 0 y((x = y + 2)even(y))
計算機科学における概念定義方法


正則表現
01(00 + 01)* 11
形式文法
S 00A
A 0A1
A 01
概念を対象とした帰納推論(3)


法則を探索・発想するプロセス
具体的事実による検証において
ある要素 x が帰納推論したい概念 S に
属しているかどうかを判定する手続き
を利用する
形式言語 ⇒ オートマトン, 構文解析
述語論理 ⇒ 数学的推論の自動化（自動証明）
計算論から見た演繹と帰納
計算の定式化・機械化
メモリ
CPU
Computer
 gf(F, w)
gf(x, y)  p(x, z),f(z, y)
 p(F, z),f(z, w)
p(F, D)
 f(D, w)
f(x, y) p(x, y), m(y)
 p(D, w), m(w)
p(D,A)
 m(A)
w=A

w=A
□
論理（演繹推論）
帰納推論と学習


学習は帰納推論の特別な場合
帰納推論は，「教師」という人間やエージェント
が具体的に設定されていない
学習の定式化・機械化
教師
Teacher
hi(仮説)
H
概念Hに関する
例示
例(データ)
d1, d2, d3,…
仮説(など)
h1, h2, h3,…
学習機械
Learner
例からを仮説を
導出する
アルゴリズム
Computer
メモリ
CPU
 gf(F, w)
gf(x, y)  p(x, z),f(z, y)
 p(F, z),f(z, w)
p(F, D)
 f(D, w)
f(x, y) p(x, y), m(y)
 p(D, w), m(w)
p(D,A)
 m(A)
w=A

w=A
□
論理（演繹推論）
Learner
例(データ) d1, d2, d3,…
概念に
関する
例示
例から仮説を
導出する
アルゴリズム
仮説(推定) h1, h2, h3,…
Learning with Logic
Logic for Learning
（L4 帰納論理）
形式化された学習
概念に関する例示
例を
伝える
ポート
仮説を
伝える
ポート
例から仮説を
導出する
アルゴリズム
述語論理と定理自動証明
記号論理(1)

記号論理 : (数学的)推論の定式化
例三角形ABCが二等辺ならば底角は等しい
∠ B =∠ C A B= A C
A
B
P
C
記号論理(2)


命題論理
命題文の内部構造に言及しない
述語論理
命題文の主述関係を扱う
全称と存在を扱う
∠ B =∠ C A B= A C
命題論理

命題を文単位で形式化記号化
△x y z △u v w  x y = u v  x z = u w
 ∠z = 90  ∠w = 90
p q  r  s  t

命題の正しさを真偽値（0, 1)でモデル化（古典
論理）すると電気回路に応用可能
推論過程の形式化

命題 j と z j から z を帰結する
j
z j
z

命題 j と z から j  z を帰結する
j
z
jz
形式的な推論の例
p : △ABP △ ACP, q : AB=AC,r : AP=AP
s : ∠P = 90
q
r
qr
s
pqrs
qrs
p
A
B
P
C
述語論理

命題内の対象と述語に注目して形式化・記号化
∠B=∠CAB=AC
"x "y "z "u "v "w (
△x y z △ u v w  x y = u v  x z = u w
 ∠ z = 90  ∠w = 90)
A
x
y
B
P
C
z
u
v
w
述語論理による概念の定義
"x even(x) x = 0 y((x = y + 2)even(y))
even(0)  "x (even(s(s(x))) even(x))
Cf. 正則表現
形式文法
(s s)* 0
S 0
S s(s(S))
これからの内容

定理自動証明



帰納論理


帰納推論の逆として
帰納推論の中の法則を探索する手法として
述語論理と定理自動証明を利用した機械学
習・帰納推論
仕様と検証

Download Report