Lean4がテレンス・タオの最近の論文で小さなバグを見つける助けに
(mathstodon.xyz/@tao)- Terence Taoは Lean4形式化プロジェクトを進める中で、論文中の小さいが些細ではない誤りを発見した
- 誤りはarXiv論文
2310.05328の 6ページ目の論証で明らかになり、1/2 log((n - 1)/(n - k - 1))がn = 3, k = 2の場合に発散する - 問題は小さい
nの値に限られ、n >= 8では従来の論証が機能し、小さいnはより粗い方法で直接処理できる - Leanは
0 < n - 3の証明を要求したが、仮定はn > 2だけだったため、linarithタクティックは必要な矛盾を得られなかった - Taoは一部の 数値定数を調整して論証を修正し、Leanでの形式化の試みの中で以前の論証の不正確さが見つかったという脚注を新しい版に入れる予定
Lean4形式化が明らかにした誤り
- Terence Taoは自身の Lean4形式化プロジェクトの過程で、論文に小さいが些細ではないバグがあることを発見した
- 形式化の対象はarXiv論文
2310.05328の6ページ目の論証だった - 問題となった式は次の形である
1/2 log((n - 1)/(n - k - 1))
- この式は
n = 3, k = 2の場合に発散する
誤りの範囲と修正方法
- この問題は小さい
nの値でのみ発生するn >= 8では当該論証は依然として機能する- 小さい
nはより粗い方法で直接処理できるが、定数は悪化する
- Taoは当該ページの一部の 数値定数を変更すれば論証を修正できると見ている
- 論文の新しい版には、以前の論証がやや不正確であり、Leanで形式化しようとして発見されたという 脚注を追加する予定
Leanが行き詰まった具体的な箇所
- 形式化が失敗した箇所で、Leanは
0 < n - 3を証明するよう要求した- 利用可能な仮定は
n > 2だけだった linarithタクティックは0 < n - 3の否定から矛盾を導けなかった
- 利用可能な仮定は
1件のコメント
Hacker Newsのコメント
彼は今月初めに GPT-4の助けを借りてLean4 を学び始めた: https://mathstodon.xyz/@tao/111208692505811257
今月の彼のMastodon投稿のかなりの数が学習の進捗に関するもので、大規模言語モデルがトップクラスの成果を上げる人たちの作業までどれほど加速できるかを示す興味深い事例だ
興味深いことに、こうしたツールは高度なスキルを持つ人だけが効果的に活用するなら、不平等をさらに広げる可能性もある
Lean4に気軽に触れたいなら Natural Number Game がよい: https://adam.math.hhu.de/#/g/hhu-adam/NNG4
ゲームなしで読むだけならこちら: https://lean-lang.org/theorem_proving_in_lean4/introduction.html
最初はAlloyをAllowと書いていた
数年前、自分が書くプログラムのミスを減らす方法を探していて、Lamportの TLA+ を知り、状態機械としてプログラムの動作を考えながら形式仕様を書く方法を学んだ
TLA+は抽象化を明確に理解させてくれ、その後Coq証明支援系を使って形式的に正しいソフトウェアを作る Software Foundations シリーズも見つけた。演習問題が小さなゲームのようになっていて、かなり楽しく解けた: https://softwarefoundations.cis.upenn.edu/
高水準の抽象である形式仕様は、コードを説明するための専用言語に集中し、低水準の抽象であるコード契約は、検証ロジックをより良いモデルで置き換える方向に近い。C#にはかつてCode Contracts[1]があり、Z3 SMTソルバー[2]でコンパイル時に契約を検査する単純だが強力な方式だったが、数年後に廃止され[3]、.NET Runtimeから削除されて事実上終わった。今のC#で最も近いものはおそらくDafny[4]で、C#開発側はいまだにこれを言語へ直接入れる方法を検討している[5]
[1] https://www.microsoft.com/en-us/research/project/code-contracts/
[2] https://github.com/Z3Prover/z3
[3] https://github.com/microsoft/CodeContracts
[4] https://github.com/dafny-lang/dafny
[5] https://github.com/dotnet/csharplang/issues/105
Idris2は汎用言語を目指しつつ、定理証明のためのより発展した型システムを提供しているように見える: https://github.com/idris-lang/Idris2
Coqの代わりにAgdaを使う、ある程度派生した本もある: https://plfa.github.io/
まだ読めていないがリストには入れていて、AgdaやIdrisはCoqよりプログラミング言語らしく感じられる可能性が高いと思う
依存型には本当に期待している。ただ、当分は出てこないだろう
Dependent Haskellは進行中だが、既存の言語に後から組み込むのは難しいと言われており、Idrisの作者もIdrisが他の言語のモデルになることを期待すると述べていたが、主流での採用は難しそうだ。Coq、Agda、F*も汎用言語として設計されたものではない。コンパイラ実装は複雑で、構文も冗長になり得るが、私が望むのは単純さだ。入力と出力について知っていることをすべてエンコードしたい。現在の主流言語では、引数や出力について、型システムに表現させてくれる以上のことを知っている場合が多い
TypeScriptのような漸進的な方式で、あらゆる場所で全部を証明しなくても、任意の場所に型レベルの値制約情報を追加できるとよい
たとえば数値のリストとその長さを一緒に知っているなら、依存型で長さを明示的に含むリスト型を作ることができ、コンパイル時に操作がその長さを守ることを保証できる。長さ3のリストだけを受け取る関数を指定したのに長さ4のものを渡すとコンパイルされないため、実行前にミスを捕まえられる。型の表現力が高まり、変数間の複雑な関係までエンコードする追加の安全検査層のようなものだ
私たちの世代で最も優れた知性の一人が、大規模言語モデルと自動証明の組み合わせによって仕事の幅を広げられるのだとしたら、この技術の組み合わせの未来は非常に楽観的に見える
始まりはバグ修正で、次に検証を助け、最終的には新しい発見を後押しして限界を広げていくことになりそうだ。ムーアの法則のようなダイナミクスが、本来そうした累積的性質を持たなかった分野を「感染」させる現象を呼ぶ用語が必要だ。補足として、Terence Tao は Lean を学ぶのに Copilot を使っている: https://mathstodon.xyz/@tao/111271244206606941
Copilot なしでもできたかもしれないが、新しいツールを受け入れる際の摩擦のせいで、始めなかった可能性もある。大規模言語モデルは、こうした「思考の自転車」のような状況で大きな可能性を持っている
数年前、Terence Tao の数学ブログ記事でもバグを1つ見つけたことがある。知らせたら修正され、感謝の言葉ももらった
もちろん Hacker News のトップページには載らなかった
Lean4 がまた別の大規模言語モデルなのかと思って心配したが、実際にはかなり堅牢で信頼できるツールだった
Lean 証明検査器のような形式証明検査器と、Lean のような形式言語で合成的な予想・証明のペアを生成する言語モデルを組み合わせられるのか気になる。
Lean 証明検査器で、言語モデルが書いた合成証明が正しいかを自動検証し、その情報を元の言語モデルに適用する強化学習の報酬信号として使えば、より良い証明を書けるようにできる。あるいは、前のラウンドで得られた正しい合成証明を学習データとして新しいモデルを訓練することもできる。さらに敵対的にすることも可能。予想生成モデルと証明／反証モデルに分け、合成証明が Lean 証明検査器で検証されるかを予測するモデルを追加する。正解確率が低いと予測されるほど、実際に正しい証明を出したときに証明生成モデルがより大きな報酬を受ける、という形。最後に、特定の合成予想について証明生成モデルが受け取る報酬を予測するモデルを追加すれば、予想生成モデルは、証明生成モデルにとって難しすぎず簡単すぎない、高い報酬が見込める予想を作るよう報酬を受ける。システム全体がだんだん難しい合成証明を作り出し、それが証明生成モデルのより良い自己学習につながる可能性がある。原理的には、証明生成で超人的能力にまで拡張でき、GAN や AlphaGo Zero の自己対局に似ている。難しいのは初期のブートストラップで、生成モデルの最初の学習には人間が提供した Lean 証明データが必要になる。しかし合成証明が十分に良くなれば、システムは自動的に自己学習を続けられる。
最終的には、数学文献のすべての定理とすべての正しい証明を知るモデルを得られるかもしれない。
既存の証明から教師あり学習を始め、新しい証明を見つける初期段階のものとしては、TacticToe (https://arxiv.org/abs/1804.00596), Tactician (https://arxiv.org/pdf/2008.00120.pdf), CoqGym/ASTactic (https://arxiv.org/abs/1905.09381), Proverbot9001 (https://arxiv.org/abs/1907.07794), Diva (https://dl.acm.org/doi/10.1145/3510003.3510138#sec-terms) などがある。大半は内部に何らかの形で言語モデルを持つが、最近大きな関心を集めている大規模言語モデルを探すなら、GPT-f (https://arxiv.org/abs/2009.03393), Baldur (https://arxiv.org/abs/2303.04910), COPRA (https://arxiv.org/abs/2310.04353) がある。ただ現時点では、これらのモデルは特化型の非大規模言語モデル系ツールほど有効ではないように見える。人間が書いた証明を超えて強化学習で学ぶ方向には、TacticZero (https://openreview.net/forum?id=edmYVRkYZv), OpenAI 論文 (https://arxiv.org/pdf/2202.01344.pdf), rlCoP (https://arxiv.org/abs/1805.07563), HOList 系の研究 (https://arxiv.org/pdf/1905.10006.pdf), HyperTree Proof Search (https://arxiv.org/abs/2205.11491) があり、University of Massachusetts のチームと私が進めている研究もある。
Tao がこの道のりで GPT-4 を含む大規模言語モデルツールをどのように使ったかについての以前の文脈はこちら: https://mathstodon.xyz/@tao/111233986893287137
彼の進捗は GitHub でも追える: https://github.com/teorth/symmetric_project/