CAPRI: Un flusso di lavoro per la riparazione di prove sensibile ai contratti per Isabelle utilizzando LLM

Un recente articolo di ricerca presenta CAPRI, un flusso di lavoro progettato per riparazioni di prove sensibili ai contratti che utilizza grandi modelli linguistici (LLM) per aiutare nella scoperta di prove Isabelle. Implementando un contratto di modifica leggibile da macchina tramite un verificatore indipendente, CAPRI colma una lacuna significativa nell'assistenza alle prove basata su LLM, garantendo che le modifiche rispettino i vincoli stabiliti. Per l'audit, il flusso di lavoro conserva prompt, proposte, repository di candidati, diagnostiche, verdetti e hash. L'analisi ha coinvolto cinque flussi di lavoro applicati a dodici prove fallite da quattro progetti, portando a 180 esecuzioni e 138 riparazioni riuscite. Tra 144 candidati terminali approvati da Isabelle, sei includevano testo protetto modificato. L'interfaccia solo-corpo-di-prova ha ottenuto 29 riparazioni valide su 36 senza violazioni contrattuali, mentre il flusso di lavoro teoria-completa ha prodotto 31 riparazioni valide su 36.