DreamProver：ウェイク・スリープ定理証明エージェントによる転用可能レマライブラリの進化
arXiv cs.AI / 2026/4/30
📰 ニュースModels & Research
要点
- DreamProverは、ウェイク・スリープのプログラム誘導手法を用いて、形式的な定理証明向けに再利用可能なレマ（補題）ライブラリを構築する新しいエージェント型の定理証明フレームワークである。
- 「ウェイク」段階で現在のレマライブラリを使って学習データの定理を証明しつつ新しい候補レマを提案し、「スリープ」段階で候補を抽象化・洗練・統合してライブラリを圧縮・最適化することで、適応性を段階的に高める。
- 従来手法のギャップである、汎用性の乏しい固定レマライブラリ、または特定の定理に強く依存して汎用性を欠く中間レマの問題に焦点を当てている。
- 複数の数学ベンチマークでの実験により、未見の関連領域の定理に対して、証明成功率の大幅な向上、より簡潔な証明、計算コストの削減が示される。
