LLMベースの定理証明プラットフォーム『LeanDojo（リーン道場）』が登場しました。
多くの複雑な定理で未踏の証明能力を示しています。
検証データセットとモデルが公開されています。
カリフォルニア工科大、NVIDIA、MITなどの研究者らによる開発です。
@ Kaiyu Yang et al., “LeanDojo: Theorem Proving with Retrieval-Augmented Language Models”
大きなプロジェクトに対応する、つまり複雑な数学の問題に取り組むには、これまでの定理証明ツールは力不足でした。
そこで研究者らはモデル『ReProver（リプルーバー）』を開発しました。
そして『LeanDojo（リーン道場）』プラットフォームで公開しました。
■フレームワークの仕組み
① 現在の証明状態に関連する前提を選択
② 状態と前提から、次の証明ステップを生成
③ LeanDojoがプログラムを解析
④ アクセス可能な前提を特定
⑤ 最も効果的な証明パスを見つける探索を行う
※ほとんどのステップは自動と考えられる
■モデルとプラットフォームの性能
以下の準備で実験が行われました。
① LeanDojoで新しいベンチマークを構築
② 98,734の定理と証明を抽出
③ ReProverは単一のGPUで5日間のトレーニング
実験の結果、ReProverは、GPT-4を使用したベースライン（29.0%）を上回る、51.2%の定理を証明できました。
■主な結論
LeanDojoとReProverは、独自のデータセットや大量の計算リソースが不要な、初のオープンソース定理証明ツールである
■おまけ
“dojo”（道場）という言葉は、日本の武道や修行の場を指す言葉として始まりましたが、現在では多くの非日本語圏でも広く使われています。プログラミングや技術の文脈では、”dojo”は学習や練習、スキル向上の場を意味することが多いです。
