End-to-End Differentiable Proving

End-to-End Differentiable Proving by Tim Rocktäschel, Sebastian Riedel arXiv:1705.11040v2 https://arxiv.org/abs/1705.11040v2

被参照

DeepLogic: Towards End-to-End Differentiable Logical Reasoning Nuri Cingillioglu, Alessandra Russo arXiv:1805.07433v3

気になった参考文献

[27] Stuart J. Russell and Peter Norvig. Artificial Intelligence - A Modern Approach (3. internat. ed.). PearsonEducation, 2010. ISBN 978-0-13-207148-2.
[7] Théo Trouillon, Johannes Welbl, Sebastian Riedel, Éric Gaussier, and Guillaume Bouchard. Complex embeddings for simple link prediction. In Proceedings of the 33nd International Conference on Machine Learning, ICML 2016, New York City, NY, USA, June 19-24, 2016, pages 2071–2080, 2016.
[34] Antoine Bordes, Nicolas Usunier, Alberto García-Durán, Jason Weston, and Oksana Yakhnenko. Translat- ing embeddings for modeling multi-relational data. In Advances in Neural Information Processing Systems 26: 27th Annual Conference on Neural Information Processing Systems 2013. Proceedings of a meeting held December 5-8, 2013, Lake Tahoe, Nevada, United States., pages 2787–2795, 2013.

内容

証明をNeural Netで学習して、高い確率で正しい証明をするモデルを作るというような話らしい。参考文献が豊富で、役に立ちそう。

この方式のことは、将来、Deep LogicあるいはNeural Theorem Prover(NTP)と呼ばれるようになる。

この論文のように、Neural networkとTheorm proverを組み合わせることは重要だと思う。この論文は、Proverをneural networkにとりこむような方向のように思う。それがどこまでできるのかは興味深い。

2年前の論文なので、これを参照している論文もあり、位置付けがわかるだろう。まだ先の論文は未読。

KB(たぶん Knowledge Baseの略)というのも出てきている。これは参考文献[27]をみないと定義はわからない。用語の定義は[27]がベースらしい。 KBは、Horn clause の集合として考えられているのかなと思う。

どのような証明を学習したのか。

Horn clauseで、関数を含まない論理式を対象としている。 Horn setの文脈で、否定のリテラルは扱わないと書かれている。

ということは

関数を使っていないので、引数に変数だけが現れる論理式になり、引数の置換が定義されるだけではないか。 Unificationで失敗するのが、定数間の不一致のみであり、命題論理とそんなに違わないような気がする。つまり、x←f(x)の形のloopは現れないから、無限についての言明はできないはず・・・ Deep Learning自体は無限の言明を生み出せないが、学習する対象が無限についての言明を持っていればそれを学習することができるだろう。しかし、その対象が無限を扱えないのでは学習しようもないか。 feature workとして関数を扱ったものをあげているので、そのような論文は見てみたい。

否定については、Horn clauseベースだと否定は出さないほうがやりやすいだろう。Resolutionを使うということは対応する否定がなければ矛盾を出せないので、そもそもFactにおける否定とはどういうものかという考察があったほうがよいような気がする。そもそもNeural Netを使う話が主で、Logicの基本については参考文献任せ。

たとえば、UnificationやSubstitutionの定義はあっさりとしか書かれていないので、どういう定義を採用しているのかが謎。[27]を参照するしかないが、昔の電話帳くらいの厚さがあり、読む気力おきず。

ベンチマーク関係

結果の評価には、既存のベンチマークを使っている。{ベンチマークについての論文[7]もあげられていて、使ってみたい。評価では[37]まだみていない。この論文では、NTPとCompExと組み合わせた方法を評価している。

Neural networkでは、sproof successという値が高くなるような学習をする(3. Differentiable Prover] このscoreは、証明のステップごとに(and と or)計算していく。

この論文だったか、これを参照している論文だったかで、NTPは、従来のProverよりも高速に証明するというようなことが書かれていた。 NTPの場合、Neural Networkを使うので、証明する段階でも行列計算をするから、時間はかかるのではないかと思ったが、考えてみれば、proverではresolutionを組み合わせ的に適用してresolventを求めるので時間がかかっているわけで、NTPではそのかわりにgradient decentを用いる。という意味で、「より高速に証明する」ということなのだろうと思う。

正しくない推論を高速にやってもなあという気はする。

理解できていない点父、祖父、祖先の関係を例としたものがFigure 2に示されている。よくわからないのは、orの右下(2)でunifyがFailしていないのがおかしい。

章のタイトルになっているキーワードは次のものがある。

Differencial Prover
Neural Inductive Logic Programming

ComplExという、neural link prediction modelを使っている。ComplExは付録で簡単に紹介されている。

後半はついていけなかった

課題は巨大なKBについて証明をしようとするとなかなかできない、ということがあり、それが解決できているかどうかは 5. Experimentにま>とめられている。が、表の見方が謎である。

これを読んでいるときに思いついたこと

🎂 Factについて

これまでFactをどうやって得るかということを、私は、分割NNで、確率の高いカテゴリをC(x)を真と考えればよいとだけ考えていたが、Factをみつける方法はいろいろありうると気づいた。
ルールについても、すでに証明ができたものでなければ使ってはいけないのだろうと思っていたが、そうでもない。
- 証明だけでなく、モデルにもとづく証明であったり、人間が正しいと信じている論理式をFactとしてよい。
- ルールも、人間が信じているあるいはへつの方法で証明ができた場合に、組み込んでいい。それは普通はFactと呼ばないかもしれないけれど。
論理学では、SoundnessとかCompletenessが重要な概念だが、この論文ではまったく触れられていない。
この論文を読む前は、NNでLogicを学習するということは、Factの大集合をもとに、NNで推論規則を学習するということだと思っていた。そのようにして、cutを学習できたら、NNがLogicを学習したということだと思っていた。この論文は違う。証明をみせて、それを学習するのがこの論文の方法。だから、cutの存在は前提条件になる。 Logicで書かれる∀や∃をNNが学習できるのかどうか。(clauseになる段階では∀しか残らないが・・・) 大有限の事実から無限についての命題を求められるだろうか。

sazare / readings