研究の成果

研究上の成果

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法について もさらなる効率化への足掛かりが得られてきている。