時相論理を用いた物語のエンティティ状態検索

近年、ゲームやアニメ、映画や漫画といった物語コンテンツ市場が世界的に拡大を続けている[1]。その中で作品の長期継続やスピンオフ、シェアード・ユニバースなどによって非常に大規模な作品世界が展開されるコンテンツも今日では珍しくない。このようなコンテンツの越境化・大規模化に伴い物語に関わる膨大な情報をどのように管理・運用するかが課題になっており、設定や内容の確認を簡便に行うための技術が必要とされている[2]。本研究では、時間を考慮して物語におけるエンティティの状態を検索する手法について提案する。1.1状態変化の記述としての物語物語(narrative)とは送り手から受け手への事象(event)の報告である[3]。事象とは、行動や行為、偶発的な事象といった「状態の変化」を指す。古典的には物語は物語内容(story/fabula)と物語言説(discourse/plot/sjuzˇet)から構成される[3]。前者が物語世界内の事象を時系列順に並べたもので、「何を」語るかに該当するのに対して後者は物語のある順序・方法での語り方すなわち「いかに」語るかに該当する。物語内容はひとつの物語に対してただひとつ想定されるのに対して物語言説は同一の物語内容であっても無数に存在し得る。我々の関心は物語コンテンツの監修や検索にある。言い換えれば、物語世界内における事実、つまり物語内容の方に主要な興味がある。Chatman(1978)は物語内容を伝達する陳述としてある時点の状態を記述する状態陳述(stasisstatement)と、状態の変化すなわちイベントを記述する経過陳述(processstatement)の2つがあるとした[4]。物語内容に着目した場合、物語は「物語世界内のエンティティの状態とその変化の記述」とみなすことができる。課題は、いかにこれら記述の集積から情報を抽出し、検索を可能にするかということになる。1.1.1物語の情報抽出あるエンティティのある時点における状態を知るには、単純に考えれば、時系列順に並んだ記述から逐一状態とその変化を抽出していけばよい。しかしながら、自然言語の文章においてはすべての情報が明示的に語られているわけではない。発話における前提(presupposition)とはある命題が発話される前にあらかじめ知られていなければならない命題のことである[5]。例として、「フランス国王は禿である」という命題は「フランス国王が存在する」という命題を前提している。人間にとって自明な情報はしばしば省略されるため、省略された前提を適宜推測して補う必要がある。一方で記述の粒度の問題もあり、周辺的・冗長な情報は捨象し、主要な情報のみを選択的に抽出する必要がある。1.1.2状態変化の表現一般的な知識ベース、たとえば知識グラフは基本的に静的な知識体系を対象にしており、時間によって動的に変化する知識をうまく扱えない。知識すなわち命題について、古典論理(一階述語論理)の範囲では複数の時点を含んだり時点によって真理値の異なる命題を表現できない1）。1）たとえば「彼はいつもおなかを空かせている」「買い続けていればいつかは宝くじが当たる」「明日は雨が降る」といった命題は表現できない。.そのような時や人、場合によって変わりうる様相(modal)を扱うのが様相論理(modallogic)である。様相論理のひとつである時相論理(temporallogic)は時間に関する論理で、「いつでも真」「将来のある時点で真」といった複数の時点に関わる命題を扱える。この時相論理を活用した技術がモデル検査である。1.2時相論理とモデル検査形式手法のひとつであるモデル検査は、ソフトウェアやシステムなどといった状態遷移系をモデル化し、時相論理式で記述された特定の性質(仕様)を系が満たすかを検証する技術である[6,7]2）。モデル検査で使われる時相論理に計算木論理(ComputationalTreeLogic;CTL)がある。1.2.1計算木論理(CTL)CTLを使って状態遷移系のモデル検査を行う場合、系の状態とその遷移関係をクリプキ構造(Kripkestructure)として表現する。クリプキ構造𝑀は以下の5つ組によって定義される[6]。𝑀=(𝑆,𝑆0,𝑅,𝐴𝑃,𝐿)ただし𝑆は状態の集合、𝑆0⊆𝑆は初期状態の集合、𝑅⊆𝑆×𝑆は状態間が直接遷移可能かを示す到達可能関係、𝐴𝑃は部分論理式を持たない原子命題(atomicproposition)の集合、𝐿:𝑆→2𝐴𝑃は各状態において真である原子命題の集合を返す付値関数(labelingfunction)である。到達可能関係によって連続する状態の系列をパス(経路)と呼び、CTLでは命題論理の演算子(¬,∧,∨,→)に加えて、以下の演算子が使える3）。状態演算子ある状態から始まるパスを対象とする演算子である。論理式を𝜙として、X𝜙:「次の(neXt)状態で𝜙が成り立つ」F𝜙:「この先いつか(Finally)𝜙が成り立つ」G𝜙:「ずっと(Globally)𝜙が成り立つ」𝜙1U𝜙2:「𝜙2が成り立つまで(Until)𝜙1が成り立つ」の4種類がある4）。パス演算子ある状態から始まるパスの集合を対象とする演算子である。論理式を𝜙として、A𝜙:「すべて(All)のパスで𝜙が成り立つ」2）たとえば「望ましくないことがずっと起きない(e.g.デッドロックは生じない)」、「望ましいことがいつか必ず起きる(e.g.リクエストがあれば必ずレスポンスが返る)」、「どの時点でも特定の性質が実現する(e.g.いつでも応答が返る)」といった形で表現される3）CTLの構文および意味論については付録Aにまとめた。4）状態演算子にR(Release)やW(Weakuntil)が追加されることもあるが、これらは他の演算子から導出できる。E𝜙:「𝜙が成り立つパスが存在(Exists)する」の2種類がある。CTLでは、パス演算子・状態演算子を単独で使用することができず、必ず組み合わせて使わなければならない5）。すなわち、AX,AF,AG,AU,EX,EF,EG,EU,の8つが基本的な演算子となる。モデル検査では系をクリプキ構造𝑀、仕様をCTL論理式𝜙で表現し、系が仕様を満たすかを𝑀が𝜙を充足するか(𝑀⊨𝜙であるか)で判定する。1.3本研究のアプローチ本研究では、物語世界をひとつの状態遷移系、物語テキストをその状態変化の記述とみなし、テキストから情報を抽出した上で事実を検索する手法を提案する。具体的には、①LLM(大規模言語モデル)を使って物語内の情報を抽出・構造化し、②時相論理を使ったクエリを用いて物語におけるエンティティに関わる事実を時間を考慮して検索する。物語の構造化にあたっては、LLMを使うことで余分な情報を捨象しつつ文脈を考慮したうえで各時点における状態の記述と状態の変化を抽出する。検索では、時相論理とモデル検査の技術を用いることで、特定の条件を満たす時点を列挙したり、時間に関する命題の真偽を調べることを可能にする。