Diffusion-Proof：基於擴散大模型的形式化定理證明新範式

本文針對自回歸大型語言模型在形式化數學推理中存在的長程連貫性差及誤差累積問題，提出了首個基於擴散大型語言模型（dLLM）的形式化定理證明框架Diffusion-Proof。該框架包含兩個核心模型：dLLM-Prover-7B，專注於利用長程連貫性進行整體證明策略的生成；以及dLLM-Corrector-7B，這是一種新穎的大塊擴散修正模型，利用雙向資訊實現局部證明的精準修正。實驗表明，Diffusion-Proof在相同資料集訓練下顯著優於自回歸基線模型，在ProofNet-Test和MiniF2F-Test基準上分別實現了1.61%和6.14%的絕對性能提升。值得注意的，該框架成功解決了一道DeepSeek-Prover-V2-7B未能解決的IMO（國際數學奧林匹亞）題目，充分展示了擴散模型在形式化證明領域的獨特優勢與潛力。