64 articoli
Questo articolo presenta un nuovo approccio che combina strategie di ricerca basate sull'ordinamento e sulla riduzione a sottobiettili, utilizzando codifiche SAT con rottura della simmetria per i calcoli di connessione nella logica del primo ordine, implementato nel risolutore upCoP per migliorare l'automazione delle dimostrazioni.
Il paper introduce le "commutation groups" e i "contextual words" come strumenti algebrici e di riscrittura per analizzare la contestualità indipendente dallo stato, caratterizzandone l'origine e fornendo rappresentazioni unitarie tramite gruppi di Pauli generalizzati.
Questo articolo presenta un framework di monitoraggio online scalabile ed efficiente per la Logica Temporale Metrica (MTL), basato sulla costruzione unificata di reti sequenziali tramite una tecnica di "future temporal marking" che utilizza rappresentazioni simboliche basate su intervalli per gestire comportamenti temporali sia discreti che densi.
Questo articolo stabilisce che il controllo modulare dei sistemi multi-agente pushdown è completo per 2EXPTIME rispetto alle specifiche ATL e 4EXPTIME rispetto alle specifiche ATL*, quest'ultima rappresentando un raro esempio di problema decisionale elementare con complessità superiore al tempo triplamente esponenziale.
Questo lavoro identifica e formalizza in Lean 4 un limite di orientabilità globale per i ricorsori duplicanti, dimostrando l'impossibilità di prove composizionali dirette su un sistema minimale e proponendo una via d'uscita tramite criteri basati su proiezioni e una catena di certificazione completa per la terminazione e la confluenza.
Questo articolo presenta MPBMC, un approccio ibrido che utilizza embedding di reti neurali grafiche e statistiche di runtime per raggruppare funzionalmente le proprietà e accelerare la verifica formale tramite model checking limitato.
Il paper dimostra che la fusione indipendente di logiche modali del primo ordine a una variabile preserva la completezza di Kripke e la decidibilità senza uguaglianza, mentre queste proprietà falliscono in presenza di uguaglianza e costanti non rigide a causa della codifica di equazioni diofantee, fornendo inoltre condizioni sufficienti per il trasferimento di completezza e decidibilità quando le logiche condividono un modale S5.
Questo lavoro presenta un'assiomatizzazione completa delle divergenze di Kullback-Leibler e di Rényi, viste come arricchimenti quantitativi di categorie di matrici stocastiche, utilizzando un linguaggio grafico di diagrammi a stringa all'interno di due strutture monoidali naturali.
Questo articolo offre una panoramica sistematica dei frammenti di logica proposizionale e modale limitati a basi di operatori, analizzando come la loro espressività e complessità computazionale dipendano dalle scelte sintattiche consentite, integrando risultati sulla classificazione della complessità e sull'apprendibilità.
Il paper introduce le logiche costruttive e , dimostrandone la completezza EXPTIME e la proprietà della modello finito, risolvendo la congettura di Afshari et al. per il frammento senza diamanti e fornendo un'incorporazione di e che ne colloca i problemi di validità in EXPTIME.
Questo articolo propone l'adozione dell'apprendimento dei vincoli nel calcolo delle connessioni di primo ordine per ridurre il backtracking nella ricerca di prove non confluenti mantenendo la completezza, attraverso un linguaggio di vincoli iterativamente raffinato.
Il paper presenta un nuovo approccio per risolvere equazioni stringa, estendendo le trasformazioni di Nielsen mediante l'integrazione di un operatore di potenza, generalizzazioni delle immagini di Parikh e la decomposizione dell'uguaglianza.
Il paper presenta NL2GDS, un framework innovativo che utilizza modelli linguistici di grandi dimensioni per tradurre descrizioni hardware in linguaggio naturale in layout GDSII completi tramite il flusso OpenLane, dimostrando significativi miglioramenti nell'efficienza di area, ritardo e consumo energetico rispetto ai progetti tradizionali.
Questo lavoro presenta SCORE, un linguaggio progettato per dimostrare come le operazioni sugli stack possano essere interpretate come biezioni totali, permettendo così di certificare formalmente che tutti i termini del modello computazionale sono funzioni biunivoche totali.
Questo articolo introduce una nuova teoria equazionale per il calcolo I basata sugli "Ohana trees", che preservano le variabili nascoste o infinite, e ne dimostra la coerenza attraverso l'analisi di approssimazione, l'espansione di Taylor e un modello denotazionale basato su un sistema di tipi relazionale modificato.
Il paper presenta LeanTutor, un sistema di tutoraggio matematico basato sull'IA che combina le capacità comunicative dei modelli linguistici con la correttezza verificabile dei prover di teoremi Lean, valutato tramite il nuovo dataset PeanoBench.
Questo studio propone un nuovo quadro geometrico che modella il ragionamento dei grandi modelli linguistici come flussi nello spazio delle rappresentazioni, dimostrando come essi interiorizzino invarianze logiche indipendentemente dal significato semantico e sfidando così l'ipotesi che siano semplici "pappagalli stocastici".
Il paper presenta Strat2Rocq, un approccio che estrae le strategie di prova interne dei modelli linguistici (LLM) per trasformarle in lemmi formali, migliorando così l'efficacia dei prover simbolici come CoqHammer e, incidentalmente, anche degli agenti di prova basati su LLM.
Il paper propone SpotIt, un nuovo metodo di valutazione per Text-to-SQL che utilizza la verifica formale dell'equivalenza per identificare differenze tra query generate e ground-truth che i tradizionali test basati su database statici spesso trascurano.
Questo articolo presenta una metodologia scalabile per la verifica formale dell'aritmetica in virgola mobile a livello RTL, che combina un approccio modulare di tipo "divide et impera", l'iniezione di fault e la generazione assistita da intelligenza artificiale per superare le limitazioni dei modelli ad alto livello e migliorare l'efficienza della copertura.