28 articoli
Questo lavoro stabilisce un legame fondamentale tra le classi di complessità computazionale e le architetture delle reti ricorrenti, dimostrando che le RNN lineari sono parallelizzabili come i transformer perché corrispondono a circuiti aritmetici di profondità logaritmica, mentre le RNN non lineari risolvono problemi completi per P che ne impediscono un'efficiente parallelizzazione.
Questo lavoro presenta un algoritmo distribuito randomizzato in un singolo round per la 2-colorazione dei cicli che riduce la frazione attesa di spigoli monocromatici a meno di 0,24118, stabilendo nuovi limiti superiori e inferiori e dimostrando che la maggior parte della prova è stata scoperta e formalizzata in Lean 4 da modelli linguistici di grandi dimensioni.
Il lavoro analizza la complessità del problema di raggiungibilità per i VASS estesi con contatori interi (VASS+Z), dimostrando che è NP-completo nel caso monodimensionale, stabilendo un limite superiore per e provando che l'aggiunta di contatori interi abbassa significativamente la soglia dimensionale necessaria per ottenere durezza PSPACE e TOWER.
Questo articolo presenta condizioni algebriche necessarie e sufficienti, verificabili in tempo costante, per garantire la reversibilità di automi cellulari di primo grado a stati su reticoli finiti di qualsiasi dimensione.
Questo studio analizza la complessità computazionale del calcolo degli allineamenti nel process mining, dimostrando che il problema è PSPACE-completo per le reti di Petri sicure, NP-completo per diverse sottoclassi come gli alberi di processo, e risolvibile in tempo polinomiale solo per le reti S sicure e vive.
Questo lavoro risolve un problema aperto da oltre un decennio dimostrando, attraverso un esempio di 65 stati ottenuto combinando intuizioni teoriche e supporto computazionale, che gli automi di Büchi storicamente deterministici possono essere più compatti di qualsiasi automa di Büchi deterministico equivalente.
Questo articolo presenta la modellazione formale, la verifica e il testing dell'ambiente di runtime per automi contrattuali (CARE) mediante l'uso di automi temporizzati stocastici e dello strumento Uppaal, al fine di migliorare l'affidabilità di questa applicazione distribuita open-source.
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.