Verso la Risoluzione di Problemi IMO Più Complessi Attraverso il Ragionamento e la Dimostrazione Disaccoppiati

Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Proving

July 7, 2025

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

cs.AI

Abstract

Il Teorema Automatico (ATP) nei linguaggi formali rappresenta una sfida fondamentale per l'IA. Sebbene i Modelli Linguistici di Grande Scala (LLMs) abbiano portato a progressi notevoli, rimane un divario significativo tra le loro potenti capacità di ragionamento informale e le loro deboli prestazioni nelle dimostrazioni formali. Studi recenti mostrano che l'accuratezza informale supera l'80%, mentre il successo formale rimane al di sotto dell'8% su benchmark come PutnamBench. Sosteniamo che questo divario persista perché i dimostratori all'avanguardia attuali, accoppiando strettamente ragionamento e dimostrazione, vengono addestrati con paradigmi che puniscono involontariamente il ragionamento profondo a favore di strategie superficiali basate su tattiche. Per colmare questo divario fondamentale, proponiamo un nuovo framework che separa il ragionamento di alto livello dalla generazione di dimostrazioni di basso livello. Il nostro approccio utilizza due modelli distinti e specializzati: un potente Ragionatore generico per generare lemmi subobiettivo strategici e diversificati, e un efficiente Dimostratore per verificarli rigorosamente. Questo design modulare libera il pieno potenziale di ragionamento del modello e aggira le insidie dell'addestramento end-to-end. Valutiamo il nostro metodo su un insieme impegnativo di problemi IMO post-2000, un set di problemi su cui nessun dimostratore open-source precedente ha riportato successo. Il nostro framework disaccoppiato risolve con successo 5 di questi problemi, dimostrando un passo significativo verso il ragionamento automatico su sfide matematiche eccezionalmente difficili. Per favorire la ricerca futura, rilasciamo il nostro dataset completo di lemmi generati e verificati per una vasta gamma di problemi IMO, disponibile all'indirizzo 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/ .