EasyProver、PutnamBenchで669/672を証明しAegisも公開

研究チームは、再帰エージェントを基盤とするLean証明システム「EasyProver」を発表しました。EasyProverは追加学習なしの既製フロンティアモデルを使い、PutnamBenchで669/672問を証明しています。研究チームは併せて、競技プログラミング問題を実コード検証タスクへ変換するパイプライン「Aegis」も公開しました。

EasyProverの構成と既存ベンチマークの結果

EasyProverは、分離されたコンテキストを持つ再帰エージェント、非同期探索、並列タクティック探索、弾力的なelaborationサービスを組み合わせています。

ベンチマーク	結果
PutnamBench	669/672問を証明
IMO 2026形式化	6/6を証明
NTP4VC	597/600の検証条件を証明または反証
VERINA	全189タスクを証明または反証

Aegis:実装レベルの検証タスク生成

論文はこれらのベンチマークが飽和に近いとし、より難しいタスクを作るためにAegisを提案しています。Aegisの処理は次の流れです。

• 競技プログラミング問題から安全なRust解を作成する
• AeneasでRustコードをLeanへ変換する
• 仕様を生成する
• 各固定文を、カーネル検査済みの証明または反証でラベル付けする

Aegisは差分検証済みのRust-Leanプログラム対を2,045組、候補仕様を11,533件生成しました。手書きのベンチマークと異なり、これらのタスクには固定幅算術、明示的な失敗、生成ループ、キャスト、関数化された可変状態といった実装レベルの義務が含まれます。

Aegisタスクでの評価

項目	値
層化サンプルの文数	2,000
1文あたりの証明予算	30分
EasyProverが証明した文数	1,054
証明率	52.7%

研究チームは、生成したタスクを他の証明器のベンチマークや強化学習の報酬として使えるとしています。