3.Java-MGTPと高度推論機構の開発

［目次］

1. 研究テーマ
2. 研究体制／研究方法
3. 想定されるソフトウェア成果

［研究テーマ］

　1) 研究テーマ名：

Java-MGTPと高度推論機構の開発

　2) 研究の背景

平成７、８年度AITEC委託研究「KLIC上のMGTP処理系」において、自動推論システムMGTPをKLIC上に構築し、MGTPをUNIX上で利用できる環境を整備し、第五世代コンピュータプロジェクト技術の普及を図ってきた。

その間にWWWブラウザが急速に普及し、これとインターネットを利用した情報配布技術が一般のものとなった。そして、多くのWWWブラウザ上で標準的に実行することのできるJava言語が注目されるようになった。Javaで実装されたソフトウェアは、その普及を図る上で必要となる二つの技術的課題(1)多くのプラットホームで利用可能であること、(2)インターネットを通じて簡単に配布できること、を自動的に解決している。

このような技術動向を受けて、平成９年度AITEC委託研究「汎用並列マシン上のMGTPと高度推論機構の開発」では、JavaによるMGTPの実装を行ない、KLIC版のMGTPと同等以上の処理性能を出すことに成功した。この委託研究では他に、汎用並列マシン上のMGTPの並列化のKLICによる実装と評価、JavaによるGUIシステムの構築、MGTPへの探索制御機能の付加の予備的実験、制約MGTPの改良を行なった。

一方、これまでに多くの版のMGTP処理系を配布してきたので、「どれがスタンダードなのかが、利用者の立場からみてわかりにくい」、といった声もある。また、配布している処理系は、エラー情報に関してはほとんど関知していなかった。このように、利用者に対して必ずしも使い勝手の良いシステムとは言えなかったので、この点に対する改善の期待が高まっている。

3) 研究の目的

上記背景のもと本研究では、主として以下の項目(i)、(ii)、(iii)に関する研究開発を行なう。

(i) Java-MGTPの改良：利用者に使いやすいシステムを目指して、GUIシステムの拡充と利用者の利便性を高める諸機能(ヘルプ機能、マニュアルなどのドキュメント類の充実、インストーラの充実)の実装を行なう。さらに高速化を目指して、弁別木インデックスや節インデックス機構などを標準的に採り入れる。また、保守を容易にするために、モジュラリティを高めたコーディングを行なうと共に、プログラムコメントの充実も図っていく。この他にMGTP用のホームページを立ち上げ、利用を促進させる。

(ii) Java-MGTPの並列化：Java言語のマルチスレッド機構を用いたJava-MGTPの並列化を行なう。実装方式としては、プロセッサ間通信を抑えたN逐次方式を基本とする。同期機構を言語の基本機能として採り入れているKLICと違い、Java言語では同期をプログラムで明示する必要がある。そこで、どのように同期を実装すれば性能向上を計れるかを探究する。

(iii) MGTPによる探索制御：MGTPにA*アルゴリズムや遺伝的アルゴリズム(GA)による探索制御機能を付加したA*-MGTPやGA-MGTPを汎用的な推論エンジンとしてまとめ提供していく。

4) 研究の内容

i) Java-MGTPの改良

利用者の利便性を第一に次のような改良を施す。

1. GUIシステム：

これまでのGUIシステムでは、証明が完了してから、証明木の表示を行なっていた。したがって、証明が完了するまでは、証明木を見ることはできない。一般に、一階述語論理を対象とした証明手続きは、停止する保証はないので、利用者はいつ描画されるかも分からない出力を待つことになる。

利用者にしてみれば、これは耐えがたい状況であり、耐えられなくなった時に証明は強制終了させられることになる。このような状況に対処するために証明木の実時間描画を行なう。証明時間が長大になった場合でも証明木の実時間描画を行なっていれば、証明を行なったところまでの証明木を見ることができる。

証明をプログラムの実行にたとえれば、証明木というのはプログラムの実行トレースに相当する。証明木の実時間描画は、MGTPシステムのGUI版トレーサに発展させる予定である。そのために、ブレークポイントの設定、ある探索枝のスキップ、探索順序の指定、などの機能を付加する。

2. 利用者の利便性を高める諸機能：

入力節集合に文法上の間違いや値域限定性の欠如を発見した場合に、単にその事実を表示するのではなく、どこが間違っているのかを表示する機能を実現する。また、ヘルプ機能を充実させ、数あるオプションもマニュアルを参照せずに、使いこなせるようなシステムを提供する。

3. 高速化技術：

弁別木による項の高速検索、節インデクシングによる節の高速検索、データの効率的な復元機構による分岐コストの低減、等による推論速度の高速化を図る。

4. MGTPホームページの作成：

MGTPの試用、MGTP(プログラムとドキュメント)のダウンロードの機能を提供するホームページを研究室内のWWWサーバで運用する。MGTPの試用はJavaのアプレット機能を用いて実現する。

ii) Java-MGTPの並列化

MGTPの並列性は、証明木が分岐した際に、各分枝を並列に探索することにより抽出される。探索に分岐が生じた場合、データによって分枝間で共有できるものとできないものがある。共有できないデータは、(論理的には)そのコピーを各分枝で保持する必要がある。

しかし、データのコピーはコストのかかる作業であるので、Java-MGTPでは、コピーを作らない。この場合、共有できないデータは、分岐の左枝の探索途中で書き換えられるかもしれないので、右枝の探索ではそのデータをそのまま使うことはできない。そのため、Java-MGTPでは、右枝の探索が始まる前に書き換えられたデータを元に戻している。もちろんこれは、探索は左から右へ(逐次的に)行なわれることを前提にしているから可能なことである。

このようにデータを復元して利用するということは、並列実行を前提にするとできない。コピーが必要となる。この点は暗黙のうちにコピーが行なわれていたKLICでは考慮する必要のなかったところである。

並列実装方式としては、プロセッサ間通信を抑えたN逐次方式を基本とする。この方式だと、分岐後証明は基本的には逐次に行なわれるので、逐次環境で様々な性能向上が計られているJava-MGTPの利点をそのまま活かすことが期待できる。

iii) MGTPによる探索制御

これまでに、評価値による探索制御機能をMGTPに導入したA*-MGTPの有用性を示すとともに、パズルの問題を通してよりよい評価値の計算法を模索し、探索能力の向上を計ってきた。また、遺伝的アルゴリズム(GA)を用いて同種のパズル問題に取り組み、A*-MGTPとの比較を行なってきている。

今年度は、GA-MGTPの適応度関数について、目標(証明すべき定理)との近さを表す評価値を考案し、その効果を検証していく。また、これまでの知見を元に、A*-MGTPやGA-MGTPを汎用的な推論エンジンとしてまとめ提供していく予定である。

［研究体制／研究方法］

1) 研究体制

	氏名	所属
研究代表者	長谷川 隆三	九州大学大学院
研究協力者	藤田 博	同上
同上	越村 三幸	同上
同上	井上 勝二	同上
同上	高井 真志	同上
同上	中田 健浩	同上
同上	中山 英俊	同上
同上	永重 務	同上

2) 研究の方法

ゼミでの技術討論、研究室での意見交換を元に研究を進める。

［想定されるソフトウェア成果］

1) ソフトウェア名称：

Java-MGTP

2) そのソフトウェアの機能／役割／特徴 （Ａ４半ページ以上）

一階論理式の充足可能性判定、及び充足可能な場合には、そのモデルを枚挙する(MGTPの)基本的な機能の他に次のような機能・特徴を有する。

i) GUI機能：問題ファイルの指定、証明の開始、証明木の表示、証明木のナビゲーション等の機能を有する。

ii) 証明トレース機能：実時間で証明木を描画する機能に加え、推論の中断／再開や探索枝の優先度指定の機能を有する。これによって対話的推論が可能となる。また、論理的帰結に至った推論課程を説明する機能や冗長な推論を削除する機能も有する。

iii) 推論エンジン付加機能：利用者は、規定された入出力プロトコルをもつ推論エンジンをシステムに付加することができる。また、証明時に利用する推論エンジンを複数の候補の中から指定することもできる。

iv) 並列実行機能：汎用並列マシン上での並列推論による高速実行を行う機能。逐次版推論エンジンをプロセッサ数分走行させるN逐次実行方式に基づいているので、逐次環境で様々な性能向上が計られているJava-MGTPの利点をそのまま活かすことが期待できる。

v) 探索制御機能：問題に対するヒューリスティックを証明探索に活かせる機能。遺伝的アルゴリズム(GA)による準最適解を求める機構に基づく。利用者は、GAの枠組(遺伝子のデザインや交配などの定義)を用いて、探索ヒューリスティックを指示する。

3) ソフトウェアの構成／構造 （Ａ４半ページ程度）

・ソフトウェアがどのような構成になるのか

・今回作る部分が大きなシステムの一部であるような場合は、どのような部分であるのか

・既存のソフトウェアに機能を付け加えるような場合には、どのようなソフトウェアにどういった機能を付け加えるのか

本システムは、大きくGUI部と推論部の二つの部分からなる。推論部は、逐次推論モジュール、並列推論モジュール、探索制御モジュール、からなる。

従来の、問題ファイルの指定、証明の開始、証明木の表示、証明木のナビゲーション等の機能に加え、証明トレースを行なうための機能を新規作成する。

ii) 逐次推論モジュール

通常の実行モード、証明木の描画のためのモード、証明トレースのためのモードをもつ。GUI部からの指示により、いずれかのモードで走行する。前二つのモードは、従来からある機能であるが、三つ目のモードは新規作成する。項と節の高速検索と分岐コストの低減機構も標準機能として取り入れる。

iii) 並列推論モジュール

指定された並列度まで並列性を抽出し並行実行を行なう。物理プロセッサ数以上の並列度を指定しても(並行実行は仮想的に行なわれるだけなので)、速度向上の点からは無意味である。

iv) 探索制御モジュール

利用者が指示する探索ヒューリスティックに基づいて探索を行なう。逐次推論モジュールと同じ三つのモジュールを持つ。

4) ブラッシュアップの内容

ソフトウェアの操作性の向上

これまでの多くの版をリリースしてきたため、利用者の立場からするとどれが標準的なMGTPであるかが分かりにくくなってきている。これは、多くの版があるのが原因ではあるが、どの版も同列に解説してきたことが直接の原因であると考える。そこで今年度は、標準的な版についての解説を主に行ない、そうではない版については、「オプショナル」な解説を行ない、標準的な使い方の習得を行ないやすくする。

さて、取り敢えずMGTPを使える段階まで達した利用者に次に待ち構えているハードルは、エラーメッセージの貧弱さである。これまでの版だとエラーがあるとそのままシステムがダウンすることもあった。エラーの主な原因は、入力節の文法エラー、入力節の値域限定性の欠如、である。これらのエラーは節の読み込み時にチェック可能なので、この部分のチェック機能の強化とエラーメッセージの充実を図る予定である。

以上の他にヘルプ機能の充実も図っていく予定である。基本的には紙に書いたマニュアルを読まずに利用できる操作環境の構築を目指す。

5) もし、ＩＦＳとの関連があれば、どのソフトウェアと関連があるのか

81. 並列定理証明器：MGTP/G Prolog版

82. 並列定理証明器：MGTP/N Prolog版

90. MGTP/G（KL1版/KLIC版）

91. モデル分散型MGTP/N（KL1版/KLIC版）

92. 制約MGTP（Prolog版/KL1版/KLIC版）

6) 使用予定言語および動作環境／必要とされるソフトウェア・パッケージ／ポータビリティなど

使用予定言語：	Java と HTML(ホームページ作成)
動作環境：	JDK1.1.xが動作する環境
必要なソフトウェア・パッケージ：	JDK1.1.x

7) ソフトウェアの予想サイズ（新規作成分の行数）：３Ｋ行

8) ソフトウェアの利用形態

利用の仕方には、二通りの方法が考えられる。一つは、WWWブラウザを利用してリモートにあるMGTPのホームページにアクセスし、そのホームページのある「アプレット」をダウンロードしてして走行させるもの、もう一つは、ローカルなマシンにインストールして「スタンドアロン」で走行させるものである。いずれにしても、JavaのAWT(Abstract Window Toolkit)を利用してGUI部は作成されているので、使用法は同じである。

MGTPの用途としては、(1) 一階論理式の充足可能性判定もしくはモデル枚挙、(2) 制約充足問題の解法、(3) 論駁、の三通りを考えている。いずれの用途でもメタ記述による探索制御やヒューリスティクスのプログラミングにより、領域知識をいかした効率的な探索を行うことができる。

証明木の探索トレースを実時間で表示する機能によって、証明の様子を追っていくことができる。これは、通常のプログラミング開発環境で提供されている実行トレースに相当する。この機能は、証明が終らない理由(証明に失敗した場合)とか、証明の性質(似たような証明を何回もやっているなど)を明らかにする際の助けになることが期待されている。

GUIを使用した対話的利用を主に考えているが、節集合を入力として与えるとその充足可能性やモデルを出力する一つのコマンドとしても利用することができ、他のシステムに組み込んで利用することも容易である。

9) 添付予定資料

ユーザマニュアル(インストール法、使用例などの記述を含む)