認識様相論理（エピステミック様相論理）は、知識と信念に関する推論を形式化する様相論理の一分野である。これは命題論理を、個々のエージェントが何を知っているか、または信じているかを表現する様相演算子で拡張し、「エージェントAは命題Pを知っている」や「エージェントBはエージェントAがPを知っていると信じている」といった文の精密な分析を可能にする。この枠組みは哲学に起源を持つが、コンピュータ科学、経済学、人工知能において、マルチエージェントシステム、分散プロトコル、ゲーム理論的シナリオをモデル化するための中心的なツールとなっている。
認識様相論理の形式言語は、通常、命題変数の集合、ブール結合子、および各エージェントiに対する様相演算子K_iを含み、K_i φは「エージェントiはφを知っている」と読む。マルチエージェントシステムでは、グループGに対する共通知識（C_G φ）と分散知識（D_G φ）の演算子を追加することが多い。標準的な意味論は、1950年代後半にソール・クリプキによって導入され、1976年にロバート・オーマンによって洗練されたもので、各エージェントに対する同値関係と可能世界の集合からなるクリプキ・フレームを用いる。式K_i φは、世界wにおいて、エージェントiがwから可能と考えるすべての世界でφが成り立つ場合に真となる。
公理系
最も一般的な認識論理であるS5は、以下の公理と推論規則によって特徴づけられる。公理Kは、エージェントが含意とその前件を知っているならば、そのエージェントは後件も知っていることを述べる：K_i(φ → ψ) → (K_i φ → K_i ψ)。公理Tは、知識は真理を含意することを述べる：K_i φ → φ。公理4（正の内省）は、エージェントがφを知っているならば、そのエージェントは自分がφを知っていることを知っていることを述べる：K_i φ → K_i K_i φ。公理5（負の内省）は、エージェントがφを知らないならば、そのエージェントは自分がφを知らないことを知っていることを述べる：¬K_i φ → K_i ¬K_i φ。必然化規則は、定理φからK_i φを導出することを可能にする。
より弱い体系はこれらの公理を緩和する。論理KT（Tとも呼ばれる）は公理4と5を落とし、エージェントが内省を持たないことを許す。論理S4は公理4を保持するが公理5を落とし、これは知識よりも信念にしばしば用いられる。信念については、公理Tは公理Dに置き換えられる：B_i φ → ¬B_i ¬φ。これは信念が一貫しているが必ずしも真ではないことを述べる。これらの区別は、エージェントが不完全または不正確な情報を持つ応用において重要である。
意味論と可能世界
可能世界意味論は、知識をすべての認識論的に到達可能な世界における真理として解釈する。認識モデルM = (W, R_1, ..., R_n, V)は、世界の集合W、各エージェントに対する到達可能性関係R_i、および各世界の命題変数に真理値を割り当てる評価Vからなる。知識については、各R_iは同値関係（反射的、対称的、推移的）であり、エージェントが認識論的に同一の世界を区別できないことを反映する。世界wにおけるK_i φの真理条件は次の通りである：w R_i vとなるすべてのvに対して、M, v ⊨ φ。
共通知識は、1969年にデイビッド・ルイス、1976年にロバート・オーマンによって形式化され、「全員が知っている、全員が知っている...」という無限の連言として定義される。グループGに対して、C_G φは、Gのメンバーの到達可能性関係の任意の有限列を通じて到達可能なすべての世界でφが真である場合に成り立つ。この概念は、分散システムにおける協調行動や、合意と慣習の分析にとって決定的に重要である。
コンピュータ科学とAIにおける応用
認識論理は、1980年代から1990年代にかけてマルチエージェントシステム研究の基礎となった。1985年、ジョセフ・ハルパーンとヨラム・モーゼスは、分散システムにおける知識と共通知識に関する基礎的な研究を発表し、認識論的条件が調整攻撃問題のような協調問題の解決可能性を特徴づけることを示した。古典的な例である泥の子パズルは、無知の公的な宣言が共通知識を生成し、高次の知識についての推論を可能にすることを実証する。
人工知能において、認識論理は知識表現と推論の形式的基盤を提供する。これは、エージェントの行動が知識状態に依存する知識ベースのプログラムをモデル化するために応用されてきた。この枠組みはまた、エージェントが目標を達成するために他者が何を知っているかを推論する認識計画の基盤でもある。ゲーム理論では、オーマンの1976年の「意見の不一致に関する合意」の結果が、エージェントが互いの事後信念について共通知識を持つならば、意見の不一致に合意することはできないことを示し、認識論理と経済的推論を結びつけた。
動的認識論理
動的認識論理（DEL）は、1989年にヤン・プラザによって開発され、後にハンス・ファン・ディトマルシュ、ウィーベ・ファン・デル・ホーク、バーテルド・クーイによって拡張されたもので、公的な宣言や私的な通信による知識の変化のための演算子を追加する。φの公的な宣言は、φが偽であるすべての世界を除去することによってモデルを変換し、宣言演算子[φ!]ψは、その宣言の後にψが成り立つことを述べる。この枠組みは、情報の開示、嘘、欺瞞の効果などの現象をマルチエージェント設定で捉える。
DELは、通信プロトコル、セキュリティプロトコル、社会的相互作用のモデル化に応用されてきた。例えば、公的宣言の論理は、φの真実の宣言の後、エージェントがそれに応じて知識を更新し、潜在的に新しい共通知識を生み出すことを表現できる。この枠組みはまた、私的メッセージや同時宣言のようなより複雑な行動も扱い、情報の流れを分析するための豊かなツールとなっている。
最近の展開と課題
認識論理は、ゲーム理論、因果性、機械学習との関連で進化し続けている。研究者たちは、マルチエージェントシステムにおける公平な分割、プライバシー、セキュリティのための認識論的条件を探求してきた。認識論理と確率を組み合わせた確率的認識論理は、不確実性の下での信念の程度と知識についての推論を可能にする。これは意思決定理論や、環境についての確率的信念を維持するAIシステムのモデル化に応用がある。
一つの未解決の課題は、認識論理におけるモデル検査と充足可能性の計算複雑性である。複数のエージェントを持つS5では、充足可能性はPSPACE完全であり、モデル検査は固定された式に対して多項式時間で行える。動的認識論理はしばしばより高い複雑性を持ち、いくつかの変種は決定不能である。これらの複雑性の結果は、実用的な推論ツールの設計を導き、大規模マルチエージェントシステムにおける形式検証のスケーラビリティを制限する。
現代のAIの文脈では、認識論理はAIシステムが何を知っているか、または知らないかを指定するための形式言語を提供し、これは透明性と堅牢性に関連する。Stanford AI LabやBAIR (Berkeley AI Research)などの機関の研究者たちは、認識論理とMachine learningモデルとの間の接続を探求しており、特にLarge language modelが知識と不確実性について推論するタスクにおいて顕著である。しかし、これらの応用は依然として活発な研究領域であり、認識論理の深層学習システムへの直接的な統合は2025年時点ではまだ初期段階にある。
関連項目
- Multi-agent system
- 知識表現
- 様相論理
- Game theory
- 形式検証