Resumo Técnico: Decodificável, mas não Fiel: Acoplando Racionales de Linguagem Natural a Verificadores Programáticos

Declaração do Problema

Embora os grandes modelos de linguagem (LLMs) possam gerar racionais de linguagem natural plausíveis para suas previsões, essas explicações frequentemente falham em representar fielmente o processo de tomada de decisão interno do modelo. Os modelos podem "racionalizar" decisões post-hoc, omitir a verdadeira fonte de uma resposta ou utilizar atalhos invisíveis no texto gerado. Trabalhos anteriores indicam que, embora o prompting de cadeia de pensamento (chain-of-thought) melhore a precisão da tarefa, as explicações geradas não são necessariamente evidência de raciocínio causal.

Verificadores programáticos externos (ex: provadores de teoremas, motores de jogos, executores de código) oferecem um mecanismo para verificar afirmações, mas o uso atual é tipicamente limitado à supervisão ao nível do resultado (verificar a resposta final). Isso deixa uma lacuna: um modelo pode produzir uma afirmação correta enquanto a explicação acompanhante não é sustentada, ou codificar informações do verificador internamente sem verbalizá-las de forma coerente. A questão central abordada é se forçar as representações dos racionais do modelo a serem decodificáveis por um verificador garante que as explicações geradas sejam fiéis ao seu raciocínio.

Metodologia: Raciocínio Acoplado ao Verificador

O artigo propõe um framework chamado Raciocínio Acoplado ao Verificador para estreitar a lacuna entre afirmações verificadas e racionais de linguagem natural.

Formato de Sequência e Objetivo

O modelo gera uma sequência contendo um racional de linguagem natural ($r$) e uma afirmação explícita inline ($c$) no formato: [CONTEXTO] x [RAT] r [CLAIM] c [EOS]. Um verificador programático $V$ fornece um rótulo alvo $y = V(x)$ (ex: aceitação/rejeição de prova, balde de taxa de vitória, classe de complexidade).

Uma cabeça de consistência auxiliar (um classificador linear) é treinada para prever o alvo do verificador $y$ a partir dos estados ocultos de pooling médio do span do racional ($z_{rat}$). O objetivo de treinamento combina a previsão do próximo token padrão ($L_{LLM}$), supervisão de afirmação opcional ($L_{claim}$) e a perda de consistência ($L_{cons}$):
$$L = L_{LLM} + \lambda_{claim}L_{claim} + \lambda_{cons}L_{cons}$$

Restrições de Fluxo de Informação

Para garantir que a cabeça de afirmação não ignore o racional, os autores utilizam uma máscara de atenção Board-Explanation-Claim (BEC) em experimentos específicos. Isso impede estruturalmente que os tokens da afirmação atentem para os tokens de contexto de entrada, forçando-os a depender exclusivamente do span da explicação.

Escada Diagnóstica

O artigo introduz um framework diagnóstico de múltiplos níveis para distinguir entre decodificabilidade (a informação do verificador está presente na representação) e fidelidade (a geração reflete essa informação):

1. Decodificabilidade: Precisão da cabeça de consistência (o rótulo do verificador pode ser linearmente decodificado dos estados do racional?).
2. Seguimento Contrafactual: Spans trocados (ex: trocar um racional com um rótulo diferente) alteram a previsão da cabeça?
3. Influência Causal: O patching de ativação (substituir estados ocultos do racional por aqueles de um estado latente diferente) altera os logits da afirmação subsequente?
4. Qualidade de Geração: O modelo produz explicações coerentes e fiéis?

Configurações Experimentais

O framework é avaliado em cinco configurações distintas:

1. Sintética: Validação controlada com estados latentes para isolar mecanismos e testar intervenções causais via patching de ativação.
2. LeanCheck: Prova de teoremas formais usando Lean 4. Testa o acoplamento específico de span (racional vs. prova) sob conflito contrafactual.
3. KataGo: Um motor de Go que fornece rótulos densos e não binários (baldes de taxa de vitória) para estados de tabuleiro complexos.
4. Acoplamento de Código (Code Coupling): Afirmações algorítmicas (complexidade de tempo/espaço, classe de algoritmo) onde o modo de falha de geração infiel é mais visível.
5. FEVER: Verificação de evidência em linguagem real, testando o trade-off entre precisão bruta e sensibilidade à evidência.

Principais Resultados

1. A Lacuna Decodificabilidade–Fidelidade

A descoberta central é que a decodificabilidade não garante a fidelidade.

• Sintética & LeanCheck: O treinamento de consistência torna a informação do verificador decodificável e causalmente influente. No LeanCheck, o pooling de apenas racional e apenas prova alcança separação direcional perfeita sob conflito contrafactual (100% de seguimento ao rótulo do span trocado).
• KataGo: Spans de comentários em linguagem natural codificam baldes de taxa de vitória de 10 vias com 81,1% de precisão, demonstrando que o método escala para domínios densos e não binários.
• Código (O Modo de Falha Crítico): Na configuração de código, o modelo atinge 98,6% de acoplamento de representação (os estados ocultos codificam perfeitamente as afirmações do verificador), mas a prosa gerada permanece infiel. O modelo emite explicações fluentes e gramaticais descrevendo um algoritmo não relacionado (ex: descrevendo uma "soma de uma lista" enquanto o código implementa "ordenação por seleção") enquanto emite corretamente as tags de afirmação estruturadas (ex: $O(n^2)$).
  • Esta lacuna é estrutural, não baseada em capacidade: resultados idênticos foram observados tanto no GPT-2 pré-treinado quanto em modelos treinados do zero.
  • A lacuna não é baseada em pesos: Aumentar o peso da perda de consistência ($\lambda_{cons}$) até $10^4$ não melhora a qualidade da geração, pois a perda de consistência atua nas representações, não nos tokens emitidos.

2. Insights da Escada Diagnóstica

• Influência Causal: Em configurações sintéticas, o patching de ativação dos estados do racional no nível 0 altera o comportamento da afirmação em 73–89% dos casos treinados com consistência (vs. 31% do baseline), confirmando que o acoplamento é causal, não meramente correlacional.
• Trade-off FEVER: Em configurações de linguagem real, o pooling sobre a sequência completa (incluindo o texto da afirmação) produz precisão quase perfeita (99%), mas falha em isolar a sensibilidade à evidência. O pooling apenas de evidência produz menor precisão (44%), mas isola melhor se o modelo realmente processa a evidência, revelando um trade-off de precisão-sensibilidade oculto pela avaliação padrão.

3. Análise por Afirmação

Na configuração de código, a perda de consistência beneficia desproporcionalmente afirmações granulares (ex: classe de algoritmo, operação chave) em detrimento das binárias. Afirmações binárias são parcialmente aprendíveis apenas pela estrutura do código, enquanto afirmações granulares dependem fortemente do objetivo de consistência para alta precisão.

Significância e Alegações

O artigo estabelece que perdas de consistência são ferramentas eficazes de diagnóstico e moldagem de representação, mas não são condições suficientes para o raciocínio fiel.

• Representação vs. Geração: O mecanismo molda com sucesso a representação interna para codificar informações relevantes ao verificador (decodificabilidade), mas sem um objetivo de nível de geração que recompense o texto por corresponder ao verificador, o modelo pode emitir explicações fluentes, porém infiéis.
• Limitações de Probing: Alta precisão de probe (decodificabilidade) não deve ser equacionada com raciocínio fiel. Um modelo pode "saber" a resposta em seus estados ocultos enquanto "diz" algo inteiramente diferente em sua saída.
• Caminho a Seguir: Fechar a lacuna requer objetivos onde o gradiente alcance os tokens gerados e os recompense pela consistência com o verificador. Os autores sugerem o Aprendizado por Reforço com Recompensas Verificáveis (RLVR) como o instrumento natural, onde o modelo é recompensado com base nas afirmações inline verificáveis que ele realmente produz, em vez de um probe auxiliar.

O trabalho fornece uma escada diagnóstica rigorosa para avaliar sistemas de raciocínio, demonstrando que, embora possamos forçar modelos a "saber" a verdade em suas representações, garantir que eles "digam" a verdade exige mais do que apenas restrições do lado da representação.