Phase-guided Corrective Sampling for Automated Theorem Proving = 단계-유도 보정 샘플링을 통한 자동 정리 증명

다국어 초록 (Multilingual Abstract)

Large language models (LLMs) have recently advanced the automation of theorem
proving, demonstrating that linguistic reasoning can be coupled with symbolic
proof synthesis. However, current LLM-based theorem provers remain limited by
unstructured reasoning and the inability to recover from failed proof attempts.
Their inference pipelines typically predict the next tactic directly from the current
proof state, lacking an explicit notion of plan or self-correction.
We introduce Phase-Guided Corrective Sampling (PCS), a structured
inference framework designed to improve the robustness of LLM-driven proof gen
eration. PCS decomposes theorem proving into three coordinated operators: Phase
(strategic planning), PhaseTac (tactic generation), and Correct (error recovery).
By explicitly separating global reasoning from local execution and embedding cor
rection as a learnable stage, PCS transforms flat sampling into a hierarchical
“plan–act–repair” process that yields more interpretable proof trajectories.
To train these operators, we construct three aligned datasets—ProofPhase,
PhaseTac, and PhaseError. Fine-tuning the InternLM-Math-Base-7B model
jointly across these datasets enables the model to perform PCS. Evaluated on
the MiniF2F benchmark, the resulting PCS model attains a pass rate of 37.7%,
outperforming prior Lean-STaR baselines.
The proposed framework suggests a new paradigm for neural theorem proving:
incorporating structured reasoning and corrective feedback as core components can
enhance the LLM’s automated theorem proving performance.

국문 초록 (Abstract)

대규모 언어 모델(LLM)은 최근 형식 정리 증명의 자동화를 크게 발전시키며, 언어적
추론이 기호적 증명과 성공적으로 결합 될 수 있음을 입증했다. 그러나 기존의 LLM
기반 정리 증명기는 비구조적 추론 및 증명 실패 시 복구 능력의 부재로 인해 여전히 한
계를 노출하고 있다. 이들의 추론 파이프라인은 현재 증명 상태로부터 다음 전술만을
직접 예측하는 방식으로, 명시적인 계획이나 자기교정 개념이 결여되어있다. 본 논문
은 LLM기반 증명 생성의 견고성(Robustness)을 향상시키기 위해 설계된 구조화된
추론 프레임워크인 단계-유도보정샘플링(Phase-Guided Corrective Sampling,
PCS)을 제안한다. PCS는 정리 증명 과정을 세 가지 협력적 연산자로 분해한다 : 전
략적 계획을 담당하는 Phase, 이에 기반한 전술을 생성하는 PhaseTac, 그리고 오류를
복구하는 Correct. PCS는 전역적 추론을 국소적 실행으로부터 명시적으로 분리하고,
보정(Correction)을 학습 가능한 단계로 내재화함으로써, 기존의 평면적 샘플링을 보
다 해석 가능한 증명 궤적을 산출하는 계층적 “계획-실행-복구”과정으로 변모시킨다.
이러한 연산자들을효과적으로학습시키기위해,저자는ProofPhase, PhaseTac,
그리고 PhaseError라는 세 가지 정렬된 데이터셋을 구축하고, 이 데이터셋을 활용하
여 InternLM-Math-Base-7B 모델을 미세 조정(Fine-tuning)하여 PCS를 수행할
수 있도록 했다. MiniF2F 벤치마크에 대한 평가 결과, 제안된 PCS모델은 37.7%의
성공률(Pass Rate)을 달성하여, 기존 Lean-STaR 기준 모델들의 성능을 능가했다. 본
프레임워크는 신경망 기반 정리 증명에 새로운 패러다임을 제시하며, 구조화된 추론
및 교정 피드백을 핵심 구성요소로 통합하는것이 LLM의 자동 정리 증명성능을
향상시킬 수 있음을 시사한다.

목차 (Table of Contents)

• 1 Introduction 1
• 1.1 Background and Motivation 1
• 1.2 Challenges in Neural Theorem Proving 2
• 1.3 Key Idea : Phase-Guided Corrective Sampling 3
• 1.4 Contributions 3
• 1.5 Organization of the Thesis 4
• 2 Related Work 5
• 2.1 Neural Theorem Proving Foundations 5
• 2.2 Subgoal-Based and Decomposition Approaches 5
• 2.3 Thought-Augmented and Rationale-Driven Proving 6
• 2.4 Retrieval, Agentic, and Search-Augmented Frameworks 6
• 2.5 Mathematics-Specific Language Models and Corpora 7
• 3 Phase-guided Corrective Sampling 8
• 3.1 Phase Declaration 9
• 3.2 Phase-Level Tactic Generation 11
• 3.3 Error Correction 13
• 4 Data Generation for Phase-guided Corrective Sampling 16
• 4.1 Proof Phase Dataset Generation 18
• 4.2 Error Sampling 19
• 4.3 Phase Error Dataset Generation 20
• 5 Experiments and Analysis 22
• 5.1 Finetuning Setup 22
• 5.2 Evaluation Results 23
• 5.3 Analysis 25
• 6 Conclusion 27
• The bibliography 29
• Abstract(in Korean) 33