Goedel-Prover-V2 - プリンストン大学が清華大学やNVIDIAなどと共同で開発したオープンソースの定理証明モデル。

ゲーデル・プローバーV2とは？

Goedel-Prover-V2は、プリンストン大学、清華大学、NVIDIAなどの主要機関によるオープンソースの定理証明モデルです。Goedel-Prover-V2モデルには、32Bと8Bの2つのバージョンがあり、多くのベンチマークで優れた性能を発揮しています。例えば、MiniF2Fテストでは、32BモデルがPass@32で90.41 TP3Tという高いスコアを記録し、より大規模なDeepSeek-Proverを凌駕しています。例えば、MiniF2Fテストにおいて、32BモデルはPass@32で90.4%のスコアを達成し、はるかに大規模なDeepSeek-Prover-V2を凌駕しました。 このモデルは複雑な数学的問題に対する証明を自動的に生成することができ、証明の質を向上させるためにLeanコンパイラからのフィードバックに基づいて自己修正します。また、Goedel-Prover-V2のオープンソースという性質は、研究者がさらなる開発や改善を行うための基盤を提供します。

Goedel-Prover-V2の主な機能

• 証明書の自動生成複雑な数学的パズルを解くために、複雑な数学的問題の形式的証明過程を生成する。
• 自己修正能力リーン・コンパイラからのフィードバックにより、モデルは証明の正確さと質を向上させるために、繰り返し修正を行うことができる。
• 効率的なトレーニングと最適化階層的データ合成とモデル平均化技術に基づき、学習効率を改善し、モデル性能を向上させることで、複数のベンチマークテストで好成績を収めることができます。
• オープンソースとスケーラビリティ研究者による開発と改良を促進するために、オープンソースのモデルとデータセットを提供する。

ゲーデル・プローバーV2の性能

• MiniF2Fベンチマーク::
  • 32BモデルのPass@32スコアは90.41 TP3Tと高く、671BのDeepSeek-Prover-V2（82.41 TP3T）を大きく上回っている。
  • 8BモデルのPass@32スコアは83.3%であり、DeepSeek-Prover-V2の約1/100のパラメータ数であるにもかかわらず、DeepSeek-Prover-V2の性能に匹敵する。
• PutnamBenchベンチマーク::
  • 32BモデルはPass@64メトリクスのトップで、64の問題を解決している。
  • Pass@32の指標では、32Bモデルは57の問題を解決し、47の問題を解決したDeepSeek-Prover-V2-671Bを大幅に上回った。
  • 8Bモデルも非常に優れた性能を発揮し、DeepSeek-Prover-V2-671Bに匹敵する。
• MathOlympiadBenchベンチマーク::
  • 32Bモデルは73の問題を解決し、50の問題を解決したDeepSeek-Prover-V2-671Bを大きく上回った。
  • 8Bモデルも32Bモデルのレベルに迫る好成績を収め、強力な定理証明能力を示している。

ゲーデル・プローバーV2公式サイトアドレス

• プロジェクトのウェブサイト:: https://blog.goedel-prover.com/
• HuggingFaceモデルライブラリ::
  • https://huggingface.co/Goedel-LM/Goedel-Prover-V2-8B
  • https://huggingface.co/Goedel-LM/Goedel-Prover-V2-32B

ゲーデル・プローバーV2の使い方

• プロジェクト・リソースへのアクセスHuggingFaceモデル・ライブラリにアクセスし、HuggingFaceからモデル・ファイルをダウンロードし、適切なバージョン（例：8Bまたは32B）を選択します。
• ハードウェア要件高性能GPUまたはGPUクラスタを推奨します。
• ソフトウェア環境PythonとPyTorchなどのディープラーニングフレームワークをインストールし、大規模なモデル推論をサポートする環境を確保する。
• 入力の問題証明を必要とする数学的問題を、モデルがサポートする形式（リーン言語など）に変換する。
• データ前処理モデル要件に従って問題をコーディングし、フォーマットする。
• 積載モデルHuggingFaceが提供するツールを使って、事前にトレーニングしたモデルをロードします。
• 世代証明問題はモデルに入力され、リーン・コンパイラを使って検証・修正された証明が自動的に生成される。
• 検証証明書リーンコンパイラを使って、生成された証明が正しいかどうかチェックしてください。
• 反復修正証明が間違っていた場合、正しい証明が生成されるまで、モデルはフィードバックに基づいて自己修正する。

Goedel-Prover-V2の主な利点

• 優れたパフォーマンス例えば、32BモデルはMiniF2FのPass@32テストで90.4%の精度を達成し、他の類似モデルを大きく引き離しています。
• 革新的な技術アーキテクチャ階層的データ合成、バリデータ誘導型自己修正、階層的データ合成に基づくモデル平均化技術により、モデル学習の効率と証明の質を効果的に向上させる。
• オープンソースとスケーラビリティオープンソースのモデルとデータセットを提供し、研究者が自由にアクセス、使用し、改良のためにさらに開発できるようにする。
• 幅広いアプリケーション・シナリオ数学研究、ソフトウェア・ハードウェアの検証、教育補助、人工知能・機械学習、科学研究・工学など幅広い分野に応用可能。
• 効率的なトレーニングと最適化階層的データ合成とモデル平均化技術に基づく効率的な学習と性能最適化により、モデルの頑健性を向上。

Goedel-Prover-V2が適応となる人

• 数学者、数学研究者数学的予想の検証、複雑な問題の証明、数学理論の探求と研究の加速に使用される。
• コンピューター科学者、ソフトウェア・エンジニアソフトウェアやハードウェアの開発において、アルゴリズム、プログラム・ロジック、回路設計の正しさを検証し、システムの信頼性と安全性を高めるために使用される。
• じんこうちのうけんきゅうしゃ機械学習モデルの数学的基礎とアルゴリズムロジックを検証し、モデルの信頼性と精度を確保する。
• 教育者と学生数学教育の一助として、生徒が数学の概念や定理をよりよく理解し、習得できるように、公式証明の例を提供する。
• 研究者とエンジニア科学研究や工学設計における数学的モデルや理論を検証し、設計ソリューションの実現可能性と信頼性を確保する。