LLM（Large Language Models）は、厳密に検証可能な数学的証明を生成できるのでしょうか？LeanDojoにご参加ください：Lean Proof Assistantで形式的な定理を証明するためのツールキット、ベンチマーク、およびモデルを備えたオープンソースのAIプレイグラウンド

LLM（Large Language Models）は数学的証明を生成できるのか？LeanDojoに参加してくださいLean Proof Assistantは、形式的な定理を証明するためのツールキット、ベンチマーク、およびモデルを備えたオープンソースのAIプレイグラウンドです

人工知能と機械学習は、現代のトレンドとなっています。AIの進歩により、新たなイノベーションが人間と機械の相互作用を変革しています。人間の知性の推論は人工知能の重要な部分です。自動定理証明（ATP）など、数多くの定理証明アプローチが研究されてきました。ATPは、形式論理で述べられる定理に対して自動的に証明を生成するプロセスです。ATPは巨大な探索空間のために困難であるため、人間の専門家が証明補助ツールと呼ばれるソフトウェアツールと対話することで証明を構築する対話型定理証明（ITP）が代替のパラダイムとして登場しました。

大規模な言語モデル（LLM）は、驚くべきコード生成能力を示していますが、事実性の欠陥や幻想により、定理証明においても困難に直面しています。これらの制約を克服するために、Caltech、NVIDIA、MIT、UC Santa Barbara、UT Austinの研究者チームは、LLMベースの定理証明のためのオープンソースツールキットであるLeanDojoを開発しました。LeanDojoは、数学者に人気のあるLean証明補助ツールを中心に構築されています。Leanとの作業やデータの抽出に関するリソースを提供しています。

データの抽出では、証明木や元のLeanコードでは直接明らかではない中間の証明状態からトレーニングデータを収集します。LeanDojoは、モデルがLeanとプログラム的に通信できるようになっています。これにより、モデルは証明状態を見たり、証明アクションやタクティクスを実行したり、Leanからフィードバックを受けたりすることができます。オープンソースのLeanプレイグラウンドは、ツールキット、データ、モデル、ベンチマークなど、プログラム的な証明環境とLeanからデータを抽出するための多数の要素で構成されています。

• 百度Ernie 3.5が中国語AIのチャンピオンとして登場：しかし、ChatGPTより本当に優れているのか？
• Contextual AIは、VQAv2においてFlamingoを9%上回る（56->65%）ビジョン補完言語モデルのためのAIフレームワークLENSを導入しました
• 3B、4B、9B のスケールで 5 つの新しいマルチモーダルモデルを備えた OpenFlamingo チームが、前モデルを上回る OpenFlamingo v2 をリリースしました

LeanDojoは、証明における前提条件の詳細な注釈を提供し、定理証明における重要なボトルネックである前提選択に貴重な情報を提供します。LeanDojoのデータ抽出機能を使用することで、研究者たちは、大規模な数学ライブラリから前提を選択するために検索を補完する初のLLMベースの証明補助プログラムであるReProverを開発しました。従来の方法とは異なり、ReProverは大量の計算リソースを必要とするプライベートデータセットに依存せず、よりアクセスしやすく、コスト効果が高いように設計されています。ReProverは、わずか1週間で1つのGPUでトレーニングすることができ、コンピューティングパワーの要件も少ないです。

LeanDojoのプログラム分析能力は、ReProverの検索メカニズムによってアクセス可能な前提条件を見つけ出し、何が間違っているかの具体的な例を示すのに使用されます。その結果、証明補助プログラムのパフォーマンスが向上し、検索手順もより効果的になります。評価とさらなる研究のために、チームはLeanの数学ライブラリから抽出した96,962の定理と証明からなる新しいベンチマークデータセットを開発しました。このベンチマークデータセットは、訓練中に使用されなかった新しい前提に依存する定理に汎化するために、チャレンジングなデータ分割を特徴としています。実験結果は、このベンチマークデータセットを使用してトレーニングと評価を行う際、ReProverが非検索ベースラインやGPT-4と比較して優れたパフォーマンスを発揮することを示しています。

結論として、LLMベースの定理証明のためのこのオープンソースソリューションは、将来において有望です。プライベートコード、データ、大規模な計算要件の障壁を、アクセス可能なツールキット、データ、モデル、ベンチマークを提供することで克服しています。

We will continue to update VoAGI; if you have any questions or suggestions, please contact us!