Rumo à Resolução de Problemas Mais Desafiadores da Olimpíada Internacional de Matemática por meio de Raciocínio e Prova 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

Resumo

A Prova Automática de Teoremas (ATP) em linguagens formais é um desafio fundamental para a IA. Embora os Modelos de Linguagem de Grande Escala (LLMs) tenham impulsionado avanços notáveis, ainda existe uma lacuna significativa entre suas poderosas capacidades de raciocínio informal e seu fraco desempenho em provas formais. Estudos recentes mostram que a precisão informal excede 80%, enquanto o sucesso formal permanece abaixo de 8% em benchmarks como o PutnamBench. Argumentamos que essa lacuna persiste porque os provadores atuais de última geração, ao acoplarem fortemente o raciocínio e a prova, são treinados com paradigmas que inadvertidamente punem o raciocínio profundo em favor de estratégias superficiais baseadas em táticas. Para superar essa lacuna fundamental, propomos uma nova estrutura que desacopla o raciocínio de alto nível da geração de provas de baixo nível. Nossa abordagem utiliza dois modelos distintos e especializados: um Reasoner poderoso e de propósito geral para gerar lemas de subobjetivos estratégicos e diversos, e um Prover eficiente para verificá-los rigorosamente. Esse design modular libera todo o potencial de raciocínio do modelo e contorna as armadilhas do treinamento de ponta a ponta. Avaliamos nosso método em um conjunto desafiador de problemas da Olimpíada Internacional de Matemática (IMO) pós-2000, um conjunto de problemas no qual nenhum provador de código aberto anterior relatou sucesso. Nossa estrutura desacoplada resolve com sucesso 5 desses problemas, demonstrando um passo significativo em direção ao raciocínio automatizado em desafios matemáticos excepcionalmente difíceis. Para promover pesquisas futuras, disponibilizamos nosso conjunto completo de dados de lemas gerados e verificados para uma ampla gama de problemas da IMO, disponível em 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/ .