Discover and Prove：Lean 4向けの「難所モード」自動定理証明を行うオープンソースのエージェント型フレームワーク

Abstract

ほとんどのATPベンチマークは、最終回答を形式的な主張の中に埋め込んでいます――これを私たちは「Easy Mode（イージーモード）」と呼びます。この設計は、人間の競技者が直面する状況に比べて課題を単純化しており、モデル能力についての楽観的な推定につながる可能性があります。より厳格で、より現実的な設定を「Hard Mode（ハードモード）」と呼びます。Hard Modeでは、システムは形式的な証明を構築する前に、答えを独立して発見しなければなりません。Hard Modeの研究を可能にするために、私たちは2つの貢献を行います。第一に、広く使われている2つのATPベンチマークの、専門家による再注釈（expert-reannotated）版であるMiniF2F-HardとFIMO-Hardを公開します。第二に、Discover And Prove（DAP）というエージェント型フレームワークを導入します。このフレームワークは、LLMの自然言語による推論と明示的な自己反省を用いて答えを発見し、その後、既存のATPプローバ向けにHard Modeの主張を書き換えてEasy Modeの主張にします。DAPは最先端の成績を更新します。CombiBenchでは、解けた問題数を7（従来のSOTA、Pass@16）から10へ引き上げます。PutnamBenchでは、Hard Modeにおいて36の定理を形式的に証明した最初のシステムです。しかも同時に、形式的なプローバが10%未満であるのに対し、同じ問題において最先端のLLMが80%超の回答精度を上回っていることを明らかにします。これは、Hard Modeベンチマークが独自に測定に適している、実質的なギャップを浮き彫りにしています。