FC2ブログ
--.--
--
上記の広告は1ヶ月以上更新のないブログに表示されています。
新しい記事を書く事で広告が消せます。

03.17
Mon
暫く書いていたものがβ版ではありますが、できたのでブログの更新をします。

その前に人工知能の歴史の話を少しだけ。

-----
ここでいう人工知能(Artificial Intelligence)とは1956年にLISPの父として有名なジョン・マッカーシーにより
発明された言葉のことです。現在、人工知能という語は使われる分野も意味も多岐に渡り漠然としていますが、ここではオリジナルに沿って、記号処理的な手法による人間のような推論のできるコンピュータの実現として考えてみます。

人間の知識・推論(思考の過程)を如何に扱うかという問題はなにも計算機や上述の意味での人工知能という概念が明確化される以前から考えられてきた問題です。
例を1つ挙げれば、ギリシアのアリストテレスは三段論法という、ある主張とある主張とから正しく結論を導く方法を初めて明確に形式化したとされています。
このような、どうすれば筋の通った正しい主張ができるのかということを研究する分野が後に論理学となるわけですが、
それら正しい人間の思考の原理を追求し体系化する試みが古くから哲学者を中心に行われ、現代に伝わりました。

さてそのような経緯と、さらに当時1900年代の数学の形式化・厳密化の流れによって
論理学が大きく発展していた事が影響してだと思われますが
計算機上で人間が行うような推論を実現するために論理学を使うのは自然の流れでした。

ところで計算機で論理学をやるというのはどういうことでしょうか?
(というより現在の計算機の理論的な発展は論理学(者)が無ければあり得ないものなのですが)
論理学ではある主張を命題という記号で表し、それらの関係を研究するのが1つの重要なテーマですが、
命題を記号で表すからには計算機で記号計算(数値計算と対比させて)を簡単に行えるシステムが必要です。
これを可能にするのがLISPでした。LISPは記号処理を得意とし、人工知能用の言語と謳われる事が多いですがその所以がこれです。
(記号処理と言えば数式処理システムで有名なMaximaなんかはLispで書かれていますね。)
このようなことから分かるように、マッカーシーは論理によって人間の知識・推論過程を形式化し計算機で表そうとしたのです。
そして初期の人工知能研究ではLISPが多用され、述語論理(論理学の1分野)の扱いの容易さから活躍しました。

が問題もありました。
今述べたような、論理による人工知能の実現はGOFAI(Good Old-Fashioned AI)と呼ばれる種別のもので
現在では活発とはいえない分野です。なぜかはいつか書こうと思います。
-----


本題に入りますが、以下ではそんな論理により形式化された推論機を実装してみましたものを紹介してみます。

前々々回ブログに書いたものをベースに1から書きなおしたような感じです

ソースコード及びスタンドアロンの実行バイナリは

git clone https://github.com/moratori/flexpr.git

で。

実行可能ファイルはLinuxとWindowsでbinary/フォルダの下に用意してありますがWindowsだと動作が不安定かもしれませんのでLinux版を出来ればおすすめします.

ソースコードから実行することもできますが、
その場合以下の事に注意して下さい。

・これがSBCL,CLISPで動作確認を行ったこと(処理系依存の処理は使ってないはずですが一応)
・Quicklisp(Lispのパッケージ管理システム)が導入されていること
・拙作namespace(https://github.com/moratori/namespace.gitにあります)がQuicklispでロードできること

以上を確認した上でLispのREPLから

(ql:quickload :flexpr)
(flexpr.interface.repl::main)

と評価すればおkです

起動すると、コマンドのヘルプ一覧が表示されます

Theorem Prover 1.0
Command Help
  :load <Filename> load a definition file
  :save <axiomatic system name> save current system
  :desc <axiomatic system name> describe axiomatic system
  :set <New axiomatic system> change current axiomatic system
  :add <Formula> add formula to current axiomatic system
  :list enumerate the axiomatic system that are currently defined
  :help show this help
  :exit exit from REPL
  :quit alias of :exit

(NIL)>>>


プロンプトが表示されていますが、ここにどんどん論理式を打ち込んで行きます。

例えば古典命題論理に於いて定理である P → P や ((P→Q)→P)→Pを証明してみます

(NIL)>>> P > P
P > P is PROVABLE under the nil
evaluation took 0 sec
(NIL)>>> ((P > Q) > P) > P
((P > Q) > P) > P is PROVABLE under the nil
evaluation took 0 sec
(NIL)>>>

入力可能な論理式は命題論理式と一階述語論理式になります。

前々々回のlexprとは違いまだ証明図を出力する機能はつけていません。

さて今の状態だと、定理となる論理式の証明しか行えないので
仮定からの証明(演繹)を試してみます

そのために仮定というか、論理式を列挙した定義ファイルを読み込む必要があります。

有名どころのソクラテスが死ぬやつをまたやってみます。

(NIL)>>> :load ~/Desktop/human
human load ok
(HUMAN)>>> :desc
human is consist of:
Ax.(human(x) > mortal(x))
human(Socrates)

(HUMAN)>>> mortal(Socrates)
mortal(Socrates) is PROVABLE under the human
evaluation took 0 sec
(HUMAN)>>> Ex.mortal(x)
Ex.mortal(x) is PROVABLE under the human
specific term: Socrates
evaluation took 0 sec
(HUMAN)>>>

はじめに:loadというコマンドを使いデスクトップ上に定義されたhumanファイルを読み込みます

ここでプロンプトのところが(NIL)から(HUMAN)に変わっている事に気をつけて下さい。
つまり今から証明する事柄がHUMANの元で証明されることであるという事を示しています.

また次に:descコマンドによりそのファイルになにが書いてあったか確認しています.

mortal(Socrates)と入力して確かにソクラテスは死ぬ運命にあるんだよね?それは証明できるよね?
という事を問いかけますと、provableであることがわかります。

最後にまた質問を変えて、死ぬようなものが存在するはずなんだけどそれは正しいか?そしてそれは誰か?
という結論を与えると、Socratesがたしかにそうだという事を答えてくれます

なお定義ファイルには任意の論理式と#(シャープ)から始まるコメント行のみを書くことができます.

見ての通りですが、入力できる論理式は全て論理学で帰納的に定義される式(well-formed formula)と同じです。

特殊な文法を覚える必要はありません。またPrologのように入力をホーン節に限定しているような論理プログラミング言語とは違い、任意の論理式を入力することができます(但しその分効率は悪くなります)

次にもう少しだけ複雑な例をやってみます。

論理プログラミングの練習でありがちな例です

(HUMAN)>>> :load ~/Desktop/isono
isono load ok
(ISONO)>>> :desc
isono is consist of:
parent(Namihei,Sazae)
parent(Namihei,Katuo)
parent(Namihei,Wakame)
parent(Fune,Sazae)
parent(Fune,Katuo)
parent(Fune,Wakame)
parent(Sazae,Tara)
parent(Masuo,Tara)
male(Namihei)
male(Katuo)
male(Masuo)
male(Tara)
female(Fune)
female(Sazae)
female(Wakame)
AxAy.(parent(x,y) & male(x) > father(x,y))
AxAy.(parent(x,y) & female(x) > mother(x,y))
AxAy.(parent(x,y) > ancestor(x,y))
AxAyAz.(parent(x,y) & ancestor(y,z) > ancestor(x,z))
AxAyAz.(parent(x,y) & parent(x,z) > sibling(y,z))
AxAyAz.(sibling(x,y) & parent(x,z) & male(z) > nephew(z,y))

(ISONO)>>> ExEyEz.(parent(x,y) & nephew(y,z))
ExEyEz.(parent(x,y) & nephew(y,z)) is PROVABLE under the isono
specific term: Sazae Tara Katuo
evaluation took 0 sec
(ISONO)>>>

isonoというサザエさんの磯家の定義ファイルを読み込んで家系に関する質問に答えることができます。

最後に論理プログラミングやプランニングとかの分野で有名なtoy problemである
猿とバナナの問題をやってみます。

どういう問題かというと、次のような状況でどのようにすれば猿がバナナを得られるかの手順を求める問題です.

部屋に猿が閉じ込められていて、天井からバナナがぶら下がっている。
手を伸ばしただけではどうにもバナナは取れなさそうです。
ただし猿は部屋にある箱を自由に動かす事ができ、その上に登ることができる

まぁ普通に"考えて"猿が箱をバナナのぶら下がっている位置まで移動させ上に登り
バナナをつかめばいいわけですが、これを計算機で解くというものです。

実はこういう問題も前提からの証明という論理プログラミングの枠組みの中で行うことができます

(NIL)>>> :load ~/Desktop/monkey-banana
monkey-banana load ok
(MONKEY-BANANA)>>> :desc
monkey-banana is consist of:
AxAs.(~onbox(s) > at(BOX,x,pushbox(x,s)))
As.onbox(climbbox(s))
As.(onbox(s) & at(BOX,TARGET,s) > have(grasp(s)))
AxAs.(at(BOX,x,s) > at(BOX,x,climbbox(s)))
~onbox(S0)

(MONKEY-BANANA)>>> Estate.have(state)
Estate.have(state) is PROVABLE under the monkey-banana
specific term: grasp(climbbox(pushbox(TARGET,S0)))
evaluation took 0 sec
(MONKEY-BANANA)>>>

前提となる論理式が少し複雑なので説明しますと

・猿が箱に乗ってないならば箱を適当な場所に押すことができる
・箱に登れば箱の上に猿がいることになる
・猿がバナナのぶら下がる目標地点にある箱の上にいるならば手でつかめばバナナを得ることができる
・猿はいつどこに箱がある時でも箱の上に登る

というような感じです。
ここでEstate.have(state)と入力すると、
それは「さるはバナナを得られるか?そして得られるなら具体的にどのような手順で得ることができるか?」という質問を
表すことになり、答えを求めることができます。
specific term の意味は 目標地点まで箱を押して行き、そこで箱に登り手でつかめば良いということを表します

このように論理プログラミングは賢く推論を行うコンピュータの実現のために応用されてきました。
スポンサーサイト

comment 0 trackback 0
トラックバックURL
http://telracsmoratori.blog.fc2.com/tb.php/184-65db5cef
トラックバック
コメント
管理者にだけ表示を許可する
 
上記広告は1ヶ月以上更新のないブログに表示されています。新しい記事を書くことで広告を消せます。