Naar het oplossen van uitdagender IMO-problemen via ontkoppeld redeneren en bewijzen

Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Proving

July 7, 2025

Auteurs: Zhenwen Liang, Linfeng Song, Yang Li, Tao Yang, Feng Zhang, Haitao Mi, Dong Yu

cs.AI

Samenvatting

Geautomatiseerd Bewijsvoeren (ATP) in formele talen vormt een fundamentele uitdaging voor AI. Hoewel Large Language Models (LLM's) opmerkelijke vooruitgang hebben geboekt, blijft er een aanzienlijke kloof bestaan tussen hun krachtige informele redeneervaardigheden en hun zwakke prestaties in formele bewijsvoering. Recente studies tonen aan dat de informele nauwkeurigheid meer dan 80% bedraagt, terwijl het formele succes onder de 8% blijft op benchmarks zoals PutnamBench. Wij stellen dat deze kloof blijft bestaan omdat huidige state-of-the-art bewijsvoerders, door het nauw te koppelen van redeneren en bewijzen, worden getraind met paradigma's die onbedoeld diepgaand redeneren bestraffen ten gunste van oppervlakkige, tactiek-gebaseerde strategieën. Om deze fundamentele kloof te overbruggen, stellen we een nieuw raamwerk voor dat hoogwaardig redeneren ontkoppelt van laagniveau bewijsgeneratie. Onze aanpak maakt gebruik van twee afzonderlijke, gespecialiseerde modellen: een krachtige, algemene Reasoner om diverse, strategische subdoel-lemma's te genereren, en een efficiënte Prover om deze rigoureus te verifiëren. Dit modulaire ontwerp bevrijdt het volledige redeneerpotentieel van het model en omzeilt de valkuilen van end-to-end training. We evalueren onze methode op een uitdagende set van post-2000 IMO-problemen, een probleemset waarop geen eerdere open-source bewijsvoerder succes heeft gerapporteerd. Ons ontkoppelde raamwerk lost met succes 5 van deze problemen op, wat een significante stap vooruit betekent in de richting van geautomatiseerd redeneren op uitzonderlijk moeilijke wiskundige uitdagingen. Om toekomstig onderzoek te bevorderen, maken we onze volledige dataset van gegenereerde en geverifieerde lemma's voor een breed scala aan IMO-problemen beschikbaar, te vinden op 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/ .