Miglioramento della scalabilità di funzioni di valore neurali di Hamilton–Jacobi verificate mediante nuove tecniche di addestramento guidato dalla verifica.

Hamilton–Jacobi reachability analysis provides a rigorous framework for identifying safe regions in dynamical systems, but traditional numerical methods suffer from the curse of dimensionality. Neural networks offer a scalable alternative for approximating Hamilton–Jacobi value functions, although the resulting zero-sublevel sets are not automatically guaranteed to satisfy the required safety properties. This thesis investigates a verification-guided synthesis approach based on probabilistic enumeration of candidate violating regions. Instead of relying only on local gradient-based counterexample search, the proposed method constructs a structured approximation of portions of the failure set and samples informative counterexamples from these regions. Formal verification remains responsible for certifying constraint satisfaction and forward invariance. The approach is evaluated by combining gradient-based and enumeration-guided refinement with MILP and α, β-CROWN on several safe-control benchmarks. The results show that regional counterexample generation can improve the quality and stability of the final verified certificate and, in several cases, reduce the fine-tuning effort required before certification.

L’analisi di raggiungibilità di Hamilton–Jacobi fornisce un quadro teorico rigoroso per l’identificazione delle regioni sicure nei sistemi dinamici. Tuttavia, i metodi numerici tradizionali sono fortemente limitati dalla cosiddetta maledizione della dimensionalità. Le reti neurali rappresentano un’alternativa scalabile per approssimare le funzioni valore di Hamilton–Jacobi, sebbene gli insiemi di sottolivello zero così ottenuti non siano automaticamente garantiti rispetto alle proprietà di sicurezza richieste. Questa tesi analizza un approccio di sintesi guidato dalla verifica, basato sull’enumerazione probabilistica di regioni candidate contenenti possibili violazioni. Anziché affidarsi esclusivamente alla ricerca locale di controesempi basata sul gradiente, il metodo proposto costruisce un’approssimazione strutturata di porzioni dell’insieme delle violazioni e campiona da tali regioni controesempi informativi. La verifica formale rimane responsabile della certificazione del rispetto dei vincoli di sicurezza e dell’invarianza in avanti. L’approccio viene valutato combinando strategie di raffinamento basate sul gradiente e guidate dall’enumerazione con verificatori MILP e α, β-CROWN su diversi benchmark di controllo sicuro. I risultati mostrano che la generazione di controesempi a livello regionale può migliorare la qualità e la stabilità del certificato verificato finale e, in diversi casi, ridurre lo sforzo di fine-tuning necessario prima di ottenere la certificazione.