    \documentclass[japanese]{jnlp_2.1}
\usepackage{jnlpbbl_1.3}
\usepackage[dvipdfm]{graphicx}
\usepackage{amsmath}
\usepackage{hangcaption_jnlp}
\usepackage{array}

\usepackage{multirow}
\usepackage{gb4ea}
\newcommand{\LF}[1]{}
\newcommand{\setof}[1]{}

\Volume{25}
\Number{3}
\Month{June}
\Year{2018}

\received{2017}{10}{15}
\revised{2018}{1}{17}
\accepted{2018}{3}{6}

\setcounter{page}{295}

\jsubject{論文}
\jtitle{自然演繹に基づく論理推論の文間類似度学習・\\
	含意関係認識への応用}
\jauthor{谷中　　瞳\affiref{Author_1} \and 峯島　宏次\affiref{Author_2} \and Pascual Mart\'{i}nez-G\'{o}mez\affiref{Author_3} \and 戸次　大介\affiref{Author_2}}
\jabstract{
文と文がどのような意味的関係にあるかという文間の関連性の計算は，情報検索や文書分類，質問応答などの自然言語処理の基盤を築く重要な技術である．文の意味をベクトルや数値で表現する手法は未だ発展途上であり，自然言語処理分野においては，様々な機械学習による手法が活発に研究されている．これらの手法では，文字や単語を単位としたベクトルを入力として，それらの表層的な出現パターンとその振る舞いを学習することで，文ベクトルを獲得している．しかし，否定表現を含む文など，文の構造的意味を正確に表現できるかは自明ではない．一方で，形式意味論においては，表現力の高い高階論理に基づいて意味の分析を行う研究が発展しているが，文間の関連性のような，連続的な意味的関係を表現することが困難である．そこで本研究では，機械学習と論理推論という二つの手法を組み合わせて文間の関連性を計算する手法を提案する．具体的には，文間の含意関係を高階論理の推論によって判定するシステムの実行過程から，文間の関連性に寄与する特徴を抽出し，文間の関連性を学習する．文間類似度学習と含意関係認識という2つの自然言語処理タスクに関して提案手法の評価を行った結果，推論の過程に関する情報を特徴量に用いることによって，いずれのタスクにおいても精度が向上した．また，含意関係認識用データセットの一つであるSICKデータセットの評価では，最高精度を達成した．
}
\jkeywords{文間類似度，含意関係認識，自然演繹，論理推論}

\etitle{Learning Semantic Textual Relatedness using Natural Deduction Proofs}
\eauthor{Hitomi Yanaka\affiref{Author_1} \and Koji Mineshima\affiref{Author_2} \and Pascual Mart\'{i}nez-G\'{o}mez\affiref{Author_3} \and \\
Daisuke Bekki\affiref{Author_2}} 
\eabstract{
Learning semantic textual relatedness is a core research subject in natural language processing. Vector-based models are often used to compute sentence representations from words or predicate-argument structures, but these models cannot capture semantics accurately with consistency. Conversely, logical semantic representations can capture sentence semantics in depth and with much greater accuracy, but their symbolic nature does not offer graded notions of textual similarity. We propose a method for learning semantic textual relatedness by combining shallow features with features extracted from natural deduction proofs using bidirectional entailment relations between sentence pairs. For the natural deduction proofs, we use ccg2lambda, a higher-order automatic inference system that converts Combinatory Categorial Grammar (CCG) derivation trees into semantic representations and conducts natural deduction proofs. We evaluate our system using two major NLP tasks: learning textual similarity and recognizing textual entailment. Our experiments demonstrate that our approach can outperform other logic-based systems and we obtain high performance levels for the RTE task using the SICK dataset. Our evaluations also demonstrate that features derived from the proofs are effective for learning semantic textual relatedness and we quantify our contribution to the research area.
}
\ekeywords{Semantic Textual Similarity, Recognizing Textual Entailment, Predicate Logic, Inference, Natural Deduction}

\headauthor{谷中，峯島，Mart\'{i}nez-G\'{o}mez，戸次}
\headtitle{自然演繹に基づく論理推論の文間類似度学習・含意関係認識への応用}

\affilabel{Author_1}{東京大学}{The University of Tokyo}
\affilabel{Author_2}{お茶の水女子大学}{Ochanomizu University}
\affilabel{Author_3}{産業技術総合研究所}{National Institute of Advanced Industrial Science and Technology}



\begin{document}
\maketitle


\section{はじめに}
\label{introduction}

ある二つの文について，それぞれの文がどのような意味を持ち，一方の文と他方の文とがどのような意味的関係にあるかという文間の関連性の評価は，情報検索や文書分類，質問応答などの自然言語処理の基盤を築く重要な技術である．これまでの自然言語処理における文の意味表現の方法は，ベクトル空間モデルが主流である．情報検索においては，単語や文字の出現頻度といった表層的な情報を用いて，統計的機械学習に基づいて文ベクトルを導出する手法が用いられてきた．また，さらに正確な文の意味表現を目指して，単語やフレーズといった構成要素を組み合わせて文の意味を計算するベクトル空間モデル~\cite{Find-similar,mitchell2010composition,DBLP:conf/icml/LeM14}が提案されてきた．近年では，深層学習を用いて高精度で文の意味表現を獲得する手法~\cite{MuellerAAAI2016,hill-cho-korhonen:2016:N16-1} が多く提案されている．これらの手法では，単語ベクトルや文字ベクトルを入力として学習を行い，文ベクトルを獲得しているが，獲得した文ベクトルが否定表現や数量表現などを含む文の意味を正確に表現しているかは自明ではない．たとえば，\textit{Tom did not meet some of the players}と\textit{Tom did not meet any of the players}という文はほとんど単語が共通しており，\textit{some}や\textit{any}といった機能語は通常捨象されるか，ほぼ同じ単語ベクトルとして扱われる．しかし，前者は「\textit{Tom}は選手の何人かとは会わなかった（別の何人かの選手とは会った）」，後者は「\textit{Tom}はどの選手とも会わなかった」という意味を表しており，これらの文の意味の違いを単語や文字からの情報を用いてどのようにして捉えるかが課題となっている．そこで，統語構造を考慮したモデルなど，より高度な意味解析を取り入れたモデルの構築が期待されている．

一方で，文の意味を論理式で表現し，論理推論によって高度な意味解析を行う手法~\cite{D16-1242,mineshima2016building,abzianidze:2015:EMNLP,abzianidze:2016:*SEM}は，論理式による意味表現と整合性の高い組合せ範疇文法 (Combinatory Categorial Grammar, CCG)~\cite{Steedman00}による頑健な統語解析の発展に伴い，近年研究が進められている．論理推論を用いた手法は，文ペアに対して一方の文を他方の文が内容的に含意しているかどうかを判定する含意関係認識のタスクで高精度を達成しており，様々な自然言語処理タスクへの応用が期待されている．一方で，論理推論を用いた手法は元来厳密な手法であり，部分的・段階的な含意関係や類似関係を扱うことが困難である．

そこで本研究では，機械学習と論理推論とを組み合わせることで，柔軟かつ正確に文の関連性を学習する方法を検討する．具体的には，文の意味を論理式で表現し，2文間の双方向の含意関係について自然演繹による推論を試み，推論の過程と結果を抽出する．このとき，必要に応じて，文間の意味的関係を正しく判定するために必要な語彙知識を公理として追加して推論を試みる．語彙知識の利用によって文間の意味的関係が判定できれば，純粋な論理推論だけでは意味的関係を判定できない文ペアにおいても，部分的な推論過程から文の関連性を示す情報を抽出することが可能となる．抽出した推論の過程と結果に関する情報を用いて，文の関連性を学習する．


\section{関連研究}
\label{related}

文の意味表現を獲得し，文の関連性を学習する手法はこれまでに幅広く研究されている．特に，文の意味は文を構成する部分の意味から合成されるという構成性の原理に基づいて，単語ベクトルの加法と乗法を用いて文の意味を表現する手法~\cite{mitchell-lapata:2008:ACLMain,mitchell2010composition} が提案された．しかし，この手法には，単語の出現順序が捨象されてしまうという問題があった．そこで，述語や機能語を高階テンソル，名詞をベクトルで表現し，縮約を用いて文の意味を計算するCategorical Compositional Distributional Semantic Model~\cite{ClarkCoeckeSadrzadeh2011,grefenstette-sadrzadeh:2011:EMNLP,kartsaklis-kalchbrenner-sadrzadeh:2014:P14-2,kartsaklis-sadrzadeh:2016:COLING}が提案されている．しかし，これらの手法では比較的単純な構造の文のみを対象としており，否定や条件などの機能的な表現をどのように扱いうるかは明らかではない．

近年では，深層学習の手法を用いた文の意味表現に関する研究が活発に進められている．文間類似度学習タスクでは，単語ベクトルと類義語ベクトルから双方向型LSTMを用いて文の意味表現を学習するモデル~\cite{MuellerAAAI2016}が提案されており，最高精度を記録している．
また，構文木に沿って文の意味表現を再帰的に構築するTree-LSTMを用いたモデル~\cite{tai-socher-manning:2015:ACL-IJCNLP,zhou2016sentpair}や，LSTMを用いて文脈全体の意味を学習したのちに，CNNを用いて各文の局所的な特徴を学習するモデル~\cite{He2016PairwiseWI}など，より文の構造を考慮した深層学習のモデルが提案されている．
しかし，深層学習によるアプローチは大量の文を入力としてend-to-endで文の意味表現を学習するため，内容語と機能語の意味をどのように区別して扱っているのかは明らかではない．

一方で，論理推論によるアプローチは個々の文について意味解析を行い，直接的に文の意味表現（論理式）を獲得する．ここでの意味解析は理論言語学の知見に基づくものであり，内容語と機能語の意味を区別して扱う．文を論理式に変換し，論理推論を用いて文間の意味的関係を判定する手法には大きく分けて2つの手法が提案されている．1つは，論理推論のみを用いていわゆる教師なし学習で文間の意味的関係を判定する手法である．具体的には，タブローを用いた手法~\cite{abzianidze:2015:EMNLP,abzianidze:2016:*SEM}や，自然演繹を用いた手法~\cite{D16-1242,mineshima2016building}が提案されている．これらの手法は，文を一階述語論理式よりも表現力の高い高階述語論理式で表現し，効率的な自然言語推論を実現することによって，含意関係認識のタスクで高精度を達成している．一方で，文間類似度の計算といった，よりソフトな推論への適用が課題となっている．

もう1つの手法は，統計的機械学習と，論理推論とを組み合わせて，教師あり学習で意味的関係を判定する手法である．この手法では，論理推論で得られた結果を機械学習や確率モデルを用いて近似することで，ソフトな推論を実現している．Bjervaらは，分散表現から導出した文中の単語間類似度と，一階述語論理による推論を用いて判定した含意関係とをそれぞれ特徴量に用いて，文間類似度や含意関係を学習する手法を提案している~\cite{bjerva:semeval14} ．また，Beltagyらは，Probabilistic Soft Logicによる類似度学習方法を提案している~\cite{beltagy:semeval14}．Probabilistic Soft Logicでは，文を一階述語論理式に変換し，含意関係を満たす度合いとして単語の分散表現を用いて一方の文と他方の文との論理式間の重みを計算する．この重みを特徴量として，加法回帰モデルを用いて文間類似度を予測している．これらの先行研究から，推論による文間の含意関係の判定結果や論理式は文の言語的な情報を良質な形式で表現しているため，文間類似度学習に有用な情報であることが示唆されている．しかし，先行研究で学習に利用している推論に関する情報は，推論の判定結果（文間の意味的関係が含意・矛盾・不明のいずれであるか）や，2つの文において共通する論理式の割合にとどまっており，これらは推論から得られる情報のほんの一部でしかない．


\section{提案手法}
\label{method}

\subsection{提案手法の全体像}
\label{overall}

本研究では文の意味を文間の含意関係に基づいて規定する証明論的意味論 (Bekki and 
\linebreak
Mineshima 2017) \nocite{BekkiMineshima2016Luo}の観点から，文間の双方向の含意関係の証明を介して文間の関連性を計算する手法を提案する．一方の文と他方の文との関連が低いほど，2文間の含意関係を証明するにはより多くの公理生成や推論規則の適用が必要となり，証明の過程が複雑になる．したがって，証明の結果だけではなく，含意関係を判定するまでの証明の実行過程も，文間の関連性の評価に有用なはずである．一方の文を前提，他方の文を結論とみなして，前提から結論を導く推論の手法である{\bf 自然演繹}~\cite{prawitz1965natural}に基づく証明では，証明の実行過程を分析することが可能である．そこで提案手法では，2文間の双方向の含意関係について自然演繹による証明を試み，証明の実行過程から文間の関連性を表現する特徴量を導出する．

\begin{figure}[b]
\begin{center}
\includegraphics{25-3ia2f1.eps}
\end{center}
\caption{提案手法の全体像} 
\label{fig:1}
\end{figure}

提案手法の全体像を図~\ref{fig:1}に示す．提案手法ではまず，自然言語の英文のペア$A, B$を入力として，CCG パーザによる統語解析によって，$A, B$をCCGの導出木に変換する．次に，ラムダ計算に基づく意味合成によって，CCGの導出木から高階述語論理式$A', B'$ に変換する．次に，定理証明器を用いて，2つの論理式$A', B'$の双方向の含意関係について，自然演繹による証明を試みる．文から論理式への変換と文間の含意関係の証明には，ccg2lambda~\cite{martinezgomez-EtAl:2016:P16-4} を用いる．
ccg2lambdaは，CCGに基づく統語解析の結果を用いて文の意味を高階述語論理式で表現し，文間の含意関係について自動推論を行う統合的システムである．各入力文に対して，CCGの導出木と意味表示を出力し，また，文ペアに対しては含意関係の判定結果を出力する．
本研究では文間の含意関係の証明の実行過程を取得できるようにccg2lambdaを改良した\footnote{改良したシステムはhttps://github.com/mynlp/ccg2lambdaにて公開している．}．
このccg2lambdaが導出した文間の含意関係の証明の実行過程と判定結果を用いて，文間の関連性に関する特徴量を設計する．最後に，ランダムフォレストを用いて，文間類似度学習では回帰分析，含意関係認識では含意・矛盾・不明の3値分類を行う．次節以降で，各手順の詳細を述べる．


\subsection{CCGに基づく意味表現}
\label{ccg}

まず，CCGパーザによる統語解析によって，英語の自然言語文をCCGの導出木に変換する．CCGは語彙化文法の一つであり，統語構造から合成的に意味表示を導出することに適した文法体系である．CCGでは，基本的な統語範疇として，$N$（普通名詞），$NP$（名詞句），$S$（文）等の基底範疇が定義されている．また，複合範疇は基本範疇と二項演算子$/,\backslash$ の組み合わせによって定義される．CCGは語の統語範疇と意味表示を記述する辞書と，語から句や文を構成する際の統語構造と意味合成の計算方法を指定する少数の組合せ規則から成り立つ．

図~\ref{fig:2}に提案手法に用いるCCGの代表的な組合せ規則を示す．たとえば，関数適用規則$(>)$を適用することによって，$X/Y$という形の統語範疇および意味$f$をもつ語は，その右側にある$Y$という形の統語範疇および意味$a$をもつ語と結びつき，$X$という統語範疇および意味$fa$をもつ句が形成される．

\begin{figure}[b]
\begin{center}
\includegraphics{25-3ia2f2.eps}
\end{center}
\hangcaption{CCGの代表的な組合せ規則．関数適用規則($<, >$)，関数合成規則($> \mathbf{B}, < \mathbf{B}$)，交差関数合成規則($> \mathbf{B}_\times, < \mathbf{B}_\times$)}
\label{fig:2}
\end{figure}

CCGの導出木から文の意味表示である高階述語論理式への変換は，
ラムダ計算に基づいて行われる．
語の意味はラムダ項によって表現され，組合せ規則によってラムダ項の意味合成を行い，
文の意味表示となる論理式を導出する．

提案手法では，Neo-Davidsonian Event Semantics~\cite{Parsons90}に基づく意味表示を採用する．
たとえば，他動詞文(\ref{transitive}a)，
量化文(\ref{some-ev}a)，否定量化文(\ref{no-ev}a)はそれぞれ
次のように分析される．
\begin{exe}
\ex \label{transitive}
\begin{xlist}
\ex Bob surprised Susan.
\ex $\exists e (\LF{surprise}(e) \wedge (\LF{subj}(e) = \LF{bob}) \wedge (\LF{dobj}(e) = \LF{susan}))$
\end{xlist}
\ex \label{some-ev}
\begin{xlist}
\ex Some women are singing loudly.
\ex $\exists x (\LF{woman}(x) \wedge \exists e (\LF{sing}(e) \wedge (\LF{subj}(e) = x)
\wedge \LF{loudly}(e)))$
\end{xlist}
\ex \label{no-ev}
\begin{xlist}
\ex No women are singing loudly.
\ex $\neg\exists x (\LF{woman}(x) \wedge \exists e (\LF{sing}(e) \wedge (\LF{subj}(e) = x) \wedge \LF{loudly}(e)))$
\end{xlist}
\end{exe}
Neo-Davidsonian Event Semanticsでは，
動詞をイベントを項に持つ1項述語として分析し，
副詞や前置詞などの修飾表現をイベントを項に持つ述語として扱う．
そのため，
(\ref{some-ev}a)や(\ref{no-ev}a)の\textit{loudly}のような修飾表現を含む文も
統一的に記述できるという利点がある．
また，ここで採用する方法では，
$x$が表す項がイベント$e$を表す動詞に対して主語の関係にあることを$\LF{subj}(e)=x$，
$x$が表す項がイベント$e$を表す動詞に対して直接目的語の関係にあることを$\LF{dobj}(e)=x$のように表すことで，
動詞の必須格にイベントを項にとる関数を対応させる．
このため，個々の動詞の必須格と非必須格の境界を定める必要がないという点で，
従来のDavidsonian形式~\cite{Davidson67}よりも柔軟な意味表現となっている．
さらに，動詞をイベントに対する1項述語として統一的に扱うことで，
動詞に関する公理もまた統一的に記述することが可能となり，
自然言語の推論により適した表現形式となっている．
なお，項とイベントとの関係（意味役割）については様々な分類手法が提案されている~\cite{culicover1984,Jackendo1990}が，本稿では英語CCGBank~\cite{ac4bfc92bbc447d9b2382f4513b2520d}に基づくCCGの解析結果から確認できる項とイベントの関係を意味表示に反映する\footnote{一例として，\textit{A tree is cut by a man}のような受動態を含む文の場合は，CCGの統語解析の結果から受動態であることを判別できるため，意味解析の結果得られた主語，すなわち，\textit{a man}はcutが表すイベントに対して主語の関係をもつ項とみなされる．}．


本論文では，$\LF{subj}(e)=x$，$\LF{dobj}(e)=y$のような
イベントに関する機能的な関係を表す論理式を{\bf 機能論理式}と呼び，
内容語を担う情報を表す
$\LF{sing}(e)$，$\LF{loudly}(e)$のような論理式を{\bf 内容論理式}と呼ぶことで区別する．

辞書では，統語範疇単位で意味を指定する意味割り当てのテンプレートと，
量化や否定表現などの論理語・機能語に対して語単位で意味を指定する語彙項目の2種類を使用する．
文の意味表現を合成的に与えるにあたって，イベントの量化をどのようにして正しく扱うかという問題がある．量化名詞句や否定を含む文では，一般的にイベントの存在量化よりも量化名詞句や否定が広いスコープをとることが知られている．そこで本論文では， 先行研究~\cite{champ2015,mineshima2016building}に従い，動詞自体をイベントの量化を導入する表現として扱う．また，副詞等の修飾表現は，動詞によって導入された存在量化子のスコープ内に出現しなくてはならない．そこで，動詞の型を繰り上げ，動詞が修飾表現を項にとるように扱う．

以上の分析に従ったCCG導出木の具体例として，文(\ref{no-ev}a)の
CCG導出木を図~\ref{fig:nowomen}に示す．
ここで，$\top$はトートロジーに対応する命題定項であり，
$\top$の挿入は意味合成の過程で必要となる操作である~\cite{D16-1242}．
最終的に導出された論理式は
(\ref{no-ev}b)の論理式と同値である．

\begin{figure}[t]
\begin{center}
\includegraphics{25-3ia2f3.eps}
\end{center}
\caption{\textit{No women are singing loudly.}のCCG導出木と意味表示} 
\label{fig:nowomen}
\end{figure}

ccg2lambdaの先行研究~\cite{EACL2017}では，複数のCCGパーザを組み合わせて統語解析に用いることによって，構文的曖昧性が解消され，含意関係の推論精度が向上したことが報告されている．提案手法ではC\&C~\cite{clark2007wide}，EasyCCG~\cite{Lewis14a*ccg}，depccg~\cite{yoshikawa-noji-matsumoto:2017:Long}という3種類のCCG パーザを用いて統語解析を行う．得られた3種類のパーズ結果を用いて意味合成と推論を行い，適切なパーズ結果を選択する．含意関係の正解ラベルが付与されたデータセットによる評価においては，トレーニングデータから特徴量を抽出する際に，含意関係の正解ラベルと同じ結果を導出するパーズ結果を優先して採用する．正解ラベルと同じ結果を導出できたパーズ結果が存在しなければ，統語解析に成功した結果を優先して採用する．含意関係の正解ラベルが存在しないデータセットによる評価では，統語解析に成功した結果を優先して採用する．また，複数のCCGパーザの結果において，含意関係の判定結果（yes, no, unknownのいずれか）が得られた場合は，より正確なパーズ結果を採用するため，パーザの精度が高い順に，depccg，EasyCCG，C\&Cの順に優先してパーズ結果を採用する．


\subsection{自然演繹による証明戦略の概要}
\label{strategy}

本節では，提案手法で用いる自然演繹による証明戦略の概要について述べる．
文間の含意関係とは一方の文の情報が他方の文の情報を含むという関係であり，方向性を持った関係であるが，類似関係は方向性を持たない対称的な関係である．よって，「$A$ならば$B$」が成り立つか否かという一方向の含意関係ではなく，「$A$ならば$B$」「$B$ならば$A$」がそれぞれ成り立つか否かという双方向の含意関係の証明を試みることによって，文間の関連性に関してより多くの情報が取得できると考えられる．そこで，本研究では文$A, B$間の双方向の含意関係の証明を介して，文$A, B$間の関連性を表す特徴を獲得する．

文間の含意関係の証明には，高階論理・型理論に基づく定理証明器であるCoq~\cite{opac-b1101046}を用いる．Coqは自然演繹に基づいて推論規則を適用し，証明を行う．また，Ltacという記述言語を用いて証明探索の手続きを定義することによって，証明の自動化が可能である．ccg2lambdaはCoqの一階述語論理の部分系に対する自動推論を含む自動証明機能と，高階の公理とを組み合わせることで，自然言語の効率的な推論を可能にしている．

提案手法で用いる文間の含意関係の証明の全体的な流れは次の通りである．まず，文$A, B$を論理式$A', B'$に変換し，一方の文を証明に用いる{\bf 前提}，他方の文を証明対象である{\bf 結論}（{\bf ゴール}）とみなして，$A' \Rightarrow B'$，$B' \Rightarrow A'$ の証明を行う．証明に失敗した場合は，結論を否定した$A' \Rightarrow  \neg B'$，$B' \Rightarrow \neg A'$ の証明を行う．これは結論の否定が証明可能な場合は，結論も結論の否定も証明不可能な場合と比較して，論理式が共通の部分を多く含み，文間の関連度が高くなることを考慮している．実際に，評価に用いる文の意味的類似度データセットであるSemEval2014 Task1 のSentences Involving Compositional Knowledge (SICK) ~\cite{MARELLI14.363} では，含意関係の正解ラベルが「矛盾」である文ペアの7割において，正解の類似度スコアが高く設定されている．

結論の証明，結論の否定の証明の両方に失敗した場合は，前提のプールにある論理式からは導くことができない論理式（{\bf サブゴール}）が結論中に残っていることを意味する．
そこで次に，前提のプールにある論理式と証明できないと判定されたサブゴールとの述語間の意味的関係について，語彙知識を用いてチェックし，公理の生成を試みる．生成した公理を用いて再度$A' \Rightarrow B'$，$B' \Rightarrow A'$の証明を試みる．$A' \Rightarrow B'$，$B' \Rightarrow A'$の証明に失敗した場合は，生成した公理を用いて結論を否定した$A' \Rightarrow \neg B'$，$B' \Rightarrow \neg A'$の証明を試みる．

公理を生成しても，結論と結論の否定の両方の証明に失敗した場合は，$A' \Rightarrow B'$，$B' \Rightarrow A'$の証明の途中で証明不可能と判定されたサブゴールをスキップして，強制的に証明を終了させる．ここまでの推論における，生成した公理に関する情報や，強制的にスキップしたサブゴールの情報といった推論の情報をCoqの出力結果から抽出し，文間の関連性を表す特徴量として利用する．


\subsection{含意関係の証明}
\label{entail}
含意関係の証明の例として，以下の2つの文$A, B$間の含意関係について，自然演繹による証明を試みる．

$A$: \textit{A man is singing in a bar.}

$B$: \textit{A man is singing.}

\noindent 文$A, B$は統語解析，意味解析を経て，以下のような論理式$A', B'$に変換できる．
\begin{align*}
& A': \exists e_1 x_1 x_2(\LF{man}(x_1) \wedge \LF{sing}(e_1)
    \wedge (\LF{subj}(e_1) = x_1) \wedge \ \LF{bar}(x_2) \wedge \LF{in}(e_1, x_2)) \\
& B': \exists e_1 x_1(\LF{man}(x_1) \wedge \LF{sing}(e_1) \wedge (\LF{subj}(e_1) = x_1))
\end{align*}
まず，$A' \Rightarrow B'$について，自然演繹による証明を試みる．
ここで，論理式$A', B'$は推論規則を適用することによって分解することができる．図~\ref{InferenceRules} に本研究で用いる推論規則の例を示す．自然演繹の推論規則には導入規則と除去規則の2つがある．導入規則は結論をどのように証明するかを指定するための規則である．除去規則は前提をどのように証明に利用するかを指定するための規則であるが，主に前提のプールにある論理式をより小さい論理式に分解するために用いられる．

\begin{figure}[t]
\begin{center}
\includegraphics{25-3ia2f4.eps}
\end{center}
\hangcaption{自然演繹の証明で用いる推論規則の例．$P, P_1, \ldots P_n$は前提の論理式，$G, G_1, G_2$は結論（ゴール）の論理式を表す．いずれの推論規則においても，規則適用前の論理式は矢印の上部に，規則適用後の論理式は矢印の下部に示す．}
\label{InferenceRules}
\end{figure}
\begin{figure}[t]
\begin{center}
\includegraphics{25-3ia2f5.eps}
\end{center}
\caption{2文間の含意関係の証明プロセスの例}
\label{ProcessEntail}
\end{figure}

$A' \Rightarrow B'$ の証明プロセスを図~\ref{ProcessEntail}に示す．図~\ref{ProcessEntail}において，論理式$A'$は前提$P_0$， 論理式$B'$は結論$G_0$に配置される．$P_0$と$G_0$は除去規則({\small$\wedge$-\textsc{Elim}, $\exists$-\textsc{Elim}})と導入規則 ({\small$\wedge$-\textsc{Intro}, $\exists$-\textsc{Intro}})の適用によって，前提の集合 $\mathcal{P} = \setof{P_2, P_3, P_4, P_5, P_6}$とサブゴールの集合$\mathcal{G} = \setof{G_2, G_3, G_4}$に分解される．
証明はサブゴール$G_j$と述語と項が一致する前提 $P_i$を探索する形で進められ，マッチする前提が見つかればそのサブゴールを解決できる．全てのサブゴールが解決できれば$A' \Rightarrow B'$の証明が示せたことになる．この例では，サブゴール$G_2, G_3, G_4$と前提$P_2, P_3, P_4$の述語と項がそれぞれマッチし，全てのサブゴールが解決できるため，公理を生成せずに$A' \Rightarrow B'$を示すことができる． 

次に，図~\ref{ProcessEntail}の前提$P_0$と結論$G_0$を逆転させて，$B'$を証明の前提， $A'$を証明の結論とみなし，$B' \Rightarrow A'$の証明を試みる．先ほどと同様に，推論規則の適用によって，前提の集合 $\mathcal{P}$とサブゴール$\mathcal{G}$の集合を得ることができる．
\begin{align*}
\mathcal{P} & = \{P_2: \mathbf{man}(x_1), \, P_3: \mathbf{sing}(e_1), \, P_4: \mathbf{subj}(e_1) = x_1\} \\
\mathcal{G} & = \{G_2: \mathbf{man}(x_1),\, G_3: \mathbf{sing}(e_1),\, G_4: \mathbf{subj}(e_1) = x_1,\, G_5: \mathbf{bar}(x_2),\, G_6: \mathbf{in}(e_1, x_2))\} 
\end{align*}
この場合，2つのサブゴール$G_5, G_6$は前提のプールにあるどの論理式ともマッチしないため， 解決できずに残り，$B' \Rightarrow A'$の証明に失敗する．そこで次に，語彙知識からの公理生成を試みる．しかし，この場合は残っているサブゴールの述語$\LF{bar}(x_2)$の項$x_2$をシェアする述語が前提$\mathcal{P}$中に存在しないため，公理を生成することができない．
そのため，このような例からも部分的な証明プロセスの情報をCoqから取得するため，本研究では解決できなかったサブゴール$\LF{bar}(x_2), \LF{in}(e_1,x_2)$をスキップして，強制的に$B' \Rightarrow A'$の証明を終了させる．


\subsection{矛盾関係の証明}
\label{contra}

矛盾関係の証明について述べる上で，まず否定の推論規則について説明する．
否定の基本的な含意関係は，論理式$A$の否定$\neg A$を，命題定項 \LF{False}を用いて，
$A \to \LF{False}$（$A$が偽を含意する）と定義することで捉えることができる．
この定義に従って，否定の推論規則は図~\ref{NegationRule}に示す規則を用いる．
否定の導入規則($\neg$-\textsc{Intro})は，もしゴールの論理式が
$\neg \mathcal{A}$という形であれば，$\mathcal{A}$を新たに前提に加えて，
矛盾(\LF{False})の証明を試みるという形をとる．
一方，否定の除去規則($\neg$-\textsc{Elim})は，
前提に$\neg \mathcal{A}$という形の論理式があり，
ゴールが矛盾(\LF{False})であるとき，ゴールを$\mathcal{A}$に更新し
この新たなゴールの証明を試みる，というものである．

\begin{figure}[b]
\begin{center}
\includegraphics{25-3ia2f6.eps}
\end{center}
\caption{否定の推論規則}
\label{NegationRule}
\end{figure}

矛盾関係の証明の例として，以下の2つの文$A, B$間の矛盾関係について，自然演繹による証明を試みる．

$A$: \textit{No man is singing.}

$B$: \textit{There is a man singing loudly.}

\noindent
図~\ref{ProveContra}に矛盾関係の証明プロセスを示す．文$A, B$は論理式$A', B'$に変換後， 前提$P_0, P_1$にそれぞれ配置され，結論$G_0$には\LF{False}が配置される．
否定の除去規則$\neg$-\textsc{Elim}を$P_0$に適用することによって，ゴールは$G_1$に更新される．
ここで，除去規則を適用することによって，
前提$P_1$は前提の集合$P_2, P_3, P_4, P_5$に分解される．
同様に，導入規則を適用することで，ゴール$G_1$は
サブゴールの集合$G_2, G_3, G_4$に分解される．
全てのサブゴールが前提とマッチするため，
文$A, B$の矛盾関係，すなわち，$A' \Rightarrow \neg B'$ を示すことができる．

\begin{figure}[t]
\begin{center}
\includegraphics{25-3ia2f7.eps}
\end{center}
\caption{\label{ProveContra}2文間の矛盾関係の証明プロセスの例}
\end{figure}


\subsection{語彙知識を用いた公理の生成}
\label{axiom_injection}

本節では，自然演繹の推論に用いる公理の具体的な生成手順について述べる．
まず，証明の途中で証明不可能と判定されたサブゴールに関して，前提と結論で同じ項をシェアしている述語を生成する公理の候補として絞り込む．さらに，同じ項をシェアしている述語の中でも，項の格が同じである述語について優先して公理を生成する．

公理生成を導入した証明の例として，以下の2つの文$A, B$間の含意関係の証明を考える．

$A$: \textit{A kitten plays in a house colored in green.}

$B$: \textit{A young cat plays in a green house.}

\noindent 文$A, B$は統語解析，意味解析を経て，以下のような論理式$A', B'$に変換できる．
\begin{align*}
 & A': \exists e_1 e_2 x_1 x_2 x_3(\LF{kitten}(x_1) \wedge \ \LF{play}(e_1)
    \wedge \ (\LF{subj}(e_1) = x_1) \\
 & \qquad \wedge \ \LF{house}(x_2) \wedge \ \LF{color}(e_2) \wedge \ (\LF{dobj}(e_2) = x_2) \wedge \ \LF{in}(e_1, x_2) \wedge \ \LF{green}(x_3) \wedge \ \LF{in}(e_2, x_3)) \\
 & B': \exists e_1 x_1 x_2(\LF{young}(x_1) \wedge \ \LF{cat}(x_1) \wedge \ \LF{play}(e_1)
    \wedge \ (\LF{subj}(e_1) = x_1) \\
 & \qquad \wedge \ \LF{green}(x_2)  \wedge \ \LF{house}(x_2) \wedge \ \LF{in}(e_1, x_2))
\end{align*}

これら2つの論理式$A', B'$について，$A'$を証明の前提，$B'$を証明の結論（ゴール）とみなし，公理生成を行わずに$A' \Rightarrow B'$の証明を試みる．
図~\ref{ProcessEntail}と同様に$A' \Rightarrow B'$の含意関係の証明を進めると，下記のような前提の集合 $\mathcal{P}$とサブゴール$\mathcal{G}$の集合が得られる．このステップでは，存在量化子が除去され，$A' $，$B' $に共通する述語については，変数の単一化が起こっている．
\pagebreak
\begin{align*}
\mathcal{P} & = \{P_1: \LF{kitten}(x_1),\ P_2: \LF{play}(e_1),\ P_3: \LF{subj}(e_1) = x_1,\ P_4: \LF{house}(x_1), \\
 & \qquad  P_5: \LF{color}(e_2),\ P_6: \LF{dobj}(e_2) = x_2,\ P_7: \LF{in}(e_1, x_2),\ P_8: \LF{green}(x_3),\ P_9: \LF{in}(e_2, x_3)\} \\
\mathcal{G} & = \{G_1: \LF{young}(x_1), G_2: \LF{cat}(x_1), G_3: \LF{green}(x_2)\}
\end{align*}

この例では，$\LF{young}(x_1), \LF{cat}(x_1), \LF{green}(x_2)$という3つのサブゴールが残り，証明に失敗する．ここで，前提中の論理式$\LF{kitten}(x_1)$と共通の項$x_1$をシェアしているサブゴール$\LF{young}(x_1), \LF{cat}(x_1)$が生成する公理の候補となる．語彙知識から\textit{young cat}と\textit{kitten}間の意味的関係が確認できれば，\textit{young cat}と\textit{kitten}間に関する公理を生成でき，生成した公理を利用することで，これら2つのサブゴールを解決できる．なお，証明に用いた公理の数や確信度はのちに文間の関連性を学習するための特徴量として使用するが，$\forall x. \LF{kitten}(x) \Rightarrow \LF{young}(x)$, $\forall x. \LF{kitten}(x) \Rightarrow \LF{cat}(x)$のように，複数のサブゴールに関して同じ前提から導出した公理については，まとめて1つのフレーズの公理とみなす．
また，残りのサブゴール$\LF{green}(x_2)$については，述語の表層形が同一である論理式$\LF{green}(x_3)$が前提中に存在するが，項は一致していない．このように，サブゴールに残っている述語と表層形が完全に一致する述語が前提中に含まれる場合に限り，例外的に，述語の型や項が異なっていても公理を生成して証明に用いる．

本研究では公理生成に用いる語彙知識として，WordNet~\cite{Miller:1995:WLD:219717.219748}と，Word2Vec~\cite{NIPS2013_5021}で学習した単語ベクトルを用いる．
まず，WordNetを用いて形態変化，派生形，同義語，反意語，上位語，類似性，下位語の順に，前提と結論中の述語間の意味的関係をチェックし，いずれかの関係にマッチした場合は確信度つき公理を生成する．WordNetに述語間の関係が存在しない場合は，Word2Vecで学習した単語ベクトルを用いて前提と結論中の述語間の類似度を計算し，やはり確信度つきの公理を生成する．本研究では，Google News Corpus（約30億語）で学習済みの200次元の単語ベクトルを語彙知識に用いる．ここで，公理の確信度には，述語間の類似度を採用し，生成された公理の中で確信度が最も高い公理を証明に採用する．また，確信度が閾値よりも低い公理は意味的関係が低い公理であるとみなして採用しない．公理の確信度はいずれも0.0から1.0の範囲の値をとり，本研究では公理の確信度の閾値を0.25とする．WordNetを用いて公理を生成した場合は，述語間に共通する上位概念への最短経路の長さを公理の確信度とし，Word2Vecを用いて公理を生成した場合は，Word2Vecのコサイン類似度を公理の確信度とする．


\subsection{証明に基づく特徴量の導出}
\label{logic}

ここまでの自然演繹の証明の実行過程と結果に関する情報から，計9種類の特徴量を導出する．いずれも0.0から1.0の範囲の値に正規化する．

\begin{itemize}
\item 公理の数と公理の確信度

証明に利用した公理の数と確信度をそれぞれ特徴量に用いる．複数の公理を生成した場合は，導入した各公理の確信度の平均を公理の確信度の特徴量として採用する．また，公理を1つも利用しなかった場合は，公理の確信度の特徴量を1.0とする．

\item 証明可能なサブゴールの数の割合

証明可能なサブゴールの数の割合が高いほど文間の関連度が高くなると仮定して，$n/m$（$m$：前提のプールに現れる論理式の数，$n$：証明でスキップしなかったサブゴールの数）を特徴量として導出する．ここで，サブゴールとして残る論理式には$\LF{bar}(x_2)$のような内容論理式と，$\LF{subj}(e_1) = x_1$のような機能論理式の2種類がある．そこで，内容論理式と機能論理式のそれぞれについてサブゴールの数の割合を計算し，それぞれ別の特徴量とした．また，公理生成による証明を試みた場合は，証明可能なサブゴールの割合は公理生成の前後によって変わるため，公理生成前と公理生成後のそれぞれについてサブゴールの数の割合を計算し，それぞれ別の特徴量とした．

\item 証明不可能なサブゴールの項の関係

文の主語や目的語が異なると，修飾語が異なる場合よりも文間の関連度が低くなると仮定して，証明不可能と判定されたサブゴールの項とイベントの関係をチェックする．本研究では，内容論理式中の主語($\LF{subj}$)，直接目的語($\LF{dobj}$)，間接目的語($\LF{iobj}$)をチェック対象とする．証明不可能と判定された全てのサブゴールにおける当該サブゴールの割合を特徴量として導出する．

\item 証明のステップ数

証明が簡潔であるほど文間の関連度が高くなると仮定して，自然演繹の証明図の推論ステップ数を特徴量に用いる．

\item 推論規則の適用回数

証明において推論規則の適用回数が多いほど証明が複雑になり，文間の関連度が低くなると仮定して，全推論規則の適用回数における各推論規則の適用回数の割合を特徴量に用いる．提案手法では図~\ref{InferenceRules}に示した
連言の除去規則と導入規則 ($\wedge$-\textsc{Elim}, $\wedge$-\textsc{Intro})，含意の除去規則と導入規則 ($\to$-\textsc{Elim}, $\to$-\textsc{Intro})，存在量化の除去規則と導入規則 ($\exists$-\textsc{Elim}, $\exists$-\textsc{Intro})，等号の除去規則 ($=$-\textsc{Elim}) という計7種類の推論規則を対象とする．

\item 証明の結果

結論が証明可能か，結論の否定が証明可能か，結論も結論の否定も証明不可能かチェックし，それぞれ該当する場合は1.0，該当しない場合は0.0を特徴量とする．

\item 前提と結論における述語の一致率

前提と結論との間で述語が一致しているほど，文間の意味的関係を証明できる可能性が高いことを考慮して，前提と結論で述語が一致している割合を特徴量に用いる．

\item 前提と結論における型の一致率

前提と結論との間で論理式の型が一致しているほど，文間の意味的関係を証明できる可能性が高いことを考慮して，前提と結論で型が一致している割合を特徴量に用いる．

\item 否定演算子の有無

前提と結論のどちらか一方だけに否定演算子 ($\neg$) が含まれる場合と，両方に含まれる，または，どちらにも含まれない場合とでは，前者の方が文間の関連度が低くなると仮定して，前者の場合は0.0，後者の場合は1.0として特徴量に用いる．
\end{itemize}


\subsection{表層情報と外部知識から導出した特徴量の設計}
\label{nonlogic}

提案手法では学習精度を向上させるため，表層情報と外部知識から導出した特徴量を自然演繹の証明に基づく特徴量と組み合わせて用いる．表層情報と外部知識から導出した特徴量は10種類の特徴量を用いる．特徴量はいずれも0.0から1.0の範囲の値に正規化する．
\begin{itemize} 
\item 品詞の一致率

文中の各単語の品詞（本研究で使用する品詞はPenn Treebank品詞体系に準ずる）をC\&C POS tagger~\cite{curran2003investigating}を用いてチェックし，2文間において単語の品詞が一致する割合を特徴量に用いる． 
\item 名詞の一致率

文中の名詞をレンマ化し，2文間の名詞が一致する割合を特徴量に用いる． 
\item 動詞の一致率

文中の動詞をレンマ化し，2文間の動詞が一致する割合を特徴量に用いる．
\item 文字列の類似度

{\sl Difflib}\footnote{\texttt{https://docs.python.org/3.5/library/difflib.html}}を用いて文字列の類似度を計算し，計算結果を特徴量に用いる． 
\item 同義語集合の一致率

2文中の全ての単語について，同義語集合をWordNetを用いてチェックし，2文間の同義語集合の一致率を特徴量に用いる．

\item 概念間の距離

一方の文と他方の文の全ての単語間について，単語間類似度をWordNetの概念間の距離を用いて導出し，概念間の距離の平均を特徴量に用いる．
\item 文の長さ

2文間の文字数の差と，2文間の文字数の平均を特徴量に用いる．

\item ベクトル空間モデルにおけるコサイン類似度

TF/IDFベクトル間のコサイン類似度，latent semantic analysis (LSA)~\cite{LSA}ベクトル間のコサイン類似度，latent Dirichlet allocation (LDA)~\cite{LDA}ベクトル間のコサイン類似度をそれぞれ特徴量に用いる．各ベクトルの次元は200次元とする．

\item CCG導出木のマッピングコスト

文ペアの導出木の形が似ていないほど，一般的には文間の関連度が低くなることが見込まれる．そこで，文ペアのCCG導出木の各ノード間の対応度合い（CCG導出木のマッピングコスト）を計算する手法~\cite{martinezgomez-miyao:2016:EMNLP2016}を用いて，マッピングコストを計算する．このマッピングコストを文ペアの導出木のノード数合計で除算した値を特徴量に用いる．

\item 受動態表現の有無

前提と結論のどちらか一方だけに受動態表現が含まれる場合と，両方に含まれる，または，どちらにも含まれない場合とでは，前者の方が類似度が低くなると仮定して，一方の文と他方の文の受動態表現の有無をチェックし，前者の場合は0.0，後者の場合は1.0として特徴量に用いる．

\end{itemize}


\subsection{文の関連度学習}
\label{model}

導出した特徴量を用いて，文の意味類似度と含意関係を予測する．本研究では，ロジスティック，SVM，ランダムフォレストという3種類の学習モデルで事前学習を行った結果，文の意味類似度学習はランダムフォレスト回帰，含意関係認識ではランダムフォレスト分類を学習モデルとして採用する．ハイパーパラメータはグリッドサーチを用いて最適化する．


\section{実験}
\label{experiment}

\subsection{データセット}
\label{dataset}

文の意味的類似度と含意関係認識の評価用データセットであるSemEval2014 Task1 SICKデータセット~\cite{MARELLI14.363}と，文の意味的類似度の評価用データセットであるSemEval2012 MSR-videoデータセット~\cite{semeval2012}の2種類のデータセットを用いて，提案手法の評価を行った．

SICKは，2つの文の意味的類似度と含意関係を予測するタスクであり，表~\ref{SICKexample}に示すように，類似度と含意関係(yes, no, unknown)が人手によって付与されている．類似度は1.0から5.0の範囲の値で付与されている．このデータセットには計9,927件の文ペアが含まれており，そのうち訓練データ，開発データ，テストデータはそれぞれ4,500件，500件，4,927件含まれている．
MSR-videoは 表~\ref{MSRexample}に示すように，含意関係のラベルは付与されておらず，類似度の正解スコアのみが0.0から5.0の範囲の値で付与されており，開発データ，テストデータが750件ずつ含まれている．SICKデータセットに含まれる文ペアの方がMSR-videoデータセットに含まれる文よりも単語数が多くなっており，それぞれのデータセットにおける一文あたりの平均単語数は，SICKデータセットは10単語，MSR-videoデータセットは6単語である．

\begin{table}[t]
\caption{SICKデータセットに含まれる文ペアの例}
\label{SICKexample}
\input{02table01.tex}
\end{table}
\begin{table}[t]
\caption{MSR-videoデータセットに含まれる文ペアの例}
\label{MSRexample}
\input{02table02.tex}
\end{table}


\subsection{既存手法との比較評価の概観}
\label{eval}

\subsubsection{文間類似度学習}
\label{eval_sts}

まず，文間類似度学習の評価を行った．なお，評価指標は，各タスクで標準的に使用されている評価指標に基づいて，SICKデータセットについては，提案手法によって計算された類似度スコアと，データセットに付与された正解スコアとのPearson相関係数$\gamma$，Spearman相関係数 $\rho$，平均二乗誤差 (MSE)という3種類の指標を，MSR-videoデータセットについてはPearson相関係数$\gamma$のみを用いる．比較対象は，SICKデータセット，MSR-videoデータセットにおける最高精度のモデル~\cite{MuellerAAAI2016,bar:semeval12} と，推論を用いた既存手法として，先行研究で紹介したThe Meaning Factory~\cite{bjerva:semeval14}, UTexas~\cite{beltagy:semeval14}とする．

表~\ref{SICK-sts}にSICKデータセットにおける提案手法と既存手法との類似度学習の評価結果を示す．提案手法の結果と推論を用いた既存手法の結果とを比較すると，Pearson相関係数とSpearman相関係数に関しては，提案手法は推論を用いた既存手法よりも高精度を達成した．一方で，MSEに関しては，既存手法よりも精度が低かった．この原因としては複数の要因が挙げられるが，大きく分けて統語解析によるエラー，意味表示の誤りによるエラー，語彙知識の不足などに起因する誤った推論によるエラーに分けられる．これらのエラーの詳細は\ref{error}節で述べる．
また，文間類似度学習においては，提案手法は深層学習を用いたモデルによる最高精度に達しなかった．この原因を分析するため，テストデータ4,927件の文例に対して，提案手法と最高精度のモデルが予測した類似度スコアの比較を\ref{deep}節で行った．

\begin{table}[t]
\caption{提案手法と既存手法との類似度学習の評価結果 (SICK)}
\label{SICK-sts}
\input{02table03.tex}
\end{table}

表~\ref{MSR-sts}にMSR-videoデータセットにおける提案手法と既存手法との類似度学習の評価結果を示す．MSR-videoデータセットにおいても，提案手法は推論を用いた既存手法よりも高精度を達成した．
また，公理生成に使用する語彙知識については，SICKではWordNetのみを語彙知識に使用した場合，MSR-videoではWordNetとWord2Vecの両方を語彙知識に使用した場合において最も精度が高かった．この原因はSICKとMSR-videoのデータセットの違いによるものであると考えられる．\ref{dataset}節で述べたように，SICKデータセットに含まれる文ペアの方がMSR-videoデータセットに含まれる文よりも単語数が多く，\textit{burrow a hole}と\textit{dig the earth}の言い換えといったフレーズレベルの言い換えが多く含まれていた．そのため，MSR-videoデータセットにおける評価ではWord2Vecを用いて単語間の語彙知識を拡充することによって精度が向上したが，SICKデータセットにおいてはフレーズ間の公理を生成できず，Word2Vecの利用によって誤った公理の過剰生成が起こり，精度が低下したと考えられる．公理の過剰生成に関する具体例については\ref{error}節で紹介する．今後，フレーズレベルの語彙知識の拡充や公理生成の改善を行うことで，更なる精度向上が見込まれる．

\begin{table}[t]
\caption{提案手法と既存手法との類似度学習の評価結果 (MSR-video)}
\label{MSR-sts}
\input{02table04.tex}
\end{table}


\subsubsection{含意関係認識}
\label{eval_rte}

次に，SICKデータセットを用いて含意関係認識の評価を行った．
評価指標は，適合率（yes, noと予測した文ペアに対して，正解ラベルと同じ結果だったケースの割合），再現率（正解ラベルがyes, noである文ペアに対して，正解ラベルと予測ラベルが同じ結果だったケースの割合），正答率（yes, no, unknownのすべての文ペアに対して正解ラベルと予測ラベルが同じ結果だったケースの割合）の3種類の指標を用いた．
比較対象は，SICKデータセットにおける最高精度のモデル~\cite{yin-schutze:2017:EACLlong}と，推論を用いた既存手法として，先行研究で紹介したThe Meaning Factory~\cite{bjerva:semeval14}, UTexas~\cite{beltagy:semeval14}，また，改良前のccg2lambda~\cite{EACL2017}の結果とする．

表~\ref{SICK-rte}に提案手法と既存手法との含意関係認識の評価結果を示す．
語彙知識にWordNetのみ，WordNetとWord2Vecの両方を使用した場合において，提案手法は最高精度を達成した．

\begin{table}[b]
\caption{提案手法と既存手法との含意関係認識の評価結果 (SICK)}
\label{SICK-rte}
\input{02table05.tex}
\end{table}

公理生成に使用する語彙知識については，含意関係認識のタスクにおいてもWordNetのみを語彙知識に使用した場合が最も精度が高かった．この原因について，\ref{eval_sts}節で挙げた問題に加えて，Word2Vecを用いた場合は\textit{season}（味付けする）と\textit{pour}（注ぐ）間の意味的関係（Word2Vecにおける単語間類似度は0.07），\textit{draw}と\textit{paint}間の意味的関係（どちらも描くという意味であるが，Word2Vecにおける単語間類似度は0.155）といった，多義語を含む単語間の意味的関係のチェックに失敗し，公理が生成されない傾向が見られた．この結果から，語義曖昧性を考慮して単語間の意味的関係をチェックすることで，公理生成の改善が見込まれることが示唆されたが，これは今後の課題とする．


\subsection{特徴量別の評価}
\label{feature}

\subsubsection{文間類似度学習}
\label{feature_sts}

SICKデータセットにおける，各特徴量単独で文間類似度を学習した場合のモデルの評価結果を表~\ref{isolation_sts}に示す．この表が示すように，述語の一致率のみを特徴量に用いた場合が最も精度が高かった．この結果は，動詞・名詞の一致率と比較して，論理式による意味表現が文の言語的な情報を良質な形式で表現しているという先行研究の知見と合致している．
導出木のマッピングコストのみを使用した場合と受動態の有無のみを使用した場合は，Pearson相関係数がほぼ0の値をとり，ほぼ全ての文ペアで3.5の類似度スコアを予測していた．この結果から，これらの特徴量は単独では予測性能はないと考えられる．しかし，SICKデータセット中の76\%の文ペアに3から5の範囲の正解スコアが付与されているという正解スコアの分布の偏りが原因で，導出木のマッピングコストのみを使用した場合と受動態の有無のみを使用した場合は予測性能がないのにも関わらず，MSEの値は1程度の結果となったと考えられる．

\begin{table}[b]
\setlength{\captionwidth}{205pt}
\begin{minipage}[t]{205pt}
\hangcaption{各特徴量単独で学習した場合の類似度学習の評価結果}
\label{isolation_sts}
\input{02table06.tex}
\end{minipage}
\hfill
\begin{minipage}[t]{205pt}
\caption{類似度学習のアブレーションの評価結果}
\label{ablation_sts}
\input{02table07.tex}
\end{minipage}
\end{table}

全特徴量から各特徴量を取り除いて学習させた場合のモデルの評価結果を表~\ref{ablation_sts}に示す．
各特徴量を単独で取り除いた結果は精度にほとんど変化が見られなかったが，推論由来の特徴量の中では証明の結果を取り除いた場合において，最も性能が低下した．この結果は\ref{strategy}で述べたように，SICKデータセットでは含意関係がyesまたはnoの文例において高い文間類似度が付与されているため，含意関係の証明の結果が文間類似度の予測性能に寄与していると考えられる．また，表層由来の特徴量の中ではベクトル空間モデルを取り除いた場合が最も性能が低下した．この結果は，文間類似度の予測においては表層的な一致率の影響が大きいことを示唆している．

推論を用いた特徴量をまとめて取り除いた場合は，推論以外の特徴量をまとめて取り除いた場合と比較して，大きな性能低下が見られた．このことから，推論を用いた特徴量は推論以外の情報を用いた特徴量よりも精度への影響が大きいことが示唆された．
また，推論由来の特徴量の中でも，論理式由来の特徴量（述語の一致率，型の一致率，否定表現の有無）をまとめて取り除いた場合よりも，推論の過程由来の特徴量（サブゴール，サブゴールの項の関係，ステップ数，推論規則，公理の確信度）をまとめて取り除いた場合の方が性能低下が見られた．この結果は証明の実行過程が文間の関連性を表す特徴として性能に寄与していることを示唆している．

\begin{table}[b]
\setlength{\captionwidth}{205pt}
\begin{minipage}[t]{205pt}
\hangcaption{各特徴量単独で学習した場合の含意関係認識の評価結果}
\label{isolation_rte}
\input{02table08.tex}
\end{minipage}
\hfill
\begin{minipage}[t]{205pt}
\caption{含意関係認識のアブレーションの評価結果}
\label{ablation_rte}
\input{02table09.tex}
\end{minipage}
\end{table}


\subsubsection{含意関係認識}
\label{feature_rte}

SICKデータセットにおける，各特徴量単独で学習した場合の含意関係認識モデルの評価結果を表~\ref{isolation_rte}に示す．含意関係認識においては，証明の結果のみを特徴量に用いた場合が最も精度が高かった．
型の一致率，受動態の有無，品詞タグの一致率，文の長さの一致率，導出木のマッピングコストは再現率が0.1以下と著しく低かった．これらの特徴量はほぼすべての文例でunknownを予測（型の一致率はすべてunknownと予測）し，単独では含意関係の予測性能がないことを示唆している．

全特徴量から各特徴量を取り除いて学習させた場合の含意関係認識モデルの評価結果を表~\ref{ablation_rte}に示す．
含意関係認識においても，各特徴量を単独で取り除いた結果は精度に大きな変動が見られなかったが，
推論由来の特徴量は推論以外の情報を用いた特徴量よりも精度への影響が大きいこと
，推論由来の特徴量の中でも，推論の過程由来の特徴量（サブゴール，サブゴールの項の関係，ステップ数，推論規則，公理の確信度）の方が論理式由来の特徴量（述語の一致率，型の一致率，否定表現の有無）よりも精度への影響が大きいことが示唆された．

また，含意関係認識においては，推論由来の特徴量の中では，証明のステップ数が性能に最も大きく寄与する特徴量であることが示唆された．この結果は，文間類似度の予測では文間の表層的な一致率の影響が大きいのに対して，含意関係の予測では文間の意味的な一致率の影響が大きいという，含意関係認識と文間類似度学習のタスク内容の違いを表していると考えられる．
さらに，公理の確信度の特徴量を取り除いた場合は性能が低下するのに対して，概念間の距離や同義語の一致率の特徴量を取り除いた場合，性能が向上した．公理の確信度と概念間の距離・同義語の一致率の特徴量の導出方法の比較からこの結果を考察すると，概念間の距離と同義語の一致率では2文中の全ての単語間について概念間の距離や同義語集合を計算し，その平均を特徴量としているのに対して，公理の確信度では2文間の意味的関係の判断に必要な単語間に限定して類似度を計算し，その平均を特徴量としている．そのため，公理の確信度は概念間の距離・同義語の一致率よりも効率的な特徴量として，含意関係の予測性能に寄与したと考えられる．


\subsection{正解ラベル別の評価}
\label{label}

\subsubsection{文間類似度学習}

SICKデータセットにおける，正解スコア別の類似度学習の評価結果を表~\ref{score-STS}に示す．この結果から，提案手法は$4\ {\leq}\ x<5$の範囲の類似度スコアが付与されている文ペアにおいて最も精度が高いことが確認された．実際に，$4\ {\leq}\ x<5$の範囲の類似度スコアが付与されている文ペアの8割が含意か矛盾の関係にある文ペアであり，提案手法は特に論理的関係がある文ペアにおいて高精度で類似度を予測することが示唆された．

\begin{table}[b]
\caption{正解スコア別の類似度学習の評価結果 (SICK)}
\label{score-STS}
\input{02table10.tex}
\end{table}


\subsubsection{含意関係認識}

次に，SICKデータセットにおける，正解ラベル別の含意関係認識の評価結果を表~\ref{score-RTE}に示す．なお，ここではyes, no, unknownの3値分類におけるすべてのラベルに関してスコアを算出し，その重み付け平均によって算出した適合率，再現率，F1値を評価指標に用いた．
この結果から，提案手法は特に文間の矛盾関係の判定において高精度を発揮することが確かめられた．SICKデータセットにおいて，矛盾関係にある文ペアの多くは否定表現を含んでいることから，この結果は，提案手法が論理推論を用いて否定表現を含む文の意味を正確に捉えていることを示唆している．

\begin{table}[b]
\caption{各正解ラベルの含意関係認識の評価結果 (SICK)}
\label{score-RTE}
\input{02table11.tex}
\end{table}


\subsection{本研究の手法と深層学習による手法との比較}
\label{deep}

SICKテストデータ4,927件の文例に対して，提案手法の推論由来の特徴量のみを用いて学習したモデルによる予測類似度と，本タスクで最高精度を達成した深層学習のモデル~\cite{MuellerAAAI2016}による予測類似度との比較を行った．その結果，4,927件中2,666件は提案手法の方が正解スコアに近い類似度を予測していた．さらに，この2666件について，特にどのような言語現象を含む文例において推論由来の特徴量が有用であるか，傾向を分析した．テストデータ全体に含まれる否定・量化・等位接続・関係代名詞を含む文例数をそれぞれカウントした結果を表~\ref{phenomena}に示す．

\begin{table}[b]
\caption{言語現象の例}
\label{phenomena}
\input{02table12.tex}
\end{table}

また，これらの文例のうち，提案手法が高精度で予測した文例数とテストデータ中の割合を計算した結果を表~\ref{phenomena_res}に示す．表から，推論由来の特徴量は否定表現や量化表現，等位接続を含む文例において，深層学習のモデルよりも高精度で類似度を予測する傾向が示唆された．

\begin{table}[b]
\caption{言語現象ごとの分析結果}
\label{phenomena_res}
\input{02table13.tex}
\end{table}


\subsection{エラー分析}
\label{error}

最後に，推論由来の特徴量のみで学習したモデルで予測したスコアが正解スコアと1.5以上離れていた文例119件について，エラー分析を行った．SICKデータセットの類似度・含意関係の評価結果のエラー分析の例を表~\ref{tab:examples_neg}に示す．

\begin{table}[b]
\caption{エラー分析}
\label{tab:examples_neg}
\input{02table14.tex}
\end{table}

1264では，各文中の\textit{onstage}と\textit{on a stage}をどちらも副詞として捉えるのが正しい統語解析結果であるが，統語解析のエラーによって\textit{onstage}が\textit{perform}の目的語として捉えられてしまい，統語解析の結果に従って誤った論理式に変換されたため，含意関係を証明できず，予測スコアが正解スコアよりも低くなってしまった例である．このような例では2文間の統語解析の結果の整合性を考慮するなど，統語解析の改善が必要である．
6637では，1文目の\textit{leap over}を1つの動詞のイディオムとして論理式に変換する必要があるが，変換に失敗し，予測スコアが正解スコアよりも低くなってしまった例である．このような例では，イディオムに関する外部知識を参照して論理式に変換するといった改善策が考えられる．
2831は含意関係がある文ペアであるが，\textit{penciling on eyeshadow}と\textit{using an eye pencil on her eyelid}間の公理を生成できなかったため含意関係を証明できず，予測スコアが正解スコアよりも低くなってしまった例である．このような例では，フレーズ間の関係知識を用いて公理を生成する必要がある．
1941は含意関係のない文ペアであるが，公理の過剰生成によって含意関係を証明できてしまい，予測スコアが正解スコアよりも高くなってしまった例である．本研究では公理の確信度に単語間類似度を採用し，確信度が閾値以上である場合のみに公理を採用しているが，このような公理の過剰生成を防ぐためには，文脈に合わせて正しく公理の確信度を算出するよう改善する必要がある．


\section{まとめ}
\label{conclusion}

本研究では，文を高階述語論理式に変換し，文間の含意関係を高階論理の推論によって判定するシステムの実行過程に関する情報から，文間の関連性に寄与する特徴を抽出し，文間の関連性を学習する手法を提案した．文間類似度学習と含意関係認識という2つの自然言語処理タスクに関して複数のデータセットを用いて評価を行った結果，推論の過程を特徴量として組み合わせることによって，いずれのタスクにおいても精度が向上した．また，含意関係認識用データセットの一つであるSICKデータセットの評価では最高精度を達成した．
今後の展望としては，統語解析，意味合成，論理推論のそれぞれのフェーズにおいて改善策を検討していく．統語解析においては，文ペア間で統語解析結果が異なるために証明に失敗した例が数件見られたため，文ペア中に同じ動詞が含まれていれば，各文の動詞に同じ統語範疇を優先して割り当てるといった改善策が挙げられる．意味合成においては，統語解析の結果に加えて外部知識を利用することで，イディオムなどを含む文についても適切な論理式に変換するといった改善策が挙げられる．論理推論においては，フレーズ間の公理の生成方法の検討，公理の確信度の計算方法の改善などが今後の課題として挙げられる．また，本稿では含意関係認識と文間類似度学習のタスクにおいて提案手法の評価を行ったが，今後，質問応答など他の自然言語処理タスクへの適用が期待される．


\acknowledgment

本研究は，JST戦略的創造研究推進事業CREST (JPMJCR1301) およびAIPチャレンジの支援を受けて行われた．
また，本研究の一部は，the 2017 Conference on Empirical Methods in Natural Language Processing (EMNLP2017) で発表したものである (Yanaka, Mineshima, Mart\'{i}nez-G\'{o}mez and Bekki, 2017) ．


\bibliographystyle{jnlpbbl_1.5}
\begin{thebibliography}{}

\bibitem[\protect\BCAY{Abzianidze}{Abzianidze}{2015}]{abzianidze:2015:EMNLP}
Abzianidze, L. \BBOP 2015\BBCP.
\newblock \BBOQ A Tableau Prover for Natural Logic and Language.\BBCQ\
\newblock In {\Bem Proceedings of the 2015 Conference on Empirical Methods in
  Natural Language Processing (EMNLP-2015)}, \mbox{\BPGS\ 2492--2502}.

\bibitem[\protect\BCAY{Abzianidze}{Abzianidze}{2016}]{abzianidze:2016:*SEM}
Abzianidze, L. \BBOP 2016\BBCP.
\newblock \BBOQ Natural Solution to FraCaS Entailment Problems.\BBCQ\
\newblock In {\Bem Proceedings of the 5th Joint Conference on Lexical and
  Computational Semantics}, \mbox{\BPGS\ 64--74}.

\bibitem[\protect\BCAY{Agirre, Cer, Diab, \BBA\ Gonzalez-Agirre}{Agirre
  et~al.}{2012}]{semeval2012}
Agirre, E., Cer, D., Diab, M., \BBA\ Gonzalez-Agirre, A. \BBOP 2012\BBCP.
\newblock \BBOQ SemEval-2012 Task 6: A Pilot on Semantic Textual
  Similarity.\BBCQ\
\newblock In {\Bem Proceedings of the 6th International Workshop on Semantic
  Evaluation (SemEval-2012)}, \mbox{\BPGS\ 385--393}.

\bibitem[\protect\BCAY{B{\"{a}}r, Biemann, Gurevych, \BBA\ Zesch}{B{\"{a}}r
  et~al.}{2012}]{bar:semeval12}
B{\"{a}}r, D., Biemann, C., Gurevych, I., \BBA\ Zesch, T. \BBOP 2012\BBCP.
\newblock \BBOQ UKP: Computing Semantic Textual Similarity by Combining
  Multiple Content Similarity Measures.\BBCQ\
\newblock In {\Bem Proceedings of the 6th International Workshop on Semantic
  Evaluation (SemEval-2012)}, \mbox{\BPGS\ 435--440}.

\bibitem[\protect\BCAY{Bekki \BBA\ Mineshima}{Bekki \BBA\
  Mineshima}{2017}]{BekkiMineshima2016Luo}
Bekki, D.\BBACOMMA\ \BBA\ Mineshima, K. \BBOP 2017\BBCP.
\newblock \BBOQ Context-Passing and Underspecification in Dependent Type
  Semantics.\BBCQ\
\newblock In Chatzikyriakidis, S.\BBACOMMA\ \BBA\ Luo, Z.\BEDS, {\Bem Modern
  Perspectives in Type Theoretical Semantics}, Studies of Linguistics and
  Philosophy, \mbox{\BPGS\ 11--41}. Springer.

\bibitem[\protect\BCAY{Beltagy, Roller, Boleda, Erk, \BBA\ Mooney}{Beltagy
  et~al.}{2014}]{beltagy:semeval14}
Beltagy, I., Roller, S., Boleda, G., Erk, K., \BBA\ Mooney, R. \BBOP 2014\BBCP.
\newblock \BBOQ UTexas: Natural Language Semantics using Distributional
  Semantics and Probabilistic Logic.\BBCQ\
\newblock In {\Bem Proceedings of the 8th International Workshop on Semantic
  Evaluation (SemEval-2014)}, \mbox{\BPGS\ 796--801}.

\bibitem[\protect\BCAY{Bertot \BBA\ Castran}{Bertot \BBA\
  Castran}{2010}]{opac-b1101046}
Bertot, Y.\BBACOMMA\ \BBA\ Castran, P. \BBOP 2010\BBCP.
\newblock {\Bem Interactive Theorem Proving and Program Development: Coq'Art
  The Calculus of Inductive Constructions}.
\newblock Springer, New York, USA.

\bibitem[\protect\BCAY{Bjerva, Bos, van~der Goot, \BBA\ Nissim}{Bjerva
  et~al.}{2014}]{bjerva:semeval14}
Bjerva, J., Bos, J., van~der Goot, R., \BBA\ Nissim, M. \BBOP 2014\BBCP.
\newblock \BBOQ The Meaning Factory: Formal Semantics for Recognizing Textual
  Entailment and Determining Semantic Similarity.\BBCQ\
\newblock In {\Bem Proceedings of the 8th International Workshop on Semantic
  Evaluation (SemEval-2014)}, \mbox{\BPGS\ 642--646}.

\bibitem[\protect\BCAY{Blei, Ng, \BBA\ Jordan}{Blei et~al.}{2003}]{LDA}
Blei, D.~M., Ng, A.~Y., \BBA\ Jordan, M.~I. \BBOP 2003\BBCP.
\newblock \BBOQ Latent Dirichlet Allocation.\BBCQ\
\newblock {\Bem Journal of Machine Learning}, {\Bbf 3}, \mbox{\BPGS\
  993--1022}.

\bibitem[\protect\BCAY{Champollion}{Champollion}{2015}]{champ2015}
Champollion, L. \BBOP 2015\BBCP.
\newblock \BBOQ The Interaction of Compositional Semantics and Event
  Semantics.\BBCQ\
\newblock {\Bem Linguistics and Philosophy}, {\Bbf 38}  (1), \mbox{\BPGS\
  31--66}.

\bibitem[\protect\BCAY{Clark, Coecke, \BBA\ Sadrzadeh}{Clark
  et~al.}{2011}]{ClarkCoeckeSadrzadeh2011}
Clark, S., Coecke, B., \BBA\ Sadrzadeh, M. \BBOP 2011\BBCP.
\newblock \BBOQ Mathematical Foundations for a Compositional Distributed Model
  of Meaning.\BBCQ\
\newblock {\Bem Linguistic Analysis}, {\Bbf 36}  (1-4), \mbox{\BPGS\ 345--384}.

\bibitem[\protect\BCAY{Clark \BBA\ Curran}{Clark \BBA\
  Curran}{2007}]{clark2007wide}
Clark, S.\BBACOMMA\ \BBA\ Curran, J.~R. \BBOP 2007\BBCP.
\newblock \BBOQ Wide-coverage Efficient Statistical Parsing with CCG and
  Log-linear Models.\BBCQ\
\newblock {\Bem Computational Linguistics}, {\Bbf 33}  (4), \mbox{\BPGS\
  493--552}.

\bibitem[\protect\BCAY{Curran \BBA\ Clark}{Curran \BBA\
  Clark}{2003}]{curran2003investigating}
Curran, J.~R.\BBACOMMA\ \BBA\ Clark, S. \BBOP 2003\BBCP.
\newblock \BBOQ Investigating GIS and Smoothing for Maximum Entropy
  Taggers.\BBCQ\
\newblock In {\Bem Proceedings of the 10th Conference on European Chapter of
  the Association for Computational Linguistics (EACL-2003)}, \mbox{\BPGS\
  91--98}.

\bibitem[\protect\BCAY{Davidson}{Davidson}{1967}]{Davidson67}
Davidson, D. \BBOP 1967\BBCP.
\newblock \BBOQ The Logical Form of Action Sentences.\BBCQ\
\newblock In Rescher, N.\BED, {\Bem The Logic of Decision and Action},
  \mbox{\BPGS\ 81--95}. University of Pittsburgh Press, Pittsburgh, PA.
\newblock Reprinted in \cite{Davidson80}, pp.~105--148.

\bibitem[\protect\BCAY{Davidson}{Davidson}{1980}]{Davidson80}
Davidson, D. \BBOP 1980\BBCP.
\newblock {\Bem Essays on Actions and Events}.
\newblock Clarendon Press, Oxford.

\bibitem[\protect\BCAY{Deerwester, Dumais, Landauer, \BBA\ Harshman}{Deerwester
  et~al.}{1990}]{LSA}
Deerwester, S., Dumais, S.~T., Landauer, T.~K., \BBA\ Harshman, R. \BBOP
  1990\BBCP.
\newblock \BBOQ Indexing by Latent Semantic Analysis.\BBCQ\
\newblock {\Bem Journal of the American Society for Information Science}, {\Bbf
  41}  (6), \mbox{\BPGS\ 391--407}.

\bibitem[\protect\BCAY{Grefenstette \BBA\ Sadrzadeh}{Grefenstette \BBA\
  Sadrzadeh}{2011}]{grefenstette-sadrzadeh:2011:EMNLP}
Grefenstette, E.\BBACOMMA\ \BBA\ Sadrzadeh, M. \BBOP 2011\BBCP.
\newblock \BBOQ Experimental Support for a Categorical Compositional
  Distributional Model of Meaning.\BBCQ\
\newblock In {\Bem Proceedings of the 2011 Conference on Empirical Methods in
  Natural Language Processing (EMNLP-2011)}, \mbox{\BPGS\ 1394--1404}.

\bibitem[\protect\BCAY{He \BBA\ Lin}{He \BBA\ Lin}{2016}]{He2016PairwiseWI}
He, H.\BBACOMMA\ \BBA\ Lin, J. \BBOP 2016\BBCP.
\newblock \BBOQ Pairwise Word Interaction Modeling with Deep Neural Networks
  for Semantic Similarity Measurement.\BBCQ\
\newblock In {\Bem Proceedings of the 2016 Conference of the North American
  Chapter of the Association for Computational Linguistics: Human Language
  Technologies (NAACL/HLT-2016)}, \mbox{\BPGS\ 937--948}.

\bibitem[\protect\BCAY{Hill, Cho, \BBA\ Korhonen}{Hill
  et~al.}{2016}]{hill-cho-korhonen:2016:N16-1}
Hill, F., Cho, K., \BBA\ Korhonen, A. \BBOP 2016\BBCP.
\newblock \BBOQ Learning Distributed Representations of Sentences from
  Unlabelled Data.\BBCQ\
\newblock In {\Bem Proceedings of the 2016 Conference of the North American
  Chapter of the Association for Computational Linguistics: Human Language
  Technologies (NAACL/HLT-2016)}, \mbox{\BPGS\ 1367--1377}.

\bibitem[\protect\BCAY{Hockenmaier \BBA\ Steedman}{Hockenmaier \BBA\
  Steedman}{2007}]{ac4bfc92bbc447d9b2382f4513b2520d}
Hockenmaier, J.\BBACOMMA\ \BBA\ Steedman, M. \BBOP 2007\BBCP.
\newblock \BBOQ CCGbank: A Corpus of CCG Derivations and Dependency Structures
  Extracted from the Penn Treebank.\BBCQ\
\newblock {\Bem Computational Linguistics}, {\Bbf 33}  (3), \mbox{\BPGS\
  355--396}.

\bibitem[\protect\BCAY{Kartsaklis, Kalchbrenner, \BBA\ Sadrzadeh}{Kartsaklis
  et~al.}{2014}]{kartsaklis-kalchbrenner-sadrzadeh:2014:P14-2}
Kartsaklis, D., Kalchbrenner, N., \BBA\ Sadrzadeh, M. \BBOP 2014\BBCP.
\newblock \BBOQ Resolving Lexical Ambiguity in Tensor Regression Models of
  Meaning.\BBCQ\
\newblock In {\Bem Proceedings of the 52nd Annual Meeting of the Association
  for Computational Linguistics (ACL-2014)}, \mbox{\BPGS\ 212--217}.

\bibitem[\protect\BCAY{Kartsaklis \BBA\ Sadrzadeh}{Kartsaklis \BBA\
  Sadrzadeh}{2016}]{kartsaklis-sadrzadeh:2016:COLING}
Kartsaklis, D.\BBACOMMA\ \BBA\ Sadrzadeh, M. \BBOP 2016\BBCP.
\newblock \BBOQ Distributional Inclusion Hypothesis for Tensor-based
  Composition.\BBCQ\
\newblock In {\Bem Proceedings of the 26th International Conference on
  Computational Linguistics: Technical Papers (COLING-2016)}, \mbox{\BPGS\
  2849--2860}.

\bibitem[\protect\BCAY{Le \BBA\ Mikolov}{Le \BBA\
  Mikolov}{2014}]{DBLP:conf/icml/LeM14}
Le, Q.~V.\BBACOMMA\ \BBA\ Mikolov, T. \BBOP 2014\BBCP.
\newblock \BBOQ Distributed Representations of Sentences and Documents.\BBCQ\
\newblock In {\Bem Proceedings of the 31th International Conference on Machine
  Learning, (ICML-2014)}, \mbox{\BPGS\ 1188--1196}.

\bibitem[\protect\BCAY{Lewis \BBA\ Steedman}{Lewis \BBA\
  Steedman}{2014}]{Lewis14a*ccg}
Lewis, M.\BBACOMMA\ \BBA\ Steedman, M. \BBOP 2014\BBCP.
\newblock \BBOQ A* CCG Parsing with a Supertag-factored Model.\BBCQ\
\newblock In {\Bem Proceedings of the 2014 Conference on Empirical Methods in
  Natural Language Processing (EMNLP-2014)}, \mbox{\BPGS\ 990--1000}.

\bibitem[\protect\BCAY{Marelli, Menini, Baroni, Bentivogli, Bernardi, \BBA\
  Zamparelli}{Marelli et~al.}{2014}]{MARELLI14.363}
Marelli, M., Menini, S., Baroni, M., Bentivogli, L., Bernardi, R., \BBA\
  Zamparelli, R. \BBOP 2014\BBCP.
\newblock \BBOQ A SICK Cure for The Evaluation of Compositional Distributional
  Semantic Models.\BBCQ\
\newblock In {\Bem Proceedings of the 9th International Conference on Language
  Resources and Evaluation (LREC-2014)}, \mbox{\BPGS\ 216--223}.

\bibitem[\protect\BCAY{Mart{\'{i}}nez-G{\'{o}}mez, Mineshima, Miyao, \BBA\
  Bekki}{Mart{\'{i}}nez-G{\'{o}}mez
  et~al.}{2016}]{martinezgomez-EtAl:2016:P16-4}
Mart{\'{i}}nez-G{\'{o}}mez, P., Mineshima, K., Miyao, Y., \BBA\ Bekki, D. \BBOP
  2016\BBCP.
\newblock \BBOQ ccg2lambda: A Compositional Semantics System.\BBCQ\
\newblock In {\Bem Proceedings of ACL-2016 System Demonstrations}, \mbox{\BPGS\
  85--90}.

\bibitem[\protect\BCAY{Mart{\'{i}}nez-G{\'{o}}mez, Mineshima, Miyao, \BBA\
  Bekki}{Mart{\'{i}}nez-G{\'{o}}mez et~al.}{2017}]{EACL2017}
Mart{\'{i}}nez-G{\'{o}}mez, P., Mineshima, K., Miyao, Y., \BBA\ Bekki, D. \BBOP
  2017\BBCP.
\newblock \BBOQ On-demand Injection of Lexical Knowledge for Recognising
  Textual Entailment.\BBCQ\
\newblock In {\Bem Proceedings of the 15th Conference of the European Chapter
  of the Association for Computational Linguistics (EACL-2017)}, \mbox{\BPGS\
  710--720}.

\bibitem[\protect\BCAY{Mart{\'{i}}nez-G{\'{o}}mez \BBA\
  Miyao}{Mart{\'{i}}nez-G{\'{o}}mez \BBA\
  Miyao}{2016}]{martinezgomez-miyao:2016:EMNLP2016}
Mart{\'{i}}nez-G{\'{o}}mez, P.\BBACOMMA\ \BBA\ Miyao, Y. \BBOP 2016\BBCP.
\newblock \BBOQ Rule Extraction for Tree-to-Tree Transducers by Cost
  Minimization.\BBCQ\
\newblock In {\Bem Proceedings of the 2016 Conference on Empirical Methods in
  Natural Language Processing (EMNLP-2016)}, \mbox{\BPGS\ 12--22}.

\bibitem[\protect\BCAY{Mikolov, Sutskever, Chen, Corrado, \BBA\ Dean}{Mikolov
  et~al.}{2013}]{NIPS2013_5021}
Mikolov, T., Sutskever, I., Chen, K., Corrado, G.~S., \BBA\ Dean, J. \BBOP
  2013\BBCP.
\newblock \BBOQ Distributed Representations of Words and Phrases and their
  Compositionality.\BBCQ\
\newblock In Burges, C. J.~C., Bottou, L., Welling, M., Ghahramani, Z., \BBA\
  Weinberger, K.~Q.\BEDS, {\Bem Advances in Neural Information Processing
  Systems 26}, \mbox{\BPGS\ 3111--3119}. Curran Associates, Inc.

\bibitem[\protect\BCAY{Miller}{Miller}{1995}]{Miller:1995:WLD:219717.219748}
Miller, G.~A. \BBOP 1995\BBCP.
\newblock \BBOQ WordNet: A Lexical Database for English.\BBCQ\
\newblock {\Bem Communications of the ACM}, {\Bbf 38}  (11), \mbox{\BPGS\
  39--41}.

\bibitem[\protect\BCAY{Mineshima, Mart{\'{i}}nez-G{\'{o}}mez, Miyao, \BBA\
  Bekki}{Mineshima et~al.}{2015}]{D16-1242}
Mineshima, K., Mart{\'{i}}nez-G{\'{o}}mez, P., Miyao, Y., \BBA\ Bekki, D. \BBOP
  2015\BBCP.
\newblock \BBOQ Higher-order Logical Inference with Compositional
  Semantics.\BBCQ\
\newblock In {\Bem Proceedings of the 2015 Conference on Empirical Methods in
  Natural Language Processing (EMNLP-2015)}, \mbox{\BPGS\ 2055--2061}.

\bibitem[\protect\BCAY{Mineshima, Tanaka, Mart{\'{\i}}nez-G{\'{o}}mez, Miyao,
  \BBA\ Bekki}{Mineshima et~al.}{2016}]{mineshima2016building}
Mineshima, K., Tanaka, R., Mart{\'{\i}}nez-G{\'{o}}mez, P., Miyao, Y., \BBA\
  Bekki, D. \BBOP 2016\BBCP.
\newblock \BBOQ Building Compositional Semantics and Higher-order Inference
  System for a Wide-coverage Japanese CCG parser.\BBCQ\
\newblock In {\Bem Proceedings of the 2016 Conference on Empirical Methods in
  Natural Language Processing (EMNLP-2016)}, \mbox{\BPGS\ 2236--2242}.

\bibitem[\protect\BCAY{Mitchell \BBA\ Lapata}{Mitchell \BBA\
  Lapata}{2008}]{mitchell-lapata:2008:ACLMain}
Mitchell, J.\BBACOMMA\ \BBA\ Lapata, M. \BBOP 2008\BBCP.
\newblock \BBOQ Vector-based Models of Semantic Composition.\BBCQ\
\newblock In {\Bem Proceedings of the 46th Annual Meeting of the Association
  for Computational Linguistics (ACL-2008)}, \mbox{\BPGS\ 236--244}.

\bibitem[\protect\BCAY{Mitchell \BBA\ Lapata}{Mitchell \BBA\
  Lapata}{2010}]{mitchell2010composition}
Mitchell, J.\BBACOMMA\ \BBA\ Lapata, M. \BBOP 2010\BBCP.
\newblock \BBOQ Composition in Distributional Models of Semantics.\BBCQ\
\newblock {\Bem Cognitive Science}, {\Bbf 34}  (8), \mbox{\BPGS\ 1388--1429}.

\bibitem[\protect\BCAY{Mueller \BBA\ Thyagarajan}{Mueller \BBA\
  Thyagarajan}{2016}]{MuellerAAAI2016}
Mueller, J.\BBACOMMA\ \BBA\ Thyagarajan, A. \BBOP 2016\BBCP.
\newblock \BBOQ Siamese Recurrent Architectures for Learning Sentence
  Similarity.\BBCQ\
\newblock In {\Bem Proceedings of the 30th AAAI Conference on Artificial
  Intelligence (AAAI-2016)}, \mbox{\BPGS\ 2786--2792}.

\bibitem[\protect\BCAY{Parsons}{Parsons}{1990}]{Parsons90}
Parsons, T. \BBOP 1990\BBCP.
\newblock {\Bem Events in the Semantics of English: A Study in Subatomic
  Semantics}.
\newblock MIT Press, Cambridge, USA.

\bibitem[\protect\BCAY{Peter \BBA\ Wilkins}{Peter \BBA\
  Wilkins}{1984}]{culicover1984}
Peter, W.~C.\BBACOMMA\ \BBA\ Wilkins, W.~K. \BBOP 1984\BBCP.
\newblock {\Bem Locality in Linguistic Theory}.
\newblock Academic Press, Florida, USA.

\bibitem[\protect\BCAY{Prawitz}{Prawitz}{1965}]{prawitz1965natural}
Prawitz, D. \BBOP 1965\BBCP.
\newblock {\Bem Natural Deduction---A Proof-Theoretical Study}.
\newblock Almqvist \& Wiksell, Stockholm, Sweden.

\bibitem[\protect\BCAY{Ray}{Ray}{1990}]{Jackendo1990}
Ray, J. \BBOP 1990\BBCP.
\newblock {\Bem Semantic Structures}.
\newblock MIT Press, Cambridge, USA.

\bibitem[\protect\BCAY{Steedman}{Steedman}{2000}]{Steedman00}
Steedman, M. \BBOP 2000\BBCP.
\newblock {\Bem The Syntactic Process}.
\newblock MIT Press, Cambridge, USA.

\bibitem[\protect\BCAY{Tai, Socher, \BBA\ Manning}{Tai
  et~al.}{2015}]{tai-socher-manning:2015:ACL-IJCNLP}
Tai, K.~S., Socher, R., \BBA\ Manning, C.~D. \BBOP 2015\BBCP.
\newblock \BBOQ Improved Semantic Representations From Tree-Structured Long
  Short-Term Memory Networks.\BBCQ\
\newblock In {\Bem Proceedings of the 53rd Annual Meeting of the Association
  for Computational Linguistics and the 7th International Joint Conference on
  Natural Language Processing (ACL/IJCNLP-2015)}, \mbox{\BPGS\ 1556--1566}.

\bibitem[\protect\BCAY{Wong \BBA\ Raghavan}{Wong \BBA\
  Raghavan}{1984}]{Find-similar}
Wong, S. K.~M.\BBACOMMA\ \BBA\ Raghavan, V.~V. \BBOP 1984\BBCP.
\newblock \BBOQ Vector Space Model of Information Retrieval: A
  Reevaluation.\BBCQ\
\newblock In {\Bem Proceedings of the 7th Annual International ACM SIGIR
  Conference on Research and Development in Information Retrieval},
  \mbox{\BPGS\ 167--185}.

\bibitem[\protect\BCAY{Yin \BBA\ Sch{\"{u}}tze}{Yin \BBA\
  Sch{\"{u}}tze}{2017}]{yin-schutze:2017:EACLlong}
Yin, W.\BBACOMMA\ \BBA\ Sch{\"{u}}tze, H. \BBOP 2017\BBCP.
\newblock \BBOQ Task-Specific Attentive Pooling of Phrase Alignments
  Contributes to Sentence Matching.\BBCQ\
\newblock In {\Bem Proceedings of the 15th Conference of the European Chapter
  of the Association for Computational Linguistics (EACL-2017)}, \mbox{\BPGS\
  699--709}.

\bibitem[\protect\BCAY{Yoshikawa, Noji, \BBA\ Matsumoto}{Yoshikawa
  et~al.}{2017}]{yoshikawa-noji-matsumoto:2017:Long}
Yoshikawa, M., Noji, H., \BBA\ Matsumoto, Y. \BBOP 2017\BBCP.
\newblock \BBOQ A* CCG Parsing with a Supertag and Dependency Factored
  Model.\BBCQ\
\newblock In {\Bem Proceedings of the 55nd Annual Meeting of the Association
  for Computational Linguistics (ACL-2017)}, \mbox{\BPGS\ 277--287}.

\bibitem[\protect\BCAY{Zhou, Liu, \BBA\ Pan}{Zhou
  et~al.}{2016}]{zhou2016sentpair}
Zhou, Y., Liu, C., \BBA\ Pan, Y. \BBOP 2016\BBCP.
\newblock \BBOQ Modelling Sentence Pairs with Tree-structured Attentive
  Encoder.\BBCQ\
\newblock In {\Bem Proceedings of the 26th International Conference on
  Computational Linguistics (COLING-2016)}, \mbox{\BPGS\ 2912--2922}.

\end{thebibliography}


\begin{biography}
\bioauthor{谷中　　瞳}{
1989年生．2011年早稲田大学先進理工学部応用化学科卒業．2013年東京大学大学院工学系研究科科学システム工学専攻修士課程修了．同年，株式会社野村総合研究所入社後，2015年東京大学大学院工学系研究科システム創成学専攻博士課程進学．
}
\bioauthor{峯島　宏次}{
2013年慶應義塾大学文学研究科博士課程修了．博士（哲学）．
現在，お茶の水女子大学シミュレーション科学・生命情報学教育研究センター特任准教授．
}
\bioauthor[:]{Pascual Mart\'{i}nez-G\'{o}mez}{
received his Ph.D. degree in Computer Science at the University of Tokyo in 2014 for his research on eye-tracking and readability diagnosis. He is a research scientist at the Artificial Intelligence Research Center in the National Institute of Advanced Industrial Science and Technology (AIST), Japan. 
}
\bioauthor{戸次　大介}{
2000年東京大学大学院理学系研究科情報科学専攻博士課程修了．博士（理学）．現在，お茶の水女子大学基幹研究院自然科学系准教授．
}

\end{biography}


\biodate





\end{document}
