🤖 AI

Faithful Autoformalization of Natural Language Assertions

O artigo apresenta o Monty, um framework de autoformalização que melhora a precisão da síntese de asserções executáveis a partir de linguagem natural ao filtrar as saídas geradas por LLMs usando novas pontuações de conformidade e validade, alcançando um ganho de precisão média de até 20 pontos sobre métodos de tradução ingênuos.

Autores originais: Hongyi Liu, Madhusudan Parthasarathy, Adithya Murali

Publicado 2026-07-16

📖 7 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Hongyi Liu, Madhusudan Parthasarathy, Adithya Murali

Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

O Dilema do Tradutor: Quando o Código Encontra as Palavras Humanas

Imagine que você está construindo uma cidade digital massiva. Para manter o tráfego fluindo e os edifícios de pé, cada esquina e arranha-céu precisa de um livro de regras. No mundo do software, esses livros de regras são chamados de "especificações formais". Elas são instruções matemáticas precisas que dizem ao computador exatamente o que um pedaço de código deve fazer e o que ele nunca deve fazer. Pense nelas como as leis inquebráveis da física para um mundo digital. O problema é que escrever essas leis é incrivelmente difícil. Requer um nível de precisão que parece falar uma linguagem inteiramente diferente, uma que a maioria dos programadores humanos considera tediosa e propensa a erros.

Surge o problema da "Autoformalização". Esta é a busca para pegar uma ideia desordenada de um humano, em linguagem natural — como "não deixe a lista ficar muito grande" — e traduzi-la automaticamente para aquele código matemático rigoroso. Durante anos, cientistas tentaram usar Inteligência Artificial (IA), especificamente Modelos de Linguagem de Grande Escala (LLMs), para agir como tradutores. Esses modelos de IA são como poliglotas superinteligentes que leram quase tudo o que já foi escrito. Eles são ótimos em adivinhar o que uma frase significa. Mas aqui está o detalhe: quando você pede a uma IA para traduzir um pensamento humano vago em um contrato legal estrito, ela frequentemente alucina. Ela pode inventar regras que não existem, omitir um detalhe minúsculo que quebra todo o sistema ou traduzir confiantemente um "talvez" em um "com certeza". A questão central que este artigo aborda é: Como podemos confiar em um tradutor de IA quando os riscos são altos e as instruções humanas são imprecisas?

Conheça o Monty: O Detetive que Verifica o Dever de Casa da IA

Este artigo apresenta um novo framework chamado Monty, um sistema projetado para ser um editor cético e detalhista para as regras de código geradas por IA. Os autores, pesquisadores da Universidade de Wisconsin-Madison e da Universidade de Illinois, perceberam que simplesmente pedir a uma IA para traduzir uma frase em código não é suficiente. Se você pedir a uma IA para traduzir "a lista deve estar vazia", ela pode adivinhar que isso significa "a lista tem zero itens" ou "a lista não tem itens de forma alguma". Ambos parecem certos, mas no código de computador, eles podem significar coisas muito diferentes.

O Monty não apenas confia na primeira resposta que a IA dá. Em vez disso, ele age como um detetive executando uma série de testes. Veja como a história se desenrola:

1. A IA Gera uma Multidão de Suspeitos
Primeiro, o Monty pede a um Modelo de Linguagem de Grande Escala para traduzir uma asserção em linguagem natural (uma frase humana) em código formal. A IA não dá apenas uma resposta; ela gera uma multidão de traduções "candidatas". Algumas podem ser perfeitas, outras podem estar ligeiramente erradas e algumas podem estar completamente incorretas.

2. O Teste de "Fuzz": Quebrando o Código
Em seguida, o Monty submete essas traduções candidatas a um teste de estresse chamado "fuzzing". Imagine um robô lançando entradas aleatórias e selvagens contra o código para ver se ele trava ou se comporta de maneira estranha.

Se uma tradução candidata trava o computador ou gera um erro, o Monty a descarta imediatamente.
Se a tradução funciona, mas falha em corresponder à lógica da frase humana original, ela recebe uma pontuação baixa.
Crucialmente, o Monty não assume que a frase humana é correta. Às vezes, um programador escreve uma regra que é, na verdade, errada (uma regra "com bug"). O Monty é inteligente o suficiente para perceber que uma tradução válida de uma regra "com bug" ainda é um bug. Ele procura tanto pela tradução correta mais provável quanto pela tradução incorreta mais provável para ver qual delas se ajusta ao contexto.

3. A Verificação de "Cobertura de Cláusulas": A Tradução Reversa
Esta é a arma secreta do Monty. Para verificar se uma tradução de IA é verdadeiramente fiel, o Monty usa um truque inteligente chamado cobertura de cláusulas (clausal coverage). Ele pega o código formal da IA e pede à própria IA para traduzi-lo de volta para o inglês simples (ou linguagem natural). Então, ele compara essa nova frase em inglês com a frase humana original.

A IA esqueceu alguma parte da frase original?
Ela adicionou algo que não estava lá?
Ela mudou o significado?
A IA atua como um juiz, dando uma pontuação baseada em quão bem as partes (cláusulas) das duas frases coincidem. Se a tradução reversa estiver faltando um detalhe fundamental, a pontuação cai e esse candidato é filtrado.

4. O Confronto Final: Aprendizado Ativo
Às vezes, a IA gera dois candidatos que parecem perfeitos e passam em todos os testes, mas que significam coisas ligeiramente diferentes. É aqui que a "ambiguidade" da linguagem humana morde de volta. Nesses casos raros, o Monty não adivinha. Ele utiliza aprendizado ativo (active learning). Ele encontra um cenário específico (uma "valoração distintiva") onde os dois candidatos se comportariam de maneira diferente. Ele então faz uma pergunta simples a um humano (ou a um oráculo simulado): "Neste caso específico, qual regra você realmente quis dizer?". O humano escolhe o vencedor, e o Monty fixa a tradução correta.

O Que o Monty Descobriu

Os pesquisadores testaram o Monty em 541 tarefas diferentes envolvendo código Java, que é uma linguagem de programação popular. Eles usaram conjuntos de dados que incluíam tanto regras perfeitamente escritas quanto regras intencionalmente quebradas para ver se o Monty conseguiria lidar com a bagunça da vida real.

Os resultados foram promissores. Quando deixaram a IA traduzir naturalmente sem a ajuda do Monty, a precisão foi decente, mas longe de ser perfeita. Por exemplo, usando um modelo específico chamado Qwen2.5-Coder, a IA bruta acertou a tradução cerca de 75% das vezes em um conjunto de dados. Mas quando o Monty interveio para filtrar e verificar as respostas, essa precisão saltou para 91,6%. Em outro conjunto de dados, subiu de 64% para 85%.

O artigo sugere que o Monty é particularmente bom em corrigir o problema da "precisão". Isso significa que, quando o Monty diz: "Aqui está a regra correta", você pode confiar muito mais do que quando apenas pergunta a uma IA e aceita sua primeira resposta. Ele conseguiu fazer isso sem descartar muitas respostas corretas (mantendo o "recall" alto).

O Que o Monty Não Faz

É importante saber o que este artigo não está alegando. O Monty não é uma varinha mágica que resolve todos os problemas de programação.

Ele não tenta descobrir a "intenção" de alto nível de um projeto de software inteiro (como "construa para mim um aplicativo de rede social"). Ele foca estritamente em traduzir regras específicas e localizadas para partes individuais de código.
Ele não afirma ter resolvido o problema da ambiguidade para sempre. Às vezes, a entrada humana é tão vaga que até o Monty precisa que um humano intervenha para esclarecer.
Os autores argumentam explicitamente contra a ideia de que devemos apenas assumir que toda regra escrita por um programador é correta. Muitas ferramentas antigas assumiam que, se uma regra foi escrita, ela devia ser verdadeira. O Monty rejeita isso, mostrando que, às vezes, o objetivo é encontrar a regra que falha, provando que o código possui um bug.

A Conclusão

No fim, o Monty sugere que o futuro de escrever código não é apenas pedir que a IA faça o trabalho. É construir um sistema onde a IA gera ideias, mas um processo rigoroso e inteligente as verifica contra a realidade. Ao combinar a criatividade da IA com o ceticismo dos testes e a precisão da "tradução reversa", o Monty mostra um caminho para tornar o software mais seguro e confiável, transformando os pensamentos desordenados e ambíguos dos desenvolvedres humanos nas leis limpas e inquebráveis do mundo digital. O artigo sugere que, embora ainda não tenhamos chegado lá, essa abordagem de "verificar o próprio trabalho" é um passo significativo para tornar a IA uma parceira confiável no desenvolvimento de software.

Resumo Técnico: Autoformalização Fiel de Asserções em Linguagem Natural

Declaração do Problema

O artigo aborda o desafio da autoformalização confiável: a síntese de asserções formais executáveis (por exemplo, em Java Modeling Language, JML) a partir de especificações em linguagem natural (LN). Embora os Grandes Modelos de Linguagem (LLMs) ofereçam um caminho para preencher a lacuna entre a intenção informal do desenvolvedor e as especificações formais, as abordagens atuais sofrem de dois problemas críticos:

Infidelidade: Os LLMs frequentemente geram formalizações que não refletem com precisão o conteúdo semântico da asserção original em LN.
Ambiguidade: A linguagem natural é inerentemente ambígua. Trabalhos existentes frequentemente assumem implicitamente que a asserção em LN descreve uma propriedade válida do código. No entanto, em contextos como busca de bugs ou testes de código gerado por IA, a asserção pode ter a intenção de ser inválida (ou seja, para revelar uma falha). Assumir a validade pode levar ao descarte da formalização correta se o código estiver com bug, ou à aceitação de uma formalização que falha em verificar a intenção do usuário.

O objetivo é produzir uma formalização que seja fiel à especificação em LN, independentemente de a asserção resultante ser válida ou inválida em relação à implementação do código.

Metodologia: O Framework Monty

Os autores propõem o Monty, um framework que combina geração por LLM com teste de programas e aprendizado ativo para resolver ambiguidades e garantir a fidelidade. O pipeline consiste em quatro estágios:

1. Geração de Candidatos

Dada uma classe de módulo de código, assinaturas de métodos, documentação e uma especificação em LN, um LLM é instruído a gerar múltiplas especificações candidatas ( $\psi_1, \dots, \psi_n$ ) em uma lógica executável (JML).

2. Filtragem e Pontuação

Os candidatos são avaliados usando dois sinais complementares:

Pontuação de Validade (Nível de Execução): Um gerador de testes (Randoop) cria entradas de teste para verificar os candidatos.
- Verificação Sintática: Garante que o código compile.
- Verificação de Segurança de Fuzz (Fuzz-Safety): Garante que a asserção não lance exceções de tempo de execução.
- Verificação Semântica de Fuzz (Fuzz-Semantic): Determina se a asserção é testável-válida ou testável-inválida para o método dado.
- Nota: O framework não descarta candidatos simplesmente porque são testáveis-inválidos; ele os preserva para lidar com casos onde o usuário pretende encontrar bugs.
Pontuação de Conformidade (Nível Semântico): Uma métrica inovadora chamada Cobertura Clausal é utilizada.
- O candidato formal é traduzido de volta para linguagem natural por um LLM.
- Um segundo LLM (atuando como juiz) compara a estrutura clausal desta descrição em LN gerada com a asserção original em LN.
- Ele verifica a Solidez (a descrição cobre todas as cláusulas da original?) e a Completude (contém informações extras/conflitantes?).
- Uma pontuação em $[-1, 1]$ é atribuída, onde $+1$ indica conformidade perfeita. Candidatos abaixo de um limite (ex: 0,6) são descartados.

3. Matriz de Decisão

O sistema seleciona as formalizações "mais provavelmente fiéis" separando os candidatos em dois grupos baseados na verificação de validade:

O candidato com a maior pontuação de conformidade entre aqueles que são testáveis-válidos.
O candidato com a maior pontuação de conformidade entre aqueles que são testáveis-inválidos.
Esta abordagem reconhece que a "correta" formalização depende da intenção do usuário (documentação vs. busca de bugs) e evita o viés de presumir a validade.

4. Desambiguação por Aprendizado Ativo

Se tanto um candidato válido quanto um inválido permanecerem (e ambos tiverem alta pontuação de conformidade), o sistema identifica uma valoração de distinção (um estado de entrada específico) onde os dois candidatos diferem.

O sistema consulta o usuário (ou um oráculo em avaliação) para determinar qual candidato satisfaz a especificação pretendida para esta valoração específica.
O sistema então seleciona a formalização correspondente.

Principais Contribuições

Framework de Autoformalização Fiel: Um pipeline que gera tanto formalizações provavelmente válidas quanto provavelmente inválidas, abordando a limitação de trabalhos anteriores que assumem que as asserções devem ser válidas.
Verificação de Conformidade por Cobertura Clausal: Uma técnica inovadora usando LLM-como-Juiz para avaliar a sobreposição semântica entre LN e asserções formais via tradução de ida e volta e análise de cobertura de cláusulas. O artigo afirma que isso supera os baselines padrão de Inferência de Linguagem Natural (NLI).
Desambiguação por Aprendizado Ativo: Um mecanismo para resolver ambiguidades inerentes à LN gerando casos de teste específicos que distinguem entre candidatas formais fiéis concorrentes.
Novas Suítes de Benchmarks: Os autores curaram conjuntos de dados contendo 541 tarefas de geração de asserção em 22 classes semelhantes a coleções Java. Estes incluem:
- C2S-Augmented: Especificações em LN geradas sinteticamente a partir de asserções formais.
- Datasets com Bugs: Cenários com código com bugs ou asserções intencionalmente incorretas/enganosas.
- Especificações em LN Manuais: Especificações escritas por humanos para testar a generalização.

Resultados Experimentais

Os autores avaliaram o Monty em 541 tarefas usando vários modelos de backbone (incluindo GPT-oss, Qwen2.5-Coder e modelos maiores).

Melhoria na Precisão: O Monty melhora significamente a precisão da autoformalização em comparação com o uso "One-shot" ingênuo de LLM.
- No dataset C2S-Augmented, o Qwen2.5-Coder (32B) melhorou a precisão de 75% para 91,6%.
- No dataset de LN Manual, a precisão melhorou de 64,1% para 85,2%.
Manutenção do Recall: O processo de filtragem mantém um alto recall (ex: 97,6% para GPT-oss em C2S-Aug), indicando que candidatos corretos raramente são descartados.
Robustez à Ambiguidade: O framework lida com sucesso com datasets "Buggy", onde a asserção pretende ser inválida, um cenário onde LLMs ingênuos frequentemente falham ou alucinam asserções válidas.
Estudos de Ablação:
- O método de Cobertura Clausal superou os baselines (incluindo NLI e verificações simples de ida e volta) em métricas de AUC.
- Informações contextuais (assinaturas de código, docs) mostraram ser críticas para a qualidade do ranking.
- O aprendizado ativo foi invocado em uma pequena fração dos casos (onde candidatos válidos/inválidos passaram na conformidade), mas provou ser eficaz (100% de precisão nos casos elegíveis para GPT-oss).

Significância e Alegações

O artigo afirma que o Monty fornece um caminho mais confiável para a autoformalização ao abordar explicitamente a ambiguidade da linguagem natural e a incerteza da validade da asserção.

Confiabilidade: Ao filtrar pela conformidade e separar candidatos válidos/inválidos, a ferramenta produz formalizações que têm maior probabilidade de serem traduções fiéis da intenção do desenvolvedor.
Praticidade: A abordagem não requer ajuste fino (fine-tuning) de modelos; ela depende de prompting, testes e uma matriz de decisão, tornando-a aplicável aos LLMs existentes.
Limitações: Os autores observam que a abordagem depende de asserções em LN localizadas (nível de módulo) e não tenta formalizar a intenção de aplicação de alto nível ou minerar especificações de documentação não estruturada sem um alvo de método específico. O componente de aprendizado ativo requer interação do usuário, embora o sistema minimize isso consultando apenas quando necessário.

O trabalho posiciona-se como um passo em direção ao desenvolvimento orientado por especificação com IA, onde especificações legíveis por humanos são criadas e, em seguida, rigorosamente verificadas contra o código usando autoformalização e testes.