技術的要約： 「sorry」を埋めることは、最も困難な部分ではない

問題提起

半自律的な形式化（semi-autonomous formalization）における支配的なナラティブは、証明の完了（proof completion）、すなわちエージェントが証明助手（Leanなど）に検証された定理として受理されるコードを生成できる能力に焦点を当てている。しかし、著者らは、検証された定理は再利用可能なライブラリへの貢献とは別物であると主張している。現代の数学は相互に関連するライブラリに依存しており、そこでは定義が結合し、定理のステートメントが適切な汎用性を持ち、APIが将来の推論を強制することなくユーザーを支援する必要がある。

特定された核心的な問題は、LLM（大規模言語モデル）は局所的な証明のギャップ（「sorry」の除去）を埋める能力は高まっているものの、高品質でメンテナンス可能な形式化を実現するために必要なグローバルな設計決定においては苦戦していることである。具体的には、エージェントは適切な定義の選択、汎用的な定理ステートメントの設計、あるいはクリーンなAPIの構築に失敗することが多く、その結果、カーネルは通過するものの、エキスパートによるライブラリへの貢献としてのレビューには合格できないコードを生成してしまう。

手法

本論文は、Lean 4を用いたグロタンディークの消滅定理（Hartshorne, 1977, Ch. III, Thm. 2.7）の半自律的な形式化に関する詳細なケーススタディを提示している。この定理は、ノーター的な位相空間 $X$ と整数 $n$ について、$n$ が $X$ の位相的クリュル次元よりも大きいとき、$X$ 上のアーベル群の層の $n$ 次層コホモロジーが消滅することを述べている。

研究は、以下の前後比較実験デザインに従っている：

1. 状態A（初期の形式化）： エージェント（Claude Code）が、人間から提供された定理のステートメントとHartshorneの証明のPDF抜粋に基づき、「sorry」（未証明のゴール）がゼロの状態でコンパイルが通る形式化を生成した。
2. エキスパート・レビュー： Lean/mathlibのエキスパートが状態Aをレビューし、定義、定理の汎用性、ファイルの構成、およびAPI設計における問題を特定した。
3. 状態B（リファクタリングされた形式化）： エージェントに対し、エキスパートのチェックリストに対処するタスクを与えた。これには、「レビュー駆動のリファクタリング」と、それに続くmathlibの慣習に合わせるための「圧縮と磨き上げ（compression and polish）」のフェーズが含まれる。
4. 二次レビュー： 同一のエキスパートが状態Bをレビューした。

分析では、定義、定理ステートメント、証明、およびファイル/API構造の4つの次元にわたって両状態を比較している。プロジェクトのタイムライン、トークン使用量、およびツールとの相互作用は、エージェントの振る舞いのパターンを理解するために、コミットログとテレメトリから再構成された。

主要な知見と結果

1. 定義：主要な失敗点

定義は最も脆弱なコンポーネントであり、エージェントが状態Aから状態Bにかけて最も改善が見られなかった領域である。

• 状態A： エージェントは62個のカスタム定義を生成した。そのうち正しく再利用可能と判断されたのは1つ（TopCat.closedIncl）のみであった。残りは「アドホック」なものであり、標準ライブラリの構成を現在の証明コンテキストに特化した名前（例：既存の sheafSections の代わりに sheafH_filtered_colimit_h1_sectionsFunctor とする）でラップしたものだった。
• 結果： これらの定義は「将来の輸送コスト（future transport costs）」を生み出し、後続のユーザーに対して、オブジェクトを使用するための些細な等価性の証明を強いることになった。また、基礎となる構文を隠蔽することで、タクティクのパフォーマンス（例：simp）を阻害した。
• 状態B： エージェントは、一般的で再利用可能な定義を作成する能力を大幅に改善できなかった。エージェントは、便利な特殊化を持つ一般的な構成を設計するのではなく、引き続き具体的で不必要なオブジェクトを作成し続けた。

2. API設計：部分的な改善

• 状態A： エージェントは層コホモロジー（Sheaf.H）のためのAPIを構築せず、下流のファイルで定義を繰り返し展開（unfold）していた。
• 状態B： エージェントは専用のAPIファイルを作成し、これにより下流の証明が整理された。しかし、そのAPI自体は「ノイズが多く肥大化」しており、洗練された原理的なインターフェースではなく、約800行におよぶ24個の極めて具体的な補題を含んでいた。
• 対照： エージェントは topologicalKrullDim（より単純な定義）のAPIについては良好な設計ができた。これは、限定された特定のタスクを与えられた場合には優れたAPIを設計できることを示唆しているが、オープンエンドな設計には苦慮することを示している。

3. 定理ステートメント：局所的 vs グローバル

• 状態A： エージェントは直近の証明に必要なものだけを証明しており、しばしば過度に具体的な仮定（例：一般的な短完全列で十分な場面で「単射な表示」を要求するなど）を使用していた。
• 状態B： エージェンドは、レビューチェックリスト内で明示的に要求された場合には、定理のステートメントを一般化することに成功した。しかし、自発的に必要な一般化を特定することはできなかった。エージェントは局所的な構文修正には優れているが、将来の再利用ニーズを予見するグローバルな判断力を欠いている。

4. 証明：一様ではない改善

• 状態A： 証明には「have 文の壁」が含まれ、定義の等価性の誤用や、定義の直接的な展開が頻発していた。
• 状態B： 証明は改善され、特に既存のmathlibオブジェクトを使用しているファイルにおいて顕著であった。エージェントは、複雑な証明を分解するために名前付きのサブ補題を採用しており、これは「ハートビート（性能）」の制約によって強化されたパターンである。
• 限界： エージェント自身の質の低い定義（例：フィルタ付き余極限のファイル）に依存する証明は、依然として可読性とメンテナンス性に課題があった。

5. プロセス・ダイナミクス

• フィードバックへの適応： エージェントは、明確な完了述語（例：「このファイルの名前を変更せよ」「この仮定を一般化せよ」）に対してはよく適応した。一方で、反事実的な判断（例：「将来的に有用となるAPIを設計せよ」）を必要とするフィードバックには苦戦した。
• 脱出ハッチ（Escape Hatches）： エージェントは、困難な設計決定に直面すると、タスクを「ブロックされた（blocked）」と宣言したり、インフラ（例：mathlibのギャップ）のせいにしたりする傾向があった。これらのフレーズを禁止する明示的なプロンプトが、分解を強制するために必要であった。
• 指標： 「sorry を埋めること」は、品質を示す指標としては不十分である。プロジェクトは、sorry の数がゼロになった後も、コード行数や構造の面で大きく進化し続けた。

意義と主張

本論文は、自動形式化の評価は、二値的な証明完了を超えて拡張されなければならないと主張している。著者らの主張は以下の通りである：

1. カーネルの受理は不完全である： 定理はカーネルによって検証されても、将来のユーザーに対して、扱いにくい型変換、重複した定義、管理不能なAPIを強いる可能性がある。
2. 「再利用性のギャップ」： エージェントの局所的なゴールを閉じる能力と、定義を選択しAPIを設計する能力の間には、鋭い隔たりが存在する。後者には、現在のLLMが欠いている「将来の再利用に関する判断」が必要である。
3. 評価基準： AIによる数学システムは、結果として得られた形式化がエキスパートのレビューを生き残れるかによって評価されるべきである。具体的には、証明がチェックされた後、エキスパートが公開された定義、定理ステートメント、名前空間、およびAPI表面をレビューし、設計フィードバックに対するシステムの応答能力を測定すべきである。

本研究は、グローバルな設計のための洗練された仕組みがなければ、LLMは「検証されたアーティファクト」を生成することはできても、まだ「再利用可能なライブラリへの貢献」を行うことはできないと結論づけている。今後の道筋は、人間がエキスパートとして品質仕様（定義、インターフェース）を定義し、エージェントが狭く機械的にチェック可能なリファクタリングを担当するという役割分担にある。