Pós-Graduação em Ciência da Computação – UFPE
Defesa de Dissertação de Mestrado Nº 2.250
Aluno: Gabriel Nogueira Leite
Orientador: Prof. Augusto Cezar Alves Sampaio
Coorientador: Prof. Filipe Marques Chaves de Arruda (IFPE – Recife)
Título: Generating formal smart-contract specifications from
natural-language requirements supported by LLM
Data: 21/11/2025
Hora/Local: 15h – Virtual – Interessados em assistir entrar em contato com o aluno
Banca Examinadora:
Prof. Alexandre Cabral Mota (UFPE / Centro de Informática)
Prof. Rodrigo Bonifacio de Almeida (UNB / Departamento de Ciência da Computação)
Prof. Augusto Cezar Alves Sampaio (UFPE / Centro de Informática)
RESUMO:
A verificação formal de contratos inteligentes é essencial para garantir a correção e segurança de aplicações blockchain, mas enfrenta desafios significativos na geração de especificações formais. Tradicionalmente, esse processo requer conhecimento especializado em métodos formais e linguagens de especificação, criando um gargalo para a adoção em larga escala. Esta dissertação apresenta DbC-GPT, um framework para geração automática de especificações de pós-condições para contratos inteligentes a partir de descrições em linguagem natural, especificamente Propostas de Melhoria do Ethereum (EIPs), utilizando Modelos de Linguagem de Grande Escala (LLMs). Nossa abordagem integra um loop guiado por contra-exemplos, aproveitando a ferramenta solc-verify, para refinar iterativamente as especificações e garantir sua validade sintática e semântica em relação a uma implementação de referência. Conduzimos uma avaliação abrangente dos padrões ERC20, ERC721 e ERC1155, comparando duas técnicas principais de adaptação de LLM: aprendizado few-shot através de contextos de demonstração e fine-tuning
supervisionado usando conjuntos de dados personalizados. Também contrastamos a geração de especificações função por função com a geração de especificações para o contrato inteiro. Nossos resultados revelam insights importantes sobre as capacidades e limitações atuais dos LLMs para geração
de especificações formais. Tanto o aprendizado few-shot quanto o fine-tuning melhoraram significativamente as taxas de sucesso na geração de especificações em comparação com um modelo base, com o processo iterativo guiado por contra-exemplos provando ser crucial. Configurações ótimas para aprendizado few-shot alcançaram altas taxas de sucesso na geração de especificações válidas (até 100% na geração em nível de contrato), enquanto modelos fine-tuned também demonstraram desempenho forte. Para essas gerações bem-sucedidas, ambas as abordagens produziram especificações que foram aproximadamente 66,7% semanticamente equivalentes às especificações de referência.
Palavras-chave: Verificação Formal. Contratos Inteligentes. Modelos de Linguagem de Grande Escala. Design-by-Contract. Ethereum.
Comentários desativados