비형식적인 정리 증명에서 통찰력을 활용하는 학습

Learning to Reason with Insight for Informal Theorem Proving

대부분의 자동 정리 증명 방법은 형식적인 증명 체계에 의존하지만, 비형식적인 정리 증명은 대규모 언어 모델(LLM)의 자연어 처리 능력을 더욱 효과적으로 활용할 수 있습니다. 본 연구에서는 비형식적인 정리 증명의 주요 난관이 통찰력 부족, 즉 복잡한 문제를 해결하는 데 필요한 핵심 기술을 인식하는 어려움에 있음을 밝힙니다. 이를 해결하기 위해, 우리는 이 필수적인 추론 능력을 키우고 LLM이 통찰력 있는 추론을 수행할 수 있도록 설계된 새로운 프레임워크를 제안합니다. 우리는 $ ext{DeepInsightTheorem}$이라는 계층적 데이터셋을 제안합니다. 이 데이터셋은 비형식적인 증명을 구성할 때, 최종 증명과 함께 핵심 기술과 증명 개요를 명시적으로 추출합니다. 이 데이터셋을 최대한 활용하기 위해, 우리는 인간의 학습 과정을 모방하는 점진적인 다단계 지도 학습(SFT) 전략을 설계하여 모델이 기본적인 증명 작성부터 통찰력 있는 사고까지 발전하도록 유도합니다. 어려운 수학적 벤치마크에 대한 실험 결과, 우리의 통찰력 기반 생성 전략이 기존 방법보다 훨씬 우수한 성능을 보임을 확인했습니다. 이러한 결과는 모델이 핵심 기술을 식별하고 적용하도록 교육하면 수학적 추론 능력을 크게 향상시킬 수 있음을 보여줍니다.

Although most of the automated theorem-proving approaches depend on formal proof systems, informal theorem proving can align better with large language models' (LLMs) strength in natural language processing. In this work, we identify a primary bottleneck in informal theorem proving as a lack of insight, namely the difficulty of recognizing the core techniques required to solve complex problems. To address this, we propose a novel framework designed to cultivate this essential reasoning skill and enable LLMs to perform insightful reasoning. We propose $\mathtt{DeepInsightTheorem}$, a hierarchical dataset that structures informal proofs by explicitly extracting core techniques and proof sketches alongside the final proof. To fully exploit this dataset, we design a Progressive Multi-Stage SFT strategy that mimics the human learning process, guiding the model from basic proof writing to insightful thinking. Our experiments on challenging mathematical benchmarks demonstrate that this insight-aware generation strategy significantly outperforms baselines. These results demonstrate that teaching models to identify and apply core techniques can substantially improve their mathematical reasoning.