ジユアン・タン (Jiyuan Tan)氏、バシリス・シーガンキス (Vasilis Syrgkanis)氏、ホセ・ブランシェット (Jose Blanchet)氏らは10月21日(現地時間)、研究論文の証明や前提に存在する小さなギャップを発見・修正し、Lean検証済みバージョンへ変換する新ツール「ペーパーフォーマライザー (PaperFormalizer)」を発表した。本ツールは、著者自身が形式化プロセスに関与することで、論文の主張の正確性を保持しつつ、その堅牢性を高めることを狙う。
ペーパーフォーマライザー (PaperFormalizer) は、Leanを基盤とするエージェント型パイプラインとして機能する。まず、LaTeX形式で書かれた論文ソースコードを取り込み、記述された声明の依存関係をグラフ形式で転記する。次に、各声明について、自然言語処理を用いてその忠実性、曖昧さ、および正確性を監査する。その後、これらの声明は、Mathlibなどの既存の数学ライブラリ、オプションのドメイン固有ライブラリ、および著者の個人的なツールキットを活用してLean言語で形式化され、証明が行われる。
このパイプラインは、声明が複数の解釈を許す場合や、形式化の過程で生じたギャップを修正する最適な方法について、著者の介入を求めるように設計されている。システムが提示する各修正提案は、自然言語とTeX記号で明確に示され、著者が提案の承認、却下、または方向転換を指示できる。これにより、論文の主張に影響を及ぼす可能性のある全ての重要な決定が著者に委ねられる仕組みが維持される。
PaperFormalizerの最終的な出力には、変更点が注釈付けされた改訂版論文、実施された変更に関する詳細な報告書、および各宣言が形式化された声明にリンクされたLeanコードが含まれる。このプロセスを通じて、著者は自身の形式化ツールキットを拡張し、検証済みの論文とそれに付随するLeanコードを共有することで、他の研究者がその成果を再利用できるようになる。
PaperFormalizerは、Claude CodeやCodexといった高度なコーディングエージェントの内部で動作する。ユーザーがPaperFormalizerを用いて形式化し、共有を許可したLeanコードを含む論文は、別途提供されるオンラインリソースを通じて閲覧可能となっている。
参考: arXiv cs.AI — 2026年10月26日 13:00 (JST)
原文ハイライト"a Lean-based agentic pipeline that helps authors find and close such gaps"