Vers la résolution de problèmes plus complexes des Olympiades Internationales de Mathématiques grâce au raisonnement découplé et à la preuve

Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Proving

July 7, 2025

papers.authors: Zhenwen Liang, Linfeng Song, Yang Li, Tao Yang, Feng Zhang, Haitao Mi, Dong Yu

cs.AI

papers.abstract

La démonstration automatique de théorèmes (ATP) dans les langages formels constitue un défi fondamental pour l'intelligence artificielle. Bien que les modèles de langage à grande échelle (LLMs) aient permis des avancées remarquables, un écart significatif persiste entre leurs puissantes capacités de raisonnement informel et leurs faibles performances en démonstration formelle. Des études récentes montrent que la précision informelle dépasse 80 %, tandis que le taux de succès formel reste inférieur à 8 % sur des benchmarks comme PutnamBench. Nous soutenons que cet écart persiste parce que les prouveurs actuels, en couplant étroitement raisonnement et démonstration, sont entraînés selon des paradigmes qui pénalisent involontairement le raisonnement approfondi au profit de stratégies superficielles basées sur des tactiques. Pour combler cet écart fondamental, nous proposons un cadre novateur qui découple le raisonnement de haut niveau de la génération de preuves de bas niveau. Notre approche utilise deux modèles distincts et spécialisés : un Raisonneur polyvalent et puissant pour générer des lemmes de sous-objectifs stratégiques et diversifiés, et un Prouveur efficace pour les vérifier rigoureusement. Cette conception modulaire libère le potentiel de raisonnement complet du modèle et évite les écueils de l'apprentissage de bout en bout. Nous évaluons notre méthode sur un ensemble difficile de problèmes post-2000 des Olympiades internationales de mathématiques (IMO), un ensemble de problèmes sur lequel aucun prouveur open-source n'a rapporté de succès auparavant. Notre cadre découplé résout avec succès 5 de ces problèmes, démontrant une avancée significative vers le raisonnement automatisé sur des défis mathématiques exceptionnellement difficiles. Pour encourager les recherches futures, nous publions notre ensemble complet de données de lemmes générés et vérifiés pour une large gamme de problèmes IMO, disponible à l'adresse 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/ .