🤖 AI

From LLM-Generated Conjectures to Lean Formalizations: Automated Polynomial Inequality Proving via Sum-of-Squares Certificates

Este artigo apresenta o NSPI, um framework neuro-simbólico que utiliza grandes modelos de linguagem para propor conjecturas aproximadas de Somas de Quadrados e computação simbólica para refiná-las em provas exatas verificadas por máquina no Lean, alcançando assim a prova automatizada escalável de desigualdades polinomiais com até 10 variáveis.

Autores originais: Ruobing Zuo, Hanrui Zhao, Gaolei He, Zhengfeng Yang, Jianlin Wang

Publicado 2026-05-18

📖 4 min de leitura☕ Leitura rápida

CC BY 4.0

Autores originais: Ruobing Zuo, Hanrui Zhao, Gaolei He, Zhengfeng Yang, Jianlin Wang

Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

Imagine que você está tentando provar que um bolo complexo, de várias camadas, é sempre "suficientemente doce" (matematicamente, não negativo), não importa como você o fatie ou altere os ingredientes. No mundo da matemática, isso é chamado de provar uma desigualdade polinomial.

Por muito tempo, os matemáticos tiveram duas maneiras principais de fazer isso, mas ambas apresentavam falhas graves:

O Método "Lógica Pura" (Simbólico): Isso é como tentar resolver o problema do bolo escrevendo cada reação química individual dos ingredientes em um quadro-negro. É perfeitamente preciso, mas se o bolo tiver muitos ingredientes (variáveis), o quadro-negro enche instantaneamente e o método falha. É lento demais e bagunçado para problemas grandes.
O Método "Adivinhação de IA" (LLMs): Isso é como pedir a um chef muito inteligente e criativo que adivinhe a receita. O chef é rápido e bom com bolos pequenos, mas quando o bolo fica enorme e complicado, o chef começa a alucinar ingredientes que não existem ou a cometer erros matemáticos. Eles não podem provar que sua resposta é 100% verdadeira.

Este artigo apresenta uma nova equipe chamada NSPI (Prova de Desigualdade Polinomial Neuro-Simbólica). Pense na NSPI como uma parceria perfeita entre um chef criativo e um inspetor de qualidade rigoroso.

Veja como sua "linha de montagem" funciona, passo a passo:

Passo 1: O Chef Criativo (O LLM)

Primeiro, a equipe pede a um Modelo de Linguagem Grande (o "Chef") que examine um problema matemático difícil. O Chef não tenta fazer a matemática difícil imediatamente. Em vez disso, usa sua criatividade para adivinhar uma estrutura.

A Analogia: Imagine que o Chef diz: "Aposto que este bolo é feito de três camadas específicas de cubos de açúcar empilhados juntos."
Em termos matemáticos, o LLM adivinha uma decomposição de Soma de Quadrados (SOS). Ele sugere: "Esta expressão complicada é provavelmente apenas a soma de algumas coisas mais simples elevadas ao quadrado."
Ponto Crucial: A adivinhação do Chef é geralmente uma aproximação. Está perto, mas pode ter pequenos erros decimais (como dizer que um cubo de açúcar pesa 1,0000001 gramas em vez de exatamente 1).

Passo 2: O Inspetor de Qualidade (Correção Simbólica)

A adivinhação do Chef é passada para o "Inspetor de Qualidade", que é um poderoso sistema de álgebra computacional.

A Analogia: O Inspetor pega o esboço grosseiro do Chef e usa um microscópio para corrigir os pequenos erros. Ele usa uma técnica chamada Método de Newton (uma maneira matemática de dar zoom na resposta exata) e Recuperação Racional (transformar decimais bagunçados em frações limpas e exatas).
Se o Chef adivinhou que as camadas eram "aproximadamente" 1,5, 2,3 e 0,7, o Inspetor calcula os números exatos: 3/2, 23/10 e 7/10.
Agora, a adivinhação foi transformada em um certificado matemático perfeito e exato.

Passo 3: O Juiz da Corte (Verificação Lean)

Finalmente, a equipe leva este certificado exato a um "Juiz" chamado Lean.

A Analogia: Lean é um juiz estrito, que não pisca, que verifica cada passo do trabalho do Inspetor. Ele não se importa com "sentimento" ou "adivinhação". Ele só aceita provas que são logicamente à prova de falhas.
Como o Inspetor forneceu um certificado exato, o Juiz pode verificar facilmente: "Sim, se você elevar esses números exatos ao quadrado e somá-los, você obtém o bolo original. E como quadrados são sempre positivos, o bolo é sempre doce."
O Juiz então emite uma prova verificada por máquina que tem 100% de garantia de estar correta.

Por que isso é um grande feito?

O artigo testou esta equipe em 522 problemas matemáticos muito difíceis, alguns com até 10 variáveis diferentes (ingredientes).

Os Antigos Métodos de Lógica desistiam quando os problemas ficavam grandes demais (muitos ingredientes).
Os Antigos Métodos de IA ficavam confusos e cometiam erros nos problemas grandes.
A Equipe NSPI teve sucesso onde outros falharam. Eles conseguiram resolver problemas com 10 variáveis que nenhum outro método conseguia tocar.

A Conclusão

O artigo afirma que, ao permitir que uma IA adivinhe a forma da solução e, em seguida, usar ferramentas matemáticas para corrigir os detalhes e um computador para verificar a verdade, eles construíram um sistema que pode resolver problemas complexos de desigualdade mais rápido e de forma mais confiável do que nunca. Eles não apenas adivinharam; construíram uma ponte de uma "boa adivinhação" para um "fato provado".

O que eles NÃO afirmaram:

Eles não disseram que isso curará doenças ou preverá o mercado de ações.
Eles não afirmaram que isso funciona para todo tipo de problema matemático, apenas para provar que certas expressões polinomiais são sempre positivas.
Eles não afirmaram que isso substitui totalmente os matemáticos humanos, mas sim automatiza um tipo muito específico e difícil de raciocínio.

Resumo Técnico: De Conjecturas Geradas por LLM para Formalizações em Lean

Declaração do Problema

A prova automatizada de desigualdades polinomiais é um desafio fundamental no raciocínio matemático, particularmente para casos de alta dimensão e multivariáveis. Abordagens existentes enfrentam limitações significativas de escalabilidade:

Métodos Puramente Simbólicos: Embora forneçam garantias robustas, métodos baseados em decomposição de Soma de Quadrados (SOS) e Programação Semidefinida (SDP) sofrem com explosão combinatória e crescimento rápido em expressões intermediárias à medida que o número de variáveis ou o grau aumenta. Frequentemente, falham em produzir provas estruturadas e legíveis por humanos.
Métodos Puramente Baseados em LLM: Grandes Modelos de Linguagem (LLMs) integrados a assistentes de prova (por exemplo, Lean, Isabelle) mostraram promessa, mas são limitados pela escassez de dados de treinamento formalizados de alta qualidade. Eles lutam com desigualdades algébricas complexas, particularmente aquelas que excedem 5 variáveis, e frequentemente carecem da capacidade de gerar certificados rigorosos e verificáveis por máquina.

O desafio central é fechar a lacuna entre a descoberta heurística e a verificação formal rigorosa, permitindo a prova automatizada de desigualdades polinomiais sem restrições em configurações de alta dimensão (até 10 variáveis) com correção verificada por máquina.

Metodologia: Framework NSPI

Os autores propõem o NSPI (Prova de Desigualdade Polinomial Baseada em SOS Neuro-Simbólica), um framework que integra as forças complementares de LLMs e computação simbólica em um pipeline de ponta a ponta. O processo consiste em três etapas principais:

1. Conjectura Neural (Geração de SOS Guiada por LLM)

Em vez de usar LLMs meramente para orientação de busca, o NSPI eleva-os a geradores primários de conjecturas.

Construção de Dados: Os autores constroem um conjunto de dados em grande escala de pares polinômio-SOS não negativos usando duas estratégias inovadoras:
- Orientada por Cálculo: Geração de matrizes de Gram via deslocamento espectral ou otimização LMI para garantir semidefinição positiva (PSD) com coeficientes controlados.
- Orientada por Estrutura: Exploração de estruturas algébricas como matrizes diagonalmente dominantes (dd) e diagonalmente dominantes escalonadas (sdd), que garantem propriedades PSD por design.
Treinamento: Um esquema de treinamento em duas etapas é empregado:
- Início Frio: Ajuste Fino Supervisionado (SFT) em mais de um milhão de pares sintéticos polinômio-SOS para estabelecer raciocínio estrutural fundamental.
- Aprendizado por Reforço Progressivo: Otimização de Política Relativa em Grupo (GRPO) baseada em currículo é aplicada a instâncias desafiadoras (aumentando contagens de variáveis de 3–5 para 9–10). A função de recompensa combina precisão (fidelidade numérica), adesão ao formato e penalidades de estrutura algébrica para garantir que o LLM gere estruturas SOS plausíveis.
Saída: O LLM propõe uma decomposição SOS aproximada (uma soma de termos quadrados) para um polinômio dado.

2. Correção Simbólica (Recuperação Racional Exata)

Para transformar a conjectura aproximada do LLM em uma prova rigorosa, um módulo de correção simbólica refina a saída:

Refinamento Gauss-Newton: A estrutura SOS aproximada é refinada usando métodos iterativos do tipo Newton para minimizar o erro reverso entre a soma de quadrados conjecturada e o polinômio alvo. Isso produz uma matriz de Gram numérica de alta precisão.
Recuperação Racional: A matriz numérica é convertida em uma matriz PSD racional exata. Dependendo de a solução estar no interior ou na fronteira do cone PSD, o sistema emprega projeção ortogonal ou fatoração LDL $^\top$ truncada combinada com aproximação diofantina simultânea. Esta etapa garante que o certificado SOS resultante seja exato e livre de erros de ponto flutuante.

3. Verificação Formal (Geração de Prova em Lean)

O certificado SOS racional exato é convertido automaticamente em uma prova Lean verificável por máquina.

Modelos de Prova: Modelos Lean predefinidos são preenchidos com os termos SOS exatos.
Verificação: O provador Lean verifica duas condições:
1. Igualdade: O polinômio alvo é igual à expressão SOS expandida (verificado via linear_combination).
2. Não Negatividade: A expressão SOS é não negativa (verificado via a tática positivity, que aplica recursivamente regras como $x^2 \ge 0$ ).

Contribuições Principais

Pipeline Neuro-Simbólico: A proposta do NSPI, um framework de ponta a ponta que automatiza a geração de provas formais completas para desigualdades polinomiais, encadeando conjectura neural, correção simbólica e verificação formal.
Ponte de Confiabilidade Principiada: Um método inovador para integrar geração heurística baseada em LLM com certificação exata simbólica. Isso transforma conjecturas neurais em provas verificáveis por máquina, permitindo escalabilidade para casos multivariáveis de alta dimensão (até 10 variáveis) sem depender de grandes quantidades de dados de treinamento formalizados pré-existentes.
Benchmark e Avaliação: A construção do PolyIneqBench, um benchmark desafiador contendo 522 problemas de desigualdade (3 a 10 variáveis), incluindo problemas de competições do mundo real e instâncias sintéticas de alta dimensão. Experimentos extensivos demonstram que o NSPI supera solvers simbólicos de última geração (Maple, Z3), provadores LLM puros (DeepSeek-Prover-V2, Goedel-Prover) e sistemas híbridos existentes (LIPS), particularmente em cenários de alta dimensão.

Resultados Experimentais

Desempenho: No PolyIneqBench, o NSPI alcançou uma taxa de aprovação de 11,7% para problemas de 10 variáveis, enquanto métodos simbólicos (Maple, Z3) e provadores LLM puros caíram para perto de 0% ou dígitos únicos.
Eficiência: O NSPI manteve o menor tempo médio de execução entre solvers bem-sucedidos, demonstrando um aumento de velocidade de mais de 10x em comparação com vários provadores baseados em LLM.
Escalabilidade: A estratégia de aprendizado por reforço progressivo deslocou com sucesso o limite de capacidade do modelo em direção a dimensões mais altas, com ganhos de desempenho observados à medida que o currículo avançava de 3–5 variáveis para 9–10 variáveis.
Ablação: Experimentos confirmaram que tanto o treinamento de início frio sintético quanto o GRPO baseado em currículo são críticos para o sucesso do sistema.

Significado e Alegações

O artigo afirma estabelecer um novo paradigma na prova de teoremas neuro-simbólica, onde LLMs funcionam como motores centrais de conjectura simbólica em vez de meros guias de busca. Ao tratar LLMs como geradores de priores simbólicos (estruturas SOS) e confiar na computação simbólica para precisão e na verificação formal para correção, a abordagem aborda o gargalo da escassez de dados dos métodos neurais puros e os limites de escalabilidade dos métodos simbólicos puros.

Os autores posicionam o NSPI como uma extensão significativa da fronteira para a prova automatizada de desigualdades polinomiais, lidando com sucesso com casos de alta dimensão (até 10 variáveis) que anteriormente eram intratáveis para sistemas automatizados existentes. O trabalho demonstra que combinar descoberta heurística com certificação rigorosa pode ampliar substancialmente o escopo prático do raciocínio matemático automatizado.