[3G5-GS-6] 言語メディア処理：

[3G5-GS-6-04] 依存型理論のための自動定理証明器Neural Waniの開発に向けて

〇宮川 夏菜子¹、田上 青空¹、戸次 大介¹ (1. お茶の水女子大学)

キーワード：依存型理論、形式意味論、自動定理証明器

waniは依存型理論(DTT)の自動定理証明器であり，自然言語推論への言語学的アプローチとして提案されたパイプラインの一部である．しかし，DTTにおける証明探索は決定不能であるため，waniの実行速度はパイプラインのボトルネックの1つとなっている．そこで，次に適用する規則を選択するニューラル分類器を実装することで，waniの実行速度を向上させるプロジェクト「Neural Wani」を立ち上げた．本研究では，Neural Waniプロジェクトの一環として，証明探索よりも一段階難易度の低いタスクである型検査のためのニューラル分類器を実装した．また，DTTの型判定を埋め込むための複数の異なる手法を比較し，評価した．