🤖 machine learning

Evidence-Grounded Verified Agentic Reasoning: A Path Toward Eliminating LLM Hallucination in Empirical Inference via Tool-Attested Kernel Proofs

O artigo introduz o EG-VAR, uma arquitetura de raciocínio agêntica baseada em Lean 4 que elimina alucinações de LLM em inferência empírica ao garantir que todas as saídas verificadas sejam estruturalmente derivadas de chamadas de ferramentas atestadas e provas verificadas pelo kernel, enquanto audita explicitamente ou se abstém de quaisquer afirmações não suportadas.

Autores originais: Junyu Ren

Publicado 2026-07-15

📖 6 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Junyu Ren

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ê tem um assistente robô superinteligente e tagarela (um LLM) que adora contar histórias sobre o mundo. O problema? Às vezes, o robô fica tão confiante em suas próprias memórias que inventa fatos ou ignora a evidência real bem diante de seus olhos. É como um aluno que, ao ser solicitado a verificar um problema matemático contra o livro didático, apenas escreve a resposta que ele acha que está certa porque se lembra dela de um sonho, mesmo que o livro diga algo diferente.

Por muito tempo, as pessoas tentaram consertar isso dando ao robô uma "caixa de ferramentas" de fontes externas, como uma calculadora ou um banco de dados. Mas o artigo argumenta que apenas entregar uma caixa de ferramentas ao robô não é suficiente. O robô ainda pode ignorar a caixa de ferramentas, ou pode usar os números da caixa de ferramentas, mas então distorcer a lógica para que ela se ajuste à sua própria história. É como dar a um chef um ingrediente fresco e verificado, mas deixá-lo cozinhar como bem entender; o prato final ainda pode ser um desastre.

A Grande Ideia: A Fábrica de "Alegações Verificadas"

Os autores, liderados por Junyu Ren, construíram um novo sistema chamado EG-VAR (Evidence-Grounded Verified Agentic Reasoning - Raciocínio Agêntico Verificado com Base em Evidências). Pense nisso não como um robô que apenas responde perguntas, mas como uma fábrica de alta segurança com um inspetor rigoroso e implacável.

Veja como a fábrica funciona, passo a passo:

A Camada de Ferramentas (O Entregador Confiável): Primeiro, uma máquina determinística, entediante e confiável (não o robô tagarela) vai até a fonte — como uma planilha ou um banco de dados — e busca os números brutos. Ela carimba esses números com um selo de "Verificado". Esta é a única maneira de colocar dados reais dentro da fábrica.
O Formalizador (O Tradutor): O robô tagarela (o LLM) é então solicitado a traduzir a pergunta humana para uma linguagem matemática estrita chamada Lean 4. É como pedir ao robô para escrever um contrato jurídico ou uma prova matemática em vez de um parágrafo.
O Kernel (O Inspetor Implacável): Esta é a parte mais importante. Um programa de computador minúsculo e superestrito (o kernel do Lean) atua como o inspetor. Ele verifica o "contrato" do robô linha por linha.
- A Regra de Ouro: O inspetor tem uma regra que diz: "Você não pode alegar que um fato é VERIFICADO a menos que possa apontar para um número carimbado e selado pelo Entregador Confiável."
- Se o robô tentar inventar um número, ou se tentar usar um número mas conectar a lógica de forma errada, o inspetor rejeita todo o processo.
O Resultado:
- Se a prova passar, a fábrica imprime uma resposta VERIFICADA. Esta resposta vem com uma "trilha de auditoria reproduzível", o que significa que qualquer pessoa pode refazer a matemática mais tarde e ver exatamente como a resposta foi construída a partir dos dados originais.
- Se a prova falhar, a fábrica não adivinha. Ela diz ABSTAIN (que significa "eu não sei" ou "não consigo provar isso"). É um "eu desisto" honesto em vez de uma mentira confiante.

O Que o Artigo Realmente Descobriu

Os autores testaram este sistema em um conjunto específico de 120 perguntas sobre tabelas (planilhas).

A Pontuação "Perfeita": Quando as perguntas eram claras e o robô recebia as ferramentas certas, o EG-VAR obteve 120 de 120 questões corretas. Foi 100% de precisão.
A Competição: Outros sistemas que usavam as mesmas ferramentas, mas não tinham o inspetor estrito, acertaram apenas 114 de 120 (95%). Eles ainda cometiam erros.
O Teste "Contrafactual": Este foi o verdadeiro teste de estresse. Os autores pegaram tabelas e secretamente alteraram os números para contradizer o que o robô "sabia" de seu treinamento (como mudar a população de um país para um número minúsculo).
- Sem o inspetor estrito, o robô ignorou os novos números e manteve suas memórias antigas 80% a 90% das vezes.
- Com o EG-VAR, o sistema manteve-se 100% fiel aos novos números alterados. Não importava o quão forte era a memória antiga do robô; o inspetor o forçou a usar os novos dados.

O Que o Artigo Descarta (As "Zonas de Proibição")

O artigo é muito claro sobre o que este sistema não é e o que ele não consegue fazer:

Não é uma cura mágica para todas as alucinações. O artigo afirma explicitamente que o robô ainda pode cometer erros ao traduzir a pergunta humana para a linguagem matemática. Se o robô entender mal a pergunta e escrever o problema matemático errado, o inspetor verificará esse problema matemático perfeitamente, mas a resposta ainda será errada para a pergunta original.
- Em seus testes, esse "erro de tradução" ocorreu cerca de 3,3% das vezes com um modelo e 1,7% com um modelo mais forte.
Não corrige dados ruins. Se a planilha original contiver uma mentira, o sistema verificará essa mentira fielmente. O sistema garante que a resposta venha da fonte, não que a fonte seja verdadeira.
Não é um sistema de "talvez". O artigo argumenta contra sistemas que fornecem uma "pontuação de confiança" (como "estou 80% seguro"). Em vez disso, o EG-VAR usa um portão estrito de "Sim/Não". Ou você tem uma prova verificada, ou tem um honesto "eu me abstenho".

O Quão Certo Eles Estão?

Os autores estão muito confiantes sobre a segurança estrutural de seu sistema. Eles provaram matematicamente (Teoremas 3.1 e 3.2) que:

Nenhuma resposta VERIFICADA pode jamais aparecer sem um chamado de ferramenta carimbado que a respalde.
Cada etapa da lógica em uma resposta VERIFICADA foi verificada pelo kernel e é matematicamente válida.

No entanto, em relação à precisão da tradução da linguagem humana pelo robô, eles são mais cautelosos. Eles mediram as taxas de erro (3,3% e 1,7%) em seus testes específicos e sugerem que esses números poderiam melhorar se treinassem mais o robô para traduzir perguntas corretamente. Mas o "piso de segurança" — a garantia de que o sistema não mentirá silenciosamente — está construído na arquitetura, não apenas no cérebro do robô.

A Conclusão

O EG-VAR é como uma fábrica que se recusa a enviar um produto a menos que possa mostrar um recibo para cada peça utilizada. Se o robô tentar contrabandear uma peça falsa, a fábrica interrompe a linha e diz: "Não, não podemos enviar isso". Ele transforma o problema dos "robôs mentirosos" em um problema de "recibos ausentes", o que é muito mais fácil de detectar e corrigir. Embora não resolva todos os problemas (o robô ainda pode entender mal o pedido), ele garante que, quando a fábrica diz "Verificado", ela realmente quer dizer "Verificado".

Resumo Técnico: Raciocínio Agêntico Verificado com Fundamentação em Evidências (EG-VAR)

Declaração do Problema

Modelos de Linguagem de Grande Escala (LLMs) frequentemente alucinam fatos empíricos durante a inferência, seja fabricando dados ou recorrendo a vieses paramétricos desatualizados que conflitam com a evidência recuperada. Embora o raciocínio auxiliado por ferramentas (RAG) permita que os modelos consultem fontes externas, ele falha em garantir alegações empíricas verificáveis. As abordagens atuais sofrem de duas falhas estruturais:

Saídas Não Atestadas: Saídas aceitas não necessariamente descendem de evidências atestadas; os modelos podem descartar dados recuperados que conflitem com seus vieses internos (viés de confirmação).
Deduções Não Verificadas: Deduções aceitas não necessariamente se sustentam sob escrutínio formal; os modelos podem realizar passos lógicos inválidos ou interpretar incorretamente as saídas das ferramentas.

Soluções existentes, como verificadores de fatos simbólicos ou provadores de teoremas impulsionados por LLM, carecem ou de fundamentação externa (provadores apenas matemáticos) ou dependem de componentes aprendidos que não podem garantir estruturalmente a ausência de alegações sem suporte.

Metodologia: Arquitetura EG-VAR

O artigo apresenta o EG-VAR (Evidence-Grounded Verified Agentic Reasoning), uma arquitetura de quatro camadas projetada para tornar o raciocínio empírico governável, integrando um assistente de prova (Lean 4) com atestação de ferramentas. O sistema trata o LLM como um componente não confiável dentro de um livro-razão de confiança estritamente definido.

A Pilha de Quatro Camadas

L1: Camada de Ferramenta (Confiável, Determinística): Um tempo de execução determinístico executa consultas contra fontes externas (ex: busca de células de tabela, agregações). Ele produz um payload Attested T — um testemunho de tempo de execução registrando a consulta, a identidade da fonte e o resultado. Apenas o tempo de execução pode gerar esses testemunhos.
L2: Formalização por Fonte (Auditada Offline): Um "curador" define um catálogo de levantamento (lift catalog) para cada fonte de dados. Isso mapeia fatos de armazenamento L1 (ex: "célula na linha $r$ , coluna $c$ possui o valor $v$ ") para fatos de ontologia de mundo L2 (ex: HasProperty, ArgmaxWhere). Esses levantamentos são auditados uma única vez e importados como axiomas.
L3: Kernel Lean 4 (Confiável, Formal): O kernel é a única autoridade para cunhar alegações de Evidence Verified (Evidência Verificada). Ele impõe uma regra única de cunhagem, mkVerified, que exige um hipotese Attested T do tempo de execução. O kernel verifica tipos de cada passo de prova; se um passo falhar, a alegação é rejeitada.
L4: LLM Solver (Não Confiável, Estocástico): O LLM recebe um objetivo tipado e propõe táticas de prova. Ele pode consumir termos Attested T introduzidos pelo tempo de execução, mas não pode sintetizá-los. Se o kernel rejeitar a tática, o sistema itera ou se abstém.

Mecanismos Principais

A Regra mkVerified: O único construtor para Evidence Verified requer um testemunho Attested T. Isso garante que nenhuma saída verificada possa existir sem uma chamada de ferramenta correspondente (Teorema 3.1).
Testemunhos de Soma Dependente: As alegações são estruturadas como somas dependentes ( $\Sigma$ ). Para uma pergunta "Qual entidade possui a propriedade $P$ ?", o objetivo é $\Sigma (e : \text{String}) (v : \text{Value}), \text{Evidence Verified}(\dots)$ . A resposta superficial é o testemunho extraído da prova verificada pelo kernel.
Abstenção Honesta: Se o kernel rejeitar a prova (devido a levantamentos ausentes, táticas inválidas ou falta de atestação), o sistema emite um ABSTAIN (Abster-se) com uma trilha de auditoria reproduzível, em vez de adivinhar.
Disciplina de Grau: A evidência carrega graus explícitos (VERIFIED, SUPPORTED, PLAUSIBLE, SPECULATIVE). O sistema impõe uma regra de "não promoção" (no-upcast): conclusões não podem ter um nível superior ao de sua premissa mais fraca.

Principais Contribuições

Garantia Estrutural de Fundamentação: O EG-VAR é a primeira arquitetura que combina um kernel de assistente de prova com atestação de ferramenta como um axioma tipado. Ele fornece uma garantia estrutural (Teorema 3.1) de que toda saída VERIFIED descende de uma chamada de ferramenta atestada, eliminando alucinações sem suporte, independentemente da força do LLM.
Segurança Formal vs. Fidelidade Semântica: O artigo distingue entre segurança formal (a prova é aceita pelo kernel) e fidelidade semântica (o objetivo formalizado corresponde à alegação em linguagem natural). O EG-VAR garante a primeira estruturalmente; a segunda é tratada como um alvo de precisão endereçável via ajuste fino do formalizador.
Trilhas de Auditoria Reproduzíveis: Cada alegação verificada é acompanhada por um arquivo de prova Lean autossuficiente. Terceiros podem re-verificar a tipagem da alegação offline sem executar novamente o LLM, usando o kernel, os levantamentos por fonte e o adaptador da ferramenta.
Protocolo de Formalização por Fonte: O artigo introduz um método para tratar fontes de dados como artefatos de confiança co-iguais, exigindo formalização (catálogos de levantamento) que separa a curadoria do lado da fonte da razão do lado da alegação.

Resultados Empíricos

A avaliação foca no TableBench (raciocínio numérico em tabelas) através de três níveis:

Nível 1 (Benchmark Gold-Goal, $n=120$ ):
- O EG-VAR alcançou 120/120 (100%) em alegações inequívocas, correspondendo à resposta padrão com uma prova verificada pelo kernel.
- As linhas de base (mesmo modelo com ferramentas, mas sem kernel) estagnaram em 95,0% (114/120).
- O EG-VAR fechou a lacuna para zero, demonstrando que a disciplina do kernel impõe a composição correta das saídas das ferramentas.
Nível 1.5 (Testes de Estresse Contrafactual, 5 domínios $\times$ 2 modelos):
- Tabelas sintéticas foram criadas onde os valores das células contradiziam o conhecimento de mundo prévio do modelo (ex: alterando a população de um país para um valor baixo).
- O EG-VAR permaneceu 100% fiel à fonte em todos os domínios e magnitudes de alteração.
- As linhas de base (mesma ferramenta) caíram para 80–90% (Sonnet) e 50–80% (sem ferramenta), mostrando que o EG-VAR previne estruturalmente o modo de falha de "sobreposição de prioridade" (prior-override), onde os modelos ignoram a evidência recuperada.
Nível 2 (Fim-a-Fim com LLM Formalizador, $n=120$ ):
- Em um cenário totalmente automatizado onde o LLM propõe o objetivo formal (removendo o bypass de fixture padrão), a taxa de erro do formalizador puro foi de 3,3% (Sonnet) e 1,7% (Opus).
- As divergências restantes foram categorizadas como ambiguidades registradas (4,2%) ou problemas de artefato do benchmark identificados (1,7%), todos explícitos e auditáveis, em vez de alucinações silenciosas.

Significância e Alegações

O artigo posiciona o EG-VAR como uma interface de governança técnica para alegações empíricas de alto risco. Sua significância reside em deslocar o fardo da segurança do aprendizado estatístico para a imposição arquitetônica:

Eliminação de Saídas Sem Suporte: A garantia estrutural assegura que "alucinações verificadas" (saídas rotuladas como VERIFIED sem evidência) são impossíveis sob o modelo de ameaça do sistema.
Incerteza Mensurável: Ao tornar a abstenção um resultado estrutural da rejeição do kernel, em vez de um comportamento aprendido, o sistema fornece uma "taxa de recusa" e incerteza tipada.
Ciclo de Feedback de Formalização (Formalization Flywheel): Os autores argumentam que, à medida que as fontes de dados evoluem para interfaces tipadas (SQL, APIs, Grafos de Conhecimento), o ônus da formalização se amortizará em infraestrutura reutilizável, reduzindo o custo de verificação por consulta.
Propriedades de Governança: O sistema permite três propriedades aplicáveis: (i) auditoria independente de cada saída verificada via provas reproduzíveis; (ii) incerteza tipada via disciplina de grau; e (iii) abstenção honesta como uma propriedade mensurável do sistema.

O artigo conclui que, embora erros de semântica-formalização permaneçam (endereçáveis via ajuste fino no corpus de curadoria liberado), o piso de segurança estrutural é estabelecido hoje, oferecendo um caminho para eliminar a alucinação de LLMs em inferência empírica.