Paper Giornalieri

Gli assistenti di dimostrazione come Lean hanno rivoluzionato la verifica delle dimostrazioni matematiche, garantendo elevata accuratezza e affidabilità. Sebbene i modelli linguistici di grandi dimensioni (LLM) mostrino promettenti capacità nel ragionamento matematico, il loro progresso nella dimostrazione formale di teoremi è ostacolato dalla mancanza di dati di addestramento. Per affrontare questo problema, introduciamo un approccio per generare un ampio set di dati di dimostrazioni Lean 4 derivati da problemi di competizioni matematiche di livello scolastico e universitario. Questo approccio prevede la traduzione di problemi in linguaggio naturale in affermazioni formali, la filtrazione di affermazioni di bassa qualità e la generazione di dimostrazioni per creare dati sintetici. Dopo aver ottimizzato il modello DeepSeekMath 7B su questo dataset sintetico, che comprende 8 milioni di affermazioni formali con dimostrazioni, il nostro modello ha raggiunto accuratezze nella generazione di dimostrazioni complete del 46,3% con 64 campioni e del 52% cumulativamente nel test Lean 4 miniF2F, superando il baseline GPT-4 al 23,0% con 64 campioni e un metodo di apprendimento per rinforzo con ricerca ad albero al 41,0%. Inoltre, il nostro modello ha dimostrato con successo 5 su 148 problemi nel benchmark Lean 4 Formalized International Mathematical Olympiad (FIMO), mentre GPT-4 non è riuscito a dimostrarne alcuno. Questi risultati dimostrano il potenziale di sfruttare dati sintetici su larga scala per migliorare le capacità di dimostrazione di teoremi nei LLM. Sia il dataset sintetico che il modello saranno resi disponibili per facilitare ulteriori ricerche in questo promettente campo.

Recenti lavori hanno proposto l'ipotesi della rappresentazione lineare: che i modelli linguistici eseguano calcoli manipolando rappresentazioni unidimensionali di concetti ("feature") nello spazio delle attivazioni. Al contrario, esploriamo se alcune rappresentazioni dei modelli linguistici possano essere intrinsecamente multidimensionali. Iniziamo sviluppando una definizione rigorosa di feature multidimensionali irriducibili, basata sulla possibilità di scomporle in feature di dimensione inferiore indipendenti o non co-occorrenti. Motivati da queste definizioni, progettiamo un metodo scalabile che utilizza autoencoder sparsi per trovare automaticamente feature multidimensionali in GPT-2 e Mistral 7B. Queste feature scoperte automaticamente includono esempi sorprendentemente interpretabili, come feature circolari che rappresentano i giorni della settimana e i mesi dell'anno. Identifichiamo task in cui questi cerchi esatti vengono utilizzati per risolvere problemi computazionali che coinvolgono l'aritmetica modulare nei giorni della settimana e nei mesi dell'anno. Infine, forniamo prove che queste feature circolari siano effettivamente l'unità fondamentale di calcolo in questi task con esperimenti di intervento su Mistral 7B e Llama 3 8B, e troviamo ulteriori rappresentazioni circolari scomponendo gli stati nascosti per questi task in componenti interpretabili.

Nonostante i significativi progressi nella generazione e modifica di video utilizzando modelli di diffusione, ottenere una modifica video accurata e localizzata rimane una sfida considerevole. Inoltre, la maggior parte dei metodi esistenti per la modifica video si concentra principalmente sull'alterazione del contenuto visivo, con una ricerca limitata dedicata alla modifica del movimento. In questo articolo, presentiamo un nuovo tentativo di Rimodellare un Video (ReVideo) che si distingue dai metodi esistenti consentendo una modifica video precisa in aree specifiche attraverso la specificazione sia del contenuto che del movimento. La modifica del contenuto è facilitata dalla modifica del primo fotogramma, mentre il controllo del movimento basato su traiettorie offre un'esperienza di interazione utente intuitiva. ReVideo affronta un nuovo compito che coinvolge l'accoppiamento e lo squilibrio di addestramento tra il controllo del contenuto e del movimento. Per affrontare questo problema, sviluppiamo una strategia di addestramento in tre fasi che progressivamente disaccoppia questi due aspetti da un livello grossolano a uno fine. Inoltre, proponiamo un modulo di fusione spazio-temporale adattivo per integrare il controllo del contenuto e del movimento attraverso vari passaggi di campionamento e posizioni spaziali. Esperimenti estensivi dimostrano che il nostro ReVideo ha prestazioni promettenti in diverse applicazioni di modifica video accurata, ovvero: (1) cambiare localmente il contenuto del video mantenendo il movimento costante, (2) mantenere il contenuto invariato e personalizzare nuove traiettorie di movimento, (3) modificare sia il contenuto che le traiettorie di movimento. Il nostro metodo può anche estendere senza soluzione di continuità queste applicazioni alla modifica multi-area senza un addestramento specifico, dimostrando la sua flessibilità e robustezza.

Stiamo sfruttando appieno il potenziale degli encoder visivi nei Modelli Linguistici Multimodali di Grande Dimensione (MLLMs)? Le recenti prestazioni eccezionali degli MLLMs nella comprensione multimodale hanno attirato un'ampia attenzione sia dal mondo accademico che dall'industria. Nell'attuale corsa agli MLLMs, l'attenzione sembra essere prevalentemente rivolta al lato linguistico. Assistiamo alla crescita di dataset di istruzioni più grandi e di qualità superiore, nonché all'impiego di LLM di dimensioni maggiori. Tuttavia, poca attenzione è stata rivolta ai segnali visivi utilizzati dagli MLLMs, spesso considerati come le caratteristiche di alto livello estratte da un encoder visivo congelato. In questo articolo, introduciamo il Dense Connector - un connettore visione-linguaggio semplice, efficace e plug-and-play che migliora significativamente gli MLLMs esistenti sfruttando le caratteristiche visive multi-livello, con un sovraccarico computazionale minimo. Inoltre, il nostro modello, addestrato esclusivamente su immagini, dimostra notevoli capacità zero-shot anche nella comprensione dei video. I risultati sperimentali su vari encoder visivi, risoluzioni delle immagini, scale di dataset di addestramento, dimensioni variabili di LLM (2.7B->70B) e diverse architetture di MLLMs (ad esempio, LLaVA e Mini-Gemini) convalidano la versatilità e la scalabilità del nostro approccio, raggiungendo prestazioni all'avanguardia su 19 benchmark di immagini e video. Speriamo che questo lavoro fornisca un'esperienza preziosa e serva come modulo di base per lo sviluppo futuro degli MLLMs.

I progressi nei modelli di diffusione latente (LDMs) hanno rivoluzionato la generazione di immagini ad alta risoluzione, ma lo spazio di progettazione dell'autoencoder, centrale in questi sistemi, rimane ancora poco esplorato. In questo articolo, introduciamo LiteVAE, una famiglia di autoencoder per LDMs che sfrutta la trasformata wavelet discreta 2D per migliorare la scalabilità e l'efficienza computazionale rispetto ai tradizionali autoencoder variazionali (VAEs), senza compromettere la qualità dell'output. Investigiamo inoltre le metodologie di addestramento e l'architettura del decoder di LiteVAE, proponendo diversi miglioramenti che ottimizzano le dinamiche di addestramento e la qualità della ricostruzione. Il nostro modello base LiteVAE eguaglia la qualità dei VAEs consolidati negli attuali LDMs con una riduzione di sei volte nei parametri dell'encoder, portando a un addestramento più veloce e a minori requisiti di memoria GPU, mentre il nostro modello più grande supera i VAEs di complessità comparabile in tutte le metriche valutate (rFID, LPIPS, PSNR e SSIM).

Accelerare l'inferenza dei grandi modelli linguistici (LLM) rappresenta una sfida importante nell'intelligenza artificiale. Questo articolo introduce l'inferenza speculativa distribuita (DSI), un nuovo algoritmo di inferenza distribuita che è dimostrabilmente più veloce dell'inferenza speculativa (SI) [leviathan2023fast, chen2023accelerating, miao2023specinfer] e dell'inferenza autoregressiva tradizionale (non-SI). Come altri algoritmi SI, DSI funziona su LLM congelati, non richiede addestramento o modifiche architetturali e preserva la distribuzione target. Studi precedenti su SI hanno dimostrato accelerazioni empiriche (rispetto a non-SI) ma richiedono un LLM "drafter" veloce e accurato. Nella pratica, i LLM pronti all'uso spesso non dispongono di drafters corrispondenti sufficientemente veloci e precisi. Mostriamo un divario: SI diventa più lento di non-SI quando si utilizzano drafters più lenti o meno accurati. Colmiamo questo divario dimostrando che DSI è più veloce sia di SI che di non-SI con qualsiasi drafter. Orchestrando più istanze del target e dei drafters, DSI non solo è più veloce di SI, ma supporta anche LLM che non possono essere accelerati con SI. Le nostre simulazioni mostrano accelerazioni di LLM pronti all'uso in contesti realistici: DSI è 1,29-1,92 volte più veloce di SI.

I metodi di addestramento del secondo ordine presentano proprietà di convergenza migliori rispetto alla discesa del gradiente, ma sono raramente utilizzati nella pratica per l'addestramento su larga scala a causa del loro sovraccarico computazionale. Questo può essere visto come una limitazione hardware (imposta dai computer digitali). Qui dimostriamo che la discesa del gradiente naturale (NGD), un metodo del secondo ordine, può avere una complessità computazionale per iterazione simile a quella di un metodo del primo ordine, quando si utilizza hardware appropriato. Presentiamo un nuovo algoritmo ibrido digitale-analogico per l'addestramento di reti neurali che è equivalente alla NGD in un determinato regime di parametri, ma evita la risoluzione di sistemi lineari proibitivamente costosi. Il nostro algoritmo sfrutta le proprietà termodinamiche di un sistema analogico in equilibrio, e richiede quindi un computer termodinamico analogico. L'addestramento avviene in un ciclo ibrido digitale-analogico, in cui il gradiente e la matrice di informazione di Fisher (o qualsiasi altra matrice di curvatura semi-definita positiva) vengono calcolati a intervalli di tempo specifici mentre si svolgono le dinamiche analogiche. Dimostriamo numericamente la superiorità di questo approccio rispetto ai metodi di addestramento digitali del primo e del secondo ordine all'avanguardia su compiti di classificazione e di fine-tuning di modelli linguistici.

Approcci recenti hanno mostrato promettenti risultati nel distillare modelli di diffusione in generatori efficienti a un singolo passo. Tra questi, la Distillazione per Matching di Distribuzione (DMD) produce generatori a un passo che corrispondono alla distribuzione del loro insegnante, senza imporre una corrispondenza uno-a-uno con le traiettorie di campionamento dei loro insegnanti. Tuttavia, per garantire un addestramento stabile, DMD richiede una perdita aggiuntiva di regressione calcolata utilizzando un ampio insieme di coppie rumore-immagine generate dall'insegnante con molti passi di un campionatore deterministico. Questo è costoso per la sintesi su larga scala di immagini da testo e limita la qualità dello studente, legandola troppo strettamente ai percorsi di campionamento originali dell'insegnante. Introduciamo DMD2, un insieme di tecniche che superano questa limitazione e migliorano l'addestramento DMD. In primo luogo, eliminiamo la perdita di regressione e la necessità di una costosa costruzione del dataset. Mostriamo che l'instabilità risultante è dovuta al fatto che il critico fittizio non stima accuratamente la distribuzione dei campioni generati e proponiamo una regola di aggiornamento a due scale temporali come rimedio. In secondo luogo, integriamo una perdita GAN nel processo di distillazione, discriminando tra campioni generati e immagini reali. Questo ci permette di addestrare il modello studente su dati reali, mitigando l'imperfetta stima del punteggio reale del modello insegnante e migliorando la qualità. Infine, modifichiamo la procedura di addestramento per abilitare il campionamento a più passi. Identifichiamo e affrontiamo il problema di disallineamento tra input di addestramento e inferenza in questo contesto, simulando i campioni del generatore durante il tempo di inferenza nel tempo di addestramento. Nel complesso, i nostri miglioramenti stabiliscono nuovi benchmark nella generazione di immagini a un singolo passo, con punteggi FID di 1.28 su ImageNet-64x64 e 8.35 su COCO 2014 zero-shot, superando l'insegnante originale nonostante una riduzione di 500X nel costo di inferenza. Inoltre, mostriamo che il nostro approccio può generare immagini megapixel distillando SDXL, dimostrando una qualità visiva eccezionale tra i metodi a pochi passi.

I modelli di diffusione hanno ottenuto un grande successo nella generazione di immagini, con l'architettura di base che è evoluta da U-Net ai Vision Transformer. Tuttavia, il costo computazionale dei Transformer è quadratico rispetto al numero di token, portando a sfide significative quando si ha a che fare con immagini ad alta risoluzione. In questo lavoro, proponiamo Diffusion Mamba (DiM), che combina l'efficienza di Mamba, un modello di sequenza basato su State Space Models (SSM), con il potere espressivo dei modelli di diffusione per una sintesi efficiente di immagini ad alta risoluzione. Per affrontare la sfida che Mamba non può generalizzare a segnali 2D, abbiamo progettato diverse architetture, tra cui scansioni multi-direzionali, token di padding apprendibili alla fine di ogni riga e colonna, e un miglioramento leggero delle caratteristiche locali. La nostra architettura DiM raggiunge un'efficienza al momento dell'inferenza per immagini ad alta risoluzione. Inoltre, per migliorare ulteriormente l'efficienza dell'addestramento per la generazione di immagini ad alta risoluzione con DiM, abbiamo investigato una strategia di addestramento "da debole a forte" che prevede il pre-addestramento di DiM su immagini a bassa risoluzione (256x256) e poi il fine-tuning su immagini ad alta risoluzione (512x512). Abbiamo inoltre esplorato strategie di upsampling senza addestramento per consentire al modello di generare immagini a risoluzione ancora più alta (ad esempio, 1024x1024 e 1536x1536) senza ulteriore fine-tuning. Gli esperimenti dimostrano l'efficacia e l'efficienza del nostro DiM.

I Modelli Linguistici Multimodali di Grande Scala (MLLMs) sono ampiamente considerati cruciali nell'esplorazione dell'Intelligenza Artificiale Generale (AGI). Il nucleo degli MLLMs risiede nella loro capacità di raggiungere un allineamento cross-modale. Per raggiungere questo obiettivo, gli attuali MLLMs seguono tipicamente un paradigma di addestramento in due fasi: la fase di pre-addestramento e la fase di ottimizzazione su istruzioni. Nonostante il loro successo, ci sono carenze nella modellazione delle capacità di allineamento all'interno di questi modelli. In primo luogo, durante la fase di pre-addestramento, il modello di solito assume che tutte le coppie immagine-testo siano uniformemente allineate, ma in realtà il grado di allineamento tra diverse coppie immagine-testo è incoerente. In secondo luogo, le istruzioni attualmente utilizzate per il fine-tuning incorporano una varietà di compiti, e le istruzioni di compiti diversi richiedono solitamente diversi livelli di capacità di allineamento, ma i precedenti MLLMs trascurano queste esigenze di allineamento differenziate. Per affrontare questi problemi, proponiamo un nuovo modello linguistico multimodale di grande scala, AlignGPT. Nella fase di pre-addestramento, invece di trattare tutte le coppie immagine-testo allo stesso modo, assegniamo diversi livelli di capacità di allineamento a diverse coppie immagine-testo. Poi, nella fase di ottimizzazione su istruzioni, combiniamo in modo adattivo questi diversi livelli di capacità di allineamento per soddisfare le esigenze dinamiche di allineamento di diverse istruzioni. I risultati sperimentali estesi mostrano che il nostro modello raggiunge prestazioni competitive su 12 benchmark.

Negli ultimi anni, grazie ai risultati di generazione realistici e a una vasta gamma di applicazioni personalizzate, i modelli generativi basati sulla diffusione hanno attirato grande attenzione sia nel campo della generazione visiva che in quella audio. Rispetto ai notevoli progressi nella generazione da testo a immagine o da testo a audio, la ricerca nella generazione da audio a visivo o da visivo a audio è stata relativamente lenta. I recenti metodi di generazione audio-visiva si affidano solitamente a enormi modelli linguistici o a modelli di diffusione componibili. Invece di progettare un altro modello gigantesco per la generazione audio-visiva, in questo articolo facciamo un passo indietro dimostrando che un semplice e leggero trasformatore generativo, non ancora completamente esplorato nella generazione multimodale, può ottenere risultati eccellenti nella generazione da immagine a audio. Il trasformatore opera nello spazio discreto audio e visivo del Vector-Quantized GAN ed è addestrato con un approccio di denoising a maschera. Dopo l'addestramento, la guida senza classificatore può essere implementata direttamente, ottenendo prestazioni migliori senza alcun addestramento o modifica aggiuntiva. Poiché il modello trasformatore è simmetrico rispetto alle modalità, può anche essere direttamente utilizzato per la generazione da audio a immagine e per la co-generazione. Negli esperimenti, dimostriamo che il nostro metodo semplice supera i recenti metodi di generazione da immagine a audio. Campioni audio generati possono essere trovati all'indirizzo https://docs.google.com/presentation/d/1ZtC0SeblKkut4XJcRaDsSTuCRIXB3ypxmSi7HTY3IyQ.

Investighiamo il compito di adattare modelli generativi di immagini a diversi dataset senza eseguire il fine-tuning. A tal fine, introduciamo Semantica, un modello di diffusione condizionato da immagini in grado di generare immagini basandosi sulla semantica di un'immagine di condizionamento. Semantica viene addestrato esclusivamente su coppie di immagini su scala web, ovvero riceve un'immagine casuale da una pagina web come input condizionale e modella un'altra immagine casuale dalla stessa pagina web. I nostri esperimenti evidenziano l'espressività degli encoder di immagini pre-addestrati e la necessità di un filtraggio dei dati basato sulla semantica per ottenere una generazione di immagini di alta qualità. Una volta addestrato, il modello può generare in modo adattivo nuove immagini da un dataset semplicemente utilizzando immagini provenienti da quel dataset come input. Studiamo le proprietà di trasferimento di Semantica su ImageNet, LSUN Churches, LSUN Bedroom e SUN397.

Estendiamo i trasformatori multimodali per includere il movimento della telecamera 3D come segnale di condizionamento per il compito di generazione video. I modelli generativi di video stanno diventando sempre più potenti, concentrando così gli sforzi di ricerca su metodi per controllare l'output di tali modelli. Proponiamo di aggiungere controlli virtuali della telecamera 3D ai metodi generativi di video condizionando il video generato su una codifica del movimento tridimensionale della telecamera durante il corso del video generato. I risultati dimostrano che siamo (1) in grado di controllare con successo la telecamera durante la generazione del video, partendo da un singolo fotogramma e da un segnale della telecamera, e (2) dimostriamo l'accuratezza dei percorsi generati della telecamera 3D utilizzando metodi tradizionali di visione artificiale.

Personalizzare i modelli di diffusione per generare immagini che preservino l'identità a partire da immagini di riferimento fornite dall'utente rappresenta un nuovo e affascinante problema. Gli approcci prevalenti richiedono tipicamente un addestramento su un ampio numero di immagini specifiche del dominio per ottenere la preservazione dell'identità, il che manca di flessibilità in diversi casi d'uso. Per affrontare questa problematica, sfruttiamo la guida del classificatore, una tecnica priva di addestramento che orienta i modelli di diffusione utilizzando un classificatore esistente, per la generazione di immagini personalizzate. Il nostro studio dimostra che, basandosi su un recente framework di flusso rettificato, la principale limitazione della guida del classificatore standard, che richiede un classificatore speciale, può essere risolta con una semplice soluzione a punto fisso, consentendo una personalizzazione flessibile con discriminatori di immagini preesistenti. Inoltre, la procedura di risoluzione si dimostra stabile quando ancorata a una traiettoria di flusso di riferimento, con una garanzia di convergenza. Il metodo derivato è implementato sul flusso rettificato con diversi discriminatori di immagini preesistenti, ottenendo risultati di personalizzazione vantaggiosi per volti umani, soggetti viventi e determinati oggetti. Il codice è disponibile all'indirizzo https://github.com/feifeiobama/RectifID.

I Neural Radiance Fields (NeRFs) incontrano generalmente difficoltà nel ricostruire e renderizzare oggetti altamente speculari, il cui aspetto varia rapidamente con i cambiamenti del punto di vista. Recenti lavori hanno migliorato la capacità dei NeRF di renderizzare l'aspetto dettagliato e speculare dell'illuminazione ambientale distante, ma non sono in grado di sintetizzare riflessi coerenti di contenuti più vicini. Inoltre, queste tecniche si basano su grandi reti neurali computazionalmente costose per modellare la radianza uscente, il che limita fortemente la velocità di ottimizzazione e rendering. Affrontiamo questi problemi con un approccio basato sul ray tracing: invece di interrogare una costosa rete neurale per la radianza uscente dipendente dalla vista in punti lungo ogni raggio della telecamera, il nostro modello lancia raggi di riflessione da questi punti e li traccia attraverso la rappresentazione NeRF per renderizzare vettori di feature che vengono decodificati in colore utilizzando una piccola rete poco costosa. Dimostriamo che il nostro modello supera i metodi precedenti per la sintesi di viste di scene contenenti oggetti lucidi, e che è l'unico metodo NeRF esistente in grado di sintetizzare un aspetto speculare e riflessi fotorealistici in scene del mondo reale, richiedendo un tempo di ottimizzazione paragonabile ai modelli di sintesi di viste all'avanguardia attuali.

La sintesi di nuove viste di oggetti speculari come metalli lucidi o vernici brillanti rimane una sfida significativa. Non solo l'aspetto lucido, ma anche gli effetti di illuminazione globale, inclusi i riflessi di altri oggetti nell'ambiente, sono componenti cruciali per riprodurre fedelmente una scena. In questo articolo, presentiamo Neural Directional Encoding (NDE), una codifica dell'aspetto dipendente dalla vista per i campi di radianza neurale (NeRF) per il rendering di oggetti speculari. L'NDE trasferisce il concetto di codifica spaziale basata su griglie di feature al dominio angolare, migliorando significativamente la capacità di modellare segnali angolari ad alta frequenza. A differenza dei metodi precedenti che utilizzano funzioni di codifica con solo input angolare, noi tracciamo anche le feature spaziali per ottenere una codifica direzionale variabile spazialmente, che affronta gli effetti di interriflessione complessi. Esperimenti estesi su dataset sia sintetici che reali dimostrano che un modello NeRF con NDE (1) supera lo stato dell'arte nella sintesi di viste di oggetti speculari e (2) funziona con reti di piccole dimensioni per consentire inferenze veloci (in tempo reale). La pagina web del progetto e il codice sorgente sono disponibili all'indirizzo: https://lwwu2.github.io/nde/.

In questo articolo presentiamo Tele-Aloha, un sistema di telepresenza bidirezionale a basso costo e alta autenticità, progettato per scenari di comunicazione peer-to-peer. Rispetto ai sistemi precedenti, Tele-Aloha utilizza solo quattro telecamere RGB sparse, una GPU di livello consumer e uno schermo autostereoscopico per ottenere una comunicazione a distanza ad alta risoluzione (2048x2048), in tempo reale (30 fps), a bassa latenza (meno di 150 ms) e robusta. Come nucleo di Tele-Aloha, proponiamo un algoritmo efficiente di sintesi di nuove viste per la parte superiore del corpo. In primo luogo, progettiamo uno stimatore di disparità a cascata per ottenere un indizio geometrico robusto. Inoltre, introduciamo un rasterizzatore neurale basato su Gaussian Splatting per proiettare le caratteristiche latenti sulla vista target e decodificarle in una risoluzione ridotta. Inoltre, grazie ai dati catturati di alta qualità, sfruttiamo un meccanismo di fusione ponderata per affinare l'immagine decodificata nella risoluzione finale di 2K. Sfruttando uno schermo autostereoscopico all'avanguardia e un tracciamento dell'iride a bassa latenza, gli utenti possono sperimentare un forte senso di tridimensionalità anche senza alcun dispositivo di visualizzazione indossabile. Nel complesso, il nostro sistema di telepresenza dimostra un senso di co-presenza in esperimenti reali, ispirando la prossima generazione di comunicazione.