When Many Answers Are Valid, Voting Fails: Symbolic Verification for Best-of-K Causal Reasoning in LLMs

Resumo Técnico: Quando Muitas Respostas São Válidas, a Votação Falha

Definição do Problema
Os métodos atuais de escalonamento em tempo de inferência para Grandes Modelos de Linguagem (LLMs), como o Self-Consistency, baseiam-se na premissa de que a resposta mais frequente entre os rastros de raciocínio amostrados é a mais confiável. Essa abordagem falha em tarefas de raciocínio causal onde múltiplas saídas distintas podem ser totalmente corretas (por exemplo, diferentes conjuntos de ajuste válidos que satisfazem o critério de backdoor de Pearl). Nesses cenários de "múltiplos satisfatores", a massa de probabilidade válida fragmenta-se entre várias strings de resposta, enquanto uma única resposta inválida pode dominar a votação simplesmente por ser o erro mais comum. Consequentemente, a votação de pluralidade exata pode selecionar uma resposta inválida mesmo quando a maioria dos rastros amostrados contém um raciocínio válido, levando a seleções inconsistentes e incorretas.

Metodologia: CALVER
Os autores introduzem o CALVER (Causal Axiom-Level VERification), um verificador simbólico livre de treinamento, projetado para selecionar o melhor candidato de um conjunto de $K$ rastros amostrados sem consultar uma resposta de referência.

• Contrato do Rastro (Trace Contract): O CALVER exige que os modelos gerem o raciocínio em um esquema tipado de seis slots: (1) Grafo, (2) Consulta (Query), (3) Estratégia, (4) Registro de Derivação, (5) Resultado Computado e (6) Resposta.
• Verificação Simbólica: Em vez de agregar frequências de respostas, o CALVER pontua cada rastro deterministicamente contra uma especificação causal executável. O verificador realiza seis verificações:
  1. Parsing do Grafo: Valida a estrutura do grafo (DAG ou ADMG).
  2. Vinculação da Consulta (Query Binding): Garante que as variáveis da consulta correspondam ao problema.
  3. Validade da Estratégia: Verifica se o conjunto proposto satisfaz critérios gráficos (ex: d-separação, m-separação, ajuste de backdoor, alcançabilidade de intervenção).
  4. Registro de Derivação: Verifica a sintaxe e a procedência das etapas de raciocínio.
  5. Resultado Computado: Recomputa independentemente o funcional (ex: Efeito Médio do Tratamento - ATE) para garantir consistência numérica.
  6. Consistência da Resposta: Confirma se a resposta final está alinhada com o resultado computado.
• Regra de Seleção: O selecionador escolhe o rastro com a maior pontuação (pontuação máxima implementada de 6). Empates são resolvidos selecionando o rastro mais antigo.
• Modos: O CALVER opera em dois modos:
  • Grafo Fornecido (Supplied-Graph): O grafo de origem é fornecido; os rastros são pontuados contra ele.
  • Grafo Construído (Constructed-Graph): O modelo deve extrair um grafo a partir de um texto; o rastro é pontuado contra seu próprio grafo reconstruído, enquanto a graduação final utiliza o grafo de origem oculto.

Principais Contribuições

1. Formulação: O artigo formula a seleção best-of-K sob multiplicidade de respostas como uma agregação sobre uma classe de validade decidível. O CALVER instancia isso com uma pontuação de rastro de seis componentes dependente do grafo para DAGs e ADMGs.
2. Teoria:
   • Solidez do Certificado de ATE Estrito: Os autores provam que um rastro de pontuação máxima que satisfaz guardas específicas (exclusão de tratamento e margem de decisão) garante uma decisão de limiar correta para consultas de Efeito Médio do Tratamento (ATE).
   • Teorema da Fragmentação de Validade: Eles provam que a pluralidade exata pode tornar-se inconsistente quando a massa de probabilidade válida é dividida entre múltiplas respostas válidas, permitindo que uma resposta inválida com uma massa individual ligeiramente superior vença.
3. Experimentos: Avaliação extensiva através de múltiplas famílias de modelos (Qwen, Mistral), famílias de grafos (CLEAR, bnlearn) e configurações (grafos fornecidos, construção de texto-para-grafo, enigmas lógicos).

Resultos

• Superioridade sobre Baselines: No benchmark CLEAR clean-core (126 problemas com múltiplas respostas válidas), o CALVER alcança 42,1% de acurácia, superando significativamente a pluralidade exata (~30,9%), um mediando consciente do conjunto (set-aware medoid), confiança do modelo, um modelo de recompensa aprendido (Skywork Reward V2) e um juiz LLM (mesmo escalado para 72B parâmetros).
• Escalonamento com $K$: A lacuna de desempenho entre o CALVER e a pluralidade aumenta conforme o orçamento de amostragem ($K$) aumenta. Enquanto o desempenho da pluralidade estagna, o CALVER continua a melhorar, atingindo 57,9% em $K=32$.
• Robustez à Recuperação de Grafo: Em configurações de texto-para-grafo onde a recuperação exata do grafo é baixa (ex: 34% em níveis narrativos naturalísticos), o CALVER ainda supera a pluralidade em 17,6 pontos percentuais. Isso demonstra que a verificação por candidato pode ter sucesso mesmo quando a estrutura global do grafo é reconstruída imperfeitamente, desde que as relações locais da consulta sejam preservadas.
• Generalização: O método transfere-se para benchmarks independentes (bnlearn, CausalGraph2LLM), diferentes famílias de modelos e domínios não causais (enigmas de lógica de Knights and Knaves) quando o predicado de verificação é adaptado (ex: consistência de tabela de verdade).
• Eficiência: A verificação simbólica adiciona um overhead mínimo (~7% sobre o custo de geração), pontuando cada rastro em 1–8 ms em um único thread de CPU.

Significância e Alegações
O artigo afirma que o CALVER fornece um sinal de seleção mais forte do que a frequência de superfície ou modelos de preferência aprendidos em regimes onde múltiplas respostas válidas existem. Estabelece que:

• A Votação Falha: A pluralidade exata é fundamentalmente falha para o raciocínio causal quando as respostas válidas fragmentam o voto.
• Validade Executável: Agregar com base na satisfação de uma classe de validade definida pela tarefa (via verificação simbólica) é mais confiável do que agregar com base na frequência da string de resposta.
• Regime Limitador: O método é mais eficaz no "regime intermediário", onde muitas respostas são válidas e nenhuma extração única é confiável. Quando as respostas são quase únicas, a votação padrão é suficiente; quando a extração de texto-para-grafo é altamente confiável, extrair um grafo e resolver diretamente é superior.
• Independência: O mecanismo de seleção baseia-se em predicados executáveis (axiomas causais ou regras lógicas) em vez de heurísticas aprendidas, tornando-o robusto entre diferentes arquiteturas de modelos e objetivos de treinamento.

Os autores enfatizam que o CALVER não pretende determinar a verdade científica sobre grafos causais do mundo real, mas sim selecionar o rastro de raciocínio formalmente mais válido dado a estrutura ou texto fornecido. A vantagem do método está estritamente ligada à capacidade de executar uma verificação de validade sobre o raciocínio do candidato.