Vitalik Buterin propone un nuovo linguaggio di programmazione per l'intelligenza artificiale

Vitalik Buterin, co-fondatore di Ethereum, ha presentato l'idea di sviluppare un nuovo linguaggio di programmazione il cui obiettivo è semplificare la verifica delle uscite dell'intelligenza artificiale. Questo linguaggio potrebbe essere compilato in strumenti di prova formale come Lean o HOL. Buterin crede che, con l'aumento dell'uso dei modelli di intelligenza artificiale nello sviluppo software, questi strumenti saranno in grado di generare prove matematiche e tecniche complesse, ma comprendere e verificare queste uscite sarà difficile per gli esseri umani. Ha suggerito che le parti leggibili per gli esseri umani dovrebbero essere separate dai dettagli tecnici delle prove. L'obiettivo di questo linguaggio è rendere più leggibili le uscite dell'intelligenza artificiale. Buterin spiega che i passaggi interni di una prova devono essere matematicamente corretti e non è necessario che un essere umano legga tutti questi passaggi. La definizione dei concetti e delle specifiche tecniche deve essere scritta in un linguaggio semplice. Ha anche accennato al fatto che i modelli di linguaggio di grandi dimensioni possono generare prove utilizzabili per Lean. Questa proposta è emersa mentre i ricercatori di Ethereum stanno lavorando allo sviluppo di una versione della macchina virtuale di Ethereum (EVM) con capacità di prova formale e basata su conoscenza zero. Buterin è convinto che l'uso di codici con prova formale possa contribuire ad aumentare la sicurezza dei software basati su blockchain. Tuttavia, ha sottolineato che questa idea è ancora in fase concettuale e non è stato pubblicato alcun prototipo.