더 도전적인 IMO 문제 해결을 위한 분리된 추론 및 증명 접근법

초록

형식 언어에서의 자동 정리 증명(Automated Theorem Proving, ATP)은 AI의 근본적인 과제입니다. 대규모 언어 모델(Large Language Models, LLMs)이 놀라운 발전을 이끌었지만, 이들의 강력한 비형식적 추론 능력과 약한 형식적 증명 성능 사이에는 상당한 격차가 존재합니다. 최근 연구에 따르면, PutnamBench와 같은 벤치마크에서 비형식적 정확도는 80%를 초과하는 반면, 형식적 성공률은 8% 미만으로 나타났습니다. 우리는 이 격차가 현재 최첨단 증명기들이 추론과 증명을 긴밀하게 결합함으로써 깊은 추론을 억누르고 피상적이고 전략 기반의 접근 방식을 선호하는 훈련 패러다임을 사용하기 때문에 지속된다고 주장합니다. 이 근본적인 격차를 해소하기 위해, 우리는 고수준 추론과 저수준 증명 생성을 분리하는 새로운 프레임워크를 제안합니다. 우리의 접근 방식은 두 가지 별개의 특화된 모델을 활용합니다: 강력한 범용 추론기(Reasoner)가 다양한 전략적 보조 정리(lemma)를 생성하고, 효율적인 증명기(Prover)가 이를 엄격히 검증합니다. 이 모듈식 설계는 모델의 전체 추론 잠재력을 해방시키고 종단간(end-to-end) 훈련의 함정을 피할 수 있게 합니다. 우리는 이 방법을 2000년 이후의 국제 수학 올림피아드(IMO) 문제 세트에서 평가했으며, 이 문제 세트에서는 이전의 어떤 오픈소스 증명기도 성공을 보고한 바 없습니다. 우리의 분리된 프레임워크는 이 중 5개의 문제를 성공적으로 해결하며, 특히 어려운 수학적 도전 과제에 대한 자동화된 추론에 있어 중요한 진전을 보여줍니다. 향후 연구를 촉진하기 위해, 우리는 다양한 IMO 문제에 대해 생성되고 검증된 보조 정리의 전체 데이터셋을 공개하며, 이는 https://tencent-imo.github.io/에서 확인할 수 있습니다.

English

Automated Theorem Proving (ATP) in formal languages is a foundational challenge for AI. While Large Language Models (LLMs) have driven remarkable progress, a significant gap remains between their powerful informal reasoning capabilities and their weak formal proving performance. Recent studies show that the informal accuracy exceeds 80% while formal success remains below 8% on benchmarks like PutnamBench. We argue this gap persists because current state-of-the-art provers, by tightly coupling reasoning and proving, are trained with paradigms that inadvertently punish deep reasoning in favor of shallow, tactic-based strategies. To bridge this fundamental gap, we propose a novel framework that decouples high-level reasoning from low-level proof generation. Our approach utilizes two distinct, specialized models: a powerful, general-purpose Reasoner to generate diverse, strategic subgoal lemmas, and an efficient Prover to rigorously verify them. This modular design liberates the model's full reasoning potential and bypasses the pitfalls of end-to-end training. We evaluate our method on a challenging set of post-2000 IMO problems, a problem set on which no prior open-source prover has reported success. Our decoupled framework successfully solves 5 of these problems, demonstrating a significant step towards automated reasoning on exceptionally difficult mathematical challenges. To foster future research, we release our full dataset of generated and verified lemmas for a wide range of IMO problems, available at https://tencent-imo.github.io/ .

더 도전적인 IMO 문제 해결을 위한 분리된 추론 및 증명 접근법

Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Proving

초록

Support