研究の成果

研究上の成果

NHM変換法の実装手法

ボトムアップ手続きであるモデル生成法には、包摂検査が自然に組み込めると いう利点がある半面、ゴールと関係ないアトムを生成し無駄な推論を行うとい う欠点がある。これに対し、トップダウン手続きとボトムアップ手続きを融合 して、この問題を解決するNHM変換法の提案がなされている。この実装におい て得られた成果は以下の通りである。

1. これまで、Prologを用いて実装されていたNHM変換システムをKLICを用い て実装しなおし、その際、従来システムの変数伝搬処理を改善した。

2. NHM変換法では、変換後の節の値域限定性を遵守するため修飾子(束縛を 示すタグbまたはf)つき述語を導入する。修飾子つき述語の数 は、述語の引数の指数オーダであるので、この数を削減するには証明に必須の 修飾子のみを求めるモード解析が必要となる。本システムは、MG節集合からモー ド情報を得るための節集合に変換し(NHMモード変換部)、このモデルをMGTP上 で求めることによりモード情報を得る。このモード情報を元にMG節集合をNHM 変換する(NHM変換部)。

   従来の方法に従えば、モード情報を得る際にモード解析のためのMG節をKL1節 に変換しさらにCコンパイルすることになるが、後で述べるインタプリタ方式 のMGTPの導入によって、このコンパイルを省略でき、効率のよい実装が可能と なった。

3. 上記の変換方式では、修飾子つき述語の数は最悪の場合、依然指数オー ダである。実際、変換後の節数および証明木のサイズが膨大となり、NHM効果 が見られない例題も見受けられた。ここで、修飾子に束構造を導入し、極小修 飾子集合についてのみNHM変換を施す新たな方式を考案した。

4. NHM変換前と変換後の性能をTPTPライブラリの20題を用いて計測した。そ の結果、多くの問題で枝数および実行時間の顕著な削減効果が見られた(木の 枝数が1/10000、制限時間(1時間)で解けなかった問題が数秒で解けるようになっ た問題もあった)。

ケース分割の重複削減：フォールディングダウン

モデル生成法の証明では、一つの枝上での重複計算は包摂検査により回避でき るが、証明のケース分割により枝が分岐すると、分岐後の枝で同じ計算を行っ てしまうという問題点がある。このようなケース分割の重複計算を削除する手 法としてLetzがタブロー法に対して提案しているフォールディングダウン(FD) 法をMGTPに適用し、その効果を定量的に調べた。

FD法では、MG節を次のように書 換える。

• 左優先：
• 右優先：

TPTPライブラリの問題52題を使って評価実験を行ったところ、そのうち22題が FDを施すと、枝数および証明時間の短縮効果が見られた(枝数および証明時間 が数十分の一に減少)。

MGTPトレーサ

これまでのMGTPは、与えられた問題が充足不能であるか、または充足可能であ るかしか答えず、1)推論木の特徴、証明性能に及ぼす主要因など、どのような 推論が内部で進められているかといった情報が得られない、2)ユーザが与えた 問題節定義(一種のプログラム)の誤りやMGTPの実装に混入しているバグを検出 するのが困難である、といった問題があった。これらの問題に対処するために、 MGTPトレーサの作成を行った。

作成にあたっては、MGTP推論エンジンの書換えは極力行わない方針で臨んだ。 作成手法として、(1)メタインタプリタ方式、(2)トレースコード埋め込み方式、 (3)トレース用KL1節付加方式を検討した結果、汎用性がある(3)を採用するこ とにした。

本方式では、トレースフラグに基づきトレース手続きを実行するKL1節を元の 定義に付加するだけであり、元の定義は変更されない。この方式はMGTPのみな らず、一般のKL1プログラムにも適用可能である。また、プログラムの修正と それに伴う引数の引き回しの変更を自動的に行うKL1プログラム開発支援ツー ルにも利用できる。

インタプリタ版MGTP

KLIC上のMGTPでは、問題は、MG節→KL1節→Cプログラム→再配置可能オブジェ クトへと変換された後、リンカによって実行可能形式になる。優れたCコンパ イラの利用により、この最終的な実行可能形式は様々な最適化が施されており、 実行効率の優れたものになっている。

しかしながら、上記変換過程でCプログラム→再配置可能オブジェクトのプロ セスに要する時間が、証明時間よりはるかに長くなる、あるいはコンパイルす らできなくなる、という問題が生じた。そこで、上記MG節から再配置可能オブ ジェクトを得る変換を省略し、MG節を直接推論エンジンが読み込みこれを解釈 するインタプリタ方式のMGTPを作成した。

TPTPライブラリを用いた評価実験を行い、(1)インタプリタ版の証明時間は、 コンパイル版の1.2〜1.5倍程度の増加に抑えられている、(2)節数が少なく探 索空間も小さい問題では、インタプリタ版の全体の処理速度は、コンパイラ版 に比べ数十倍から数百倍速い、(3)節数が多く探索空間も巨大となる問題では、 インタプリタ版とコンパイラ版の全体の処理速度比は、証明速度比(0.67〜 0.83)に近づくが、節が1万個を越えるとコンパイルすらできなくなる、ことを 確認した。

ソフトウェアとしての成果

本年度は、Unix上でのMGTP開発環境を整えることを主な目的とし、図１中に示されているMGTPライブラリ群 とインタプリタ版MGTP、MGTPトレーサおよびKLICユーティリティを作成した。

先ず、ユーザはMG節形式で問題を記述し拡張子.mgのファイルに格納する。な おTPTP問題形式の問題(*.p)は、「TPTP→MG変換器」によって、MG節形式 (*.mg)に変換される。MG節は、(1)そのまま、(2)「NHM変換器」によってノン ホーンマジックセット法を実現するNHM変形節に変換される、(3)「FD変換器」 によってフォールディングダウンを行うMG節に変換される、の3通りの処理が あり、この後「dom挿入器」に渡され、値域限定性を満たすようにエルブラン 空間を張るdom述語が挿入される。

そして、コンパイル版MGTPを使用する場合には、「MGTPトランスレータ」によ りMG節はKL1節に変換される。インタプリタ版MGTPを使用する場合には、この トランスレータを介さず、直接MG節を「インタプリタ版MGTP」に入力する。

MGTPライブラリ群

MGTPライブラリ群は、Unixのフィルターとして実現されており、相互に結合が 可能である。今回作成したKLICソフトウェア( 図１中、網掛部分)は次の通りである。

NHM変換器

NHM変換器は、モード情報を得るNHMモード変換部とモード情報からNHM変 形節を得るNHM変換部からなり、コードサイズは、それぞれ380行と480行であ る。モード情報を伝播するためのMG節を元の節から作り、インタプリタ版MGTP によってそのモデルを求めることにより、モード情報を得る点が特徴的である。

FD変換器

オプションにより、左優先FDと右優先FDの指定が可能である。変換後の MG節は否定アトムを含むので、制約MGTPを用いて証明を行う。FD変換器のコー ドサイズは、84行である。

TPTP→MGTP変換器

通常は、TPTP節形式からMG節形式に変換する。この他、各節の対偶をとっ た対偶節集合を得るため、オプションにより、アトムの極性を反転させること が可能である。コードサイズは、97行である。

Dom挿入器

値域限定を満たさないMG節に対して、dom述語を挿入していく。コードサ イズは、249行である。

インタプリタ版MGTP

MG節を直接読み込み内部データベースに格納し、MG節を解釈しながら推論を進 める。各節の前件リテラルとモデル候補との照合および後件部の拡張には、 KLICで書かれた 照合ルーチンおよび変数束縛情報を後件部に伝える 変数置換ルーチンを使用する。変数環境のデータベースは、二分木構 造である。現在、モデル候補およびMG節の検索は、線形検索を用いている。

照合ルーチンと変数置換ルーチンを合わせたコードサイズは129行、 これらを使用するインタプリタ版MGTPのコードサイズは491行である。 オプションとして、

(1)全解探索(デフォルトは単解探索)、

(2)計算終了後に統計情報を表示する(デフォルトは表示しない)、

(3)トレースを行う(デフォルトは行わない)、

(4)モデルを表示する(デフォルトは表示しない)、

(5)結果(充足可能性)を表示しない(デフォルトは表示する)、

MGTPトレーサ

MGTPトレーサは、図２に示すよう に、

(1)トレース対象のMGTPエンジン(mgtp.kl1)、

(2)付加KL1節(mgtp-aux.kl1)、

(3)トレーサ本体(tracer.kl1)、

 
図２　MGTPトレーサ

MGTPエンジン中のトレースポート(トレース対象のユーザ定義述語)に対して、 対応する付加KL1節を呼び出すためのモジュール名(aux:)およびトレーサ本体 で用いるパラメータを挿入する。付加KL1節は、トレースポートに対するトレー サ呼び出し手続き節を集めたものである。この節は、トレースフラグを見てオ ンであればトレーサを呼び出し、オフであれば単に元の節(main:)を実行する。 トレースポートでは、ポートに入る前の引数の値およびポートから出る時の引 数の値を表示できる。

トレーサ本体では、ユーザからのコマンドを解析し、対応する処理を行う。ト レーサの機能としては、(1)トレースポートの設定と解除、(2)skip、leap、 killなどのトレース実行の制御および分岐の優先度指定、(3)モデル候補、モ デル拡張候補等の各種内部情報の表示と内容検索、などが行える。

トレーサ本体のコードサイズは、コマンド解析ルーチンを含めて1031行である。 このトレーサは、MGTPエンジンのみならず、一般のKL1プログラムのトレース にも利用可能である。

KLICユーティリティ

KLIC_RUNは、対話的なKL1開発環境を提供するシステムである。プログラムの 一部を作成しその部分の走行テストを行う際、全体をコンパイルせずに関連す る部分のみをコンパイルした後、引数の値を次々に変更して結果を見ることが できる。コードサイズは、420行である。

コマンド読み込みツールは、対話的なシステムを作成する際に有用である。ピ リオドによる項の終りを指定しなくてもよくgettのような使用が可能である。 コードサイズは、255行である。

残された課題

既システムの整備に関しては、KLIC上のMGTPの各種推論部を一つの推論部に統 一し、利用の簡便化を図る必要がある。

NHM変換法については、NHM変換後、木の枝数がNHMの原理に反して増えている 例題が数題あった。この原因としては、関連節が複数あった場合その評価順序 によって、証明木が異なることが考えられるが、得られた証明を分析しこれを 確認していく。また、極小修飾子集合に基づくNHM変換を実装し、その効果を 定量的に評価する予定である。

変換方式によるフォールディングダウン実装法については、より多くの例題を 用いて評価を行う他、フォールディングアップを同様の変換方式により実現す る方法を検討していく。

トレーサについては、モジュール名/パラメータ挿入の自動化および付加KL1節 の自動生成を実現する。また、KL1プログラムのトレーサとしても利用可能に していく予定である。トレース情報に基づき証明木を図形表示する可視化シス テムやMGTPプログラムのデバッガなどを開発していく。

インタプリタ方式のMGTPについては、モデル候補やMG節検索にインデキシング 機構を導入すること、および照合ルーチンの実装を改良することにより、さら なる高速化を図る。

現在のKLIC_RUNシステムは、ユーザの操作の誤りに対して脆弱であるので、誤 り処理を充実し、利便性を高める。

成果についての自己評価

本研究は2年計画であり、初年度は(1)既システムの整備(開発・デバッグ)、 (2)NHMの導入(開発)、(3)MGTPプログラミング環境の開発(方式検討)、(4)MG節 の推論記述言語としての拡張(方式検討)、(5)推論速度の高速化(方式検討)、 (6)その他ツール(開発・デバッグ)、を予定していた。

2年目に開発を予定していた(3)(4)(5)を除き、概ね当初の計画通り研究が進捗 した。また(5)については、計画にはなかったが、研究の副産物としてフォー ルディングダウン方式やインタプリタ版MGTPなどの成果が生まれた。NHM法に ついてもさらなる効率化への足掛かりが得られてきている。