Continual Graph Memory for Mathematical Research Agents
Abstractの概要
本論文では、長期的な証明探索のための構造化メモリシステムであるContinual Graph Memoryを中心に構築された数学研究エージェント「Ansatz」を提案する。このメモリは、承認された事実、計画や反例などの探索的成果物、およびプロジェクト横断的な知見を統合グラフ内に明示的に保存し、依存関係を考慮したコンテキスト選択、キュレーターによるアノテーション、スコープ付き想起を通じて検索と再利用を制御する。本システムは、新たな問題において過去の結果が自動的に有効であると見なすことなく、エージェントがプロジェクト間で数学的探索を持続、再開、転移できるように設計されている。評価には、First Proof Second Batchの10課題、構成要素のアブレーション、および一連の未解決数学問題が含まれる。
新規性
際立った貢献は、検証済みの事実を探索状態や再利用可能な知見から分離する、数学研究エージェント向けの複数問題横断的なグラフベースメモリアーキテクチャである。型付き探索グラフ、証拠に敏感なキュレーション、依存関係を考慮した検索、および必須の局所的再証明を伴うスコープ付き想起の組み合わせが、主要な新しいシステム設計要素とみられる。
成果
報告されたベンチマーク評価において、AnsatzはFirst Proof Second Batchの10課題すべてで解決を達成し、GPT-5.6ベースのベースラインを含む論文記載の他システムを上回った。構成要素の研究では、探索とキュレーション、独立した検証、戦略の参照が性能に実質的に寄与していることが示された一方、テストされたサブセットでは明示的な事実グラフ構造単独での測定可能な向上は見られなかった。ベンチマークにとどまらず、著者らはJamison caterpillar予想およびエルデシュ問題289、348、488の完全な解決と、さらに6つの未解決問題における部分的な進展を報告している。
論文の注目点
- Ansatzは、承認された事実、計画、反例、その他の途中結果を明示的な依存関係および出所構造のもとでリンクする統合メモリによって数学的証明探索を体系化する。
- ベンチマークの実証結果では、First Proof Second Batchにおいて10/10の課題解決が報告されており、グラフベースの検索は一定の割合ではなく問題ごとに大きく変動しつつ多用されている。
- アブレーションと監査により、キュレーション、外部検証、戦略参照が実用上重要である一方、プロジェクト横断的な再利用は無条件の転移ではなく局所的な再証明によって制約されていることが示唆されている。