Hacia la Resolución de Problemas Más Desafiantes de la Olimpiada Internacional de Matemáticas mediante Razonamiento y Demostración Desacoplados

Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Proving

July 7, 2025

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

cs.AI

Resumen

La Demostración Automática de Teoremas (ATP, por sus siglas en inglés) en lenguajes formales representa un desafío fundamental para la IA. Aunque los Modelos de Lenguaje a Gran Escala (LLMs) han impulsado avances notables, persiste una brecha significativa entre sus potentes capacidades de razonamiento informal y su débil desempeño en demostraciones formales. Estudios recientes muestran que la precisión informal supera el 80%, mientras que el éxito formal se mantiene por debajo del 8% en benchmarks como PutnamBench. Sostenemos que esta brecha persiste porque los demostradores actuales de última generación, al acoplar estrechamente el razonamiento y la demostración, se entrenan con paradigmas que, sin querer, penalizan el razonamiento profundo en favor de estrategias superficiales basadas en tácticas. Para cerrar esta brecha fundamental, proponemos un marco novedoso que desacopla el razonamiento de alto nivel de la generación de pruebas de bajo nivel. Nuestro enfoque utiliza dos modelos especializados y distintos: un Razonador potente y de propósito general para generar lemas de subobjetivos diversos y estratégicos, y un Demostrador eficiente para verificarlos rigurosamente. Este diseño modular libera todo el potencial de razonamiento del modelo y evita los inconvenientes del entrenamiento de extremo a extremo. Evaluamos nuestro método en un conjunto desafiante de problemas de la Olimpiada Internacional de Matemáticas (IMO) posteriores al año 2000, un conjunto de problemas en el que ningún demostrador de código abierto previo ha reportado éxito. Nuestro marco desacoplado resuelve con éxito 5 de estos problemas, demostrando un avance significativo hacia el razonamiento automatizado en desafíos matemáticos excepcionalmente difíciles. Para fomentar investigaciones futuras, publicamos nuestro conjunto completo de datos de lemas generados y verificados para una amplia gama de problemas de la IMO, disponible en 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/ .