IA e os Problemas Difíceis do Mundo · Matemática · arXiv · 2026-10-23
LLM2Cert: síntese de certificados por LLM com verificação SMT/Lean
Título original: LLM2Cert: LLM Synthesis of Certificates with SMT/Lean Verification
As funções de Lyapunov e os certificados de barreira garantem estabilidade e segurança em sistemas dinâmicos, mas sintetizá-los e verificá-los continua sendo difícil para sistemas não lineares de alta dimensão. Os autores apresentam o DynaCertBench, um benchmark com 105 instâncias, e o LLM2Cert, um framework orientado por LLM que sintetiza certificados candidatos e encaminha cada obrigação de prova a um solver SMT ou ao agente de reparo de provas em Lean. O LLM2Cert verifica 81 das 105 instâncias (77,1%), 17,1 pontos percentuais a mais do que a proposta em uma única tentativa sem feedback, e verifica 22 certificados que o All-SMT deixa sem resolução.