63 articoli
Questo articolo studia come le presentazioni come monadi di codensità di diverse monadi di misure di probabilità permettano di derivare proprietà fondamentali come leggi di Kleisli, strutture monoidali e affini, fornendo nuove caratterizzazioni universali e collegamenti alla teoria delle categorie di Markov, con particolare attenzione al monade di Giry e a quello di Radon.
Questo articolo introduce un operade di diagrammi di cablaggio diretti dipendenti per comporre sistemi istantanei come le macchine di Mealy e i diagrammi di stock and flow, fornendo una semantica che mappa quest'ultimi nelle prime.
Il paper presenta Preguss, un framework modulare che combina analisi statica e modelli linguistici per generare e raffinare specifiche formali, permettendo la verifica automatizzata di programmi su larga scala (oltre 1000 righe di codice) con una riduzione dell'80,6%-88,9% dello sforzo umano necessario.
Questo lavoro presenta un metodo di verifica formale scalabile per i circuiti di stima della fase quantistica, basato su un'astruzione simbolica dei qubit e logica a vettori di bit, che permette di verificare circuiti con oltre 1.000 qubit utilizzando meno di 3,5 GB di memoria.
Questo articolo stabilisce esplicitamente un limite costruttivo secondo cui la dimensione ottimale di un circuito cambia al massimo di in seguito a perturbazioni della tabella di verità, estendendo il risultato a distanze di Hamming generali e convalidandolo sperimentalmente per nel basis AIG, dove la differenza massima osservata è esattamente .
RoadLogic è un sistema open-source che colma il divario tra le specifiche dichiarative OpenSCENARIO e le simulazioni eseguibili per i veicoli autonomi, utilizzando la programmazione logica a insiemi di risposte e la pianificazione del movimento per generare automaticamente scenari realistici e conformi alle specifiche.
Questo articolo presenta un nuovo quadro generale che estende la compilazione in d-DNNF al livello SMT, permettendo di rispondere a query complesse in tempo polinomiale combinando formule SMT con lemmi teorici pre-calcolati e sfruttando ragionatori proposizionali esistenti.
Il documento presenta BemaGANv2, un vocoder basato su GAN avanzato per la generazione audio a lungo termine che integra innovazioni architetturali come il modulo AMP e una valutazione sistematica di diverse strategie di combinazione dei discriminatori, tra cui il nuovo Multi-Envelope Discriminator, per migliorare coerenza temporale e fedeltà del suono.
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 formalizza in teoria dei tipi omo-topica la corrispondenza di Galois tra spazi di ricoprimento e sottogruppi del gruppo fondamentale, sviluppando una generalizzazione n-dimensionale e classificando i ricoprimenti degli spazi lenticolari per costruire la sfera di omologia di Poincaré.
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.
Il paper confronta tre diverse semantica di soddisfacibilità per la logica quantistica in spazi di Hilbert a dimensione finita, dimostrando che la semantica standard ammette più formule rispetto a quelle commutative globali e parziali booleane, e fornendo un esplicito separatore che soddisfa la prima ma non le altre due.
Il paper presenta "Agent Hunt", un esperimento che utilizza un mercato simulato basato su ricompense per coordinare agenti LLM nella formalizzazione collaborativa e decentralizzata della topologia algebrica all'interno di un ambiente di dimostrazione interattiva.
Il paper presenta Twitch, uno strumento che scopre automaticamente astrazioni (pattern di termini) utili per la dimostrazione di teoremi equazionali, estendendo il prover Twee per ottenere risultati significativi su problemi di uguaglianza unitaria.
Questo studio presenta LLM2SMT, un agente di codifica basato su LLM che ha sviluppato autonomamente, senza alcun codice scritto da umani, un solver SMT completo e competitivo per la logica QF_UF, implementando l'algoritmo di chiusura congruente e generando prove formali in Lean.
Il paper presenta Elenchus, un sistema dialogico basato su LLM che costruisce basi di conoscenza attraverso l'interazione tra un esperto umano e un'opponente artificiale, mappando lo stato dialettico risultante nella logica NMMS per formalizzare e verificare le relazioni inferenziali, come dimostrato nell'ontologia PROV-O.
Questo studio dimostra che l'uso di reti neurali grafiche per prevedere un ordine di ramificazione iniziale può accelerare significativamente i risolutori SAT su istanze casuali e pseudo-industriali, sebbene tale approccio perda efficacia su istanze industriali complesse a causa della rapida sovrascrittura delle euristiche dinamiche del solver.
Questo articolo introduce i database orientati agli schizzi, un quadro categorico che codifica paradigmi e schemi di database come modelli di schizzi a limite finito, illustrando come concetti come percorsi e attributi siano catturati uniformemente e proponendo meccanismi come i localizzatori e gli schizzi di "stuttering" per l'inferenza di percorsi e la composizione modulare.
Questo articolo presenta un metodo per la generazione automatizzata di esercizi di dimostrazione matematica con livelli di complessità comparabili, basandosi su una procedura di estrazione meccanizzabile di regole per prove tableaux analitiche che catturano formalmente lo sforzo richiesto per la risoluzione.
Questa pubblicazione raccoglie gli atti della VIII Conferenza Internazionale sulla Teoria delle Categorie Applicata, tenutasi all'Università della Florida nel giugno 2025, che ha riunito contributi multidisciplinari che spaziano dall'informatica alla chimica e alla computazione quantistica.