すごい! でも、すこし違うかも

【 すごい! でも、すこし違うかも 】 

前回は、Open-AI Theorem Proverが何を学習したかということで、"miniF2F-curriculum" 、"synth-ineq"、"mathlib-train"という三つの「カリキュラム」があることを紹介しました。

今回は 、5,600の訓練用の定理からなる"synth-ineq" を、もう少し見てみようと思います。といっても、僕は、このデータを全て見た訳ではありません。イリヤ達の論文にそのデータの作り方が、Appendix  D. にサンプルが、紹介されています。

サンプルの二つ目に、次のような定理が挙げられています。

  2a(a - 68) <= a^2 + (a - 68 )^2

(a - 68 ) の '68' という数字は、ランダムに選ばれたものです。それ自体に意味はないと思います。ただ、イリヤ達の論文で、synth-ineq の作り方を見ていると、いったん '68' が選ばれると、次のような命題も、生成されるべき定理の候補になるような気がします。

  2a(a - 1/68) <= a^2 + (a - 1/68 )^2
  2a(a - log 68) <= a^2 + (a - log 68 )^2
         ・・・

ただ、これらは全て、次のより一般的な定理から、簡単に導かれるものです。

  2xy <= x^2 + y^2
 ( なぜなら、(x - y)^2 >= 0 から、 x^2 - 2xy + y^2 >= 0 ですから。)

この定理の学習だけでは、足りないのでしょうか?

イリヤ達が紹介しているように、不等式型の定理の生成では先行する論文があります。

"INT: AN INEQUALITY BENCHMARK FOR EVALUATING GENERALIZATION IN THEOREM PROVING"
https://arxiv.org/pdf/2007.02924.pdf 
https://github.com/albertqjiang/INT

これは、なかなかすごい論文で力作です。GitHubが公開されていますので、動かしてみてください。

不等式型の定理を生成するだけでなく、その定理の証明に利用される定理(論文ではaxiom と言っていますが)の数や、証明の中でのその出現順序、証明の長さについて、導かれた不等式型定理の証明を分析しています。こうしたメルクマールでの証明の複雑さについてのアプローチは、イリヤ達にも引き継がれています。

ただ、この論文 INT のアプローチは、イリヤ達が方法論的には断念したはずの、セルフ・プレイのような事実上無限の訓練データの生成を、別の形で追求しているように思います。


【「彼は、何を学習したのか (2) synth-ineq 」を公開しました 】

https://youtu.be/T9mG2uWrvv8?list=PLQIrJ0f9gMcPP8LOejaQQlYufAMEQbcdg

スライドのpdfは、こちらからアクセスできます。https://drive.google.com/file/d/1uUCklH7sXhSpJkFrUj87FdmHSet_UHjE/view?usp=sharing

このトピックのまとめページは、こちらです。ほぼ毎日更新されると思います。https://www.marulabo.net/docs/math-proof/

セミナーへのお申し込みは、こちらからお願いします。
https://math-proof.peatix.com/

コメント

このブログの人気の投稿

マルレク・ネット「エントロピーと情報理論」公開しました。

初めにことばありき

人間は、善と悪との重ね合わせというモデルの失敗について