Resumo Técnico: LLMs Dependem de Priores, Não da Semântica de Linguagens de Programação

Declaração do Problema

Os atuais modelos de linguagem de grande escala (LLMs) são cada vez mais implantados para resolver tarefas de programação que ostensivamente exigem o raciocínio sobre o comportamento de programas, como prever saídas, reparar código ou gerar novo código. Uma questão fundamental permanece aberta: esses modelos dependem primariamente de regularidades estatísticas adquiridas durante o pré-treinamento (priores lexicais) ou podem condicionar flexivelmente seu raciocínio a regras comportamentais explicitamente fornecidas?

Embora os LLMs frequentemente tenham um bom desempenho em tarefas de programação padrão, não está claro se eles conseguem adaptar seu raciocínio a sistemas formais especificados externamente quando esses sistemas conflitam com os priores arraigados aprendidos nos dados. Por exemplo, se o símbolo '+' for explicitamente definido para realizar uma subtração em um conjunto de regras fornecido, um modelo que depende de priores provavelmente ainda outputará uma adição, enquanto um modelo condicionado às regras se adaptará. Este artigo investiga se os LLMs podem condicionar seu raciocínio em semânticas formais através da execução de programas, testando especificamente sua capacidade de sobrescrever associações de significado de símbolos aprendidas em favor de regras de inferência fornecidas.

Metodologia

Os autores introduzem o PLSEMANTICSBENCH, um benchmark orientado à semântica projetado para sondar o raciocínio condicionado por regras sob mudanças controladas de distribuição. A metodologia envolve três componentes principais:

1. Formalismo e Linguagem

O benchmark utiliza uma linguagem imperativa de peso leve, C⋆, derivada do C, mas simplificada para evitar ambiguidades sintáticas (ex: delimitadores de bloco explícitos {} são usados para evitar problemas de sensibilidade à indentação encontrados no Python). A linguagem é pareada com dois sistemas semânticos formais distintos:

• Semântica Operacional Estrutural de Passo Único (S): Um sistema de grão fino onde cada regra representa um passo de computação atômico.
• Semântica K (K): Um sistema de reescrita mais grosseiro.

Esses formalismos permitem a alteração sistemática das definições de regras sem alterar a sintaxe de superfície dos programas.

2. Deslocamentos Semânticos e Estressores

Para desacoplar o raciocínio semântico da familiaridade sintática, o benchmark introduz dois tipos de mutações semânticas:

• KeywordSwap: Operadores sintáticos selecionados (ex: +, -) trocam suas interpretações semânticas. Por exemplo, + é definido para realizar subtração. Isso cria um conflito direto com os priores de pré-treinamento enquanto preserva a sintaxe de superfície.
• KeywordObf: Palavras-chave e operadores padrão são substituídos por novos símbolos (extraídos do alfabeto caucasiano-albanês) cujos significados são definidos apenas pelas regras fornecidas. Isso remove todos os priores sintáticos.

O benchmark avalia os modelos em três divisões de dataset com complexidade estrutural crescente:

• Escrito por Humanos: Programas adaptados de benchmarks de codificação padrão (LeetCode, HumanEval, etc.).
• Traduzido por LLM: Soluções em C++ traduzidas para C⋆ por LLMs.
• Gerado por Fuzzer: Programas gerados automaticamente por um fuzzer consciente de semântica e com controle de profundidade para maximizar a complexidade de fluxo de controle e fluxo de dados.

3. Tarefas de Avaliação

O benchmark sonda quatro hipóteses específicas sobre as capacidades dos modelos:

• H1 (Condicionamento de Regra Global): Os modelos conseguem compor múltiplas aplicações de regras para prever corretamente os estados finais do programa? (Tarefa: PredState)
• H2 (Condicionamento de Regra Independente de Estado): Os modelos conseguem selecionar as regras operacionais corretas quando o estado do programa não muta? (Tarefa: PredRule)
• H3 (Condicionamento de Regra de Longo Horizonte): Os modelos conseguem sustentar o raciocínio condicionado por regras através de rastros de execução longos (loops, fluxo de controle aninhado)? (Tarefa: PredTrace)
• H4 (Condicionamento de Regra sob Deslocamento Semântico): Os modelos continuam a seguir as regras fornecidas sob novas semânticas que conflitam com os priores?

O estudo avalia 11 LLMs de fronteira, incluindo modelos de não-raciocínio (ex: Llama-3.3, Qwen2.5-Inst) e modelos orientados ao raciocínio (ex: variantes do DeepSeek-R1, O3-mini, GPT-5-mini, Gemini-2.5-pro).

Contribuições Principais

1. PLSEMANTICSBENCH: O primeiro benchmark de larga escala explicitamente projetado para testar se os LLMs condicionam o raciocínio em regras formais em vez de priores estatísticos, utilizando a execução de programas como uma sonda controlada.
2. Deslocamentos Semânticos Formais: A introdução das transformações KeywordSwap e KeywordObf que perturbam sistematicamente os mapeamentos de símbolo-significado enquanto preservam a estrutura da regra, permitindo o isolamento da dependência de associações lexicais versus definições formais.
3. Análise Granular de Raciocínio: Uma decomposição do raciocínio de execução de programas em previsão de estado global, seleção de regra local e geração de rastro de longo horizonte, revelando modos específicos de falha nos modelos atuais.
4. Avaliação Empírica Abrangente: Uma avaliação sistemática através de 11 modelos, três complexidades de dataset e dois formalismos semânticos, fornecendo um mapa detalhado das capacidades e limitações atuais.

Resultados

Os experimentos produzem várias descobertas críticas:

• Dependência de Priores: Sob semântica padrão, muitos modelos alcançam alta precisão (até 90%) em tarefas simples. No entanto, sob mutações semânticas (KeywordSwap), o desempenho cai drasticamente entre 40 a 60 pontos percentuais. Isso indica que os modelos dependem predominantemente de associações lexicais pré-treinadas em vez das regras formais fornecidas.
• Sensibilidade ao Deslocamento Semântico: A mutação KeywordSwap causa uma degradação de desempenho significativamente maior do que a KeywordObf. Isso sugere que a presença de sintaxe familiar (mesmo com significado alterado) dispara respostas baseadas em priores fortes que os modelos falham em sobrescrever.
• Fragilidade de Longo Horizonte: Sustentar o raciocínio condicionado por regras em rastros de execução longos é extremamente frág ability (frágil). Apenas um punhado de modelos alcança precisão não nula na tarefa PredTrace, e mesmo os melhores sistemas atingem apenas ~35% de precisão. A maioria dos modelos colapsa para precisão zero quando exigido o rastreamento de estado e a aplicação repetida de regras ao longo de dezenas de passos.
• Impacto da Complexidade: O desempenho deteriora-se sistematicamente com o aumento da complexidade estrutural (profundidade de fluxo de controle, dependências de fluxo de dados). Embora modelos orientados ao raciocínio se beneficiem do acesso a regras formais em programas simples escritos por humanos, essa vantagem muitas vezes desaparece ou se inverte em programas complexos gerados por fuzzer.
• Limitações do Chain-of-Thought (CoT): O prompting de CoT aumenta o desempenho em semântica padrão para modelos de não-raciocínio, mas falha em superar o viés introduzido por trocas semânticas, indicando que rastros de raciocínio sozinhos não permitem que os modelos sobrescrevam priores de operadores arraigados.
• Compreensão de Notação: Os modelos demonstram, em geral, alta competência em entender a notação formal (tarefas NL→Regra e Regra→NL), sugerindo que as falhas nas tarefas de execução decorrem de limitações de raciocínio e não de uma incapacidade de processar o formalismo.

Significância e Alegações

O artigo posiciona o condicionamento de regra inferencial como um eixo de capacidade amplamente não resolvido para sistemas de aprendizagem em linguagens de programação. Os autores afirmam que os LLMs contemporâneos frequentemente falham em condicionar seu raciocínio em sistemas formais especificados externamente quando estes conflitam com os priores derivados de dados.

A significância deste trabalho reside em:

1. Capacidade Diagnóstica: Fornecer um método rigoroso para distinguir entre o emparelhamento de padrões estatísticos e o verdadeiro seguimento de regras em LLMs.
2. Identificação de Limitações: Destacar que os modelos atuais carecem da robustez para se adaptar a novas semânticas formais, um requisito crítico para aplicações envolvendo sobrecarga de operadores, linguagens de domínio específico (DSLs) e verificação formal.
3. Direção Futura: Motivar o desenvolvimento de modelos que possam raciocinar de forma mais fiel sobre especificações formais, indo além da dependência de "associações lexicais arraigadas" em direção a sistemas capazes de verdadeiro raciocínio condicional baseado em regras fornecidas.

Os autores concluem que, embora os LLMs mostrem promessa em tarefas de execução padrão, sua capacidade de condicionar o raciocínio em regras formais explícitas permanece um gargalo significativo, particularmente sob deslocamentos semânticos e horizontos de execução longos.