Diffusion-Proof: 자기회귀적 생성(Auto-Regressive Generation)을 넘어선 형식적 정리 증명을 위한 레시피

최근 몇 년 동안 대규모 언어 모델(LLMs)의 형식적 수학 추론 능력을 향상시키는 것은 수학 및 컴퓨터 과학 커뮤니티 모두에서 핵심적인 초점이 되었습니다. 최첨단 자기회귀(Auto-Regressive, AR) LLM을 형식적 정리 증명에 사용하는 데 있어 상당한 진전이 있었지만, 이러한 모델들은 내재적인 한계를 겪고 있습니다. 이들의 다음 토큰 예측(next-token prediction) 생성 방식은 장기적 일관성(long-range coherence)의 어려움과 긴 시퀀스에 걸친 오류의 누적으로 인해 최적화되지 않은 성능을 낼 수 있습니다. 멀티 토큰 블록의 반복적인 디노이징(denoising)을 통해 텍스트를 생성하는 확산 LLM(diffusion LLMs, dLLMs)의 최근 발전은 유망한 대안을 제시합니다. 그러나 장기적 일관성을 유지하는 것이 매우 중요한 형식적 수학 분야에 dLLMs를 적용하는 것은 여전히 거의 연구되지 않은 상태로 남아 있습니다. 위의 과제들을 해결하기 위해, 우리는 우리가 아는 바로는 형식적 정리 증명을 위해 dLLMs를 훈련하고 적용하는 최초의 프레임워크인 Diffusion-Proof를 제안합니다. 우리의 프레임워크는 두 가지 모델에 대한 훈련 및 추론 방법을 포함합니다. 첫 번째는 장기적으로 일관된 전술(tactic) 사용을 통해 전체 증명 작성을 수행하는 dLLM-Prover-7B입니다. 두 번째는 새로운 대규모 블록 확산 기반 교정 모델인 dLLM-Corrector-7B입니다. 이는 dLLMs의 인필링(in-filling) 능력을 활용하여 양방향 정보를 사용하여 국소적 증명 교정을 수행합니다. 광범위한 실험을 통해 Diffusion-Proof가 동일한 데이터셋으로 훈련된 AR LLM 베이스라인을 상대적으로 상당히 능가함을 입증했습니다. Diffusion-Proof는 베이스라인과 비교하여 ProofNet-Test에서 1.61%, MiniF2F-Test 벤치마크에서 **6.14%**의 절대적인 성능 향상을 달성했습니다. 특히, Diffusion-Proof는 더 발전된 사고 모델인 DeepSeek-Prover-V2-7B가 해결하지 못한 IMO 문제 하나를 성공적으로 해결하여, 형식적 정리 증명에서 dLLMs의 독특한 이점을 보여주었습니다.