LLM推論重要度 ★10
Diffusion-Proof: 定式化された定理証明のためのレシピ、自動回帰生成を超えて
Diffusion-Proof: Recipe for Formal Theorem Proving Beyond Auto-Regressive Generation
https://export.arxiv.org/api/query·2026/6/17
AI要約
自己回帰型LLMの定理証明における限界を克服するため、「Diffusion-Proof」という形式定理証明の新しいレシピを提案。長距離の整合性やエラー伝播の問題に対処する。
AI要点
- Diffusion-Proofは、形式定理証明のためのDiffusion LLM (dLLM) を用いた初のフレームワークである。
- dLLM-Prover-7Bは、長距離の整合性を保ちながらタクティクスを使用する全証明作成を行う。
- dLLM-Corrector-7Bは、双方向情報を用いた局所的な証明修正を可能にする。
- Diffusion-Proofは、AR LLMベースラインをProofNet-Testで1.61%、MiniF2F-Testで6.14%上回った。
- IMO問題の一つを、DeepSeek-Prover-V2-7Bでさえ解けなかった問題を解決し、dLLMの優位性を示した。
なぜ重要か
形式定理証明におけるLLMの性能向上は、数学的推論の自動化を加速させ、AIによる科学的発見の可能性を広げる。特に長距離の整合性が求められるタスクでdLLMが有効である可能性を示唆している。