28 articoli
Il paper introduce FATE, una nuova serie di benchmark formali in algebra che copre difficoltà fino al livello di ricerca avanzata, rivelando che gli attuali modelli LLM faticano enormemente a formalizzare il ragionamento matematico, ottenendo prestazioni quasi nulle rispetto ai risultati nei concorsi matematici tradizionali.
Questo articolo costruisce automi per riconoscere relazioni sulle sequenze -automatiche, analizza la loro complessità di stati, stabilisce una relazione tra la complessità delle parole e quella delle sottosuccessioni lineari, risolve una questione recente di Zantema e Bosma e discute la complessità computazionale della costruzione di tali automi tramite l'aritmetica di Büchi.
Questo paper presenta un approccio che estende l'estrazione di specifiche dai tracciati di esecuzione oltre le astrazioni booleane, unendo tecniche di sintesi guidata dalla sintassi e la logica temporale TSL per apprendere trasformazioni dei dati e specifiche temporali, dimostrando una maggiore robustezza ed efficienza rispetto ai metodi di apprendimento passivo.
Questo articolo studia i giochi su grafi concorrenti con randomizzazione distribuita, dimostrando che le strategie senza memoria sono sufficienti per il problema della soglia (che risulta NP-difficile e in ) e per la raggiungibilità quasi certa (NP-completa), introducendo la logica IRATL e un solver pratico per tali problemi.
Questo articolo risolve le asimmetrie logiche e le ambiguità nella semantica degli automi di dimensioni superiori (HDA) sviluppando un fondamento indipendente dall'ordine degli eventi basato su ipomset a intervalli, dimostrando l'isomorfismo tra presentazioni categoriali e fornendo una base unificata per la bisimulazione e l'applicazione del framework delle mappe aperte.
Questo lavoro dimostra che non è decidibile se il numero minimo di inversioni (turn) nelle computazioni di automi a pila e a contatore sia limitato, stabilendo un trade-off non ricorsivo tra le classi di automi e rivelando una gerarchia infinita di complessità basata su funzioni sublineari non costanti.
Questo articolo indaga i veri alberi context-free, dimostrandone una descrizione tramite automi non deterministici a più archi e stabilendo che il problema dell'isomorfismo per tali alberi deterministici è NL-completo sia nella versione radicata che in quella non radicata.
Questo articolo dimostra nuove proprietà della rappresentazione degli interi in base al rapporto aureo , confermando in particolare una congettura di Kimberling del 2012 con l'aiuto degli strumenti di dimostrazione automatica Walnut e ChatGPT 5.
Questo articolo individua sei dimensioni fondamentali, tra cui due nuove (direzionalità e temporalità), che rivelano l'asimmetria operativa tra generazione e riconoscimento nella teoria dei linguaggi formali, sfatando il mito che la generazione sia intrinsecamente semplice e collegando tale asimmetria temporale al framework della sorpresa, anche nel contesto dei moderni modelli linguistici.
Questo articolo dimostra che i fattori delle parole lisce sono parole f-lisce e conferma la congettura di Sing sulla complessità delle parole f-lisce su alfabeti binari, provando il caso esatto per gli alfabeti pari, il limite inferiore per qualsiasi alfabeto binario e migliorando il limite superiore per gli alfabeti dispari.
Il paper presenta ZipLex, un framework verificato formalmente per l'analisi lessicale invertibile e lineare che garantisce l'equivalenza tra lessing e stampa, superando le limitazioni temporali quadratiche delle soluzioni precedenti e offrendo prestazioni significativamente superiori.
Questo articolo sviluppa un approccio basato sui dati per il controllo supervisionato non bloccante dei sistemi a eventi discreti con modelli sconosciuti, introducendo e formalizzando il concetto di "informatività dei dati di marcatura" per determinare le condizioni necessarie alla progettazione di un supervisore valido e proponendo algoritmi per la sua verifica e per l'ottimizzazione delle specifiche quando i dati sono insufficienti.
Questo lavoro stabilisce un legame fondamentale tra l'efficienza strutturale e la reachability nel decoding vincolato da grammatica, dimostrando che grammatiche linguisticamente equivalenti possono generare costi computazionali drasticamente diversi e fornendo limiti inferiori teorici, metriche di ambiguità strutturale e strategie di ottimizzazione per l'implementazione di modelli linguistici vincolati.
Questo lavoro dimostra che è possibile realizzare esattamente le macchine di Moore come modelli a spazio di stato, proponendo un metodo ibrido che utilizza l'apprendimento simbolico degli automi per inizializzare tali modelli, ottenendo così una convergenza più rapida e prestazioni superiori rispetto all'inizializzazione casuale.
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.
Il documento studia teoremi di tipo Ramsey per alberi infiniti e strumenti combinatori correlati, applicandoli al problema dell'espansione delle algebre di alberi.
Questo articolo propone un metodo per la guida autonoma che bilancia i rischi di collisione e le violazioni delle regole stradali, estendendo una metrica di rischio umano tramite specifiche di logica temporale lineare (LTL) formulate come problemi di raggiungibilità risolvibili mediante programmazione lineare e validati nel simulatore Carla.
Questo articolo dimostra le congetture di Clark Kimberling sulla sua sequenza binaria, ne stabilisce la relazione con la parola di Tribonacci e ne determina la complessità dei fattori e l'esponente critico, utilizzando anche il dimostratore di teoremi Walnut.
Questo lavoro presenta una classificazione completa della complessità computazionale distribuita per i problemi di ottimizzazione locale nei cicli diretti, identificando quattro possibili classi di complessità e fornendo un algoritmo centrale efficiente per determinare automaticamente la classe di un dato problema e sintetizzare un algoritmo distribuito asintoticamente ottimale.