🤖 AI

Theoria: Rewrite-Acceptability Verification over Informal Reasoning States

O artigo apresenta o Theoria, uma arquitetura de verificação que aumenta a confiabilidade das respostas de IA ao reescrever soluções em transições de estado tipadas e auditáveis com justificativas explícitas, superando, assim, juízes de LLM holísticos na detecção de premissas ocultas e citações fabricadas, ao mesmo tempo em que mantém alta precisão em problemas de nível especialista.

Autores originais: Ben Slivinski, Michael Saldivar

Publicado 2026-07-02

📖 5 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Ben Slivinski, Michael Saldivar

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á contratando um arquiteto brilhante, mas às vezes excessivamente confiante, para projetar uma ponte. Você não quer apenas a planta final; você precisa saber por que cada viga está colocada onde está. Se o arquiteto disser: "Esta viga vai aqui porque parece certo", você não pode confiar na ponte. Mas se ele disser: "Esta viga vai aqui por causa da Lei X, e aqui está o cálculo provando isso", você pode conferir a matemática.

Este é o problema que o Theoria resolve para a Inteligência Artificial.

O Problema: Duas Formas Falhas de Confiar na IA

Atualmente, temos duas formas principais de verificar se a resposta de uma IA é boa, e ambas possuem lacunas:

A Abordagem do "Matemático" (Assistentes de Prova Formal): Isso é como contratar um robô que fala apenas em um código matemático estrito e inquebrável. É perfeito, mas só consegue entender problemas que já foram traduzidos para esse código. A maioria dos problemas do mundo real (como argumentos jurídicos ou teorias científicas) é desordenada e informal, então o robô não consegue lê-los.
A Abordagem do "Pressentimento" (Juízes Escalares): Isso é como pedir a um humano para ler a redação de uma IA e dar uma nota de 1 a 10. Cobre muita coisa, mas a pontuação é uma caixa preta. Você não sabe por que ela tirou 7. Ela esqueceu alguma premissa oculta? Ela inventou uma citação? Você apenas recebe um número, e não pode auditá-lo posteriormente.

A Solução: O Detetive de "Reescrita de Estado"

O Theoria introduz uma terceira via. Em vez de pedir à IA para escrever uma longa redação ou traduzir tudo para código matemático, o Theoria força a IA a reescrever sua resposta como um log de mudança de estado passo a passo.

Pense nisso como um arquivo de salvamento de videogame ou um sistema de controle de versão (como o Git) para o raciocínio.

A Configuração: A IA começa com um "Estado 0" (o enunciado do problema).
O Movimento: Para chegar à resposta, a IA deve fazer um movimento para o "Estado 1", depois para o "Estado 2", e assim por diante.
A Regra: Para cada movimento, a IA deve fornecer um ticket (uma justificativa). O ticket só pode ser de um dos três tipos:
1. Uma Citação: "Estou usando o Teorema X."
2. Um Cálculo: "Eu fiz a conta: 2+2=4."
3. Um Fato Dado: "O problema me informou isso."

O Truque de Mestre: "Completude da Mudança"

Aqui está o ingrediente secreto. O Theoria tem uma regra estrita: Cada mudança entre o Estado A e o Estado B deve ser explicada pelo ticket.

Se a IA tentar introduzir uma premissa oculta (como "Assuma que a ponte é feita de ouro") sem um ticket, o sistema a pega. A "mudança" (adicionar a premissa do ouro) aparece no log, mas o ticket (a justificativa) não cobre essa mudança. O sistema grita: "Espere! Você mudou o estado, mas não nos mostrou o recibo!"

Isso força a IA a ser honesta. Ela não pode esconder uma mentira em um longo parágrafo de texto; ela tem que mostrar o momento exato em que a mentira entrou na conversa.

Como Funciona na Prática

O Solucionador (Solver): Uma IA tenta resolver um problema.
O Formalizador: Uma segunda IA reescreve essa solução no "Log de Mudança de Estado" descrito acima. Se o solucionador deu um salto na lógica, o formalizador tem que registrar isso como um passo específico.
Os Juízes: IAs especializadas auditam cada passo.
- Um "Juiz de Matemática" verifica os cálculos.
- Um "Juiz de Citação" verifica se o teorema referenciado realmente existe e se se aplica.
- Um "Juiz de Fatos" verifica se aquele fato estava presente no problema original.
O Veredito: Se todos os passos tiverem um ticket válido, a resposta é Certificada. Se mesmo um único passo estiver sem um ticket ou com um ticket falso, a resposta é Rejeitada.

O Que o Artigo Descobriu

Os autores testaram isso em problemas difíceis (como os encontrados em exames de especialistas) e descobriram:

Alta Confiança: Quando o Theoria diz que uma resposta está correta, ela está correta 91,4% das vezes.
Melhor em Pegar Mentiras Espertas: Quando a IA tenta esconder uma premissa (uma premissa oculta) ou inventar uma citação, o Theoria a pega 90,6% das vezes. Um juiz padrão de "pressentimento" só pega isso 62,5% das vezes.
Não é Mágico para Erros Matemáticos: Se a IA apenas errar um cálculo simples (como dizer que 2+2=5), tanto o Theoria quanto o juiz padrão o pegam quase a mesma quantidade de vezes. A vantagem especial do Theoria é especificamente para detectar lógica oculta e fontes falsas.
Complementaridade: O Theoria e os juízes padrão falham em problemas diferentes. Se você usar ambos, pode capturar quase todos os erros.

A Conclusão

O Theoria não tenta tornar a IA mais inteligente; ele tenta tornar o raciocínio da IA auditável.

Ele transforma uma redação vaga e pouco confiável em um livro de contabilidade transparente de mudanças. Ele não promete que todas as respostas estarão certas (ele rejeita cerca de 43% das respostas porque não consegue verificá-las), mas para as respostas que ele aprova, você pode olhar o recibo, conferir a matemática e saber exatamente por que é seguro confiar.

Em um mundo onde a IA pode alucinar fatos, o Theoria é o sistema que diz: "Mostre-me o recibo de cada passo, ou eu não assinarei embaixo disso."

Resumo Técnico: Theoria – Verificação de Aceitabilidade de Reescrita sobre Estados de Raciocínio Informal

1. Declaração do Problema

O artigo aborda o "problema da confiança" no raciocínio de IA: distinguir quando uma resposta gerada por IA deve criar uma confiança justificada, particularmente em campos de alta criticidade (ciência, direito, finanças, medicina). As abordagens atuais enfrentam uma dicotomia:

Assistentes de Prova Formais (ex: Lean, Coq): Oferecem certeza matemática, mas falham em cobrir a maioria das distribuições de problemas devido ao alto custo e à fragilidade semântica da autoformalização de requisitos informais em linguagem natural.
Juízes de LLM Escalares: Oferecem ampla cobertura, mas produzem pontuações opacas que não podem ser auditadas, herdam os problemas de coerência dos LLMs e falham em identificar por que uma prova é falha (ex: premissas ocultas, citações fabricadas).

O desafio central é verificar o raciocínio informal sem exigir a formalização completa, garantindo que erros — especificamente suposições não declaradas e saltos lógicos — sejam visíveis e auditáveis.

2. Metodologia: A Arquitetura Theoria

A Theoria introduz uma arquitetura de verificação que reescreve a resposta em linguagem natural de um solver em uma testemunha de prova (proof witness): uma sequência de transições de estado tipadas.

2.1 O Enquadramento da Reescrita

Em vez de tratar uma prova como um bloco de prosa, a Theoria a decompõe em uma trajetória de estados $(S_0, S_1, \dots, S_n)$ .

Estado ( $S_i$ ): Uma lista ordenada de strings representando fatos estabelecidos e o objetivo atual.
Transição: Um passo de $S_{i-1}$ $S_{i - 1}$ para $S_i$ $S_{i}$ é licenciado por um tipo de justificativa específico:
1. Citação: Um teorema, definição ou regra de inferência.
2. Computação: Manipulação aritmética ou simbólica.
3. Dado do Problema: Fatos explicitamente declarados no texto do problema.
O Invariante de Completude de Mudança: Cada diferença semântica entre $S_{i-1}$ e $S_i$ deve ser explicada pela justificativa declarada. Se uma premissa é necessária para derivar o novo estado, mas não está presente no estado anterior ou na justificativa, isso constitui uma mutação não licenciada.

2.2 Pipeline de Verificação

O sistema opera em um ciclo: Resolver $\to$ Formalizar $\to$ Julgar $\to$ Filtrar $\to$ Reparar.

Solver: Propõe uma solução em linguagem natural (com auxílio de ferramentas, ex: busca na web).
Formalizador: Reescreve a solução na forma de testemunha de transição de estado. Ele impõe que as premissas devem ser explícitas antes de serem usadas.
Julgamento Especializado Paralelo:
- Juízes de Computação: Recalculam os passos do zero.
- Juízes de Citação: Verificam a existência e aplicabilidade dos teoremas citados contra o diferencial (diff) específico do estado.
- Juízes de Dados do Problema: Verificam os fatos contra o texto original.
- Juiz do Estado Inicial: Audita $S_0$ para garantir que nenhuma premissa injustificada seja introduzida no início.
- Todos os juízes são instruídos adversariamente para encontrar erros em vez de confirmar a plausibilidade.
Filtro de Pedantismo: Distingue entre erros substantivos e excesso de rigor em relação à notação informal ou compressão.
Elevação de Convenção (Convention Lift): Permite que o sistema aceite um passo se uma convenção de domínio padrão e citável resolver uma rejeição, desde que a suposição seja explicitamente registrada.
Certificar-ou-Declinar: O sistema emite uma decisão binária. Se todos os passos passarem (ou forem resolvidos via elevação de convenção), a resposta é Certificada. Se qualquer passo falhar e não puder ser reparado dentro dos limites, a resposta é Declinada.

3. Principais Contribuições

A principal contribuição do artigo não é o uso de múltiplos modelos ou verificação de passos (que são comuns), mas o formato de testemunha específico e suas garantias teóricas:

Garantia de Exposição (Proposição 4.4): O invariante de completude de mudança converte premissas ocultas (lacunas de raciocínio global) em mutações não licenciadas locais e observáveis. Uma premissa oculta deve aparecer como um novo elemento no estado (disparando uma verificação de licença) ou violar o invariante. Isso força os erros à superfície, onde podem ser detectados por juízes locais.
Previsões de Classe de Erro (Proposição 4.5): O formato prevê que as vantagens de verificação se concentrarão em:
- Premissas Ocultas: Expostas como mutações não licenciadas.
- Citações Fabricadas: Expostas porque a evidência é explicitamente tipada e verificada contra o diferencial.
- Sem Vantagem: Erros aritméticos e aplicações incorretas de teoremas (onde o teorema existe, mas é aplicado erroneamente) não recebem vantagem estrutural de exposição sobre a prosa, pois o erro é semântico e não estrutural.
Decomposição de Falha: O artigo distingue entre Falha de Exposição (o formato esconde o erro) e Falha de Juiz (o juiz não detecta um erro exposto). A Theoria visa minimizar a primeira, deixando a segunda para ser abordada empiricamente.

4. Resultados Empíricos

A avaliação foi realizada no HLE-Verified Gold (185 problemas de especialistas) e no GPQA Diamond (65 problemas científicos de nível de pós-graduação).

4.1 Desempenho no HLE-Verified Gold

Precisão Certificada: 91,4% (96/105 corretos) com um IC de Wilson de 95% de [84,5%, 95,4%].
Cobertura: 56,8% (105/185 problemas certificados).
Assimetria: As respostas declinadas foram aproximadamente 5,0 $\times$ mais propensas a estarem erradas do que as certificadas (taxa de erro de 42,5% vs. 8,6%).
Comparação com Solver-Apenas: Um solver com auxílio de busca na web alcançou 83,8% de precisão com 100% de cobertura. O pipeline da Theoria filtrouu uma parte significativa dos erros, reduzindo a taxa de erro no grupo certificado para 8,6%.
Comparação com Juízes Holísticos: Juízes de LLM holísticos (atribuindo uma pontuação de confiança única) alcançaram precisão comparável (92,4–93,3%) com cobertura equivalente. No entanto, eles falharam em problemas diferentes (índice de Jaccard 0,14–0,36), indicando coberturas de erro complementares.

4.2 Robustez Adversária

Em um benchmark de 95 provas envenenadas (injetando tipos específicos de erro):

Detecção Geral: A Theoria detectou 94,7% (90/95) contra 83,2% (79/95) para o julgamento holístico ( $p = 0,0017$ ).
Especificidades de Classe de Erro:
- Premissas Ocultas: Theoria 90,6% vs. Holístico 62,5% (diferença de 28 pp).
- Citações Fabricadas: Theoria 100% vs. Holístico 90%.
- Aritmética/Teoremas Mal Aplicados: O desempenho foi idêntico (~95% e ~93% respectivamente), confirmando a previsão teórica de que o formato não oferece vantagem estrutural para esses tipos de erro.

4.3 Fora de Distribuição (GPQA Diamond)

Precisão Certificada: 97,1% (33/34).
Cobertura: 52,3%.
A alta precisão em um benchmark diferente sugere que a fronteira "certificar-ou-declinar" é impulsionada pela formalizabilidade do raciocínio, e não pela calibração específica do benchmark.

4.4 Potencial de Ensemble

Como a Theoria e os juízes holísticos falham em conjuntos de problemas distintos, estratégias de ensemble (ex: voto de maioria) alcançaram 93,6% de precisão com 58,9% de cobertura, superando qualquer método individual.

5. Significância e Alegações

O artigo afirma que a Theoria fornece um mecanismo de supervisão escalável que preenche a lacuna entre a saída bruta do LLM e a verificação formal.

Auditabilidade: Ao contrário das pontuações escalares, a Theoria produz um traço de prova legível por humanos onde cada passo pode ser independentemente contestado.
Vantagem Estrutural: O sistema não depende do juiz reconstruir uma prova a partir da prosa. Em vez disso, ele reduz a tarefa de verificação a uma questão local: "Esta justificativa licencia esta mudança de estado específica?"
Complementaridade: O artigo argumenta que a Theoria não é um substituto para juízes holísticos, mas uma abordagem complementar. A baixa sobreposição de Jaccard nos erros sugere que combinar arquiteturas de verificação estruturalmente diferentes gera maior confiabilidade.
Limitações: Os autores reconhecem que a Theoria não pode detectar erros que não produzem mutação de estado observável (ex: interpretações sutis do enunciado do problema em $S_0$ ) e que atualmente depende de juízes de LLM em vez de backends formais (como Lean ou solvers SMT), embora seja projetada para ser compatível com eles.

Em resumo, a Theoria demonstra que, ao impor um invariante de completude de mudança sobre o raciocínio informal, é possível trazer à tona suposições ocultas e evidências fabricadas que a avaliação holística padrão deixa passar, fornecendo um limite rigoroso e auditável para a confiança no raciocínio gerado por IA.