🤖 AI

ALPS: Measuring Valid Creativity in Large Language Models with Mathematical Construction

O artigo apresenta o ALPS, um novo benchmark que mede rigorosamente a criatividade válida em grandes modelos de linguagem ao desafiá-los a gerar provas ou construções matemáticas originais e verificáveis para leis equacionais geradas aleatoriamente, revelando que os modelos atuais enfrentam dificuldades significativas com o lado da construção e que a maioria das instâncias permanece sem solução mesmo por provadores automatizados avançados.

Autores originais: Eric Xie, Wenqian Ye, Aidong Zhang

Publicado 2026-08-18

📖 5 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Eric Xie, Wenqian Ye, Aidong Zhang

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

No cenário científico moderno, a inteligência artificial começou a sair do papel de processadora de dados para assumir o papel de descobridora. Estamos vendo máquinas que podem propor novos compostos químicos, sugerir novos materiais e até formular conjecturas matemáticas que os humanos ainda não consideraram. Essa mudança levanta uma questão profunda: quando uma máquina produz uma resposta que parece um avanço, como sabemos se ela é verdadeiramente criativa e não apenas uma repetição astuta de algo que ela memorizou durante seu treinamento? A verdadeira criatividade na ciência exige duas coisas: a solução deve ser original, significando que não foi vista antes, e deve ser eficaz, significando que realmente funciona e resolve o problema em questão. A dificuldade reside em verificar essas qualidades. Em muitos campos, julgar se uma nova ideia é válida requer que especialistas humanos analisem o resultado e decidam se ele é bom, um processo que é lento e subjetivo. Na matemática, onde as respostas podem ser verificadas com absoluta certeza, o desafio é diferente: os problemas são frequentemente tão complexos que um computador não pode simplesmente percorrer todas as possibilidades para encontrar a resposta, e os próprios problemas são frequentemente conjuntos fixos que a máquina já pode ter estudado.

Para resolver esse dilema, pesquisadores da Universidade da Virgínia desenvolveram uma nova maneira de testar a inteligência artificial, um benchmark que chamam de ALPS. Este sistema é projetado para medir a "criatividade válida" ao apresentar à máquina um tipo específico de enigma matemático que não pode ser resolvido por memória ou seguindo uma rotina padrão. Os enigmas baseiam-se em regras sobre como um conjunto de itens pode ser combinado. Imagine uma coleção de objetos e uma regra para misturar quaisquer dois deles. Os pesquisadores geram uma regra específica, ou lei, que descreve como esses objetos devem se comportar. A tarefa da máquina é decidir uma de duas coisas: ou a regra é tão restritiva que força todos os objetos a serem idênticos, ou a regra permite uma estrutura complexa e infinita de objetos que satisfaça a condição. Se a máquina alegar que a estrutura existe, ela deve construir uma descrição dela. Se alegar que os objetos devem ser idênticos, deve provar que nenhuma outra possibilidade existe. A genialidade dessa configuração é que as respostas podem ser verificadas por um computador com perfeição, sem que nenhum humano precise olhar o resultado. Além disso, o sistema pode gerar um suprimento infinito desses enigmas, garantindo que a máquina esteja sempre enfrentando um problema que nunca viu antes.

Os pesquisadores testaram este sistema usando uma variedade de ferramentas poderosas de raciocínio automatizado, que são programas de computador especializados projetados para resolver problemas lógicos. Eles rodaram essas ferramentas contra um conjunto de mais de quatro mil dessas leis geradas. Os resultados foram drásticos. Mesmo com um aumento massivo de poder computacional, as ferramentas automatizadas conseguiram resolver apenas uma fração minúscula dos problemas. Especificamente, um portfólio de oito configurações diferentes dos melhores provadores disponíveis conseguiu resolver apenas cerca de dois por cento das leis. Quando os pesquisadores aumentaram o orçamento computacional em vinte vezes, encontraram apenas um punhado de soluções adicionais, e nenhuma delas eram as estruturas complexas que procuravam; eram apenas provas de que os objetos tinham que ser idênticos. Isso sugere que a barreira para resolver esses problemas não é a falta de poder computacional, mas a falta de um método para inventar as estruturas específicas e personalizadas que cada lei única exige. A máquina simplesmente não sabe como construir o tipo certo de estrutura infinita do zero.

Os pesquisadores então voltaram-se para os grandes modelos de linguagem, o tipo de inteligência artificial que alimenta muitas das ferramentas conversacionais usadas hoje. Eles testaram os modelos de raciocínio mais fortes disponíveis, dando-lhes os mesmos enigmas e a mesma chance de provar suas respostas. No lado da tarefa onde a máquina tinha que provar que todos os objetos eram idênticos, o melhor modelo teve sucesso em cerca de quatorze por cento dos casos, mas apenas nos problemas mais simples. No lado onde a máquina tinha que construir uma nova estrutura infinita, os resultados foram ainda mais reveladores: nenhum dos modelos teve sucesso. Quando os modelos tentavam construir uma estrutura, eles falhavam consistentemente de duas maneiras: ou propunam uma estrutura muito rígida, colapsando todos os objetos em um único ponto e, assim, falhando em mostrar uma solução complexa, ou propunham uma estrutura muito frouxa, falhando em seguir as regras da lei que tentavam satisfazer. Em todos os casos, a máquina não conseguia equilibrar a necessidade de seguir as regras com a necessidade de criar algo novo e complexo.

O estudo conclui que, embora esses sistemas de inteligência artificial estejam ficando melhores em seguir instruções e verificar seu próprio trabalho, eles ainda lutam com o ato central da descoberta científica: inventar uma nova estrutura que se ajuste a um conjunto de restrições. Os pesquisadores liberaram todo o seu sistema, incluindo o gerador que cria os enigmas e o juiz automatizado que verifica as respostas, para o público. Isso permite que outros cientistas continuem testando e melhorando esses modelos sem ficarem sem problemas inéditos. As descobertas sugerem que o caminho a seguir para a IA na ciência pode não ser dar às máquinas mais dados ou mais tempo, mas sim ensiná-las a propor e refinar suas próprias ideias em um ciclo de criação e verificação. Até que as máquinas possam construir de forma confiável essas soluções personalizadas, seu papel na descoberta científica permanecerá limitado, incapaz de atravessar o abismo entre o processamento de informações e a geração de conhecimento verdadeiramente válido e original.

Resumo Técnico: ALPS – Medindo a Criatividade Válida em Grandes Modelos de Linguagem com Construção Matemática

1. Declaração do Problema

As avaliações atuais de Grandes Modelos de Linguagem (LLMs) em domínios científicos (ex: demonstração de teoremas, design de moléculas) lutam para distinguir entre criatividade válida e mera memorização ou execução rotineira. Uma solução é considerada "validamente criativa" apenas se satisfizer dois critérios conjuntos:

Originalidade: A solução não é uma repetição de dados de treinamento ou de um procedimento geral conhecido.
Efetividade: A solução é objetivamente correta e fornece valor para a tarefa específica.

Os benchmarks existentes falham em medir essa combinação de forma confiável porque carecem de pelo menos uma das três propriedades necessárias:

Verificabilidade: As soluções devem ser objetivamente verificáveis (não sujeitas a julgamento subjetivo).
Renovabilidade: Novas instâncias de problemas devem ser geráveis sem limite para evitar a contaminação por dados de treinamento.
Construtividade: A tarefa deve exigir uma solução adaptada à instância específica, impedindo soluções via memória ou algoritmos padrão.

Corpora estáticos (ex: MATH, miniF2F) falham na renovabilidade; puzzles sintéticos (ex: SAT aleatório) frequentemente falham na construtividade, pois podem ser resolvidos por procedimentos conhecidos; e tarefas de descoberta aberta (ex: design de moléculas) frequentemente falham na verificabilidade devido ao julgamento humano subjetivo.

2. Metodologia: O Benchmark ALPS

Os autores introduzem o ALPS (Austin-Law Proof-Synthesis), um benchmark projetado para cumprir todas essas três propriedades simultaneamente dentro do domínio da teoria equacional.

Formulação do Problema:

Domínio: O ALPS opera sobre magmas (conjuntos com uma operação binária única $\diamond$ ) e leis equacionais (identidades universalmente quantificadas).
Tarefa: Cada instância é uma lei $L$ da forma $x = T[x, y, z, \dots]$ , onde $T$ é um termo de ordem cinco ou superior.
A Dicotomia: Para qualquer lei desse tipo, exatamente uma de duas condições ocorre:
1. Trivial: A lei implica $x = y$ , colapsando cada modelo a um único elemento.
2. Austin: A lei possui um modelo não trivial, que deve ser necessariamente infinito (já que todos os modelos finitos não triviais são descartados pelo processo de certificação do benchmark).
O Desafio: O solver deve fornecer uma prova dedutiva de que $L \models x=y$ (lado Trivial) ou construir um magma infinito que satisfaça $L$ (lado Austin).

Construção do Corpus:

Geração: O corpus é expandido via um mecanismo de extensão. Partindo de leis Austin conhecidas, as variáveis no termo $T$ são recursivamente substituídas por novas operações (ex: $v \to v \diamond w$ ). Isso garante que problemas novos e inéditos possam ser gerados indefinidamente.
Triagem e Admissibilidade: Os candidatos passam por um rigoroso pipeline de triagem:
1. Filtro de Modelo Finito: Descarta leis com modelos finitos não triviais.
2. Provedor de Admissibilidade: Utiliza provedores automatizados para certificar que nenhum modelo finito não trivial existe. Isso baseia-se em uma consequência lógica da finitude: em um suporte finito, um mapa injetivo é sobrejetivo. O provedor tenta derivar uma contradição da lei e da sobrejetividade de um subterm, certificando que qualquer modelo deve ser infinito.
3. Deduplicação: Leis equivalentes (mutuamente implicantes) são agrupadas em classes de equivalência para garantir contagens distintas de problemas.
Pool Resultante: A partir de uma geração inicial de candidatos, os autores produziram um pool de 4.141 leis não resolvidas (o "nível difícil") e um conjunto menor de leis "certificadas-fáceis".

Verificação de Resposta (O Juiz Automatizado):
O juiz verifica as submissões através de dois canais distintos e totalmente automatizados, sem envolvimento humano:

Lado Trivial: O LLM submete uma cadeia de igualdades. Um harness realiza a formalização automática para uma prova em Lean (verificada pelo kernel do Lean) para verificar que $L \implies \forall a, b: a=b$ .
Lado da Construção: O LLM submete um conjunto finito de equações $E$ $E$ (uma apresentação). O juiz verifica duas afirmações usando provedores de teoremas automatizados (ex: Vampire, E, Twee):
- Derivação: $E \vdash L$ (Todo modelo de $E$ satisfaz $L$ ).
- Satisfatibilidade: $E \cup \{a \neq b\}$ é satisfatível (Existe um modelo de $E$ com pelo menos dois elementos distintos).
- Se ambos ocorrerem, o certificado de admissibilidade da instância garante que o modelo é infinito.

3. Principais Contribuições

Uma Tarefa de Construção de Dois Lados: Um benchmark onde cada instância é certificada para ter uma resposta determinada (ou trivial ou infinita), isolando a necessidade de construção criativa.
Corpus Renovável & Gerador: Um gerador público que cria instâncias novas sem limite, garantindo que a avaliação nunca seja contaminada pelos dados de treinamento.
Juiz Automatizado: Um sistema que certifica submissões via canais independentes (Lean para trivialidade, certificados de provedores automatizados para construção) sem juízes humanos.
Baseline Automatizada Forte: Um portfólio de oito configurações de oito provedores líderes (Vampire, E, Twee) que estabelece o limite "limitado pelo método" da automação atual.

4. Resultados Experimentais

Performance dos Provedores Automatizados:

Um portfólio de oito configurações resolveu apenas 2,2% do pool de avaliação de 4.141 leis.
Aumentar o orçamento de computação em um fator de 20 adicionou apenas 0,6% mais leis resolvidas (todas provas de trivialidade, nenhum novo modelo).
97,2% do pool permanece não resolvido por qualquer configuração testada, indicando que o obstáculo é a ausência de métodos para construir estruturas infinitas customizadas, não a falta de computação.
Descoberta Lateral: Os autores resolveram uma lei de ordem 5 anteriormente deixada em aberto pelo Equational Theories Project (ETP), confirmando a existência de um modelo infinito via saturação.

Performance dos LLMs:

Lado Trivial: Em um conjunto de 63 leis "certificadas-fáceis", o modelo mais forte testado (o3) alcançou uma taxa de aprovação de 14% (9 soluções) com waypoints (lemmas derivados de provedores) e 9,5% sem eles. O GPT-4.1 e o o4-mini alcançaram 0%.
- Modo de Falha: Os LLMs falharam principalmente ao submeter cadeias contendo passos inválidos (passos não deriváveis da lei), que o harness rejeitou.
Lado da Construção: Em uma amostra de 25 leis do "nível difícil" (não resolvidas pela automação), nenhum LLM produziu uma solução verificada.
- Modo de Falha: As submissões foram ou fortes demais (implicavam a lei, mas colapsavam para um único elemento, falhando no teste de distinção) ou fracas demais (permitiam elementos distintos, mas falhavam em implicar a lei).
- O o3 superou exatamente um dos dois testes em todas as 25 leis. O o4-mini e o GPT-4.1 falharam em ambos os testes em muitas leis.

5. Significância e Alegações

O artigo afirma que o ALPS isola com sucesso a criatividade válida ao remover os confundidores de memorização e execução rotineira.

Necessidade de Criatividade: A alta taxa de falha tanto de provedores automatizados quanto de LLMs no "nível difícil" demonstra que esses problemas não podem ser resolvidos por procedimentos gerais existentes ou busca de força bruta.
Natureza da Falha: Os perfis de falha específicos (passos inválidos em provas triviais; apresentações "fortes demais/fracas demais" na construção) destacam que os modelos atuais têm dificuldade com a geração criativa sob restrições. Eles conseguem frequentemente esboçar uma estrutura, mas falham em equilibrar especificações globais sem colapsar em soluções degeneradas.
Paralelo Científico: O artigo traça um paralelo com o ciclo "especificar–construir–verificar" na descoberta científica (ex: design de moléculas), observando que o ALPS torna cada fase verificável por máquina.
Direção Futura: Os autores sugerem que o caminho a seguir reside em loops de verificar-e-refinar (semelhantes à Síntese Indutiva Guiada por Contraexemplos, CEGIS), onde os solvers esboçam estruturas, recebem feedback automatizado sobre a validade e revisam as mesmas.

Os autores mantêm-se modestos, observando que, embora os LLMs mais fortes mostrem alguma capacidade em instâncias fáceis, eles atualmente falham em construir estruturas infinitas válidas em instâncias difíceis, e o benchmark permanece amplamente não resolvido pela tecnologia atual.