К решению более сложных задач ММО через раздельное рассуждение и доказательство

Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Proving

July 7, 2025

Авторы: Zhenwen Liang, Linfeng Song, Yang Li, Tao Yang, Feng Zhang, Haitao Mi, Dong Yu

cs.AI

Аннотация

Автоматизированное доказательство теорем (ATP) в формальных языках представляет собой фундаментальную задачу для ИИ. Хотя крупные языковые модели (LLM) привели к значительному прогрессу, сохраняется существенный разрыв между их мощными возможностями неформального рассуждения и слабыми результатами в формальном доказательстве. Последние исследования показывают, что точность в неформальных задачах превышает 80%, в то время как успешность в формальных задачах остается ниже 8% на тестах, таких как PutnamBench. Мы утверждаем, что этот разрыв сохраняется, потому что современные системы доказательства, тесно связывая рассуждение и доказательство, обучаются с использованием парадигм, которые непреднамеренно наказывают глубокое рассуждение в пользу поверхностных, тактически-ориентированных стратегий. Чтобы преодолеть этот фундаментальный разрыв, мы предлагаем новую структуру, которая разделяет высокоуровневое рассуждение и низкоуровневую генерацию доказательств. Наш подход использует две специализированные модели: мощную, универсальную модель для генерации разнообразных стратегических лемм-подцелей и эффективную модель для их строгой проверки. Этот модульный подход раскрывает полный потенциал рассуждения модели и избегает недостатков сквозного обучения. Мы оцениваем наш метод на сложном наборе задач Международной математической олимпиады (IMO) после 2000 года, на котором ни одна из существующих открытых систем доказательства не сообщала об успехах. Наша разделенная структура успешно решает 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/ .