Banca de QUALIFICAÇÃO: NIKSON BERNARDES FERNANDES FERREIRA

Uma banca de QUALIFICAÇÃO de DOUTORADO foi cadastrada pelo programa.
DISCENTE : NIKSON BERNARDES FERNANDES FERREIRA
DATA : 15/01/2026
HORA: 11:00
LOCAL: CIC/LaForCE
TÍTULO:

Llama-PVS: A LLM for Proof Recommendation System

PALAVRAS-CHAVES:

Provadores de Teoremas Interativos, Large Language Models (LLMs), PVS, Sugestão de Passos de Prova, IA Explicável (XAI), Modelos Autoregressivos, Busca por Provas, Seleção de Premissas, Assistentes de Código

PÁGINAS: 1
RESUMO:

Os provadores de teoremas interativos (ITPs) são cruciais para a certificação de sistemas, mas impõem uma curva de aprendizado acentuada e exigem alta especialização. Embora técnicas de aprendizado de máquina tenham sido empregadas para sugerir comandos de prova, as abordagens atuais frequentemente dependem de pipelines de "dupla tradução" que consomem muitos recursos para processar os dados da prova. Este trabalho aborda essa ineficiência ao propor uma metodologia que treina modelos de linguagem autorregressivos diretamente nos estados brutos da prova. Apresentamos o Llama-PVS, uma estrutura de integração na IDE VSCode que permite que os usuários recebam recomendações de provas de modelos locais sem pré-processamento extensivo. Embora as avaliações iniciais indiquem que essa abordagem direta alcança desempenho competitivo em contextos restritos, desafios relacionados a alucinações do modelo, à falta de explicabilidade e à escalabilidade na seleção de premissas permanecem. Portanto, a trajetória desta pesquisa vai além da mera previsão de comandos. Trabalhos futuros se concentrarão em aprimorar a confiança e a precisão, incorporando uma camada de "raciocínio" em que o modelo gera explicações em linguagem natural antes de sugerir comandos. Além disso, para mitigar alucinações e melhorar a automação, propomos acoplar o modelo generativo a uma interface de busca de provas supervisionada (por exemplo, Busca em Profundidade) e investigar técnicas avançadas de representação para uma recuperação mais eficiente em grandes bibliotecas de lemas.

MEMBROS DA BANCA:
Presidente - 2180096 - MAURICIO AYALA RINCON
Interno - 1702036 - VANDER RAMOS ALVES
Externo à Instituição - JOSEPH TANNER SLAGEL - NASA
Externo à Instituição - MARIANO MIGUEL MOSCATO