Banca de DEFESA: GABRIEL NOGUEIRA LEITE

Uma banca de DEFESA de MESTRADO foi cadastrada pelo programa.
DISCENTE: GABRIEL NOGUEIRA LEITE
DATA : 21/11/2025
HORA: 15:00
LOCAL: Virtual
TÍTULO:

Generating formal smart-contract specifications from
natural-language requirements supported by LLM

 

PALAVRAS-CHAVES:

Verificação Formal. Contratos Inteligentes. Modelos de
Linguagem de Grande Escala. Design-by-Contract. Ethereum.

 

PÁGINAS: 81
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.

 

MEMBROS DA BANCA:
Presidente - 2133438 - ALEXANDRE MARCOS LINS DE VASCONCELOS
Interno - 1174650 - AUGUSTO CEZAR ALVES SAMPAIO
Externo à Instituição - RODRIGO BONIFACIO DE ALMEIDA - UnB