rat360

A personal schizophrenic idea blog

仮定から結論を導出する一般ルールはあるか [日本語]

ATP (自動定理証明) は数学とアルゴリズムをつなげるトピックだと思います。FOLとHOLは少し毛色が異なりますが、GoogleはHOLのためのアルゴリズムとして"deephol"を開発し、"HOList"という共有タスクとして公開しています。

この問題について少し考えてみたいと思いました。HOLのためのATPは基本的に以下のステップを取るようです:

  • 前提の選択: 証明対象のゴールに関係しそうな前提を選択する。
  • 推論: 何らかのアルゴリズムを適用して、対象のゴールに対して証明を検索する。

Tactics, Premises, Goals, という要素がありますが、これらを総じて「仮定」ということが出来ると思います。仮定をいくつか選択して、それを推論アルゴリズムの入力に渡しているわけです。

しかし、ある理論的質問について気になっています: そのアルゴリズムそのものを見つけるための仮定を定義できるでしょうか。

f:id:anon_programmer:20201106123815j:plain

この画像はこの考えを説明しています。

A: assumptions
A': selected assumptions
C: possible conclusions
f: selecting assumptions
g: inferring

X_f: assumptions to infer f
X_g: assumptions to infer g
F: possible conclusions of Φ_f○φ_f(X_f)
G: possible conclusions of Φ_g○φ_g(X_g)
φ: selecting assumptions
Φ: inferring

無限ループになるじゃないか!

しかし、fとgはAからCに向かってエントロピーを減らしているのではないかということに気が付きました。そこで質問: 結論集合Cのエントロピーは0でしょうか。

もし、たった1つのバリエーションの結論集合Cが常に導けるなら、そのエントロピーは0と言えるはずです。しかし、我々は「時間」や「空間」を気にしなければならないのです。計算時間を減らすことは、結論導出のエントロピーを増大させるでしょうか。また、「アルゴリズムを見つけるためのアルゴリズム」である Φ○φ について気になっています。

ところで、「オッカムの剃刀モデリングに良い」という話を聞いたことがあるかもしれません。でも、なぜでしょうか。それはおそらく、「エントロピー」に関係します。コルモゴロフ複雑性はエントロピーへのある種の関連事項だと思います。うまく説明できる段階にありませんが、ATPアルゴリズムを見つけるという問題に対して、エントロピーやコルモゴロフ複雑性という概念が関わっているように私は思っています。

我々の世界は物理制約と論理制約を持ちます。もし、物理制約が一切存在しないなら、ほとんどなんでもブルートフォースで一瞬で解ける可能性があるので、その場合は結論導出のエントロピーは低いはずです(それが一様分布とは異なっている可能性が高い)。物理制約は、計算複雑性において、時間と空間を気にする必要があることを意味するのではないでしょうか。

なので、時間制約が存在する場合の計算が本質的に確率的にならざるを得ないのかが気になっています。言い換えれば...結論集合を導出するためにエントロピーを増加させる必要があるでしょうか?

(ちなみに、ここで用いた「エントロピー」という語は一様分布において最大になるものとして仮定しています。言い換えれば、当該の確率変数の不確実性の平均値です。)

English: Is there a general rule to infer conclusions from assumptions? - rat360