スタンフォード大学の研究者は、因果推論の理論研究を自動化するエージェント型パイプライン「CausalSmith」を開発しました。結果を提案し、言語モデルによる査読を経て、Lean 4で証明を形式検証します。さらに、対話型ウェブページとスライドを備えた論文を作成します。支援ライブラリー「Causalean」には、統計学と因果推論に関するLean検証済みの定義・定理が15,000件以上収録されています。

CausalSmithは、発見、形式化、発表の3段階で動きます。発見段階ではエージェントが成果と自然言語による証明を提案し、別のエージェントが正しさと新規性を確認します。Leanが証明を検査し、監査工程では形式化された主張と論文の仮定・結論を照合して、定理が論文の主張より弱くなっていないか調べます。最後に、読みやすい論文、対話型ページ、20分間の発表用スライドを作成します。

研究者は、離散的な交絡がある場合に平均処置効果を推定する成果を例に挙げました。Zengらの2024年の論文は下限を示しましたが、その下限に達する推定量があるかは未解決でした。CausalSmithは差を埋め、ミニマックス率を達成する推定量を提案しました。Leanで証明を完成させるため、パイプラインはLeanの標準数学ライブラリーMathlibに不足していたランダムな度数に関する集中不等式を証明し、Causaleanに追加しました。研究者は、例に使った論文を手作業で確認し、因果推論では従来使われていなかった証明手法を見つけたと述べています。

2026年10月時点で、チームはCausalSmithを1,732回実行しました。うち41回（2.4%）は、正しく、Leanで完全に証明され、各実行で定めた査読基準上の新規性も十分として採択されました。さらに1,388回は数学的には正しいものの進歩が限定的と査読者が判断し、格下げされました。提案または数学が却下された303回は失敗となりました。採択・格下げ・失敗の各実行は記録され、後続の実行に活用されます。再利用できる補題や定理は一般化して査読したうえでCausaleanに追加され、同じ問題を扱った後の採択成果では、集中不等式を再証明せずに利用しました。

研究者は、Mathlibに因果推論の内容がほとんどなかったため、Causaleanを構築しました。文献からよく使われる成果を選び、言語モデルの支援で整理・形式化し、各記述を人手で確認しました。後続の実行でも、言語モデルの査読を経て不足している古典的成果を追加できます。収録分野は因果グラフ、潜在結果、構造的因果モデル、推定、実験、パネルデータです。査読者は、項目が出典と一致し、再利用可能で、空虚な主張ではないことも確認します。プロジェクトページでは、論文の評価、文章へのコメント、個別の主張の認証ができ、自然言語の定義・定理と監査済みのLean版を比較できます。新規性審査とLean検証を通過した論文にはDOIと引用情報が付与されます。

研究者によると、2026年10月時点で作成された論文のうち、人手で確認したのは一部にとどまり、全体的な質はまだ分かっていません。現段階では、プロジェクトページの評価、認証、コメントが人による判断を集める主な手段です。今後の方向性として、より体系的な新規性指標と、言語モデルが新しい研究を行う能力を評価するベンチマークを挙げました。

スタンフォード大学の研究者は、因果推論の理論研究を自動化するエージェント型パイプライン「CausalSmith」を開発しました。結果を提案し、言語モデルによる査読を経て、Lean 4で証明を形式検証します。さらに、対話型ウェブページとスライドを備えた論文を作成します。支援ライブラリー「Causalean」には、統計学と因果推論に関するLean検証済みの定義・定理が15,000件以上収録されています。

CausalSmithは、発見、形式化、発表の3段階で動きます。発見段階ではエージェントが成果と自然言語による証明を提案し、別のエージェントが正しさと新規性を確認します。Leanが証明を検査し、監査工程では形式化された主張と論文の仮定・結論を照合して、定理が論文の主張より弱くなっていないか調べます。最後に、読みやすい論文、対話型ページ、20分間の発表用スライドを作成します。

研究者は、離散的な交絡がある場合に平均処置効果を推定する成果を例に挙げました。Zengらの2024年の論文は下限を示しましたが、その下限に達する推定量があるかは未解決でした。CausalSmithは差を埋め、ミニマックス率を達成する推定量を提案しました。Leanで証明を完成させるため、パイプラインはLeanの標準数学ライブラリーMathlibに不足していたランダムな度数に関する集中不等式を証明し、Causaleanに追加しました。研究者は、例に使った論文を手作業で確認し、因果推論では従来使われていなかった証明手法を見つけたと述べています。

2026年10月時点で、チームはCausalSmithを1,732回実行しました。うち41回（2.4%）は、正しく、Leanで完全に証明され、各実行で定めた査読基準上の新規性も十分として採択されました。さらに1,388回は数学的には正しいものの進歩が限定的と査読者が判断し、格下げされました。提案または数学が却下された303回は失敗となりました。採択・格下げ・失敗の各実行は記録され、後続の実行に活用されます。再利用できる補題や定理は一般化して査読したうえでCausaleanに追加され、同じ問題を扱った後の採択成果では、集中不等式を再証明せずに利用しました。

研究者は、Mathlibに因果推論の内容がほとんどなかったため、Causaleanを構築しました。文献からよく使われる成果を選び、言語モデルの支援で整理・形式化し、各記述を人手で確認しました。後続の実行でも、言語モデルの査読を経て不足している古典的成果を追加できます。収録分野は因果グラフ、潜在結果、構造的因果モデル、推定、実験、パネルデータです。査読者は、項目が出典と一致し、再利用可能で、空虚な主張ではないことも確認します。プロジェクトページでは、論文の評価、文章へのコメント、個別の主張の認証ができ、自然言語の定義・定理と監査済みのLean版を比較できます。新規性審査とLean検証を通過した論文にはDOIと引用情報が付与されます。

研究者によると、2026年10月時点で作成された論文のうち、人手で確認したのは一部にとどまり、全体的な質はまだ分かっていません。現段階では、プロジェクトページの評価、認証、コメントが人による判断を集める主な手段です。今後の方向性として、より体系的な新規性指標と、言語モデルが新しい研究を行う能力を評価するベンチマークを挙げました。