語句の真相とあやまち

なにもないことにまつわるあれこれとか関係のないこととか

ニューラルネットで個体という概念を学習できるのだろうか

ニューラルネットで画像認識をした場合、二つの像が似ていることは学習できるけれど、その二つの像の示す個体の同一性までは学習できていないと思う。

 

たとえば、セキュリティで同じ人間かどうかは判定するとき、顔や指紋に基づいて処理するが、それは同一人物であるということを学習しているわけではない。ようだ。

 

同一性という概念はあいまいで難しいから人間でもわからなくなる。

 

その部分は人間がプログラムを組んでいるのだろうけれど、

量子計算と論理について考え始める

ある像aがNNでカテゴリーPに属する確率をrと判定されたとき、P(a,r)と書くとすると事実は+P(a,r)として得られる。

では-P(a,1-r)なのかというと違うような気がする。

否定と確率の関係を理解するために、あれこれ考えているうちに、量子計算が関係するかもしれないと思いこの本を読み始めた。量子コンピュータ入門(宮野, 古澤)。

最近、数理科学でも量子情報の特集があったりしていて、ブームに押し流されているのかもしれない。

 

この本を読んでいて、4章のあたりで論理ゲートのふるまいの説明を読んで書いてあることの意味が分からなくなったのだけれど、|0>=1|0>+0|1>と|1>=0|0>+1|1>の定義にもどって考えなくてはならないことに気づいたら、先に進むことができた。

 

 

今後したいことの整理

  1. 確率と否定
    1. P(a,r) でrをP(a)である確率だとする。
    2. このとき、¬P(a,r)はP(a,1-r)と同じではないみたいだ。
    3. ¬P(a,1-r)を含めた四つの関係は?
  2. 量子計算-トポス-論理-確率と否定
  3. 全proofの有限表現と操作
    1. 証明のカバリング
    2. proofの情報とはなにか?
      1. Capical変数なのか?
  4. 時間によって変化するAxiomと自動証明
    1. A=>A' のときTh(A)=>Th(A')はどう対応するのか
    2. Aに対して、+a, -a, -a+b
  5. Resolution
    1. よいrenameとは?
      1. unification
      2. substitution
      3. 情報抽出
      4. 証明
    2. literl evaluation
    3. term evaluation/partial
    4. rid,cidの有効性は?
    5. varidの扱いは?
    6. templateといってていいのか?
    7. 実装について
      1. literal, clause, termをjuliaのExprにしていていいのか? parserを作らなくていいのか
      2. timeoutをいれてはどうか
      3. 必要なloopのみ実行できるようにしたい
  6. NN
    1. NNでLogicにたどりつけるのか
      1. たとえば、三段論法を学習できるのか。
      2. 例) 同一性を学習できるか
        1. 像が似ていることは判定できても、それの背景に同じ個体があることを学習できるのか。 双子の問題とか
        2. 力学では、量質が同じ物体は区別されないというようなこともあり、同一性とは何か
        3. 同じとはどういう意味か
        4. そもそもNNで学習するとはどういうことか?
      3. 音と像をあわせてNNで学習すると、音と像の対応関係が学習されるのか
        1. 楽器の写真を見せるとその音がわかったり、音を聞かせると楽器の写真がわかったり?
        2. それができるのなら、声から人物を特定することができるのか
      4. NNとLogicを繋ぐことの意味
        1. NNでLogicまで学習するのはコストが高すぎる
        2. すべてをAIでできるということ
  7. 具象と抽象の間をいききできる
    1. P(x,r)とφ(P,x,r)が同値だとすると、いろいろできる
    2. そのとき証明のloopを抑制する必要がある。必要のないloopをしないですませる方法は?

λx,z,E.y F(x,y),F(y,z)→F(x,z)

clause形に変換するとき、違うclauseの変数は独立になる。

 

λx,z,E.y F(x,y),F(y,z)→F(x,z)

は、全順序のようにも見えるが本当は、友達の友達は友達の関係。

ここでは、yが存在すればF(x,z)であるということで、存在が重要。

 

存在を全称にしてしまってこれをclauseにすると

¬F(x,y),¬F(y,z),F(x,z)

となり、これの否定は

F(x,y),F(y,z),¬F(x,z)

になる。

この否定が矛盾を導けば、元の主張は正しいということになる。

 

Fact1={F(a,b), F(b,c),F(a,c)}

のとき、確かに反証できる。

しかし、

Fact2={F(a,b), F(d,c), F(a,c)}

でも成り立ってしまうのはおかしい。

これはおそらく、yは存在なのでclauseを超えて同じ値にならなくてはならないということではないだろうか。

 

もともとclause formにするとき存在変数は定数に置き換えられることになるので、同一性は必要とされる。しかし、定数では代入ができないのでこの問題が解決できない。

 

mguを代入とだけ考えるのではなく、{x←t}を{x=t}という条件と考えれば、対処できるとは思う。

 

いずれにせよ、存在変数(とは呼ばないと思うが)は、clauseを超えた変数の同一性と考えればいいのではないか。

 

あるいは問題の視点が間違っているかも。

 

 

 

 

Factのadjustについて

Factの述語記号P、定数記号cとし、FactにP(c)が含まれていないとき

 

  • Pが2つに一つだったら、-P(c)を加えてもいいはず。
    つまり、G(x)が'xは少女'という意味なら、FactにG(c)が含まれていなければ'-G(c)'にしても、だいたい正しい
  • 一方で、友達を表す'F(x,y)'について、Factの中で、F(a,b), F(b,c)からF(a,c)が導けるかどうかを判定しようとしてるときに、勝手にF(a,c)を加えてはならない。

こんな証明はできないのか

clauseの集合を

{P(a), Q(a), Q(b)}

としたとき

any x. P(x) → Q(x)

は証明できるのか?

 

できないみたい。

Herbrand Universeで成り立っても、必ずしも成り立たないようなかんじ。

 

もしも、

{P(a), P(f(x))}

P(f(x))

の証明は当然できる。

 

 

そしてResolution

Juliaで論理式を表す方法について、ずっと試行錯誤している。

いまは、parse("[x,y].[+P(x,f(x)),-Q(x,y)]") のようにparse()を使うことにして、Exprベースで式を扱っている。

内部で[x,y] と :([+(P(x,f(x)),-(Q(x,y))] に分けているのだけれど、これも[:(+(P(x,f(x)))), :(-(Q(x,y))]にしたほうがいいかもしれない。

 

Resolutionについては、だいぶ忘れてしまったので、思い出すためにいろいろ調べているけれど、今のAIブームの中では自動証明はほとんど話題になっていないように見える。

 ニューラルネットと自動証明はAIの両輪のような気がするけれど、そうでもないのかもしれない。そもそもAIという言葉も意味不明ではあるけど。

 

話題がそれたので戻すと、unificationはできていて、単体のResolutionもできているはず。

あとはclause集合からcontradictionを導出するtactics/strategyをどうするか・・・

 

まず、命題論理でgoalからの証明の枠組みを作り、一階でその証明にmguが存在するかどうかでステップの刈り込みを行う。

このとき、繰り返される証明ステップパターンが無限の証明になるのをどうするか。

 

これは先の場合と同じく、

  • 世界の事実(Fact)をground unit clauseの集合で表し
  • それに対する仮説(理論, Theory)を変数を含むclauseの集合で表す
  • queryはいまのところunit clauseを想定

というようなもの。

仮説は、すべてのFactについて成立するものを考えているので、少なくとも

Fact + Theory は無矛盾にしたい。これは、Theoryの各clauseをFactに加えたとき矛盾がでないことで分かるが、たぶん有限時間に検証できるだろう。

複数のTheoryの間の矛盾は有限時間では分からないかもしれない。たぶん分からない。