자기 대국(Self-Play) 정리 증명 알고리즘을 위한 이론적 프레임워크

모델이 스스로 개선될 수 있도록 하는 훈련 알고리즘의 일종인 자기 대국 (Self-play)은 최근 대규모 언어 모델 (LLMs)을 이용한 형식적 정리 증명 (formal theorem proving) 맥락에서 유망한 경험적 결과를 보여주었습니다. (Dong & Ma, 2025)는 두 개의 협력하는 에이전트, 즉 정리를 증명하는 증명기 (prover)와 증명기에게 커리큘럼으로서 새로운 정리를 생성하는 추측기 (conjecturer)를 통해 자기 대국을 구체화합니다. 본 논문에서 우리는 정리 증명을 위한 자기 대국 알고리즘의 자기 개선 (self-improvement) 능력을 이해하기 위한 이론적 프레임워크를 제공합니다. 첫째, 우리는 정리의 집합을 노드를 정리로, 유사한 의미론적 관계를 가진 정리 쌍 사이의 에지를 갖는 그래프로 정식화합니다. 우리는 훈련된 증명기의 보장을 특징짓는 일련의 기본 가정 (primitive assumptions)과 추측기가 그래프의 구조에 어떻게 접근할 수 있는지를 소개합니다. 둘째, 정리의 기저 그래프가 잘 연결되어 있다면, 추측 알고리즘이 가역적 랜덤 워크 (reversible random walk)에 기반하는 증명기-추측기 시스템은 증명된 정리의 집합을 기하급수적으로 성장시키기에 충분함을 보여줍니다. 셋째, 추측기가 인위적으로 복잡하고 근본적이지 않은 정리를 생성하는 경향이 있는 자기 대국 알고리즘의 경험적 문제에서 영감을 얻어, 우리는 추측기에 의해 생성된 정리의 훈련 분포에 대한 다양성 측정치 (diversity measure)와, 정리 그래프 내 인접한 정리들 사이의 확산 유사도 (diffusion similarity)를 계산함으로써 이 다양성 측정치를 국소적으로 최대화하는 개선된 추측 알고리즘을 제안합니다. 마지막으로, 우리는 대조 학습 (contrastive learning)을 사용하여 노드를 유클리드 공간 (Euclidean space)에 임베딩한 다음 임베딩 간의 내적 (inner-product)을 계산함으로써 확산 유사도를 계산하는 방법을 설명합니다.