27 articoli
Questo articolo estende l'equivalenza tra categorie di azione destre e categorie arricchite con copotermini a basi monoidali non chiuse e non simmetriche, fornendo la fondazione semantica necessaria per supportare processi di ordine superiore nel linguaggio concorrente CaMPL.
Questo studio empirico su larga scala analizza l'uso dell'aritmetica in virgola mobile in milioni di repository GitHub per linguaggi staticamente tipizzati, fornendo un dataset di 10 milioni di funzioni reali e valutando la rappresentatività degli attuali benchmark rispetto al codice di produzione.
Il paper presenta Turn, un linguaggio di programmazione compilato e basato su attori progettato per il calcolo agentiche, che integra sicurezza dei tipi cognitiva, un operatore di confidenza, un modello di processo isolato, un sistema di identità basato sulle capacità e l'assorbimento degli schemi a tempo di compilazione per garantire invariants critici come l'isolamento delle credenziali e la validazione dell'output dei modelli linguistici.
Il paper presenta Arbiter, un framework che combina regole di valutazione formale e analisi multi-modello per rilevare pattern di interferenza nei prompt di sistema degli agenti LLM per la codifica, identificando vulnerabilità critiche e dimostrando come l'architettura del prompt influenzi le classi di fallimento.
Questo lavoro formalizza il concetto di "fette idempotenti" e presenta un algoritmo efficiente per estrarle dalla forma GSA, permettendo una riduzione dello spazio del codice fino al 7,24% attraverso la fusione di istruzioni non contigue.
Il paper presenta vLLM Hook, un plugin open-source che abilita la programmazione passiva e attiva degli stati interni dei modelli LLM su vLLM, permettendo applicazioni come il rilevamento di prompt injection, il miglioramento del RAG e il controllo tramite attivazioni.
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 presenta PolyBlocks, un'infrastruttura di compilazione modulare basata su MLIR per framework AI e chip, che genera automaticamente codice ad alte prestazioni per nuove architetture e dimostra prestazioni competitive rispetto a Torch Inductor e XLA su GPU NVIDIA.
Questo lavoro propone tre approcci complementari per superare i limiti delle attuali registrazioni delle tracce creative, che spesso perdono l'intento e le relazioni strutturali, presentando rispettivamente un'interfaccia basata su nodi per la gestione degli artefatti GenAI, un vocabolario di segnali visivi per l'autoria di visualizzazioni e un modello di programmazione che integra direttamente le storie semantiche nello stato di interazione.
Il paper presenta EAGLE-Pangu, un sistema riproducibile che implementa il decoding speculativo ad albero su NPU Ascend per il modello Pangu, risolvendo problemi di compatibilità hardware e migliorando il throughput di decodifica fino a 2,46 volte rispetto all'approccio teacher-only.
Questo lavoro sviluppa una teoria delle specifiche GSOS astratte per i linguaggi di ordine superiore, trasferendo i principi del quadro di Turi e Plotkin a tale contesto mediante trasformazioni dinaturali chiamate leggi GSOS di ordine superiore puntate, al fine di garantire risultati generali di composizionalità che si applicano, tra gli altri, al calcolo SKI e al -calcolo.
Il paper presenta VyZX, una libreria verificata che permette di ragionare formalmente su linguaggi grafici induttivi, come il calcolo ZX per il calcolo quantistico, superando le limitazioni degli assistenti di prova tradizionali e fornendo uno strumento di visualizzazione integrato per l'IDE.
Il documento presenta RightTyper, un approccio ibrido innovativo che genera annotazioni di tipo Python precise e affidabili basandosi sul comportamento effettivo del programma, superando i limiti dei metodi statici, dinamici e basati sull'IA con un sovraccarico di esecuzione ridotto a circa il 27%.
Questo articolo presenta una teoria completamente simbolica per l'analisi della località dei cicli che deriva polinomi di prestazioni della cache con un'accuratezza del 99,6%, permettendo previsioni di movimenti di dati in meno di un millisecondo dopo un'analisi di circa 41 secondi.
Queste note di lezione offrono una breve introduzione alla teoria delle categorie, focalizzandosi su algebre iniziali e monadi per caratterizzare rispettivamente i tipi di dati e gli effetti nella programmazione funzionale, e includono numerosi esercizi con soluzioni.
Il paper introduce "Linear Layouts", un approccio innovativo che modella le disposizioni dei tensori tramite algebra lineare su per generare codice efficiente, offrire definizioni generiche e conversioni flessibili, riducendo l'errore umano e i costi computazionali nell'integrazione con Triton.
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.
Il paper propone l'editing strutturato ibrido, un approccio che garantisce ai creatori di strumenti la manipolazione sicura della struttura del codice attraverso vincoli dichiarativi, offrendo contemporaneamente agli utenti un'interfaccia di modifica testuale familiare e coerente.
Questo articolo analizza le insidie specifiche nell'implementazione di macchine virtuali su CHERI, emerse durante il porting di CRuby, evidenziando come le assunzioni sul comportamento indefinito del linguaggio C tipiche delle architetture tradizionali causino fallimenti sotto il modello di sicurezza più rigoroso di CHERI e proponendo soluzioni validate.
Questo studio valuta l'efficacia di nove modelli linguistici su larga scala in un corso di programmazione funzionale basato su OCaml, utilizzando tre nuovi benchmark (CodeGen, Repair e Explain) che rivelano come, sebbene i modelli migliori siano competenti nella correzione di errori e nella spiegazione di concetti, le loro prestazioni siano inferiori rispetto a quelle osservate in linguaggi ad alta risorsa come Python e Java.