ChatPaper.aiChatPaper

Auf dem Weg zur Lösung anspruchsvollerer IMO-Probleme durch entkoppeltes Denken und Beweisen

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

Das automatisierte Theorembeweisen (Automated Theorem Proving, ATP) in formalen Sprachen stellt eine grundlegende Herausforderung für die KI dar. Während große Sprachmodelle (Large Language Models, LLMs) bemerkenswerte Fortschritte erzielt haben, besteht nach wie vor eine erhebliche Lücke zwischen ihren leistungsstarken Fähigkeiten im informellen Schließen und ihrer schwachen Leistung beim formalen Beweisen. Aktuelle Studien zeigen, dass die informelle Genauigkeit 80 % übersteigt, während der formale Erfolg auf Benchmarks wie PutnamBench unter 8 % bleibt. Wir argumentieren, dass diese Lücke bestehen bleibt, weil aktuelle State-of-the-Art-Beweiser durch die enge Kopplung von Schließen und Beweisen mit Paradigmen trainiert werden, die unbeabsichtigt tiefes Schließen zugunsten oberflächlicher, taktikbasierter Strategien bestrafen. Um diese grundlegende Lücke zu überbrücken, schlagen wir ein neuartiges Framework vor, das hochrangiges Schließen von der Erzeugung niedrigrangiger Beweise entkoppelt. Unser Ansatz nutzt zwei spezialisierte Modelle: einen leistungsstarken, allgemeinen Schließer (Reasoner), um vielfältige, strategische Subziel-Lemmata zu generieren, und einen effizienten Beweiser (Prover), um diese rigoros zu verifizieren. Dieser modulare Ansatz befreit das volle Schließpotenzial des Modells und umgeht die Fallstricke des End-to-End-Trainings. Wir evaluieren unsere Methode anhand eines anspruchsvollen Satzes von IMO-Problemen ab dem Jahr 2000, einem Problembereich, bei dem bisher kein Open-Source-Beweiser Erfolge gemeldet hat. Unser entkoppeltes Framework löst erfolgreich 5 dieser Probleme und zeigt damit einen bedeutenden Schritt in Richtung automatisierten Schließens bei außergewöhnlich schwierigen mathematischen Herausforderungen. Um zukünftige Forschung zu fördern, veröffentlichen wir unseren vollständigen Datensatz generierter und verifizierter Lemmata für eine Vielzahl von IMO-Problemen, verfügbar unter 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/ .
PDF131July 10, 2025