本論文では，プログラミング言語HaskellのWebアプリケーションフレームワークYesodにて実装された，日本語自動推論システムlightblueの開発環境expressを提案する．本環境は，lightblueの推論フロー（統語・意味解析，型検査，および証明探索）に対話的な操作性を導入したものである．また，事前計算およびキャッシュ機構を取り入れることで，特定条件下での推論の検証を可能にし，対話的な試行錯誤に基づく開発作業の効率化に貢献する．

理論言語学に基づく自然言語推論は，統語・意味解析を明示的に行い，推論の妥当性や説明可能性を保証できる点で重要である．特に，形式理論に基づく推論システムは，照応解決や前提束縛といった複雑な言語現象を厳密に取り扱うことを可能にし，人間の言語理解に関する理論仮説を計算機上で検証するための基盤を提供してきた．1.1日本語自動推論システムlightbluelightblue[1,2]は，理論言語学に基づく日本語自動推論システムである．統語理論には組合せ範疇文法(CombinatoryCategorialGrammar;CCG)[3,4]を、意味理論には依存型意味論（DependentTypeSemantics;DTS）[5]をそれぞれ採用している．また，DTSの部分体系における定理自動証明器wani[6,7]と接続し，証明探索を行うことで，照応解決や前提束縛を含む複雑な言語現象の解析・自動推論を実現している．このようにlightblueは，形式的に定義された統語・意味理論に基づき，高い説明性を備えた推論を行うことを特徴とする．1.2lightblueによる推論の処理過程本節では，lightblueによる推論の処理過程を紹介する．1.2.1統語・意味解析lightblueでは，入力文に対してCCGに基づく統語解析を行い，詳細な統語情報を含む構造を導出する．解析にはCYKチャートパーシングを用いるため，文法的に許容される複数の統語構造が得られる場合がある．続いて，得られた各統語構造に対して，DTSに基づく意味合成が行われる．なお，DTSは依存型理論(DependentTypeTheory;DTT)[8]に依拠する意味論の枠組みである．1.2.2型検査合成された文の意味表示に対しては，その整合性を確認するための型検査が行われる[9]．型検査では，文の意味表示がDTTにおけるtype型を持つかどうかが検証される．意味表示に未指定項が含まれている場合には，証明探索を通じた照応解決が同時に行われる．このとき，複数の証明項が得られる場合があり，型検査の結果は複数に分岐しうる．また，入力文が複数文からなる場合には，先行文の意味表示が後続文の型検査における文脈として与えられる．この過程においても，未指定項の解決により分岐が生じるため，文脈の分岐と照応解決の分岐が組み合わさることで，型検査の結果は文ごとに乗算的に増加する．1.2.3証明探索すべての文に対する型検査が成功した後，証明探索が行われる．具体的には，前提文の意味表示から，仮説文の意味表示の型を持つ証明項が構成可能かどうかを判定する．証明項が見つかった場合にはYes，意味表示の否定への証明項が見つかった場合にはNo，いずれも得られない場合にはUnknownという推論結果を出力する．この過程において出力される証明図は，推論結果の妥当性を明示的に示すものであり，lightblueの説明性を支える重要な要素となる．Thisworkispublishedwithoutpeerreviewandislicensedbytheauthor(s)underCCBY4.0(https://creativecommons.org/licenses/by/4.0/).org/licenses/by/4.0/).程として捉え直し，その過程を文法開発者が段階的・選択的に操作可能な対象として再定義した点にある．lightblueにおける推論は，統語解析，型検査，証明探索という複数の段階から構成され，各段階において理論的に許容される複数の候補を保持しながら進行する．従来の実行方式では，これらの候補をすべて列挙した上で推論を進める「全列挙型」の枠組みが採られていたが，本研究では，推論過程に内在する分岐点そのものを明示化し，それらを操作単位として定義することを設計の中心に据える．具体的には，推論過程を以下の二種類の操作単位に分解した．第一に，統語解析段階における統語構造の選択である．CCGに基づく解析では，一つの文に対して複数の統語構造が与えられるが，本環境では，それらを並列に保持したまま，文法開発者が注目する統語構造を明示的に選択できるようにした．第二に，型検査段階における型検査結果の選択である．意味表示に未指定項が含まれる場合，照応解決の結果として複数の証明項と型検査の証明図が得られうるが，それらを個別の分岐として捉え，文脈としてどの結果を採用するかを指定可能とした．型検査結果の分岐を選択しながら，段階的に推論を進める流れを示す．このように，推論過程を分岐選択の列として再構成することにより，文法開発者は，関心のある条件下でのみ推論を進めることが可能となる．これにより，全列挙型の実行方式では困難であった特定条件下での詳細な検証や，分岐の影響を追跡する分析を実用的に支援する．3.2実装提案する開発環境expressは，関数型プログラミング言語HaskellのWebアプリケーションフレームワークYesod[11]を用いて実装されている．lightblue本体がHaskellによって実装されているため，Yesodの採用により，lightblueの内部データ構造や推論のための関数を直接呼び出すことが可能となっている．システム構成としては，サーバ側で推論の実行おorg/licenses/by/4.0/).よび推論状態の管理を行い，クライアント側で，推論結果の可視化と分岐選択の入力を担当する．サーバ側で，統語解析・型検査・証明探索の各段階において生成される結果を段階的に保持し，ユーザの選択に応じて必要な部分のみを再計算する．これにより，全列挙型の実行方式に比べ，不要な推論経路の計算を避けることができる．また，対話的操作における応答性を確保するため，推論結果を段階ごとに事前計算し，その結果をキャッシュとして保持する機構を導入した．同一の条件下で要求される推論については，キャッシュされた結果を再利用することで，文法開発者の操作に対する待ち時間を低減している．3.3主要機能3.3.1部分文字列解析expressは，入力文の一部を選択して解析を行う部分文字列解析機能を提供する．lightblueでは，CYKチャートパーシングにより，文全体だけでなく部分文字列に対応する統語構造も内部的に保持されている．本機能では，この性質を利用し，文法開発者が関心を持つ部分文字列に対して，統語・意味解析結果を即座に確認できるようにした．例を付録図5に示す．これにより，特定の部分文字列や現象に起因する問題を局所的に調査することが可能となる．3.3.2証明探索クエリのエクスポートexpressは，また，選択された推論経路に対応する証明探索クエリをエクスポートする機能を備えている．lightblueにおける証明探索クエリとは，前提文の意味表示から仮説文の意味表示の型を持つ証明項が存在するかどうかを判定する探索問題を指し，lightblueではこれを定理自動証明器waniに与えて証明探索を行う．従来の開発環境では，理論的には成立するはずの推論がwaniによる証明探索に失敗した場合でも，その際の推論条件を再現・共有する手段が整備されておらず，証明探索クエリを手作業で再構築せざるを得なかった．また，統語構造選択や型検査結果の分岐を含むlightblueの推論では，同一入力文に対して最大