Resumo Técnico: LOVER (Verificador Regularizado por Lógica)

Declaração do Problema

Os verificadores são essenciais para aprimorar as capacidades de raciocínio dos Modelos de Linguagem de Grande Escala (LLMs), otimizando parâmetros (via RL) ou selecionando as saídas ótimas (via escalonamento de inferência). No entanto, os verificadores existentes enfrentam duas limitações primárias:

1. Dependência de Dados: Verificadores supervisionados tradicionais exigem conjuntos de dados rotulados caros e intensivos em recursos. A coleta de anotações de alta qualidade, particularmente para domínios especializados ou anotações de processo em nível de etapa, é custosa e demorada.
2. Diversidade e Generalização: A dependência de anotações de especialistas pode levar à falta de diversidade de soluções, pois os anotadores podem favorecer padrões de raciocínio familiares em detrimento de outros igualmente válidos, mas menos intuitivos. Além disso, abordagens não supervisionadas recentes, como CoT-Decoding, são sensíveis à escolha do modelo base, enquanto outras, como CCS, limitam-se a perguntas de Sim/Não e têm dificuldade em escalar para tarefas de raciocínio geral.

A questão central abordada é se é possível construir verificadores eficazes sem o processo de supervisão, aproveitando o conhecimento intrínseco já presente nos LLMs.

Metodologia: LOVER

Os autores propõem o LOVER (Verificador Regularizado por Lógica), um verificador probabilístico não supervisionado regularizado por regras lógicas. O LOVER trata a tarefa de verificação como a inferência de uma variável latente binária (valor de verdade) com base nas ativações internas de um LLM, sem modificar os pesos do LLM ou exigir dados rotulados.

Componentes Principais

1. Afirmações Contrastivas:
   Para uma dada pergunta $q$ e um caminho de raciocínio gerado $s_i$, a entrada é aumentada com modelos de texto para formar afirmações contrastivas:

   • $x^+_i = q \oplus s_i \oplus \text{"Esta é uma resposta verdadeira."}$
   • $x^-_i = q \oplus s_i \oplus \text{"Esta é uma resposta falsa."}$
     Este processo visa elicitar as "crenças" ou "conhecimentos" internos do modelo em relação à validade do caminho de raciocínio.

2. Modelo Verificador Latente:
   O verificador é uma Rede Neural Perceptron Multicamada (MLP) leve que toma como entrada as representações do estado oculto (especificamente das camadas intermediárias) das afirmações. Ele produz uma probabilidade $p_\theta(z|x)$, onde $z \in \{0, 1\}$ indica a validade da afirmação.

3. Restrições Lógicas (Regularização):
   Para conectar regras lógicas discretas com redes neurais contínuas, o LOVER impõe três restrições lógicas por meio de objetivos probabilísticos suaves:

   • Consistência da Negação: Para um par de afirmações contrastivas ($x^+_i, x^-_i$), suas probabilidades de verdade devem somar 1 e diferir significativamente (Lei do Terceiro Excluído). Isso previne soluções degeneradas onde ambas recebem a mesma probabilidade.
   • Consistência Intra-grupo: Caminhos de raciocínio agrupados pela mesma resposta final devem compartilhar probabilidades de correção semelhantes. Isso impõe consistência entre soluções que levam à mesma conclusão.
   • Consistência Inter-grupo: Entre múltiplos grupos de caminhos de raciocínio (cada grupo correspondendo a uma resposta final distinta), exatamente a afirmação "verdadeira" de um grupo deve ser válida. Isso é imposto usando uma restrição de soma e um termo de regularização de entropia para evitar uma distribuição de probabilidade uniforme entre os grupos.

4. Treinamento e Inferência:

   • Treinamento: O modelo é treinado de ponta a ponta minimizando a soma das três funções de perda derivadas das restrições lógicas. Nenhum rótulo de verdade fundamental é utilizado.
   • Inferência: Dada uma pergunta, $N$ soluções candidatas são geradas. Para cada solução, o verificador prevê a probabilidade de correção da afirmação "verdadeira". As soluções são agrupadas por suas respostas finais, e o grupo com a pontuação agregada mais alta (usando estratégias de máximo ou soma) é selecionado como a resposta final.

Contribuições Principais

1. Framework Não Supervisionado Principiado: O LOVER fornece um framework escalável para verificar caminhos de raciocínio, aproveitando o conhecimento intrínseco dos LLMs regularizado por regras lógicas, eliminando a necessidade de dados supervisionados.
2. Objetivos Probabilísticos Suaves: O artigo introduz formulações probabilísticas suaves para restrições lógicas discretas, permitindo o treinamento diferenciável e de ponta a ponta do verificador.
3. Compatibilidade Geral: O método é compatível com qualquer LLM de caixa branca pronto para uso e aplicável a tarefas de raciocínio geral, não se limitando a tipos específicos de perguntas como Sim/Não.

Resultados Experimentais

Os experimentos foram conduzidos em 10 conjuntos de dados, incluindo raciocínio matemático (GSM8K, iGSM), conhecimento de domínio aberto (HotpotQA, MMLU-Pro) e tarefas fora da distribuição (OOD) do BIG-Bench Hard.

• Desempenho vs. Baselines: O LOVER supera significativamente as baselines não supervisionadas (Greedy, Votação Majoritária, CoT-Decoding).
  • Em média, o LOVER (soma) alcança desempenho comparável a verificadores supervisionados, atingindo aproximadamente 95% do nível de desempenho do verificador supervisionado.
  • O LOVER (soma) alcança um ganho absoluto médio de precisão de 3,3% sobre a Votação Majoritária e 2,9% sobre o CoT-Decoding.
  • O LOVER demonstra robustez em diferentes escalas de modelos (de 0,5B a 32B parâmetros) e estratégias de decodificação.
• Estudos de Ablação:
  • Restrições Lógicas: A remoção da perda de consistência inter-grupo ($L_{inter}$) causou a queda mais significativa de desempenho, indicando seu papel crítico na distinção de grupos de respostas corretas. A consistência da negação ($L_{nega}$) também foi crucial para evitar a pontuação idêntica de afirmações verdadeiras/falsas.
  • Estratégia de Decodificação: O LOVER performa melhor com decodificação CoT natural e é menos sensível a mudanças na estratégia de decodificação em comparação ao CoT-Decoding, que depende fortemente de formatos de saída específicos.
  • Estados Ocultos: A utilização de estados ocultos de camadas intermediárias (por exemplo, camada 15 ou 20 no Mistral-7b) produz o desempenho ótimo.
• Generalização OOD: O LOVER demonstra forte generalização em conjuntos de dados OOD (Expressões Booleanas, Web of Lies, etc.), superando a Votação Majoritária e o CoT-Decoding em todos os cenários testados, sugerindo que ele aprende padrões agnósticos de domínio para avaliar a correção de afirmações.

Significado e Alegações

O artigo alega que o LOVER representa um passo significativo rumo à construção de verificadores que não dependem do processo de supervisão caro. Ao tratar o verificador como uma variável latente binária e impor consistência lógica em múltiplos caminhos de raciocínio, o LOVER aproveita efetivamente o "conhecimento latente" dentro dos LLMs.

Os autores posicionam o LOVER como uma sonda não supervisionada guiada por regras lógicas, oferecendo uma alternativa prática aos verificadores supervisionados. Ele aborda as limitações dos métodos não supervisionados existentes (que são baseados em heurísticas e sensíveis à escolha do modelo, ou limitados a tipos específicos de perguntas) ao fornecer uma solução flexível e escalável para tarefas de raciocínio geral. O trabalho sugere que as restrições lógicas podem servir como priores eficazes para desbloquear as capacidades de raciocínio dos LLMs sem anotação humana.

Limitações Notadas: O método requer inerentemente acesso aos estados ocultos do LLM, restringindo sua aplicação a modelos de caixa branca e impedindo o uso direto em cenários de caixa preta.