言語処理学会 第24回年次大会 発表論文集 (2018年3月)

知識ベース補完を用いた高階論理推論のための自動公理生成
吉川 将司 1

峯島 宏次 2

能地 宏 1奈良先端科学技術大学院大学 1

戸次 大介 2

お茶の水女子大学 2yoshikawa.masashi.yh8@is.naist.jp, mineshima.koji@ocha.ac.jp,
noji@is.naist.jp, bekki@is.ocha.ac.jp

1

はじめに構築する．本研究ではまた，そうして構築したデータに VerbOcean からの知識を加えることで，メモリ量，含意関係認識 (Recognizing Textual Entailment; 以

計算時間における効率を損なわずに RTE における性下 RTE) などの深い意味処理を扱うタスクでは，大能向上を導くデータ拡張が可能であることを示す．

量の知識データが必要である．高階論理による RTE加えて，論理推論をさらに効率的に行うための改良システムである ccg2lambda[6] は，WordNet[2] やを行う．既存研究 [8] では，新たな公理を追加するた

VerbOcean[1] などの知識ベースから証明に必要な知識を検索し，論理式の形で公理として利用することで大きな性能改善を示した [8](§2.1 参照)．しかし，これらのような大規模な知識ベースを離散的なデータ構造として保持しておくことは，使用するメモリ量や計算効率の面からは問題であり，性能の改善のために知識データを拡充しようとすると，問題を処理する効率性を失ってしまうというジレンマがある．
一方で，近年機械学習を用いた知識ベース補完(Knowledge Base Completion) の技術の発展が目覚ましい [11, 10]．これらの研究の多くでは，計算効率の良さが重視されており，知識ベースの entity s, o とrelation r はパラメータ n の次元のベクトルとして表現され，三つ組 (s, r, o) が事実として真であるか偽であるかの判定は O(n) のスコア計算で行われる．これ
らの手法は，WordNet を基に作られたベンチマークにおいてすでに高い精度を示しており，上述の公理生成における離散的な知識ベースの検索を置き換えることが期待できる．さらに，これらの研究は，既存の知識ベースに欠けた事実（三つ組）をスコア関数で補完することに動機づけられているが，このような潜在的な知識は当然 RTE においても有用である．
そこで本研究では，ccg2lambda を知識ベース補完による自動公理生成で拡張する．具体的には，これまでの WordNet を検索することで行っていた公理生成を，上述のスコア関数で置き換えることにより，RTE の問題をより高精度かつ高速に処理可能にすることを目指す．そのため，論理推論に有用なスコア関数を学習するために適した新たなデータセットを WordNet からめに定理証明器 (Coq[5]) を一度終了し，公理を追加した後に定理証明を再実行する必要があった．本研究では Coq を実行しながら同時に WordNet の検索や知識ベース補完モデルによる評価を実行できる Coq のabduction tactic を開発する．
SICK[7] データセットで実験を行い，ベースラインに対して精度においては僅かに下回る結果となったが，処理速度において大きな改善を示した．

2

既存研究

2.1

ccg2lambda

ccg2lambda[6] は，RTE の前提文 (P ) と帰結文 (H)を，統語構造と意味表示が透明な関係を持つ組み合
わせ範疇文法 (Combinatory Categorial Grammar;CCG)[3, 13] の構文解析器によって解析した後，λ 計
算による意味合成によって高階述語論理式に変換する(図 1a, b)．それらの論理式に対し，含意（もしくは矛盾）が成り立つかを調べるため，含意の論理演算子で結合し (P → H ，P → ¬H)，証明支援システムである Coq[5] で自動推論を行う (図 1c)．
Coq は tactic と呼ばれる命令を組み合わせることで人による定理証明を支援するシステムであるが，firstorder tactic では一階述語論理の論理式に対する自動の定理証明を行うことができる．またその際に高階の自然言語の論理表現についてはその推論規則を公理として登録しておくことで高階の推論にも対応できる．

― 113 ―

Copyright(C) 2018 The Association for Natural Language Processing.
All Rights Reserved.

(a)CCG
構文解析

前提&帰結

(b)論理式に変換(c)定理証明(Coq)

述語のリスト

帰結前提
Aman

NP /NN

NP>

hikes

A

manwalks

S \NP

NP /N

N

S \NPNP<>

再挑戦
Wordnet

公理の追加を検索<S:∃x.(man(x) ∧ ∃e.walk(e, x))S :∃x.(man(x) ∧ ∃e.hike(e, x))Yes, No,
Unknown

8x.(hike(x) ! walk(x))(hike, hypernyms, walk)(d) 自動公理生成

図 1: ccg2lambda の処理過程．前提 (P ) と帰結 (H) を CCG パーザで解析し (a)，論理式へ変換する (b)．それらを含意演算子で結合し (P → H,P → ¬H)，Coq で推論を行う (c)．証明に失敗した場合，公理生成を試みる (d)．
既存研究 [8] による拡張では，まず Coq で RTE の問関係 r

生成する公理題の証明を行い，失敗した場合に証明を完了するため

synonym, hypernym∀⃗x.(s(⃗x) → o(⃗x))に有用な公理の探索を行う (abduction)．WordNet[2]例．(make, r, build) ; ∀⃗x.(make(⃗x) → build(⃗x))と動詞間の関係を記述した VerbOcean[1] から語彙間

antonym∀⃗x.(s(⃗x) → ¬o(⃗x))

例．(parent, r, child) ; ∀⃗x.(parent(⃗x) → ¬child(⃗x))

知識を検索し，論理式に変換してから公理として宣言hyponymを行い，再度証明を試みる (図 1d)．ここでの問題点と∀⃗x.(o(⃗x) → s(⃗x))

例．(talk, r, advise) ; ∀⃗x.(advise(⃗x) → talk(⃗x))

して，WordNet 等を検索するために Coq プログラムを一度終了する必要があり，全体の処理速度が下がっ

表 1: 三つ組 (s, r, o) と r に関して生成される公理．述てしまうことが挙げられる．本研究では Coq を実行

語の引数の数・型は ccg2lambda の意味解析時に決定しながら同時に WordNet の検索や知識ベース補完をし，公理生成時はそれを用いる．

実行できる abduction tactic の開発を行う (§3.2)．
価し，スコアが閾値 θ 以上のものを表 1 に従い論理式2.2に変換し，公理として宣言する．

知識ベース補完以下，§3.1 で公理生成を主眼においたデータセット

本研究では知識ベース補完のモデルとして

ComplEx[10] を 使 用 す る ．ComplEx で は 三 つ 組構築手順を，§3.2 で Coq 実行時に動的に公理生成を行う abduction tactic について述べる．

1(s, r, o) に対して，複素数 を用いてその関係をモデル化する:

3.1
f (s, r, o) = σ(Re(⟨es , er , eo ⟩)).

ここで，es , er , eo ∈ Cn ，⟨x, y, z⟩ =(1)∑i xi yi zi であり，n は埋め込みベクトルの次元数である．

データセットの作成

自動公理生成のためのデータセットを WordNet から構築する上での問題点として，WordNet では (hyper-nym，hyponym など) 多くの関係が見出し語 (lemma)の集合である同義語集合 (synset)2 の間で定義されていることがある．ccg2lambda では文から論理式に変3提案法換する際に表層形から見出し語に正規化しているため，
3見出し語間の知識データが必要である．
以下，この隔提案法では，ccg2lambda による論理推論において前提と帰結の間に語彙的な隔たりが存在する場合に，たりを考慮しながら各 r ∈ R について WordNet を走査して三つ組を収集し，データセットを構築する．

知識ベース補完のスコア関数を用いて新たな公理を追加する．具体的に，ComplEx モデル (式 1) で前提と帰結に存在する論理述語のペアをすべての関係 r ∈ R ={synonym, hypernym, antonym, hyponym} について評1 ここで複素数の集合を C で示し，x ∈ C について，その実部を Re(x)，複素共役を x と表す．

ま ず synonym に つ い て ，同 義 語 集 合 s1 に 対
し て WordNet 上 で also sees，verb groups，similar tos の関係にある同義語集合 s2 を s1 と同2 以下，簡略のため同義語集合 s に見出し語 l が含まれることを集合論の記法を用い l ∈ s と示す．
3 このことは，後に見出し語間で関係を定義している VerbOcean
や，生テキストなど他のデータを利用した拡張を行う上でも重要である．

― 114 ―

Copyright(C) 2018 The Association for Natural Language Processing.
All Rights Reserved.

義語 (synonym) の関係にあるとみなし，すべての

1 subgoall1 ∈ s1 , l2 ∈ s2 の組みについて (l1 , synonym, l2 ) としてデータセットに含める．また，ある l ∈ s1 について，l ∈ s2 であるような任意の s2 も同義語とみなの見出し語の組を hypernym としてデータに含めた．

hypernym は，推移律が成り立つと考え4 ，その推移閉包から得られる関係についてもデータセットに含述語のペアリストを構築

t < intro.
1 subgoal

し同様の処理を行う．上位語 (hypernym) の関係にある s1 と s2 についても，synonym と同様にすべてコンテキストとゴールから============================(exists x : Entity, man x /\ hike x) ->exists x : Entity, man x /\walk x

Pythonサーバに送信

H : exists x : Entity, man x /\ hike x============================
exists x : Entity, man x /\ walk x(man, walk)ComplExモデルで述語の関係を評価(man, hike)t < abduction.
(hike, walk)
1 subgoal
スコアでフィルタ
H : exists x : Entity, man x /\ hike x
NLax1 : forall x : Entity, hike x -> walk x============================
公理として追加
exists x : Entity, man x /\ walk x(hike, hyper, walk)

める．hyponym についても hypernym と同様の処理を行う．反意語 (antonym) については WordNet におい

図 2: abduction tactic の実行例．て見出し語間で定義されているため，それらをデータセットに含めた．
このようにして取り出した三つ組の量は多く，また

手法

正答率

適合率

再現率

ベースライン (WN)

83.55

97.20

63.63

10.92+ VO

83.84

96.70

64.66

11.06

abduction tactic

83.60

97.15

63.91

7.41+ WN

82.82
82.95

97.07
96.87

62.13
62.55

4.63
4.63

現在の RTE タスクを解く上で有用ではない見出し語5も多く含まれるため，見出し語リスト を用いて，三+ VOつ組 (l1 , r, l2 ) について l1 , l2 の両方がリストに含まれ処理速度るもの以外は取り除いた．結果として構築されたデー

表 2: SICK データセットにおける実験結果． WN

タセットは 2, 588, 186 の三つ組からなり，entity の総は WordNet，VO は VerbOcean を表す．処理速度は数は 40, 488 となった．開発用に 5, 000 組を取り，そRTE 問題 1 題あたりに要した時間（秒）のマクロ平均．

れ以外すべて学習に用いる．

VerbOcean は，見出し語の間に関係を定義しているに従い論理式に変換し，公理として宣言する．

ため，先述の見出し語リストによるフィルタを行った

Coq では tactic をつなげて新たな tactic を作るこ

後，VerbOcean 上で定義された関係から R へのマッとが可能であるから，先述の firstorder 等とあわせて6ピングを行った．
VerbOcean からは 24,953 組の三つ

abduction も含めて自然言語の高階推論を自動で行う組を抽出した．

tactic を構成可能である．
スコア関数の評価を Python サーバの別プロセスに3.2することで，既存の機械学習ライブラリを利用でき，abduction tactic による公理生成

機械学習を用いた前提選択 [4] など，より高度な計算

既存研究 [8] では，公理生成を行うために Coq のプログラムを一度終了する必要があった．本研究では，を要する定理証明上の問題にも利用可能である．§4 でabduction tactic の有効性を示す．

より効率よく論理推論を行うために，Coq を実行しながら同時に WordNet の検索や知識ベース補完のモデルを実行できる abduction tactic を開発した．tacticの具体的な動作を図 2 に示す．abduction が実行されたとき，動作途中のコンテキスト（仮定の集合）とゴー

4実験

4.1

実験設定

ル（証明が必要な命題）の間のすべての論理述語の組

RTE の実験データセットである SICK[7] で提案みを取り出し，別プロセスで動作する Python サーバ法の評価を行う．SICK は前提と帰結それぞれ 1 文に送信する．Python サーバはそれぞれの組について，

か ら な り，そ の よ う な ペ ア が 学 習/開 発/評 価 用 に

すべての r ∈ R に対し ComplEx (式 1) で評価し，閾4,500/500/4,927 文用意されている．本研究では学習値 θ 以上の三つ組を Coq に送り返す．Coq 側で表 1

データについては使用せず，開発データを処理速度の評価に用いる．

ComplEx のについて，埋め込みベクトルの大きさ

4 (puppy,hypernym, dog),(dog, hypernym, animal) ならば(puppy, hypernym, animal) など．
5 SICK[7] と SNLI[9] の学習データ，GloVe (https://nlp.
stanford.edu/projects/glove/) に含まれる見出し語．
6具 体 的 に
similar, stronger-than→synonym，opposite-of → antonym. それら以外の関係については取り除いた．

n = 200 とし，学習は以下のロジスティック損失を― 115 ―

Copyright(C) 2018 The Association for Natural Language Processing.
All Rights Reserved.

Adam で最小化することで行った．
∑L=t log f (s, r, o)+(1−t) log(1−f (s, r, o)),((s,r,o),t)∈D

おわりに

5

本研究では知識ベース補完による高階論理推論のための自動公理生成の手法を提案した．SICK データセッ

ここで，D は学習データであり，§3.1 で作成されたトで実験を行い，処理速度における大きな向上を示した

データの要素なら t = 1，それ以外なら t = 0 であが，精度においては課題が残った．精度面の課題についる．学習を高速化するため，negative sampling の代ては，上述の単語埋め込みベクトルとの同時学習によるわりに，一対多のスコア計算 [11] を行う（詳細は論文対処を検討する．今後の課題として，複数の述語からな参照）．

る公理の生成 (e.g. ∀x.have(x) ∧ fun(x) → enjoy(x))

ccg2lambda については公理生成を除いて標準の設が挙げられる．ccg2lambda の性能の大きな向上には定を用いる．公理生成の閾値 θ = 0.4 とする．ベース

この種の公理を正確に生成できることが鍵となっていラインとして研究 [8] のものを再現し，評価データにる．そのためには，have と fun の埋め込みベクトルかおける正答率/適合度/再現率，開発データにおける処ら構成的な演算で得られたベクトルと enjoy のベクト7
理速度（5 回実行したマクロ平均）を報告する．

ルについて synonym 等の関係を学習できるような枠組みを構築する必要がある．

4.2

実験結果と考察謝辞

この研究は，JST CREST「ビッグデータ統合表 2 に実験結果を示す．表において，abduction tac-利活用のための次世代基盤技術の創出・体系化」領域

tic は §3.2 で開発した tactic を用いるが，知識ベース「知識に基づく構造的言語処理の確立と知識インフラ補完モデルではなく WordNet を検索して公理生成をの構築」プロジェクトの支援を受けたものである．

行った場合である．+WN で WordNet から作成したデータセットで学習した ComplEx モデルに置き換えたもの，+VO でさらに VerbOcean の三組を学習デー
タに追加した場合を示す．ベースラインと比較して，証明に要する時間は大きく短縮することができたが，RTE の性能については下がってしまう結果になった．
注目すべき点として+WN と+VO の比較で，処理速度の変化はない一方で RTE の性能は改善している．

VerbOcean によるデータ拡張を行ったが，パラメータ数の増加はしておらず，計算効率の面では変わらない．

RTE の性能低下に関して，今回学習したモデルの弱点は単語間の派生関係を捉えにくいことである．例
えば WordNet 上では sandy と sand は，派生的な関係にある (derivationally-related) として情報が付与されているが，今回の学習データにそのような関係は含めなかった．ある語についての形態的な派生をすべて三つ組として表現し，知識ベース補完の枠組みで扱うことは学習データの爆発的増加につながり困難であると考えられる．既存研究 [12] では，知識ベース補完とword2vec 等の単語ベクトルを同時に学習することでより強力なスコア関数の学習が可能なことが示されている．単語ベクトルの学習は，同義語や派生的な関係にある語の類似度の学習に強力であるから，この問題を解決するために応用することが考えられる．
7 構文解析と論理式への変換は事前に済ませ，解析時間には含めない．また，各 RTE の問題に対して制限時間 100 秒を設定する．
これらの実験は 16 コア 2.20 GHz Intel Xeon CPU × 2 を用いて行われた．

参考文献[1] Timothy Chklovski and Patrick Pantel. VerbOcean: Mining the Web for Fine-Grained Semantic Verb Relations.
In Proc. of EMNLP, 2004.
[2] George A. Miller. WordNet: A Lexical Database for English. 1995.
[3] Mark Steedman. The Syntactic Process. The MIT Press,
2000.
[4] Alex A. Alemi et al. DeepMath - Deep Sequence Models
for Premise Selection. 2016.
[5] Gilles Dowek et al. The COQ Proof Assistant: User’sGuide: Version 5.6. INRIA, 1992.
[6] Koji Mineshima et al. Higher-order logical inference withcompositional semantics. In Proc. of EMNLP, 2015.
[7] Marco Marelli et al. A SICK cure for the evaluation ofcompositional distributional semantic models. In Proc.
of LREC, 2014.
[8] Pascual Martı́nez-Gómez et al. On-demand Injection of
Lexical Knowledge for Recognising Textual Entailment.
In Proc. of EACL, 2017.
[9] Samuel R. Bowman et al. A large annotated corpus forlearning natural language inference. In Proc. of EMNLP,2015.
[10] Théo Trouillon et al. Complex embeddings for simplelink prediction. In Proc. of ICML, 2016.
[11] Tim Dettmers et al. Convolutional 2D Knowledge GraphEmbeddings. AAAI, 2017.
[12] Zhen Wang et al. Knowledge Graph and Text JointlyEmbedding. In Proc. of EMNLP, 2014.
[13] 戸次大介. 「日本語文法の形式理論−活用体系・統語構造・意味合成−」. くろしお出版 日本語研究叢書２４, 2010.

― 116 ―

Copyright(C) 2018 The Association for Natural Language Processing.
All Rights Reserved.