Imagine que você está tentando resolver um problema matemático complexo, mas em vez de pedir a um gênio brilhante, porém às vezes excessivamente confiante, você está pedindo a um bibliotecário muito organizado, levemente rígido, mas incrivelmente honesto.

Essa é a ideia central por trás do AXIOM, um novo sistema projetado para realizar o raciocínio matemático com uma mentalidade de "confiança em primeiro lugar". Veja como ele funciona, dividido em conceitos e analogias simples.

O Problema: O Gênio "Confidentemente Errado"

Os modelos de IA atuais (como os com os quais você conversa) são como estudantes brilhantes que adoram adivinhar. Se eles não sabem a resposta, podem simplesmente inventar uma e apresentá-la com total confiança. Na matemática, isso é perigoso porque uma resposta errada parece exatamente igual a uma certa para o usuário. Você não tem como saber se a IA está mentindo ou apenas alucinando.

A Solução AXIOM: A "Linha de Montagem Especializada"

O AXIOM não tenta ser um gênio que resolve tudo do zero. Em vez disso, ele atua como uma fábrica altamente eficiente com quatro regras estritas:

1. O Classificador (O Roteador Regex)

Quando uma pergunta chega, ela não vai direto para a IA. Primeiro, ela atinge um Classificador. Pense nisso como um funcionário da sala de correspondência que olha para o formato do envelope.

Se a carta parece uma nota de "aritmética simples", ela é enviada para a Via Rápida.
Se parece uma nota de "álgebra", ela vai para a Estação de Álgebra.
Se o formato não corresponde a nenhuma categoria conhecida, o funcionário carimba imediatamente como "Desconhecido" e para. Ele não adivinha.

2. O Tradutor (A IA como um "Reescritor")

Se a carta passa para uma estação, o sistema não pede para a IA resolver o problema. Em vez disso, a IA atua como um Tradutor.

Jeito Antigo: "Aqui está um problema de lógica, por favor resolva-o." (A IA adivinha os passos).
Jeito AXIOM: "Aqui está um problema de lógica. Por favor, reescreva-o neste formato específico e restrito que nosso calculador entende."
A IA está estritamente proibida de fazer a matemática em si. Ela apenas limpa a frase para que a próxima etapa possa lê-la perfeitamente.

3. O Calculador (O Mecanismo Determinístico)

Uma vez que a IA reescreve o problema, ela o passa para um Calculador (um sistema de álgebra computacional). Este é um robô que nunca adivinha, nunca se cansa e nunca alucina.

Ele pega o problema reescrito e processa os números.
Se ele conseguir resolver o problema, ele fornece a resposta.
Se ele não conseguir resolver (talvez a matemática seja estranha demais ou a entrada esteja ligeiramente incorreta), ele para e diz: "Não posso verificar isso."

4. A Regra da "Honestidade" (Abstenção)

Esta é a parte mais importante. Na maioria dos sistemas, se o calculador falha, o sistema pode tentar adivinhar de qualquer maneira. No AXIOM, dizer "eu não sei" é uma resposta válida e estruturada.
Se qualquer parte da linha falhar (o Classificador não reconheceu o formato, o Tradutor não conseguiu reescrever ou o Calculador não conseguiu resolver), o sistema exibe uma mensagem clara: "Estou me abstendo." Ele nunca dá uma resposta errada e confiante.

Os Resultados: Velocidade e Segurança

O artigo relata estatísticas impressionantes ao testar este sistema:

Zero Erros Confiantes: Em milhares de testes, o sistema nunca deu uma resposta errada que parecesse uma certa. Se ele deu uma resposta, ela foi verificada.
Alta Precisão: Em testes matemáticos padrão, ele acertou cerca de 94% das questões.
Velocidade: Para matemática simples (como "2 + 2"), ele pula todo o tradutor de IA e resolve em 1 milissegundo (mais rápido do que você pode piscar). Para coisas mais difíceis, ainda é mais rápido do que pedir para uma IA padrão "pensar passo a passo".
Custo: Como não pede para a IA escrever longos ensaios ou adivinhar, custa quase nada para rodar.

O "Dinâmica de Avanço": Melhorando Sem Quebrar

Os autores enfatizam que este sistema foi projetado para crescer.

Imagine que o sistema encontra um novo tipo de problema matemático que não conhece. Em vez de falhar silenciosamente ou adivinhar, ele registra: "Eu vi este formato, mas não tenho uma estação para ele."
Os desenvolvedores podem então construir uma nova "Estação" (uma nova regra) especificamente para esse formato.
Como cada estação é isolada, adicionar uma nova nunca quebra as antigas. É como adicionar uma nova faixa a uma rodovia; isso não causa congestionamentos nas faixas existentes.

Resumo da Analogia

Pense em uma IA padrão como um mágico que tira respostas de dentro de um chapéu. Às vezes o coelho está lá; às vezes é uma meia, mas o mágico age como se fosse um coelho.

O AXIOM é um inspetor de controle de qualidade.

Ele verifica se o item cabe na caixa.
Ele rotula o item claramente.
Ele o passa por uma máquina que o mede.
Se a máquina não consegue medi-lo, ele coloca uma etiqueta de "Rejeitado".

Ele pode rejeitar mais itens do que um mágico rejeitaria, mas cada item que sai da fábrica com uma etiqueta de "Aprovado" é garantido como correto.

Resumo Técnico: AXIOM – Uma Arquitetura de Execução Neuro-Simbólica Baseada em Confiança (Trust-First)

1. Problema

O artigo aborda a falta fundamental de verificabilidade no raciocínio matemático de modelos de linguagem de grande escala (LLMs) de fronteira. Embora os LLMs alcancem alta precisão em benchmarks, eles operam através de uma interface "prompt-em-texto-saída", onde uma resposta errada e confiante é estruturalmente indistinguível de uma correta. As alternativas existentes apresentam trade-offs significativos:

Provadores baseados em Lean exigem que os problemas sejam pré-formalizados em uma sintaxe específica (ex: Lean), criando um gargalo para consultas em linguagem natural.
Sistemas especialistas fechados (ex: Wolfram Alpha) oferecem backends simbólicos, mas carecem de aumento por LLM na fronteira de entrada e não fornecem traços de derivação inspecionáveis.

Os autores argumentam que o "confiante-errado" é o pior modo de falha no raciocínio matemático. Eles propõem mudar o objetivo de design de "precisão-primeiro" para "confiança-primeiro", definindo confiança como $1 - \frac{\text{errado}}{\text{tentado}}$ , onde "errado" exclui registros dos quais o sistema explicitamente se abstém de responder.

2. Metodologia: A Arquitetura AXIOM

AXIOM é uma arquitetura de execução neuro-simbólica onde o LLM funciona estritamente como um canonicalizador, não como um solucionador. O sistema roteia a entrada de linguagem natural (NL) através de um pipeline determinístico de Sistema de Álgebra Computacional (CAS). O design central baseia-se em quatro compromissos:

2.1 Alinhamento de Roteamento de Tarefa 1:1:1

Em vez de um LLM monolítico ou um manipulador genérico, o AXIOM emprega um invariante 1:1:1:

Gatilho (Trigger): Um regex de forma de problema que seleciona exatamente uma tarefa.
Prompt: Um prompt específico de esquema com exemplos de poucos disparos (few-shot) adaptados para aquela forma específica.
Manipulador (Handler): Um manipulador de CAS determinístico que consome apenas aquele esquema específico.

Este alinhamento garante que a adição de uma nova tarefa ( $T_{N+1}$ ) não cause regressão nas tarefas existentes ( $T_1 \dots T_N$ ), pois seus caminhos de código são disjuntos. Isso evita a competição de "orçamento representacional" encontrada em modelos monolíticos.

2.2 Abstenção como uma Saída de Primeira Classe

O sistema trata answer=null como uma saída estrutural e válida, não como uma falha. Três canais independentes podem disparar uma abstenção:

Falha de Roteamento (Router Miss): Nenhum gatilho de regex corresponde à entrada.
Abstenção do Tradutor (Translator Abstain): O LLM retorna explicitamente unknown (ensinado via exemplos de poucos disparos) quando não consegue reescrever a entrada no esquema sem adivinhar.
Abstenção do Manipulador (Handler Abstain): O pipeline de CAS não consegue derivar uma resposta verificada (ex: ao encontrar um predicado não reconhecido ou um ConditionSet).

Crucialmente, o sistema impõe uma guarda de lista branca (whitelist guard): se um manipulador encontrar um predicado não reconhecido, ele deve se abster em vez de assumir um valor padrão (ex: zero), prevenindo saídas "confiante-errado".

2.3 Framework de Cadeia de Tarefas Compostas (Composed-Task Chain)

Para problemas de múltiplos passos (ex: funções por partes que exigem parsing, resolução por ramo e agregação), o AXIOM utiliza um framework de ComposedTask. Ele encadeia operadores determinísticos (funções puras) onde o LLM é chamado apenas uma vez no início (InitialExtractor). A cadeia valida dependências no momento do registro, garantindo que a falha em qualquer etapa resulte em uma abstenção limpa em vez de um erro silencioso.

2.4 Caminho de Apenas Regras (Rule-Only Path)

Para aritmética pura de forma fechada (dígitos e operadores sem prosa), o passo do LLM é totalmente ignorado. O sistema roteia diretamente para um avaliador CAS determinístico. Este caminho garante equivalência de bits entre as execuções e custo zero de inferência.

3. Principais Contribuições

O artigo enfatiza a dinâmica forward da arquitetura em vez de uma figura de precisão estática. As principais contribuições são:

Framework Arquitetural: Um sistema de roteamento 1:1:1 com um bypass de apenas regras e uma cadeia de tarefas compostas para lógica de múltiplos passos.
Disciplina Operacional: Um conjunto de princípios para sistemas neuro-simbólicos confiáveis, incluindo:
- Agrupamento por template matemático (Math-template bucketing): Roteamento baseado na estrutura do solucionador, não na fraseologia superficial.
- Escaneamento LOST_CORRECT: Um oráculo de regressão pré-commit que reproduz benchmarks arquivados para garantir que novas tarefas não quebrem as existentes.
- Predicado-não-reconhecido = Abster-se: Uma defesa estrutural contra saídas "confiante-errado".
- Onboarding focado em parseabilidade: Otimizar a taxa de entradas analisáveis antes de otimizar a confiança em novos domínios.
Retornos Lineares-Aditivos: Ao contrário dos LLMs monolíticos que exibem retornos logarítmicos (ganhos de precisão decrescentes), a cobertura do AXIOM cresce linearmente com o número de tarefas registradas, pois as tarefas não suprimem umas às outras.

4. Resultados Empíricos

A arquitetura foi avaliada no benchmark MATH (4 categorias), na suíte aritmética lm-eval-harness e em uma implantação de produção pública (~30.000 consultas).

Benchmark MATH (4 Categorias):
- Corretude Cumulativa: 94,36% (2.592/2.747).
- Confiança sobre Analisável (Trust on Parseable): 100,00% em todos os quatro domínios (Álgebra, Teoria dos Números, Contagem e Probabilidade, Pré-Cálculo). Houve zero respostas erradas confiantes.
- Latência: Mediana de 446 ms para tarefas dependentes de LLM; 1 ms para tarefas de apenas regra.
lm-eval-harness Arithmetic:
- Corretude: 100,0% (20.000/20.000).
- Custo: Zero chamadas de API de LLM; 21,6s de tempo de parede (wall time) em CPU comum.
Implantação em Produção:
- Atendeu ~30.000 consultas com zero incidentes de "confiante-errado" na fronteira da API.
- Separação de Latência: Diferença de ~400x entre o caminho de apenas regra (1 ms) e o de dependência de LLM (446 ms).
Comparação com LLM Puro (Qwen 2.5 7B CoT):
- O AXIOM superou significativamente a linha de base de CoT puro em precisão em domínios mais difíceis (ex: +38,2 pp em Pré-Cálculo), enquanto emitiu 0 respostas erradas comparado a centenas do baseline de CoT.
- O AXIOM foi ~24x a ~40x mais rápido em média devido ao prompting estreito e à ausência de loops de raciocínio iterativo.

5. Significância e Alegações

O artigo afirma que o AXIOM estabelece uma garantia de confiança em tempo de execução (runtime trust guarantee) indisponível para LLMs monolíticos ou provadores pré-formalizados. A significância não reside em atingir um escore de precisão específico, mas na dinâmica forward que ele permite:

Melhoria Monotônica: Cada abstenção registrada em produção é um candidato para uma resposta correta no próximo ciclo de entrega (ship cycle). O sistema é projetado para converter abstenções em respostas corretas via criação de tarefas direcionadas sem regredir o desempenho existente.
Verificabilidade: A confiança é uma propriedade arquitetural derivada do caminho de verificação (CAS determinístico), não uma propriedade do modelo subjacente.
Escalabilidade: A arquitetura suporta a adição incremental de milhares de triplas de tarefas (mais de 3.100 enviadas) com zero regressões de lost_correct ao longo de mais de 250 commits.

Os autores reconhecem limitações, incluindo um teto para problemas de geometria travados em visão (devido à falta de integração de visão) e problemas de linguagem natural irreduzíveis, mas os enquadram como os próximos pontos de inflexão para o registro, em vez de paredes assintóticas. A principal contribuição é o framework que permite que o "abster-se de hoje" se torne o "correto de amanhã" através de um processo de engenharia disciplinado e verificável.

AXIOM: A Trust-First Neuro-Symbolic Execution Architecture for Verifiable Mathematical Reasoning