立命館大学 情報理工学部 知能情報学科 谷口忠大. Information このスライドは「イラ ストで学ぶ人工知能概 論」を講義で活用した り,勉強会で利用した りするために提供され ているスライドです.イラ ストで学ぶ人工知能概 論.

Slides:



Advertisements
Similar presentations
Information このスライドは「イラ ストで学ぶ人工知能概 論」を講義で活用した り,勉強会で利用した りするために提供され ているスライドです.イラ ストで学ぶ人工知能概 論.
Advertisements

ロボット制御のソフトウェ ア: シミュレータ試作 情報理工学部 情報知能学科 H 207051 中谷聡太郎.
コンピュータプラクティ スⅠ アンケート 水野嘉明 1. 本日の予定 「アンケート」  人間的な要因を評価するための 一手段として、アンケートの方 法について学ぶ  実験では、アンケートの集計を 行う 2.
一階述語論理 (first-order predicate logic) 一階述語論理入門 構文論(論理式の文 法) 意味論(論理式の解 釈) 認知システム論 知識と推論(4) 知識と論理でを組み合わせて問題を解決する.
Information このスライドは「イラ ストで学ぶ人工知能概 論」を講義で活用した り,勉強会で利用した りするために提供され ているスライドです.イラ ストで学ぶ人工知能概 論.
プログラミング言語論 第10回(演習) 情報工学科 木村昌臣   篠埜 功.
人工知能特論2011 No.4 東京工科大学大学院 担当教員:亀田弘之.
白井 良明 立命館大学情報理工学部 知能情報学科
融合原理による推論 (resolution)
間接疑問文 I know him. I know (that) he is a doctor. ↓ why he is a doctor.
知的インタフェース 例示によるプログラミング 予測インタフェース 制約インタフェース.
ジャーナリズム論 第8回 ニュースとは何か 担当:野原仁.
法とコンピュータ 法的知識の構造(3) 慶應義塾大学法学部 2008/11/25 吉野一.
充足不能性と導出原理 充足不能性の証明 スコーレム標準形 エルブラン解釈 導出原理 基礎節に対する導出 導出原理の完全性と健全性.
情報とコンピュータ 静岡大学工学部 安藤和敏
プログラミング言語論 第6回 型 情報工学科 篠埜 功.
Prolog演習 PowerPointのアニメーション機能を利用すると分かりやすいと思います.
8chSteppingMotorのプログラム について
人工知能特論2011 資料No.6 東京工科大学大学院 担当教員 亀田弘之.
立命館大学 情報理工学部 知能情報学科 谷口忠大
情報科学1(G1) 2016年度.
Semantics with Applications
人工知能概論 第6章 確率とベイズ理論の基礎.
数理論理学 第1回 茨城大学工学部情報工学科 佐々木 稔.
データ構造と アルゴリズム 知能情報学部 新田直也.
エージェントアプローチ 人工知能 7章・8章 B4 片渕 08/07/18.
数理論理学 第11回 茨城大学工学部情報工学科 佐々木 稔.
自動定理証明と応用 (automated theorem proving and its application)
共通言語アイコンを用いたネットワーク コミュニケーション
寄せられた質問: 演習問題について この講義の範囲に含まれる適切な演習問題が載っている参考書がありますか? できれば解答や解説が付いているものがあると良いのですが… 第3回の授業の中で、演習問題に取り組む方法を説明します.
不完全な知識 不完全な知識に基づく問題解決 フレーム問題 制約条件記述問題 非単調推論 極小限定 常識の定式化 並列極小限定.
プログラミング言語論プログラミング言語論 プログラムの意味論 水野嘉明
人工知能概論 第14回 言語と論理(3) 証明と質問応答
形式言語の理論 5. 文脈依存言語.
計算の理論 II 帰納的関数2 月曜4校時 大月美佳.
数理論理学 第3回 茨城大学工学部情報工学科 佐々木 稔.
第4回  推 論(2).
Prolog入門 ーIT中級者用ー.
導出原理とProlog -論理と形式化 授業資料-
プログラミング言語論 第10回 練習問題解答例 情報工学科 篠埜 功.
論理と推論 命題論理 推論 命題論理体系の健全性と完全性 構文と意味 → 同値関係と標準形(節形式) 決定問題と意味木 推論規則
計算機科学概論(応用編) 数理論理学を用いた自動証明
論理プログラミング 導出の効率化 論理プログラム ホーン節 ホーン集合に対する導出戦略 論理式の手続き的解釈 Prolog
(1)序論 人工知能とは 歴史 方法論 人工知能の基礎 問題解決 探索 推論 知識.
知能情報システム特論 Introduction
第5章 計算とプログラム 本章で説明すること ・計算の概観と記述法 ・代表的な計算モデル ・プログラムとプログラム言語.
数理論理学 第12回 茨城大学工学部情報工学科 佐々木 稔.
ロボット工学 第10回 力制御と作業座標系PD制御
コンパイラ 2011年10月20日
融合原理 (resolution) 人工知能 論理と推論(2) 論理的帰結 節形式 融合原理 知識を組み合わせて知識を生み出す
「アルゴリズムとプログラム」 結果を統計的に正しく判断 三学期 第7回 袖高の生徒ってどうよ調査(3)
東京工科大学 コンピュータサイエンス学部 亀田弘之
第7回  命題論理.
東京工科大学 コンピュータサイエンス学部 亀田弘之
東京工科大学 コンピュータサイエンス学部 亀田弘之
香川大学工学部 富永浩之 知識工学1 第1-1章 人工知能と知識工学 香川大学工学部 富永浩之
数理論理学 第9回 茨城大学工学部情報工学科 佐々木 稔.
プログラミング言語論 第10回 情報工学科 篠埜 功.
述語論理式の構文と意味 一階述語論理式の構文 一階述語論理式の意味 述語,限量記号 自然言語文の述語論理式表現 解釈 妥当,充足不能
自然言語処理2015 Natural Language Processing 2015
計算の理論 I -講義について+αー 月曜3校時 大月美佳 平成31年5月18日 佐賀大学理工学部知能情報システム学科.
矛盾した知識 デフォルト推論 仮説を用いた推論 準無矛盾推論 デフォルト規則 デフォルト理論の拡張 → デフォルト証明 シナリオ
情報とコンピュータ 静岡大学工学部 安藤和敏
計算の理論 I -講義について+αー 火曜3校時 大月美佳 平成31年8月23日 佐賀大学理工学部知能情報システム学科.
自然言語処理2016 Natural Language Processing 2016
mi-8. 自然言語処理 人工知能を演習で学ぶシリーズ(8)
数理論理学 最終回 茨城大学工学部情報工学科 佐々木 稔.
立命館大学 情報理工学部 知能情報学科 谷口忠大
練習問題.
練習問題.
Presentation transcript:

立命館大学 情報理工学部 知能情報学科 谷口忠大

Information このスライドは「イラ ストで学ぶ人工知能概 論」を講義で活用した り,勉強会で利用した りするために提供され ているスライドです.イラ ストで学ぶ人工知能概 論

STORY 言語と論理 ( 3 ) ホイールダック2号は単純な論理を理解できるようになった. スフィンクスに対峙するホイールダック2号.スフィンクス が語りだす. 「貴子は洋子の娘」「子供の子供は孫」「娘ならば子供であ る」「洋子は豪太郎の娘だ」「靖は洋子のいとこだ」 そして,スフィンクスは問う. 「さて,豪太郎の孫は誰だ?」 はたして,ホイールダック2号はこの問いに答えられるのか.

仮定 言語と論理 ( 3 ) ホイールダック2号に文法に関する知識,語彙に関 する知識は事前に与えてよいものとする. ホイールダック2号は誤りのない音声認識が可能で あるとする. ホイールダック2号は与えられた自然言語文を論理 式に変換する処理系を備えているものとする.

Contents 14.1 導出原理 14.2 述語論理による質問応答 14.3 スフィンクスの謎かけ

導出原理と証明 与えられた文から得られた一階述語論理式が恒真式 (正しい)かどうか,判断するためにはどうすれば よいか? 証明 証明:対象となる式が恒真式であるということを示 すこと 導出原理 ∀ xP(x) が真であるかどうかを直接しらべ るには,全ての x について考えないといけ ない. 無理! 反駁による証明

導出とは何か? 節集合 C= {C1,...., Cn} における節 Ci, Cj が,あるリ テラル P とその否定リテラル¬ P を含んでいた時,こ れら二つの節から新たな節を導く推論形式を導出 (resolution) という. 親節 導出節 三段論法と等価

単一化置換 述語論理式に対する導出は述語論理式に含まれる個体変 数にあらかじめ適切な処置を施さないと導出を行なうこ とが出来ない. 例えば ∀ x,y,z で下式があったとき C i ≡ P(x,f(y)) ∨ Q C j ≡ ¬ P(a,z) ∨ R x=a, z=f(y) であると仮定すれば,置換 (a/x),(f(y)/z) の後に 導出を行える. 単一 化 (unification) このように,個体変数を別の項に置き換える操作を単一 化 (unification) という. 必要最小限の置換を行なう それ以降の置換の自由度を確保することが出来る.

反駁による証明 人手によって証明するのではなく,何らかのアルゴ リズムによって自動的に証明したい. 前提 X と結論 Y に対して, X → Y 「 X ならば Y 」を証 明する. P が恒真式 ⇔ ¬ P が恒偽式・・矛盾が ある. 前提 X の節集合結論の否定¬ Y 前提 X の節集合に,結論の否定¬ Y を節として加えた節集合 に対して導出を繰り返すことで,空節 を導けばよいことが わかる.

反駁による証明の例

演習 14-1 前提 (P ∧ Q) → R, P → Q, P から結論 Q ∧ R が導けることを, 導出原理を用いて証明せよ.

導出制御戦略 親節内の特定の二つの節を具体的にどう選んだら良 いかが決まらない. どの順番で どれとどれをくっつける?

導出制御戦略 機械的な制御戦略 幅優先戦略 (breadth-first strategy) 線形導出 (linear resolution) 意味的な制御戦略 支持集合戦略 支持集合戦略 (set-of-support strategy) 意味導出 (semantic resolution) などなど 基本的な探索 前提 X 結論¬ Y 大体間違っているとしたら 結論の方なので,結論の 節から重点的に攻める.

Contents 14.1 導出原理 14.2 述語論理による質問応答 14.3 スフィンクスの謎かけ

質問応答システム ゴジラは大きいです か? はい 前提知識  monster(x) → big(x)  monster( ゴジラ ) 前提知識  monster(x) → big(x)  monster( ゴジラ ) これができるか?

一般疑問文に対する質問応答 一般疑問文 「 Do you ~ ? 」「 Is this ~ ? 」 → はい,いいえ で回答 ( 事前知識 ) → ( 疑問文中で問われている事実 ) という述 語論理式を構成し,これが恒真式であることを示せば よい. (monster(x) → big(x)) ∧ monster( ゴジラ ) → big( ゴジ ラ )

演習 14-2 一般疑問文 「ネズミは動物だ」 「あらゆる動物は生き物だ」 「山田は人間だ」 という知識をロボットに述語論理式で持たせた上で 「ネズミは生き物か?」 という質問に対する答えを反駁による証明を用いて求 めさせよ.

特殊疑問文に対する質問応答 特殊疑問文 What, When, Where, Why, Who, How といった 5W1H を問わ れる疑問文 「由美子さんは何の食べ物が好きですか?」⇒ 「何か x が存在して,由美子さんはその x が好きである」 前提知識 like( 由美子,イクラ ) があったとすると, ← 単一化 単一化を逆にたどれば由美子さんが 好きなのがイクラだとわかる.

演習 14-3 特殊疑問文 「ネズミは動物だ」 「あらゆる動物は生き物だ」 「山田は人間だ」 「あらゆる人間は動物だ」 という知識をロボットに述語論理式で持たせた上で 「動物なのは誰か?」 という質問に対する答えを反駁による証明を用いて求 めさせよ.

Prolog 導出原理を用いた定理証明や質問応答を行うプログ ラミング言語に Prolog (PROgraming in LOGic) があ る. Prolog は論理型プログラミング言語の一種であ る.

Contents 14.1 導出原理 14.2 述語論理による質問応答 14.3 スフィンクスの謎かけ

スフィンクスの謎かけ

スフィンクスの問い 「貴子は洋子の娘」「子供の子供は孫」「娘ならば子供で ある」「洋子は豪太郎の娘だ」「靖は洋子のいとこだ」 そしてスフィンクスは問う 「さて,豪太郎の孫は誰だ?」 1. 「貴子は洋子の娘」 -> 娘(貴子,洋子) 2. 「子供の子供は孫」 -> 子 (y,x) ∧子 (z,y) → 孫 (z,x) 3. 「娘ならば子供である」 -> 娘 (x,y) → 子 (x,y) 4. 「洋子は豪太郎の娘だ」 -> 娘 ( 洋子,豪太郎 ) 5. 「靖は洋子のいとこだ」 -> いとこ(靖,洋子) 6. 「さて,豪太郎の孫は誰だ?」 -> ∃ w 孫 (w, 豪太郎 )

演習 14-4 スフィンクスの問 い C1: 娘(貴子,洋子) C2: ¬子 (y,x) ∨¬子 (z,y) ∨孫 (z,x) C3: ¬娘 (x,y) ∨子 (x,y) C4: 娘 ( 洋子,豪太郎 ) C5: いとこ(靖,洋子) C6: ¬孫 (w, 豪太郎 ) 節集合形式 上記の節集合形式にもとづいて, 反駁による証明を用いてスフィンクスの問の答えを導け.

反駁による証明 1.娘(貴子,洋子) 2.¬子 (y,x) ∨¬子 (z,y) ∨孫 (z,x) 3.¬娘 (x,y) ∨子 (x,y) 4.娘 ( 洋子,豪太郎 ) 5.いとこ(靖,洋子) 6.¬孫 (w, 豪太郎 ) 支持集合戦略 ¬子 (y, 豪太郎 ) ∨¬子 (w,y) ¬娘 (y, 豪太郎 ) ∨¬娘 (w,y) ¬娘 (w, 洋子 ) □ ( 貴子 /w) で単一化置換 (w/z),( 豪太郎 /x) で単一化置換 二回作用 単一化付き 二回作用 単一化付き ( 洋子 /y) で単一化置換

孫は貴子 テヘペロ~ ( ・ ω<) スフィンクス 「さて,豪太郎の孫は誰 だ?」 スフィンクス 「さて,豪太郎の孫は誰 だ?」 ホイールダック 2 号 「豪太郎の孫は『貴子』 だ!」 ホイールダック 2 号 「豪太郎の孫は『貴子』 だ!」

な・ん・だ・ と・・・・・ !!!!!??? ゴゴゴゴゴ・・・

スフィンクスは驚き,岩の台座 から飛び降りて,海に落ちて死 んだ

おめでとうホイールダック 2 号!

まとめ 導出原理について学んだ. 述語論理による質問応答システムを反駁による証明 に基づいて実現する仕組みについて学んだ. 導出原理に基づいた質問応答の実行事例を学んだ.

これからの人工知能 過去から現在に至るまでの人工知能研究についてみ てきた この講義は「概論」なのであまり深い理論や技術に ついては述べられなかった 卒業研究などを通して、自分の研究テーマに関連し たところを仲間とともに勉強してほしい 人工知能研究はプログラム(やデータ)が公開され ているものが多いので、プログラムを動かしながら 学んでいくとよいだろう 深層学習が人工知能研究に大きな影響を与えてきて いる。この研究の動向に注意しておいたほうが良い。