【DL輪読会】HyperTree Proof Search for Neural Theorem Proving

DEEP LEARNING JP [DL Papers] HyperTree Proof Search for Neural Theorem Proving 塚本 慧 http://deeplearning.jp/ 1

• http://deeplearning.jp/

書誌情報 タイト HyperTree Proof Search for Neural Theorem Proving ル： https://arxiv.org/pdf/2205.11491.pdf 著者： Guillaume Lample, Marie-Anne Lachaux, Thibaur Lavril, Xavier Martinet, Amaury Hayat, Gabriel Ebner, Aurelien Rodrigue 概要： • トランスフォーマーに基づいた自動定理証明のためのオンライン学習のモデルの提案。 • モンテカルロ木探索を導入。 • miniF2Fの問題の正答率を大幅に改善 Copyright (C) Present Square Co., Ltd. All Rights Reserved. 2

• https://arxiv.org/pdf/2205.11491.pdf

アジェンダ 1. イントロダクション 1. 前提知識・関連研究 1. 証明の環境 1. HyperTree Proof Search 1. 証明探索でのオンライン学習 1. 実験 1. 結果 1. 結論 Copyright (C) Present Square Co., Ltd. All Rights Reserved. 3

１. イントロダクション イントロダクション • これまで数学の証明の検証は人間の手で行われてきたが、数学の証明の複雑さが増している現在においては 不十分になってきている。数学を形式化することによってコンピュータに検証させようとする動きがある。 数学の形式化 • 形式的な数学はプログラミング言語で書かれたソースコードに近く、伝統的な数学とはかけ離れている ため、使うのが難しい。 • 既に証明されている定理を形式化するのにも膨大な労力がいる。 素数が無限個あることの証明 Copyright (C) Present Square Co., Ltd. All Rights Reserved. 4

１. イントロダクション イントロダクション • 本研究では与えられた定理を人間の支援抜きでタクティックの列を生成して証明する。 • この研究により既に証明されている数学の形式化にかかる労力を大幅に削減できる。 • 証明をハイパーツリーとみなすことでモンテカルロ木探索を導入する。（後述） Copyright (C) Present Square Co., Ltd. All Rights Reserved. 5

２. 前提知識・関連研究 証明プログラミング言語 • まだ検証されていない命題をゴールとし、タクティックによってゴールと仮定を変形したり分割する。 • ゴールに何も表示されない時に証明されたということになる 編集 仮定とゴールの表示 解きたい命題 タクティック （使っていい補題） lean and_commutative Copyright (C) Present Square Co., Ltd. All Rights Reserved. 6

• https://leanprover-community.github.io/lean-web-editor/

２. 前提知識・関連研究 ゴールの分割 Copyright (C) Present Square Co., Ltd. All Rights Reserved. 7

２. 前提知識・関連研究 自動定理証明は人工知能における長年の難問として知られている。近年の大規模言語モデルや、 モデルによる探索手法の成功に伴い自動定理証明への関心が再び高まっている。 ニューラル定理証明 • 深層学習の手法を定理証明に適用されている 言語モデルの推論能力 • 大規模トランスフォーマーの推論能力に注目が集まっている モンテカルロ木探索と二人用ゲーム • AlphaZeroのような二人用ゲームでの探索と同様に、定理証明は既に証明されている定理や補題、テクニック を用いて探索しているとみなせる Copyright (C) Present Square Co., Ltd. All Rights Reserved. 8

３. 証明の環境 証明の環境（使う証明プログラミング言語とそのライブラ リ） • Metamath, Lean, Equationsの三種類の環境で実験を行った(Equationsは本研究で新しく作った環境) 仮定とゴール（木構造の ノードと呼ぶ） タクティック Copyright (C) Present Square Co., Ltd. All Rights Reserved. 9

４. HyperTree Proof Search 証明は木構造であるとみなせる 証明の仮定とゴールは木構造のノード タクティックは木構造の枝 Copyright (C) Present Square Co., Ltd. All Rights Reserved. 10

４. HyperTree Proof Search HyperTree Proof Search 選択 • 次に取るべきタクティックを探索と知識利用のバランスを取りながら選択する 展開 • 葉ノードを訪れた回数が閾値以上となった場合に、そのノードから先を展開する 更新 • 得られた報酬を記録し、期待報酬を更新する Copyright (C) Present Square Co., Ltd. All Rights Reserved. 11

４. HyperTree Proof Search 選択 選択 • タクティックごとに計算を行う • 報酬の総和をWとする（ここでの報酬は証明可能性を表している（解ける = 1, 解けない = 0）） • 訪問回数をNとする • 評価値をQ=W/Nとする 探索のアルゴリズムはPUCTとRegularized Policyの両方を試す Copyright (C) Present Square Co., Ltd. All Rights Reserved. 12

４. HyperTree Proof Search 展開 展開 • 言語モデルを用いてタクティックを文章として生成 • 評価値の高いノードを優先して展開（証明においてタクティック を実行） Copyright (C) Present Square Co., Ltd. All Rights Reserved. 13

４. HyperTree Proof Search 更新 更新 • 子ノードの評価値を元にノードの評価値を更新 • ゴールが分割されていて子ノードが複数ある時 子ノードの評価値の総積でノードの評価値を更新 （評価値は0~1で証明可能性を表す、また子ノード同士の独立性を仮定） Copyright (C) Present Square Co., Ltd. All Rights Reserved. 14

５. 証明探索でのオンライン学習 学習の対象 • タクティックのモデル ゴールを入力としてタクティックを出力する（言語モデルと同じ） • クリティックのモデル ノードの評価値（証明可能性）を予測 Copyright (C) Present Square Co., Ltd. All Rights Reserved. 15

５. 証明探索でのオンライン学習 オンライン学習 非同期で分散学習を行う • タクティックのサンプル ゴールとタクティックのペアを抽出して訓練データとして使う • クリティックのサンプル 探索が終わった後のすべてのノードの評価値を訓練データとして使う 探索の途中で正しいことが証明されたノードの評価値は１ 探索の途中で間違いであることが証明されたノードの評価値は０ Copyright (C) Present Square Co., Ltd. All Rights Reserved. 16

５. 証明探索でのオンライン学習 訓練の全容 • 事前学習 (数学に関する文章を大量に学習) • ファインチューニング（学習の環境に合わせた証明プログラミング言語（Metamath, Lean, Equations）の学習） • オンライン学習（HyperTree Proof Search） Copyright (C) Present Square Co., Ltd. All Rights Reserved. 17

６. 実験 モデルのファインチューニングとラベル付きのデータセット • MetaMath set.mmライブラリから37091個の証明を抽出 • Lean Mathlibライブラリから24kの証明と、144kのゴールとタクティックのペアを抽出 • Equations • 本研究のために自作で作った環境なのでライブラリがないためランダムにタクティックを実行し定理を 生成した モデルの事前学習 • 数学に関するarxivの論文のLatexのソースコード（60億トークン）を マスク付きのSeq2Seqのモデルで学習 Copyright (C) Present Square Co., Ltd. All Rights Reserved. 18

６. 実験 モデルのアーキテクチャと訓練 • 12層のエンコーダと6層のデコーダを持つトランスフォーマーのアーキテクチャを使用 • エンコーダの埋め込み次元は1600, デコーダは1024(Equationsのときのみデコーダは512) • Equationsのときのパラメータ数は440M, MetaMathとLeanは600M ファインチューニング • 最適化アルゴリズムはAdam • 逆平方根学習率スケジューリングを用いる • ドロップアウト率は0.2 • レイヤードロップアウト率は0.1 オンライン学習 • Warmupのあとは学習率を3×10-5 • 48 V100 GPUで16つの訓練機と32つの証明機を用い た • Pytorchを用い学習を高速化するためにfloat16を使用 Copyright (C) Present Square Co., Ltd. All Rights Reserved. 19

７. 結果 主要な結果（モンテカルロ木探索を実行した回数は定理ごとに64） Copyright (C) Present Square Co., Ltd. All Rights Reserved. 20

７. 結果 Lean 1日の訓練でminiF2F-curriculumの327の問題を110問解く(GPT-fは100問) 7日の訓練で137問解く オンライン学習中の正答率は58.6% テスト用のデータセットでは41%(GPT-fは36.6%) MetaMath オンライン学習により正答率を61%から82.6%に向上 Equations Copyright (C) Present Square Co., Ltd. All Rights Reserved. 21

7. 結論 まとめ • AlphaZeroから生まれた自動定理証明のための証明探索アルゴリズムを紹介した • 複数の証明の環境で最高の結果を出した • 数学の形式化のデータが限られているため、探索で新しいデータを増やす方法が必要になる • 新しい定理を生成できるかも将来の課題になりそう Copyright (C) Present Square Co., Ltd. All Rights Reserved. 22

Appendix 参考文献 Leanのチュートリアル https://leanprover.github.io/theorem_proving_in_lean/ Leanの素数に関するライブラリ https://github.com/leanprover-community/mathlib/blob/master/src/data/nat/prime.lean#L418 Copyright (C) Present Square Co., Ltd. All Rights Reserved. 23

• https://leanprover.github.io/theorem_proving_in_lean/
• https://github.com/leanprover-community/mathlib/blob/master/src/data/nat/prime.lean