知能情報システム特論 Introduction 山本 章博 京都大学 情報学研究科 知能情報学専攻 http://www.iip.ist.i.kyoto-u.ac.jp/member/akihiro/ akihiro@i.kyoto-u.ac.jp

概要 定理証明とその機械学習とプログラム開発への応用 離散データを対象とした機械学習のためのデータ構造の基礎理論 構造体（木），文字列，テーブル，グラフ，… 連続値データからの機械学習が実数論を基盤にしているように

内容 定理自動証明 節論理 論理プログラミング 帰納論理 極限同定とMIS 正データ学習 反単一化 計算代数 仕様と検証

講義資料 山本：帰納論理プログラミングの基礎理論とその展開，コンピュータソフトウェア，5月号，2006 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 20 30 40 50 60 T 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 一般的法則の探索・発想 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) (表現) 仮説空間 H 全体集合 U の部分集合のクラス 帰納推論したい概念を含む 概念の表現全体の集合 個々の概念はある法則で表現されている U H h h1 h2

概念を対象とした帰納推論(2) 観測事実は全体集合U の要素と正負のラベル付け 許容性：個々の概念は一つ以上の仮説で表現されている 正負のラベルとは、帰納推論の対象となる概念の特徴関数 CS(x) = 1 Û x Î S の値 許容性：個々の概念は一つ以上の仮説で表現されている

計算機科学における概念定義方法 述語論理 S = { x | x は自然数 かつ x mod 2 = 0 } 数学的推論の形式化・機械化 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 論理（演繹推論）

帰納推論と学習 学習は帰納推論の特別な場合 帰納推論は，「教師」という人間やエージェントが具体的に設定されていない

学習の定式化・機械化 教師 Teacher H hi(仮説) 学習機械 Learner 概念Hに関する 例示 仮説(など) 例(データ) 　仮説(など) h1, h2, h3,… 例(データ) d1, d2, d3,… 学習機械 例からを仮説を導出する アルゴリズム Learner

Computer Learner CPU 仮説(推定) h1, h2, h3,… Learning with Logic 論理（演繹推論） 例(データ)　d1, d2, d3,… 　仮説(推定)　h1, h2, h3,… 例から仮説を 導出する アルゴリズム 概念に 関する 例示 メモリ CPU □ Learning with Logic Logic for Learning 　（L4 帰納論理） 論理（演繹推論）

形式化された学習 概念に関する例示 例を 伝えるポート 仮説を 伝える ポート 例から仮説を 導出する アルゴリズム

述語論理と定理自動証明

記号論理(1) 記号論理 : (数学的)推論の定式化 例 三角形ABCが二等辺ならば底角は等しい ∠ B =∠ C ¬ A B= A C A P

記号論理(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

形式的な推論の例 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 C P

述語論理 命題内の対象と述語に注目して形式化・記号化 ∠ B = ∠ C ¬ A B = A C "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 B C P x y 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))

これからの内容 定理自動証明 帰納論理 仕様と検証 帰納推論の逆として 帰納推論の中の法則を探索する手法として 述語論理と定理自動証明を利用した機械学習・帰納推論 仕様と検証