🤖 machine learning

Evaluating the Architectural Reasoning Capabilities of LLM Provers via the Obfuscated Natural Number Game

Este artigo apresenta o Jogo dos Números Naturais Ofuscado como um benchmark para avaliar o "Raciocínio Arquitetural"—a capacidade de sintetizar provas usando apenas axiomas locais sem pistas semânticas—e demonstra que, embora modelos de linguagem grandes gerais sofram degradação de desempenho sob ofuscação, modelos de raciocínio especializados mantêm sua precisão, distinguindo assim o raciocínio lógico genuíno do reconhecimento de padrões.

Autores originais: Lixing Li

Publicado 2026-05-04

📖 4 min de leitura☕ Leitura rápida

CC0 1.0

Autores originais: Lixing Li

Artigo original dedicado ao domínio público sob CC0 1.0 (http://creativecommons.org/publicdomain/zero/1.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á ensinando um aluno a resolver um quebra-cabeça de matemática. Geralmente, o quebra-cabeça vem com rótulos úteis como "Adição", "Multiplicação" ou "Sucessor". Um aluno inteligente pode não entender realmente as regras do jogo; ele pode apenas reconhecer a palavra "Adição" e recordar um truque memorizado que já viu antes.

Este artigo faz uma pergunta difícil: Esses modelos de IA estão realmente fazendo matemática, ou são apenas bons em reconhecer palavras?

Para descobrir, os pesquisadores criaram uma versão "vendada" de um famoso jogo de matemática chamado Natural Number Game. Aqui está como eles fizeram isso e o que descobriram, explicado de forma simples:

O Experimento: O Jogo "Alienígena"

Os pesquisadores pegaram um jogo de matemática padrão onde cada regra e número tem um nome claro (como add ou zero). Em seguida, aplicaram um "embaralhador" nele. Eles substituíram cada nome significativo por strings aleatórias e sem sentido, como x9z, q22 e b7a.

O Jogo Original: Você vê add e sabe que significa adição.
O Jogo Embaralhado (NNG Ofuscado): Você vê x9z e não faz ideia do que significa. Você não pode adivinhar; precisa observar a lógica de como as peças se encaixam para descobrir o que x9z faz.

Isso testa algo que os autores chamam de "Raciocínio Arquitetural". É a capacidade de construir uma solução usando apenas os projetos estruturais (a lógica), ignorando os sinais úteis nas portas (os nomes).

Os Resultados: A "Taxa de Latência"

Os pesquisadores testaram vários modelos de IA de ponta tanto no jogo original quanto no jogo embaralhado. Eles encontraram duas coisas principais:

1. A "Taxa de Latência Universal" (Todos ficam mais lentos)
Quando os nomes foram embaralhados, cada modelo de IA levou mais tempo para resolver os problemas.

Analogia: Imagine que você está dirigindo para uma cafeteria familiar. Você conhece os sinais, os nomes das ruas e os pontos de referência. Agora, imagine que alguém pintou sobre todos os sinais e renomeou as ruas com letras aleatórias. Você ainda sabe como dirigir, mas precisa parar, olhar o mapa e pensar mais em cada curva. Você chega eventualmente, mas leva muito mais tempo.
A Descoberta: Os modelos de IA tiveram que fazer essa "reconstrução de mapa mental" para cada problema. Eles não podiam apenas confiar na memória; precisavam processar a lógica bruta, o que lhes custou tempo.

2. A Divisão "Raciocínio vs. Decoreba"
Embora todos ficassem mais lentos, a precisão dos modelos dividiu-se em dois grupos distintos:

Os Modelos "Genéricos" (por exemplo, GPT-4o, Claude): Esses modelos são como alunos que são ótimos em memorizar flashcards. Quando os nomes foram embaralhados, eles ficaram confusos. Sua taxa de sucesso caiu significativamente.
- O que isso significa: Eles estavam dependendo dos "sinais" (os nomes) para resolver o quebra-cabeça. Quando os sinais desapareceram, eles não conseguiram encontrar o caminho.
Os Modelos de "Raciocínio" (por exemplo, DeepSeek-R1, GPT-5, DeepSeek-Prover-V2): Esses modelos são como alunos que realmente entendem as regras do jogo. Mesmo quando os nomes foram embaralhados, sua taxa de sucesso permaneceu exatamente a mesma.
- O que isso significa: Eles não precisavam dos rótulos. Eles olharam para a estrutura lógica (a "arquitetura") e descobriram a solução tão bem quanto antes.

A Conclusão

O artigo conclui que há uma diferença real entre a IA que apenas combina padrões (como reconhecer a palavra "add") e a IA que pode realmente raciocinar através de estruturas lógicas.

Modelos genéricos são como turistas que precisam de um guia com nomes nele. Se você tirar o guia, eles se perdem.
Modelos de raciocínio são como arquitetos que conseguem ler as plantas baixas. Mesmo que o prédio não tenha sinais, eles ainda conseguem descobrir como as paredes e vigas se encaixam.

O estudo prova que, embora todos os modelos de IA fiquem "mais lentos" quando forçados a pensar sem rótulos, apenas os verdadeiros modelos de "raciocínio" conseguem manter sua precisão alta nesse ambiente "alienígena". Isso sugere que, para a IA descobrir nova matemática no futuro (onde ainda não existem nomes ou rótulos), precisamos desses modelos focados em raciocínio, e não apenas daqueles que são bons em combinar padrões.

1. Declaração do Problema

Apesar do sucesso dos Modelos de Linguagem de Grande Escala (LLMs) em benchmarks de matemática formal como MiniF2F e PutnamBench, uma ambiguidade crítica permanece: esses modelos possuem capacidades de raciocínio lógico genuíno ou estão meramente realizando correspondência de padrões semânticos contra seus dados de pré-treinamento?

A Lacuna: Os benchmarks atuais frequentemente dependem da recuperação de bibliotecas (por exemplo, Mathlib), onde o sucesso depende do reconhecimento de lemas de alto nível e identificadores semânticos (por exemplo, add, succ). Isso falha em testar a capacidade de um modelo de sintetizar provas em domínios matemáticos "alienígenas" onde não existem bibliotecas externas ou pistas semânticas familiares.
A Necessidade: Para alcançar a descoberta automatizada de teoremas, a IA deve demonstrar Raciocínio Arquitetural: a capacidade de sintetizar provas formais usando apenas axiomas locais, definições e lógica estrutural, independentemente do significado semântico ou de repositórios externos.

2. Metodologia

Os autores introduzem o Jogo dos Números Naturais Ofuscado (O-NNG), um benchmark de conhecimento zero projetado para isolar o raciocínio estrutural da recuperação lexical.

A. O Algoritmo de Ofuscação

A inovação central é a remoção sistemática de pistas semânticas do Jogo dos Números Naturais (NNG) no Lean 4:

Nível de Ruído ( $\lambda$ ): Definido no intervalo $[0, 1]$ $[0, 1]$ .
- $\lambda = 0$ : NNG original (identificadores semânticos intactos).
- $\lambda = 1.0$ : Randomização completa dos identificadores.
Mecanismo de Perturbação: Uma relação exponencial $P = \lambda^{2.5}$ $P = λ^{2.5}$ determina a probabilidade de perturbações em nível de caractere.
- Substituição: Substitui caracteres por candidatos válidos de Unicode/ASCII.
- Inserção: Injeta novos caracteres (probabilidade $0.4P$ ).
- Deleção: Remove caracteres (probabilidade $0.3P$ ), garantindo que os identificadores permaneçam não vazios.
Objetivo: Este processo transforma o conjunto de dados em um "ambiente fechado" onde os identificadores (por exemplo, axiomas, teoremas, táticas) são strings aleatórias, forçando o modelo a depender exclusivamente da estrutura lógica dos axiomas de Peano.

B. Configuração Experimental

Conjunto de Dados: 68 problemas formais do NNG, organizados em 8 módulos (Adição, Multiplicação, etc.).
Modelos Avaliados: Cinco modelos de última geração via API:
- Modelos de Raciocínio: DeepSeek-R1, GPT-5, DeepSeek-Prover-V2.
- Modelos Gerais: GPT-4o, Claude-Sonnet-4.5.
Pipeline:
1. Análise Sintática: Extração do NNG com ordenação estrita de dependências.
2. Ofuscação: Aplicação de perturbações em nível de caractere baseadas em $\lambda$ .
3. Geração de Consulta: Construção de prompts contendo axiomas "alienígenas", teoremas-alvo e táticas disponíveis.
4. Inferência: Os modelos produzem um JSON com um plano em linguagem natural ("Rascunho") e código Lean 4 ("Código").
5. Verificação: Validação automatizada usando o compilador Lean 4 (v4.27.0) para verificar erros de sintaxe e lógica.
Métricas:
- Taxa de Correção (%): Razão de teoremas provados com sucesso.
- Tempo Médio (s): Latência de inferência.

3. Contribuições Principais

Definição de Raciocínio Arquitetural: Formalizado como a capacidade de sintetizar provas usando exclusivamente definições e axiomas locais dentro de uma teoria fechada, excluindo bibliotecas externas e táticas automatizadas de alto nível (como linarith).
O Benchmark O-NNG: Um novo framework de avaliação de conhecimento zero que quantifica a "Lacuna Semântico-Raciocinante" medindo a degradação de desempenho quando os identificadores semânticos são removidos.
Quantificação do "Imposto de Latência": Estabeleceu que navegar em domínios alienígenas impõe um custo computacional universal (aumento do tempo de inferência) a todos os modelos, independentemente da arquitetura.

4. Resultados e Análise

O estudo revela uma divergência aguda no comportamento dos modelos quando as pistas semânticas são removidas:

Imposto de Latência Universal:
- Todos os modelos exibiram um aumento estatisticamente significativo no tempo de inferência à medida que $\lambda$ aumentava.
- Implicação: A remoção de identificadores semânticos força os modelos a realizar buscas internas mais intensas ou reconstrução lógica, independentemente de sua capacidade base.
Divergência na Robustez (Precisão):
- Modelos de Raciocínio (DeepSeek-R1, GPT-5, DeepSeek-Prover-V2): Mantiveram precisão estável em todos os níveis de ruído ( $\lambda \in [0, 1]$ $λ \in [0, 1]$ ). A queda no desempenho não foi estatisticamente significativa.
  - Conclusão: Esses modelos dependem da lógica estrutural e podem navegar pelos axiomas de Peano sem âncoras semânticas.
- Modelos Gerais (GPT-4o, Claude-Sonnet-4.5): Sofreram uma queda estatisticamente significativa nas taxas de sucesso à medida que $\lambda$ $λ$ aumentava.
  - Conclusão: Seu desempenho em tarefas formais padrão depende fortemente da correspondência de padrões semânticos e da familiaridade com convenções de nomenclatura, em vez de síntese lógica pura.
Significância Estatística: A ANOVA de uma via confirmou que a queda no desempenho para modelos gerais e o aumento de latência para todos os modelos foram estatisticamente significativos ( $p < 0.05$ ).

5. Significado e Implicações

Avaliação do Verdadeiro Raciocínio: O O-NNG fornece uma métrica rigorosa para distinguir entre modelos que "conhecem" matemática via correspondência de padrões e aqueles que podem "raciocinar" via lógica estrutural.
Direção Arquitetural: Os resultados sugerem que, para o futuro da descoberta automatizada de teoremas (IA4Math), arquiteturas focadas em raciocínio (como DeepSeek-R1 e GPT-5) são superiores aos modelos de propósito geral, pois são robustas à ausência de priores semânticos.
O "Vale da Estranheza do Raciocínio": Os dados sugerem uma relação não linear onde ruído parcial pode ser mais prejudicial do que ofuscação total, indicando que pistas semânticas residuais podem atuar como heurísticas distrativas.
Agentes de IA Futuros: As descobertas defendem o desenvolvimento de "Agentes Semânticos Fundamentados em Conhecimento" capazes de operar em domínios com ontologias incompletas ou obscurecidas, um pré-requisito para a descoberta de novos teoremas matemáticos.

Em resumo, o artigo demonstra que, embora os LLMs atuais possam resolver problemas conhecidos via correspondência de padrões, apenas arquiteturas específicas de "raciocínio" possuem o Raciocínio Arquitetural necessário para resolver problemas em ambientes lógicos totalmente desconhecidos e ofuscados.