LLM2Cert: sintesi di certificati mediante LLM con verifica SMT/Lean

Abstract degli autori

Le funzioni di Lyapunov e i certificati di barriera forniscono garanzie di stabilità e sicurezza nello spazio degli stati, ma sintetizzarli e verificarli, soprattutto per sistemi non lineari ad alta dimensionalità, resta una sfida aperta. Le procedure esistenti verificano i certificati candidati mediante solutori numerici (programmi basati su somme di quadrati), metodi intervallari o solutori SMT (*satisfiability modulo theories*), che spesso richiedono rilassamenti, sono conservativi o scalano male all’aumentare della dimensionalità e della non linearità del modello. Questi limiti hanno influenzato anche la progettazione dei benchmark: nelle suite di test standard predominano sistemi polinomiali a bassa dimensionalità, scelti in base a ciò che i solutori riescono a gestire anziché alle esigenze delle applicazioni ingegneristiche. Affrontiamo entrambi gli aspetti della sfida. Per prima cosa, introduciamo DynaCertBench, un benchmark di 105 istanze: 80 sistemi non ridondanti selezionati dalla letteratura, ampliati con varianti ad alta dimensionalità e soggette a vincoli di controllo e con nuovi sistemi ad accoppiamento non lineare, che coprono in modo completo problemi di stabilità, regione di attrazione, invarianza in avanti e sicurezza. Presentiamo poi LLM2Cert, un framework basato su LLM che sintetizza certificati candidati e li verifica rispetto ai relativi obblighi di dimostrazione: ogni obbligo viene assegnato a un solutore SMT o direttamente all’agente Lean Proof-Repair. Su DynaCertBench, LLM2Cert verifica 81 delle 105 istanze ($77.1\%$), con un miglioramento di $17.1$ punti percentuali rispetto a una proposta in un unico tentativo senza feedback. Sugli 81 certificati fissati, LLM2Cert ne verifica 22 che All-SMT lascia irrisolti. Codice e dati sono disponibili all’indirizzo https://github.com/FormalCert-AI/llm2cert.