💬 NLP

Designing FSMs Specifications from Requirements with GPT 4.0

Este artigo propõe um framework baseado em LLMs para gerar máquinas de estados finitos (FSM) a partir de requisitos textuais, complementado por uma abordagem centrada no especialista para corrigir os modelos gerados, apresentando uma análise experimental das capacidades dessas tecnologias na engenharia de sistemas orientada a modelos.

Autores originais: Omer Nguena Timo, Paul-Alexis Rodriguez, Florent Avellaneda

Publicado 2026-04-01

📖 5 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Omer Nguena Timo, Paul-Alexis Rodriguez, Florent Avellaneda

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

Imagine que você precisa construir um robô muito inteligente, mas você só pode falar com ele em "idioma humano" (texto comum), e ele precisa entender exatamente o que fazer em cada situação. O problema é que os humanos às vezes escrevem instruções de forma confusa, e o robô pode interpretar errado, causando acidentes ou falhas.

Este artigo é como um manual de instruções para usar um super-robô de texto (o GPT-4) para traduzir essas instruções humanas confusas em um diagrama de fluxo perfeito (chamado de Máquina de Estados Finitos ou FSM), que é o "cérebro" lógico do sistema.

Aqui está a explicação passo a passo, usando analogias do dia a dia:

1. O Problema: O Tradutor Imperfeito

Pense no GPT-4 como um tradutor super-rápido, mas que às vezes alucina.

A Entrada: Você dá ao tradutor um texto: "Quando o usuário clica no botão vermelho, se a bateria estiver baixa, o sistema deve apitar e ir para o modo de economia."
A Saída Esperada: Um diagrama lógico perfeito, onde cada seta (transição) e cada cor (estado) estão corretos.
O Perigo: Se o tradutor errar uma seta, o robô pode apitar quando não deve, ou pior, travar. Em sistemas reais (como freios de carros ou usinas de energia), um erro de tradução pode ser catastrófico.

2. A Solução: O "Tira-Teima" com o GPT-4

Os autores criaram um sistema onde o GPT-4 tenta desenhar esse diagrama lógico baseado no texto. Eles testaram isso com dados simulados (como se fossem "robôs de brinquedo" gerados por computador) para ver o quão bem o GPT-4 funciona.

O que eles descobriram?
O GPT-4 é ótimo, mas não é perfeito. Ele comete dois tipos principais de erros:

Esquecer uma regra: (Ex: O robô não sabe o que fazer se a bateria estiver cheia).
Mudar o resultado: (Ex: O robô apita em vez de desligar a tela).

3. A Parte Genial: Como Consertar os Erros (O "Mecânico")

Como o GPT-4 erra, os autores criaram 4 métodos diferentes de conserto, como se fossem diferentes tipos de mecânicos para o seu carro:

Método 1: O Mecânico "Olho no Olho" (Baseado em Sintaxe)

Como funciona: Imagine que você tem o manual original perfeito (o "Oráculo"). Você compara o desenho feito pelo GPT-4 com o manual.
A Ação: Você aponta para o GPT-4 e diz: "Você esqueceu essa seta aqui e desenhou essa outra errada. Corrija!".
Resultado: Funciona muito bem! O GPT-4 entende o erro específico e conserta quase tudo. É como ter um professor corrigindo a lição de casa linha por linha.

Método 2: O Detetive de Testes (Baseado em Sequências de Distinção)

Como funciona: Em vez de olhar o desenho, você dá um "teste" ao robô. "Se eu apertar o botão A, depois o B, o que acontece?".
A Ação: Se o robô errar a resposta, você diz: "Você errou nessa sequência específica. Tente de novo."
Resultado: Funciona, mas é mais difícil. O GPT-4 às vezes se perde porque tem que lembrar de muitas sequências de testes ao mesmo tempo. É como tentar consertar um quebra-cabeça olhando apenas as peças soltas, sem ver a imagem completa.

Método 3: O Teste Definitivo (Baseado em Sequência de Verificação)

Como funciona: Você cria um "teste mestre", uma sequência longa de comandos que, se o robô passar, significa que ele está 100% certo.
A Ação: Você pede ao GPT-4 para passar nesse teste. Se ele falhar, você pede para corrigir.
Resultado: É o método mais realista para o mundo real (onde não temos o manual perfeito), mas é lento e cansativo. Às vezes, o teste é tão longo que o GPT-4 se confunde.

Método 4: O Especialista em Falhas (Baseado em Modelos de Falha)

Como funciona: Os autores estudaram onde o GPT-4 costuma errar (ex: ele sempre esquece de apitar em certas situações). Eles criaram um "campo de reparo" que contém todas as versões possíveis de conserto baseadas nesses erros comuns.
A Ação: Em vez de pedir para o GPT-4 "adivinhar" o conserto, o sistema testa todas as variações possíveis dentro desse campo de erros comuns até encontrar a que funciona com os testes do especialista humano.
Resultado: É o método mais promissor e inteligente. Ele não depende do GPT-4 "pensar" na correção, mas sim de um sistema lógico que escolhe a melhor peça de reposição de uma caixa de ferramentas pré-definida.

4. A Conclusão Simples

O artigo diz que:

O GPT-4 é um ótimo assistente, mas não podemos confiar cegamente nele para criar sistemas críticos.
A qualidade do desenho cai conforme o sistema fica mais complexo (mais estados, mais botões). O GPT-4 perde o foco quando a informação é demais.
O segredo é a correção humana: A melhor maneira de usar essa tecnologia é deixar o GPT-4 fazer o "rascunho" e usar métodos automáticos (como os descritos acima) para encontrar e corrigir os erros, com a ajuda de um especialista humano apenas para validar os pontos mais críticos.

Em resumo: É como usar um estagiário super-inteligente (o GPT-4) para desenhar o plano de uma casa. Ele faz rápido, mas pode colocar uma janela no lugar errado. O papel do engenheiro (o sistema de reparo) não é desenhar a casa do zero, mas sim pegar o plano do estagiário, apontar a janela errada e garantir que, no final, a casa fique segura e perfeita.

1. Problema

O projeto de especificações formais para sistemas reativos, como Máquinas de Estado Finito (FSM) ou Máquinas de Mealy, é fundamental para análise, geração de código, teste e verificação de software. Tradicionalmente, essas especificações são derivadas de requisitos escritos em linguagem natural por engenheiros humanos, um processo demorado e propenso a erros.

A qualidade da especificação FSM é crítica: especificações de baixa qualidade levam a falhas que escapam das fases de teste, aumentando o risco de falhas catastróficas em produção. Embora modelos de linguagem grandes (LLMs) como o GPT-4 tenham mostrado potencial para automatizar a geração de código e especificações, ainda existem desafios significativos:

Precisão: LLMs podem gerar FSMs com erros sintáticos (ex: estados não determinísticos) ou semânticos (comportamento incorreto).
Correção: Métodos existentes para reparar modelos gerados automaticamente são complexos e muitas vezes não foram aplicados em abordagens baseadas em LLMs.
Dependência de Especialistas: A correção manual é custosa, exigindo métodos semi-automáticos que integrem o conhecimento de especialistas de forma eficiente.

2. Metodologia

Os autores propõem um framework baseado em LLM (utilizando o GPT-4/GPT-4o) para projetar FSMs a partir de descrições textuais em inglês, seguido por um conjunto de estratégias de reparo. O trabalho foi conduzido utilizando dados simulados para garantir a reprodutibilidade e o controle experimental.

Geração de Especificações

Engenharia de Prompt: Foi desenvolvido um processo de prompt engineering onde o LLM recebe uma descrição textual de uma máquina e é instruído a gerar uma representação rigorosa (formato CSV) da FSM.
Dados de Teste: Um módulo em Python gerou aleatoriamente FSMs "Oráculo" (corretas) e suas respectivas descrições textuais sintéticas (frases em inglês descrevendo transições).

Avaliação e Reparo

O framework avalia a correção da FSM gerada comparando-a com o Oráculo e aplica quatro abordagens distintas de reparo quando falhas são detectadas:

Reparo Baseado em Falhas Sintáticas:
- Assume-se a existência de um Oráculo FSM.
- Compara-se a FSM gerada com o Oráculo para identificar transições ausentes, extras, erros de saída ou de transferência.
- O prompt é refinado iterativamente, listando explicitamente as transições que devem ser adicionadas, removidas ou mantidas.
Reparo Baseado em Sequências de Distinção (Distinguishing Sequences):
- Foca na semântica (trajetórias de entrada/saída).
- Gera-se sequências de entrada que distinguem o comportamento do Oráculo do comportamento da FSM gerada.
- O prompt é atualizado com essas sequências e as saídas esperadas para forçar o LLM a corrigir o comportamento.
Reparo Baseado em Sequência de Verificação (Checking Sequence):
- Uma abordagem mais realista onde o especialista não conhece a estrutura interna da FSM, apenas o comportamento esperado.
- Utiliza-se uma única sequência de verificação (que distingue a FSM correta de todas as outras FSMs possíveis com $n$ estados).
- O especialista fornece a saída esperada para essa sequência, e o prompt é refinado com base nisso.
Reparo Baseado em Modelos de Falha (Fault Models) e Mutação:
- Utiliza o conhecimento prévio sobre os tipos de erros mais comuns cometidos pelo GPT-4 (ex: falhas de saída e transições ausentes).
- Constrói-se uma "Máquina de Mutação" (um FSM não determinístico) que define um domínio de reparo contendo todas as FSMs plausíveis geradas pela aplicação de mutações (patches) na FSM original.
- Um algoritmo (baseado em SAT) interage com um especialista para eliminar FSMs incorretas desse domínio até encontrar a correta, sem depender de novos prompts de geração para o LLM.

3. Contribuições Principais

Geração de Dados Simulados: Criação de um conjunto de dados com FSMs oráculo aleatórias e suas descrições textuais para avaliação sistemática.
Framework de Geração e Reparo: Proposta de um pipeline completo que vai da descrição textual à FSM executável, incluindo mecanismos de correção.
Estratégias de Reparo Diversificadas: Desenvolvimento e avaliação de quatro métodos distintos de reparo, variando de correções sintáticas diretas a abordagens semânticas complexas e mineração de domínios de reparo.
Análise Empírica de LLMs: Avaliação detalhada da capacidade do GPT-4 em gerar especificações corretas e sua resposta a prompts de correção iterativos.

4. Resultados Experimentais

Os experimentos foram realizados com FSMs de 5, 10 e 25 estados.

Geração Inicial: O GPT-4 demonstrou capacidade de gerar FSMs corretas, mas a taxa de erro aumentou com a complexidade (número de estados e transições). As falhas mais comuns foram falhas de saída e transições ausentes.
Reparo Sintático: Teve 100% de sucesso na correção das FSMs falhas (para máquinas de 5 e 10 estados) em poucas iterações. Isso indica que, quando o LLM recebe instruções sintéticas precisas sobre o que corrigir, ele consegue ajustar o modelo.
Reparo por Sequências de Distinção: Teve desempenho inferior (0% de sucesso em máquinas de 10 estados). A conclusão é que o mecanismo de atenção do LLM tem dificuldade em processar grandes volumes de informações de entrada/saída simultaneamente para inferir a estrutura correta.
Reparo por Sequência de Verificação: Teve sucesso parcial (40% em máquinas de 5 estados). O cálculo de sequências de verificação é computacionalmente caro (NP-completo) e a complexidade da sequência única dificultou a correção pelo LLM.
Reparo por Modelos de Falha: Alcançou 100% de sucesso em todos os casos testados. Ao delimitar o espaço de busca (domínio de reparo) e usar métodos formais para filtrar as opções com base em consultas ao especialista, o método provou ser robusto e não dependente da capacidade de "raciocínio" do LLM para a correção final.

5. Significado e Conclusão

O artigo demonstra que, embora os LLMs sejam ferramentas poderosas para a geração inicial de especificações formais a partir de requisitos naturais, eles não são infalíveis e sofrem com a degradação de desempenho à medida que a complexidade do sistema aumenta.

A principal lição é que a correção automática pura via prompt engineering (tentar fazer o LLM corrigir a si mesmo apenas com exemplos de comportamento) é ineficiente para sistemas complexos. Em vez disso, a abordagem mais promissora é híbrida:

Usar o LLM para a geração inicial.
Usar métodos formais (como mutação e mineração de domínios) para delimitar o espaço de soluções possíveis.
Envolver especialistas humanos apenas para validar comportamentos críticos (saídas de sequências de teste) dentro desse espaço delimitado.

Este trabalho abre caminho para a integração de IA generativa em Engenharia de Sistemas Orientada a Modelos (MDE), sugerindo que o futuro reside na combinação da capacidade de geração de linguagem natural com a rigorosidade e eficiência dos métodos formais de verificação e reparo.