Hybrid MKNF with Classical Negation in the Rule Component

あなたは、世界を理解できる超スマートなロボットを作ろうとしていると想像してください。これを行うには、2つの全く異なる思考方法を教える必要があります。1つ目は、膨大な百科事典のあらゆる事実を知っている厳格な司書のようなものです。もし本にドラゴンが存在すると書いてなければ、その司書はドラゴンは存在しないと仮定しますが、書かれていることのみを慎重に述べます。2つ目は、手がかりを探して謎を解く探偵のようなものです。もし探偵が容疑者の証拠を見つけられなければ、新しい証拠が現れるまでは、その容疑者は無実であると仮定するかもしれません。

長年、科学者たちはこれら2つの思考者を一つの脳に結合しようと試みてきました。この分野は「知識表現（Knowledge Representation）」と呼ばれ、医療診断から自動運転車に至るまで、コンピュータが複雑な事柄について推論するためのバックボーンとなっています。この論文が注目している特定の手法は、「ハイブリッドMKNF」と呼ばれるものです。これは、司書の百科事典（記述論理：Description Logics）と、探偵のルールブック（論理プログラミング：Logic Programming）の結婚のようなものです。目的は、コンピュータが世界の構造を理解するために百科事典を使用させつつ、交通状況や天候のような変化する状況に対処するためにルールブックを使用させることです。しかし、落とし穴があります。探偵のルールブックには盲点があるのです。それは、「雨が降っているかどうかはわからない」（報告がないため）と言うことはできますが、「雨が降っていないことは事実として知っている」（空が晴れているという報告があるため）と言うことに苦労するという点です。これは、空港の滑走路のように、何かが「壊れていない」と確実に知ることが、何かが「壊れている」と知ることと同じくらい重要な安全重視のシステムにおいて、大きな問題となります。

この論文は、この探偵のルールブックに対する新しいアップグレードを紹介しています。それは「古典的否定（classical negation）」、つまり単に欠落しているために偽であると推測するのではなく、ある事柄が偽であることを明示的に述べる能力を扱うものです。著者であるSheela、Rey、De Granceyは、**hMKNF¬**と呼ばれる新しいシステムを提案しています。彼らは単にこのアイデアを提案しただけでなく、それが機能することを証明するための完全な数学的フレームワークを構築しました。彼らは、この新しいシステムのルールを定義する方法を示し、コンピュータが「最適」な答え（「よく定義されたモデル（well-founded model）」として知られるもの）を見つけるためのステップバイステップのレシピ（アルゴリズム）を作成しました。彼らは、この新しい方法が、たとえ複雑になっても、あらゆる事実とルールの混合を扱えることを証明し、コンピュータが情報の欠落や矛盾する手がかりによって混乱しないようにするための、3つの明確なフェーズによる計算方法を提供しました。

探偵の新しいスーパーパワー

あなたが忙しい空港を管理していると想像してください。あなたには、すべての滑走路、すべての空港、すべての飛行機のリストを持つ巨大なデータベース（「オントロジー」）があります。このデータベースは「司書」です。それは、滑走路4が空港Xにあることを知っています。しかし、データベースは現在の天候については知りません。そこで「探偵」の出番です。探偵は、ルールセットを使用して、滑走路が使用可能かどうかを判断します。

古いシステムでは、探偵の安全な滑走路に関するルールは次のようになっていました。「もし滑走路がある空港にあり、かつ、閉鎖されていることがわかっておらず、かつ、障害物があることがわかっていないならば、その滑走路は開放されている。」

ここに問題があります。もし気象レポートが遅れたらどうなるでしょうか？探偵は障害物があるかどうかを知りません。古いシステムでは、探偵は障害物の報告を見つけられないため、障害物はないと仮定して、「滑走路は開放されている！」と言うかもしれません。しかし、もし滑走路の上に巨大な岩があったとしても、その報告がまだ届いていないだけだったらどうでしょう？古いシステムは、「情報の欠如」を「不在の証明」として扱うため、危険な間違いを犯す可能性があります。

この論文は、安全が重視される状況においては、探偵が「私は確認した、そして障害物は存在しないことを知っている」と言える必要があると主張しています。これは「古典的否定」と呼ばれます。これは、「幽霊を見たことがない」と言うことと、「幽霊が存在しないことを検証した」と言うことの違いです。

3フェーズの探偵のワークフロー

著者たちは、この「それが偽であることを知る」という力を加えることが、数学をはるかに難しくすることを理解しました。単に答えを推測することはできません。確信を持たなければならないのです。そのため、彼らは、まるで調査の厳格さを増していく探偵のように、パズルを解くための3つのフェーズを設計しました。

フェーズ1：クイックスキャン（不動点計算：Fixpoint Computation）
まず、システムは素早い自動スキャンを実行します。すべてのルールと事実を調べ、「今、確実に証明できることは何か？」と問いかけます。それは、確実に真であるものと、確実に偽であるもののリストを作成します。もしパズルが単純であれば、このフェーズで即座に解決されます。システムは「よく定義された演算子（well-founded operator）」を使用します。これは、これ以上新しい事実を追加できなくなるまで、新しい事実を追加し続ける機械のようなものです。もし機械が停止し、その答えが理にかなっていれば、完了です！

フェーズ2：ロジックチェーン（単一伝播：Unit Propagation）
時として、クイックスキャンは行き詰まります。例えば、「Aが真であればBは偽である」というルールは見つけたものの、Aが真であるかどうかはまだわからない、といった場合です。しかし、もしAが真であった場合にルールが壊れることがわかる場合があります。そこで、システムは決定を強制します。「よし、もしAが真であることが矛盾を引き起こすならば、Aは偽でなければならない」と。これは「単一伝播」と呼ばれます。これは、探偵が「もし執事が犯人なら、時計は壊れているはずだ。時計は壊れていない。したがって、執人は犯人ではない」と気づくようなものです。このフェーズは、最初のフェーズが見逃した論理的な推論を強制させます。

フェーズ3：猜定と検証（最後の手段：Guess-and-Check）
クイックスキャンとロジックチェーンを経てもなお、システムが行き詰まることがあります。可能性が多すぎたり、ルールが複雑に絡み合っていたりする場合です。ここで、著者たちは、時には単に推測しなければならないこともあると認めています。彼らは「猜定と検証」フェーズを提案しています。システムは、残りの未知数に対して、「真」と「偽」のあらゆる可能な組み合わせを試します。それぞれの推測が、安定しており、一貫した物語を作成するかどうかをチェックします。もし、機能する物語、かつ「最も安全な（つまり、未定義のものが最も少ない）」物語を見つけた場合、それが答えとなります。論文では、このフェーズが最も計算コストがかかること（巨大なキーリングのすべての鍵を試すようなもの）を記していますが、システムが決して有効な解を見逃さないためには、それは必要不可欠です。

なぜこれが重要なのか

著者たちは単に新しいゲームを発明したのではなく、この新しいシステムが機能することを示す厳密な数学的証明を構築しました。彼らは、彼らの手法である hMKNF¬ が、たとえ矛盾が生じるような厄介なケースであっても、あらゆる事実とルールの混合を扱えることを示しました。彼らは、彼らの3フェーズのプロセスが、常に「よく定義されたモデル」、つまり最も信頼でき、最もリスクの低い答えを見つけ出すことを証明しました。

また、彼らは彼らの方法を以前の試みと比較しました。古い手法は単純なケースしか扱えないか、あるいはルールが非常に限定的（複雑なグループではなく、単一のアイテムのみを扱うなど）である必要がありました。彼らの新しい方法は、より柔軟で強力です。しかし、彼らはトレードオフについても正直に述べています。この追加の力（古典的否定）を許可しているため、「猜定と検証」フェーズは非常に複雑な問題に対して長い時間を要することがあります。しかし、滑走路が塞がっている状態で飛行機が離陸しないようにするといった、安全が重視されるアプリケーションにおいては、100%確信するために少し時間がかかることは、支払う価値のある代償なのです。

要約すると、この論文はコンピュータに新しいスーパーパワーを与えます。それは、単に情報が欠落していることではなく、何が「真ではない」かを明示的に知る能力です。クイックスキャン、ロジックチェーン、そして慎重な猜定と検証を組み合わせることで、彼らは世界についてより高い精度と安全性を持って推論できるシステムを構築しました。