Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs

Motivation

• Known: LLM 기반 formal theorem proving은 SFT, RL, compiler 피드백 기반 self-correction, 대규모 파이프라인/agentic 시스템 등 다양한 방법론으로 발전해왔으며, compiler 피드백을 활용하면 성능이 향상된다는 것이 알려져 있다.
• Gap: 기존 접근법들은 compiler 신호를 binary 성공 지표나 단순 텍스트 오류 메시지로 단순화하여 사용하기 때문에, compiler 출력에 내재된 풍부한 구조적 정보를 활용하지 못하고 누적적인 다중 라운드 self-correction에 의존하게 되며, 이는 context window 확장과 탐색 깊이 제약이라는 확장성 병목을 초래한다.
• Why: state-of-the-art formal theorem proving 성능이 막대한 test-time compute(대규모 roll-out 또는 긴 context window)를 요구하는 확장성 문제를 안고 있어, 이를 해결하는 것은 실용적인 verifier-guided reasoning 시스템 구축에 핵심적이다.
• Approach: Lean compiler를 차원 압축기(dimension compressor)로 재해석하여, 실패 모드에 조건화된 국소적 오류 수정을 학습하는 learning-to-refine 프레임워크를 제안하고, 이를 supervised fine-tuning과 expert iteration으로 LLM에 내재화한 뒤 학습된 value 모델로 guided tree search를 수행한다.

Achievement

Figure 4. Visualization of random tree search strategy and value-guided tree search on problem Putnam-1971-b1 under Goed

1. PutnamBench SOTA: 공개적으로 보고된 ~8B 및 ~32B 파라미터 모델 중 비슷한 test-time budget 조건에서 PutnamBench 최고 성능을 달성함.
2. 모델 규모에 걸친 일관된 성능 향상: 다양한 크기의 base prover에 대해 추론 능력을 일관되게 증폭시킴을 실험적으로 검증함.
3. 효율적인 탐색 메커니즘 확립: Chain of Distributions(CoD) 개념을 통해 반복적 self-correction이 program space에서 어떻게 OOD 솔루션에 도달하는지 시각화하고, 학습된 검색 전략과 결합해 확장 가능한 패러다임을 제시함.

How

Figure 2. Refinement training data synthesis pipeline. Experiments

• Kimina-Prover-Preview-7B 등 기존 prover가 MiniF2F-test와 PutnamBench에서 생성한 증명들의 compiler 오류 메시지를 분석하여, 소수의 오류 유형이 대부분의 실패를 차지함을 실증함(Table 1).
• 문제 공간 P, 프로그램 공간 C, compiler 메시지 공간 M을 정의하고, verifier Φ: C→M을 many-to-one 매핑으로 formalize하여 동일 오류를 유발하는 프로그램 집합 Ψ(c)를 정의함.
• 정답 프로그램은 synthesis supervision, 오답 프로그램은 refinement supervision을 유도하는 통합 supervision operator S(c)를 설계함(failure-mode driven refinement).
• refinement 학습 데이터 합성 파이프라인(Figure 2)을 구축하고 SFT 및 expert iteration을 통해 생성·수정 능력을 하나의 정책으로 distill함.
• 학습된 neural value model을 이용해 test-time에서 random search 대비 value-guided tree search를 수행하여 탐색 효율을 높임(Figure 4).

Originality

• Lean compiler의 출력을 단순 오류 메시지가 아닌 정보이론적 압축 연산자(compression operator)로 재해석하여 formal theorem proving의 학습 및 탐색 문제를 재구성한 관점이 참신함.
• 프로그램 공간의 등가류(Ψ(c))에 기반한 failure-mode driven refinement라는 귀납적 편향을 명시적으로 정식화함.
• 반복적 self-correction을 Chain of Distributions(CoD)로 개념화하여 program space에서의 분포 변화 과정을 시각화한 점이 독특함.

Limitation & Further Study

• 발췌된 내용상 실험 세부사항(구체적 벤치마크 수치, ablation 결과)이 충분히 제시되지 않아 방법의 정량적 우수성 검증이 제한적임.
• compiler 메시지가 lossy하다는 점을 저자들도 인정하는데, 이로 인해 일부 미묘한 의미적 오류가 동일한 오류 signature로 뭉뚱그려질 위험이 있으며, 이것이 refinement 품질에 미치는 영향에 대한 심도 있는 분석이 부족해 보임.
• Lean 특화 접근이므로 다른 formal 언어(Coq, Isabelle 등)로의 일반화 가능성 검증이 후속 연구로 필요함.
• 대규모 파이프라인/agentic 시스템과의 직접 비교가 어렵다고 명시했는데, 이는 실제 실무 적용 시 상대적 위치를 판단하기 어렵게 함.

Evaluation

총평: Compiler 피드백을 정보압축 관점에서 재해석하여 효율적인 self-correction 학습을 가능케 한 참신하고 실용적인 기여로, formal theorem proving의 확장성 문제에 의미있는 해법을 제시한다.