Quando la verifica non equivale all’accordo: formalizzazione da LLM a Dafny tra agenti

Abstract degli autori

Una postcondizione verificata in Dafny certifica che una formula è valida, ma non garantisce che il risultato sia stato raggiunto attraverso un ragionamento davvero indipendente. Presentiamo un protocollo di formalizzazione tra agenti in cui un modello specificatore traduce i criteri di una sperimentazione clinica in un predicato Dafny, mentre un modello implementatore scrive un metodo operativo verificato rispetto a quel predicato. Un controllo con lo stesso modello mostra che, anche in assenza di differenze di capacità, due estrazioni indipendenti dallo stesso testo concordano solo nel 59,3% dei casi. Valutando quattro configurazioni di modelli su 96 documenti di sperimentazioni cliniche, rileviamo che l’accordo dipende in misura significativa da come le capacità dei modelli sono ripartite tra i due ruoli: la configurazione GPT-4.1-nano/GPT-4.1-mini raggiunge un accordo del 53,0% quando il modello più potente è l’implementatore, ma solo del 14,3% quando i ruoli sono invertiti. La configurazione più potente tra quelle testate, GPT-5.6-luna/GPT-5.4-mini, porta l’accordo al 34,4%, ma resta al di sotto del valore di riferimento ottenuto con lo stesso modello ed è caratterizzata soprattutto da contraddizioni dirette (42,7%). Rileviamo inoltre un artefatto critico della verifica: un implementatore più debole soddisfa la postcondizione richiamando direttamente il predicato dello specificatore; dopo una verifica strutturale, l’accordo corretto scende dal 14,3% al 13,2%. I nostri risultati mostrano che il solo esito positivo della verifica non costituisce una prova sufficiente di accordo indipendente tra agenti e che la capacità dei modelli non garantisce l’accordo quando formalizzano indipendentemente la stessa fonte.