본 논문은 기존의 언어 모델 기반 정리 증명 방식의 한계를 극복하기 위해, 형식적인 증명 데이터뿐만 아니라 비형식적인 정보를 활용하는 새로운 프레임워크인 Lean-STaR을 제시합니다. Lean-STaR은 증명 과정의 각 단계 이전에 비형식적인 생각 과정(thoughts)을 생성하도록 언어 모델을 학습시켜 정리 증명 능력을 향상시킵니다. 역추적 기반의 정답 전략(tactics)을 이용해 합성적인 생각 과정 데이터를 생성하고, 학습된 모델은 추론 시 각 증명 단계에서 전략 예측 전에 생각 과정을 직접 생성합니다. Self-taught reasoner 프레임워크를 기반으로 전문가 반복(expert iteration)을 적용하여 Lean 솔버를 사용하여 검증하고 샘플링된 정답 증명에 대해 모델을 미세 조정합니다. 결과적으로 Lean-STaR은 Lean 정리 증명 환경의 miniF2F-test 벤치마크에서 최첨단 성능을 달성하여 기존 모델 대비 성능을 크게 향상시켰습니다 (Pass@64 기준 43.4% → 46.3%). 또한, 증강된 생각 과정이 정리 증명 과정의 다양한 측면에 미치는 영향을 분석하여 그 효과에 대한 통찰력을 제공합니다.
