Reducing Hallucinations in LLM-Generated Code via Semantic Triangulation

1. O Problema

Os Grandes Modelos de Linguagem (LLMs) são capazes de gerar código executável a partir de descrições em linguagem natural. No entanto, essa capacidade vem com um custo significativo: os programas gerados frequentemente contêm bugs ou vulnerabilidades devido a alucinações (ou confabulações) do modelo.

O desafio central identificado pelos autores é a correlação de erros. Quando se tenta validar a correção do código gerado (por exemplo, através de votação por pluralidade ou testes gerados pelo próprio LLM), os métodos falham porque:

• Votação por Pluralidade: Se o modelo tende a cometer o mesmo erro em várias amostras (erro correlacionado), a votação majoritária selecionará o erro mais comum em vez da solução correta.
• Proxies Corrompidos: Métodos que usam testes ou especificações formalizadas automaticamente pelo mesmo LLM falham porque o "testador" ou o "especificador" compartilha a mesma lógica falha e as mesmas alucinações do "gerador", corroborando erroneamente o código defeituoso.
• Problemas Inexatos: Muitos problemas de programação permitem múltiplas soluções corretas não equivalentes, o que torna difícil estabelecer um consenso baseado apenas na similaridade de saída.

2. Metodologia: Triangulação Semântica

Os autores propõem a Triangulação Semântica, um framework teórico e prático que visa "descorrelacionar" os erros do modelo. A ideia central é transformar o problema original em uma variante dissociativa que exige um algoritmo fundamentalmente diferente, mas que mantém uma relação verificável com a solução original.

Princípios Teóricos

O framework baseia-se em duas propriedades fundamentais para a transformação do problema ($\tau$) e a relação de verificação ($\phi$):

1. Indução de Bijetividade (Bijection-Inducing): A transformação deve estabelecer uma correspondência um-para-um entre as classes de equivalência de programas. Isso garante que erros distintos no problema original sejam mapeados para erros distintos no problema transformado, tornando improvável que dois programas incorretos gerados independentemente coincidam sob a transformação.
2. Acoplamento de Correção (Correctness-Coupling): A correspondência deve preservar a correção. Uma solução correta para o problema original deve mapear para uma solução correta para o problema transformado.

Transformações Dissociativas

Para garantir que o LLM não consiga manter a mesma "mentira" (alucinação) em ambas as versões, o sistema aplica transformações que exigem algoritmos diferentes. O paper propõe quatro métodos concretos:

• Inversão de Problema (FWD-INV / FWD-SINV): Transforma o problema original em sua inversa (ex: de "gerar saída a partir de entrada" para "gerar entrada a partir de saída"). Para problemas não bijetivos, usa-se Inversão de Conjunto (Set-valued Inverse), que retorna todos os inputs possíveis para uma dada saída.
• Enumeração de Respostas (ENUM-SINV): Transforma o problema em um que enumera todas as soluções válidas para uma entrada. Isso é crucial para problemas inexatos.
• Decomposição (STREAM): Para problemas de processamento de fluxo, decompõe o problema em operações ponto a ponto.

O Fluxo de Trabalho (Ferramenta just-tri-it)

1. O LLM gera soluções para o problema original ($d$).
2. O sistema usa o LLM para transformar $d$ em problemas derivados ($d'$ e $d''$), como enumeração e inversão parcial.
3. O LLM gera soluções para esses problemas derivados.
4. O sistema verifica a consistência entre as soluções usando hiperpropriedades (como ENUM-SINV ou FWD-SINV).
5. Se uma solução para $d$ for consistente com uma solução validada para $d'$, ela é considerada um "testemunho de plausibilidade" e selecionada. Caso contrário, o sistema pode abster-se de escolher uma resposta.

3. Contribuições Principais

• Framework Teórico: Introdução da Triangulação Semântica, fundamentada em modelos matemáticos de alucinação de LLMs (considerando-os "papagaios estocásticos" com erros correlacionados). O paper prova que, sob certas suposições, a triangulação aumenta a probabilidade de identificar o código correto em comparação com a votação por pluralidade.
• Provas Mecanizadas: Todas as quatro metodologias de triangulação foram formalmente provadas no assistente de prova Lean, garantindo que as transformações e hiperpropriedades satisfaçam os requisitos teóricos de bijetividade e acoplamento.
• Ferramenta Prática (just-tri-it): Implementação de um sistema que automatiza a transformação de problemas, geração de soluções e verificação de consistência.
• Solução para Problemas Inexatos: É o primeiro método capaz de lidar consistentemente com problemas que admitem múltiplas soluções válidas não equivalentes, um cenário onde métodos anteriores falham.

4. Resultados Experimentais

A ferramenta foi avaliada nos benchmarks LiveCodeBench (LCB) e CodeElo (focando em problemas inexatos), utilizando modelos de ponta como GPT-4o, DeepSeek-V3 e Gemini 2.5 Flash.

• Melhoria na Seleção: A triangulação aumentou a probabilidade de selecionar um programa correto em 24% em comparação com as melhores linhas de base (geração de testes, metamorfismo e especificações auto-formalizadas).
• Desempenho em Abstenção: Em cenários de "seleção ou abstenção" (onde o sistema recusa responder se não tiver confiança), o método alcançou um F1-score de abstenção 26% maior que as linhas de base.
• Robustez em Baixa Probabilidade: Diferente de métodos que só selecionam soluções com alta probabilidade de amostragem ($\ge 0.5$), a triangulação conseguiu identificar corretamente soluções com probabilidade de amostragem tão baixa quanto 0.07, permitindo resolver tarefas mais difíceis com confiabilidade.
• Problemas Inexatos: Foi a única metodologia que lidou consistentemente com problemas inexatos, superando significativamente a votação por pluralidade e métodos baseados em testes.
• Custo: O método exige mais tempo e tokens (aprox. 2.5x mais tempo e 4.9x mais tokens que a pluralidade simples), mas oferece um ganho substancial em confiabilidade.

5. Significado e Impacto

Este trabalho representa um avanço significativo na garantia de qualidade de código gerado por IA.

• Mudança de Paradigma: Move-se da ideia de "verificar se o código passa nos testes" para "verificar se o código é consistente com uma solução de um problema semanticamente diferente".
• Segurança Teórica: Ao provar que a triangulação reduz a probabilidade de erros correlacionados através de desigualdades matemáticas (como a desigualdade de rearranjo), o trabalho oferece uma base teórica sólida para técnicas de consenso em LLMs.
• Aplicabilidade Prática: Demonstra que é possível construir sistemas robustos de verificação de código que não dependem de oráculos perfeitos, mas sim de consistência cruzada entre tarefas relacionadas, sendo especialmente útil para problemas complexos e ambíguos onde a validação tradicional falha.

Em resumo, a Triangulação Semântica oferece uma abordagem "caixa-preta" rigorosa para mitigar alucinações, transformando a verificação de código de um problema de consenso cego em um processo de validação cruzada estruturada e matematicamente fundamentada.