Daily Arxiv

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

DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theorems

Created by
  • Haebom

作者

Meiru Zhang, Philipp Borchert, Milan Gritta, Gerasimos Lampouras

概要

LLMを活用した自動整理証明で最大の課題は、辞書数学の知識とLeanなどの言語での対応する形式的表現を把握して活用することです。 DRIFTは、非公式の数学的記述をより小さく、処理しやすいサブコンポーネントに分解する新しいフレームワークを提案します。これにより、Mathlibなどの数学ライブラリで前提をターゲットにして検索できるようになります。さらに、DRIFTは、モデルが前提をより効果的に使用できるように、説明的なクリーンアップを検索します。 DRIFTはProofNet、ConNF、MiniF2Fテストなどのさまざまなベンチマークで評価されており、前提検索を一貫して改善し、ProofNetのDPRベースよりもF1スコアをほぼ倍増しました。特に、DRIFTはアウト・オブ・ディストリビューションのConNFベンチマークでGPT-4.1とDeepSeek-V3.1を使用して37.14％と42.25％のBEq + @ 10を向上させ、強力なパフォーマンスを示しました。

Takeaways、Limitations

•
Takeaways：
◦
非公式の数学的ステートメントをサブコンポーネントに分解するDRIFTフレームワークを介してLLMの前提検索能力を向上させます。
◦
さまざまなベンチマークで既存の方法論と比較してパフォーマンスが向上しました。
◦
特に、Out-of-distribution ベンチマークで高いパフォーマンスを記録。
◦
モデル別の知識境界に合った適応型検索戦略の必要性を提示
•
Limitations：
◦
モデル固有の知識境界によって性能の違いが生じる可能性があります。
◦
自動クリーンアップ証明に関する特定のモデルの知識依存性を完全に解決できない
👍
Made with Slashpage