Self-Supervised Theorem Discovery in a Formal Axiomatic System
Abstractの概要
本論文は、人間が作成した定理ライブラリや証明コーパス、自然言語による教示に依存せずに、エージェントが形式システム内で有用な定理を自律的に発見できるかどうかを調査している。著者らは、命題論理のヒルベルト体系においてこの問題を具体化し、公理のインスタンス化とモーダスポネンスをアクションとするスタックマシンの決定過程として証明構築を定式化している。彼らの自己教師ありアルゴリズムは証明探索と定理抽出を交互に行い、探索中に到達した論理式は将来の目標となり、選択された定理は再利用可能な補題アクションとして追加される。複数世代にわたり、この手法は定理ライブラリを成長させ、数万もの定理を発見し、自身の探索と外部のLLMベースの証明試行の両方を支援できる定理を生成する。
新規性
最大の貢献は、公理と推論規則のみから開始し、発見した定理を再利用可能な補題アクションに変換することで独自のアクション空間を拡張する、自己教師ありの定理発見フレームワークである。また、発見された定理がヒューリスティックにもっともらしいか有用かを判断するだけでなく、それらをプロンプトの補題として提供した際にLLMの証明探索を向上させることを実証し、外部への有用性を直接評価している。
成果
実験において、エージェントは6世代にわたって数万の定理を発見し、最終的に38の定理アクションからなるライブラリを構築した。発見された定理群は、命題論理における30問の人間作成ベンチマークの30%をカバーし、抽出された定理をプロンプト補題として提供することでGPT-4oやGPT-5バリアントの証明成功率が向上した。定性的な事例では、発見された補題がない状態ではGPT-5-highが失敗するものの、それらが提供されると成功するケースも示されている。
論文の注目点
- この手法は、ヒルベルト式の定理証明をスタックマシンプロセスとして表現し、自身の証明軌跡中に到達した定理から目標条件付きポリシーを学習する。
- 有用な定理の抽出では、一般性フィルターと再証明可能性の基準を組み合わせ、選択された定理を後続世代の探索のための新しいライブラリアクションとして再挿入する。
- 発見された定理は、エージェントの内部で再利用可能であるだけでなく外部のLLMにも転用でき、ヒルベルト体系における形式的証明の構築を向上させる。