Daily Arxiv

世界中で発行される人工知能関連の論文をまとめるページです。
このページはGoogle Geminiを活用して要約し、非営利で運営しています。
論文の著作権は著者および関連機関にあり、共有する際は出典を明記してください。

APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning

Created by
  • Haebom

作者

Azim Ospanov, Farzan Farnia, Roozbeh Yousefzadeh

概要

APOLLOは、LeanコンパイラとLLMの推論能力を組み合わせて数学のクリーンアップを証明する自動化されたクリーンアップ証明システムです。従来のLLMベースのクリーンアップ証明方式は、多くのサンプリング（数千回）を介して検証システムを通過する証明を生成しますが、APOLLOはLLMが証明を生成し、エージェントが証明の構文エラーを修正し、Leanを使用して間違いを特定し、失敗した部分クリーンアップを分離し、自動ソルバーを活用し、残りの目標に対して低コストでLLMを使用します。変更された部分証明を再結合して再検証するプロセスを、ユーザー制御可能な最大試行回数まで繰り返します。 miniF2Fベンチマークでは、8B未満のパラメータモデルのうち84.9％の精度が達成され、サンプリングコストは100未満に維持されました。さらに、GoedelProverSFTの精度を65.6％に上げ、サンプルの複雑さを25,600から数百に減らしました。

Takeaways、Limitations

•
Takeaways：
◦
LLM出力のターゲットコンパイラガイドを変更することで、効率と精度が大幅に向上することを示しています。
◦
自動クリーンアップ証明のための拡張可能な一般的なパラダイムの提示。
◦
安価なサンプリングコストで高い精度を達成しました（MiniF2Fベンチマークでは84.9％、GoedelProverSFTでは65.6％）。
◦
一般目的モデルの精度を大幅に向上（3-7％から40％以上）。
•
Limitations：
◦
現在、特定のベンチマーク（MiniF2F、GoedelProverSFT）のパフォーマンスのみが提示されており、他のベンチマークやより複雑な整理の一般化の可能性にはさらなる研究が必要です。
◦
APOLLOのパフォーマンスは、使用されているLLMとLeanコンパイラに依存しており、他のシステムとの互換性と移植性に関するさらなる研究が必要です。
◦
ユーザー制御可能な最大試行回数の設定など、パラメータの最適化に関するさらなる研究が必要です。
👍
Made with Slashpage