Resolvendo Provas de Desigualdade com Modelos de Linguagem de Grande Escala

Resumo

A prova de desigualdades, crucial em diversos campos científicos e matemáticos, testa habilidades avançadas de raciocínio, como a descoberta de limites estreitos e a aplicação estratégica de teoremas. Isso a torna uma fronteira distinta e desafiadora para grandes modelos de linguagem (LLMs), oferecendo insights além da resolução geral de problemas matemáticos. O progresso nessa área é dificultado por conjuntos de dados existentes que frequentemente são escassos, sintéticos ou excessivamente formais. Abordamos isso propondo uma formulação de tarefa informal, mas verificável, transformando a prova de desigualdades em duas subtarefas automaticamente verificáveis: estimativa de limites e previsão de relações. Com base nisso, lançamos o IneqMath, um conjunto de dados curado por especialistas, contendo desigualdades de nível olímpico, incluindo um conjunto de teste e um corpus de treinamento enriquecido com soluções passo a passo e anotações de teoremas. Também desenvolvemos uma estrutura de avaliação inovadora usando LLM-como-juiz, combinando um juiz de resposta final com quatro juízes passo a passo projetados para detectar falhas comuns de raciocínio. Uma avaliação sistemática de 29 LLMs líderes no IneqMath revela uma realidade surpreendente: mesmo modelos de ponta como o o1 alcançam menos de 10% de precisão geral sob escrutínio passo a passo; isso representa uma queda de até 65,5% em relação à sua precisão considerando apenas a equivalência da resposta final. Essa discrepância expõe cadeias dedutivas frágeis e uma lacuna crítica para os LLMs atuais entre simplesmente encontrar uma resposta e construir uma prova rigorosa. Aumentar o tamanho do modelo e a computação no momento do teste gera ganhos limitados na correção geral da prova. Em vez disso, nossas descobertas destacam direções de pesquisa promissoras, como raciocínio guiado por teoremas e autorrefinamento. Código e dados estão disponíveis em https://ineqmath.github.io/.

English

Inequality proving, crucial across diverse scientific and mathematical fields, tests advanced reasoning skills such as discovering tight bounds and strategic theorem application. This makes it a distinct, demanding frontier for large language models (LLMs), offering insights beyond general mathematical problem-solving. Progress in this area is hampered by existing datasets that are often scarce, synthetic, or rigidly formal. We address this by proposing an informal yet verifiable task formulation, recasting inequality proving into two automatically checkable subtasks: bound estimation and relation prediction. Building on this, we release IneqMath, an expert-curated dataset of Olympiad-level inequalities, including a test set and training corpus enriched with step-wise solutions and theorem annotations. We also develop a novel LLM-as-judge evaluation framework, combining a final-answer judge with four step-wise judges designed to detect common reasoning flaws. A systematic evaluation of 29 leading LLMs on IneqMath reveals a surprising reality: even top models like o1 achieve less than 10% overall accuracy under step-wise scrutiny; this is a drop of up to 65.5% from their accuracy considering only final answer equivalence. This discrepancy exposes fragile deductive chains and a critical gap for current LLMs between merely finding an answer and constructing a rigorous proof. Scaling model size and increasing test-time computation yield limited gains in overall proof correctness. Instead, our findings highlight promising research directions such as theorem-guided reasoning and self-refinement. Code and data are available at https://ineqmath.github.io/.

Resolvendo Provas de Desigualdade com Modelos de Linguagem de Grande Escala

Solving Inequality Proofs with Large Language Models

Resumo

Support