DreamProver: 각성-수면 증명 에이전트를 활용한 전이 가능한 보조정리 라이브러리 진화

DreamProver: Evolving Transferable Lemma Libraries via a Wake-Sleep Theorem-Proving Agent

본 논문에서는 "각성-수면" 프로그램 유도 패러다임을 활용하여 형식적 증명에 사용될 수 있는 재사용 가능한 보조정리(lemma)를 발견하는 에이전트 기반 프레임워크인 DreamProver를 소개합니다. 기존 방식들은 고정된 보조정리 라이브러리에 의존하여 적응성이 제한되거나, 개별 정리에 특화된 매우 구체적인 중간 보조정리를 생성하여 일반성을 결여하는 경우가 많습니다. DreamProver는 이러한 한계를 극복하기 위해 반복적인 두 단계 프로세스를 사용합니다. 각성 단계에서는 DreamProver가 현재 보조정리 라이브러리를 사용하여 훈련 데이터 세트의 정리를 증명하는 동시에 새로운 후보 보조정리를 제안합니다. 수면 단계에서는 이러한 후보들을 추상화, 정제 및 통합하여 라이브러리를 압축하고 최적화합니다. 이러한 반복적인 과정을 통해 DreamProver는 점진적으로 고수준의 전이 가능한 보조정리 집합을 진화시키며, 이를 통해 관련 분야의 새로운 정리를 효과적으로 증명할 수 있습니다. 실험 결과는 DreamProver가 다양한 수학적 벤치마크에서 증명 성공률을 크게 향상시킬 뿐만 아니라, 보다 간결한 증명을 생성하고 계산 비용을 줄이는 것을 보여줍니다.

We introduce DreamProver, an agentic framework that leverages a "wake-sleep" program induction paradigm to discover reusable lemmas for formal theorem proving. Existing approaches either rely on fixed lemma libraries, which limit adaptability, or synthesize highly specific intermediate lemmas tailored to individual theorems, thereby lacking generality. DreamProver addresses this gap through an iterative two-stage process. In the wake stage, DreamProver attempts to prove theorems from a training set using the current lemma library while proposing new candidate lemmas. In the "sleep" stage, it abstracts, refines, and consolidates these candidates to compress and optimize the library. Through this alternating cycle, DreamProver progressively evolves a compact set of high-level, transferable lemmas that can be effectively used to prove unseen theorems in related domains. Experimental results demonstrate that DreamProver substantially improves proof success rates across a diverse set of mathematical benchmarks, while also producing more concise proofs and reducing computational cost.