LLM2Cert verifica 81 de 105 certificados de estabilidade e segurança

Os modelos de linguagem aprenderam a escrever código e a provar teoremas. Agora, pesquisadores tentam aplicá-los a um problema de engenharia em que o erro custa caro: confirmar que um sistema dinâmico permanece estável e seguro. Os autores do preprint LLM2Cert (arXiv 2610.30524) construíram um framework em que a LLM propõe certificados e verificadores formais os checam. No novo benchmark DynaCertBench, com 105 tarefas, o sistema verifica 81, ou seja, 77,1%. É 17,1 pontos percentuais a mais que a geração única, sem feedback (cerca de 60%).

Por que os certificados ainda são um gargalo

Funções de Lyapunov e certificados de barreira oferecem garantias no espaço de estados. As primeiras mostram que o sistema é estável; os segundos provam que ele não entrará em uma região perigosa. A dificuldade é que essas funções precisam primeiro ser encontradas e depois verificadas com rigor. Para sistemas não lineares multidimensionais, isso continua sendo um problema em aberto.

Os pipelines existentes verificam candidatos de três maneiras: solvers numéricos (programas de sum-of-squares), métodos intervalares e solvers SMT. Os três compartilham os mesmos problemas. Exigem relaxações, são conservadores ou escalam mal conforme aumentam a dimensão e a não linearidade do modelo.

Os autores apontam ainda um efeito colateral. Os conjuntos de teste padrão são compostos, em sua maioria, por sistemas polinomiais de baixa dimensão, escolhidos de acordo com a capacidade dos solvers, e não com as necessidades da engenharia. Os benchmarks refletem o que as ferramentas sabem fazer, não o que é preciso na prática.

DynaCertBench e o roteamento das obrigações

A primeira parte do trabalho trata do conjunto de testes. O DynaCertBench contém 105 tarefas:

• 80 sistemas não redundantes, selecionados da literatura;
• extensões desses sistemas com variantes multidimensionais e com restrições de controle;
• novos sistemas com acoplamento não linear;
• quatro classes de tarefas: estabilidade, região de atração (region of attraction), invariância direta (forward invariance) e segurança.

A segunda parte é o próprio LLM2Cert. O modelo gera um certificado candidato, e o framework o decompõe em obrigações de prova. Cada obrigação segue por um de dois caminhos: para um solver SMT ou diretamente para o agente Lean Proof-Repair. O Lean atua aqui como verificador formal rigoroso, e o agente corrige a prova quando ela não fecha. É o feedback dos verificadores que gera o principal ganho: sem ele, o modelo que entrega um único candidato resolve bem menos tarefas.

Os números que vale ter em mente

• DynaCertBench: 105 tarefas, das quais 80 vêm da literatura.
• O LLM2Cert verifica 81 das 105 tarefas, ou 77,1%.
• Ganho sobre a proposta one-shot sem feedback: 17,1 p.p.
• Dos 81 certificados encontrados, 22 foram verificados em casos nos quais a abordagem All-SMT, que envia tudo ao solver SMT, deixa a questão em aberto.

Esse último número talvez seja o mais revelador. É quase um quarto dos certificados do conjunto que o SMT puro não alcança. O roteamento híbrido resolve parte das tarefas que o SMT sozinho não consegue resolver.

O artigo é assinado por Zhipeng Cao, Peiyang Song, Nikolaus Vertovec, Weiru Cui, Zhihao Yang, Mingkang Liu, Luxia Lin, Bai Xue e Alessandro Abate. Código e dados foram publicados no repositório FormalCert-AI/llm2cert.

Quem deve se beneficiar primeiro

O efeito prático é esperado onde o controle de sistemas não lineares exige garantias formais: robótica, transporte autônomo, redes de energia e aviônica. Hoje, o engenheiro precisa escolher o certificado manualmente ou por meio de programas SOS, que esbarram na dimensão do problema. O esquema "a LLM propõe, o solver e o Lean verificam" transfere a parte criativa para o modelo e deixa a confiança com a verificação formal. Mesmo que o modelo erre, um certificado incorreto não passa na verificação.

Para pesquisadores, o próprio DynaCertBench é útil: permite comparar novos métodos de síntese em tarefas mais próximas de sistemas reais do que os polinômios de baixa dimensão habituais. O código aberto permite reproduzir os resultados e conectar outro modelo. Restam 24 das 105 tarefas que o LLM2Cert não resolveu, e elas mostram onde estão os limites do método.