Rassegna preparata con l'IA a partire dalle fonti linkate, sotto la supervisione di Alberto Gaia.
Prendere 123 librerie open source già compilate e dimostrare matematicamente che non vanno in crash: è il risultato della verifica formale con Claude pubblicata ieri da Anthropic, con circa 180 milioni di righe di dimostrazioni e centinaia di bug trovati lungo la strada. Nella rassegna di oggi ci sono anche il sistema diagnostico di Microsoft che su Science batte i medici nei casi difficili, il red teaming di METR e Redwood sul monitor interno degli agenti di OpenAI, quattro nuovi progetti nella fondazione open source per gli agenti, il maxi round di DeepSeek e un esperimento su cosa pensano gli umani i modelli linguistici.
Verifica formale con Claude: 123 librerie dimostrate a prova di crash
Il Frontier Red Team di Anthropic, insieme alla startup Theorem, ha usato Claude per scrivere dimostrazioni formali sul codice binario di 123 librerie open source. Il punto di partenza sono stati i test di fuzzing del progetto OSS-Fuzz di Google: Claude li ha trasformati in specifiche e ha dimostrato che 239 punti d’ingresso non possono andare in crash con input inferiori a 64 MB. Le prove lavorano direttamente sull’assembly RISC-V, sono scritte nel linguaggio Rocq e in totale contano circa 180 milioni di righe; il lavoro ha richiesto qualche settimana.
Durante il processo sono emersi e sono stati corretti centinaia di bug, alcuni molto difficili da raggiungere: una scrittura fuori dai limiti in un decompressore che si manifestava solo con input di circa 20 MB e una disposizione dei dati rara, o una lettura fuori dai limiti in un decoder di immagini che richiedeva un file da 64 MB e oltre 2 GB di memoria. Anthropic stessa precisa i limiti: le prove valgono per binari statici a singolo thread su RISC-V con musl e Linux, non per le configurazioni x86 o ARM con glibc più diffuse, e “verificato” non vuol dire “senza bug”. Una parte delle dimostrazioni è pubblicata su GitHub.
Microsoft MAI-DxO su Science: 83% di diagnosi corrette contro il 36% dei medici
Microsoft AI ha pubblicato su Science lo studio su MAI-DxO, il sistema che coordina più agenti come se fossero un gruppo di medici al lavoro su un caso. Secondo l’annuncio di Microsoft, su 304 casi complessi del New England Journal of Medicine il sistema ha dato la diagnosi giusta nell’83% dei casi, contro il 36% dei medici che potevano consultare materiale di riferimento e il 22% di quelli senza. Sui casi di pronto soccorso del dataset MIMIC-IV-ED il confronto è 80% contro 47%, e secondo Microsoft il sistema ottiene questi risultati con costi ridotti alla metà o a un terzo.
Come nota TechCrunch, nel confronto c’erano medici di base e internisti che lavoravano da soli, non specialisti o équipe. Microsoft ha avviato uno studio sul campo con il Beth Israel Deaconess Medical Center di Boston e sta addestrando con la Mayo Clinic un modello di base per la sanità, la cui uscita è prevista per il prossimo anno.
METR e Redwood hanno messo alla prova il monitor degli agenti di OpenAI
Redwood Research e METR hanno pubblicato il resoconto di un red teaming sul sistema interno con cui OpenAI sorveglia i propri agenti, quello che controlla il traffico agentico della Responses API usato anche da Codex. Il test, condotto da un dipendente di ciascuna delle due organizzazioni tra il 21 luglio e l’11 agosto 2026, ha prodotto un rapporto interno di 61 pagine, diffuso in una versione di 38 pagine con le parti riservate oscurate da OpenAI.
Tra i punti deboli segnalati: le fasi di compattazione del contesto non venivano monitorate, tanto che fra maggio e luglio circa il 10% del traffico interno di Codex potrebbe essere sfuggito ai controlli; la revisione scattava solo quando l’agente restituiva il controllo all’utente; esisteva un modo per aggirare la sandbox di Codex; due intestazioni gestite dal client potevano disattivare il monitoraggio per nuove istanze. OpenAI afferma di aver corretto tutte le vulnerabilità che riguardavano il sistema in produzione.
Pausa dalla rassegna, giusto il tempo di una vignetta.
Agent Skills e Open Responses entrano nella Agentic AI Foundation
Alla AGNTCon + MCPCon di San Jose la Agentic AI Foundation della Linux Foundation ha accolto quattro nuovi progetti: Agent Skills, il formato per impacchettare istruzioni, script e risorse che gli agenti caricano al bisogno, donato da Anthropic; Open Responses, la specifica di OpenAI per interfacce compatibili tra fornitori diversi, basata sulla sua Responses API; OpenEnv di Hugging Face, per creare e condividere ambienti di reinforcement learning; OpenSandbox di Alibaba, una piattaforma sandbox con runtime Docker e Kubernetes.
Con queste aggiunte la fondazione arriva a 10 progetti ospitati, contro i 3 del lancio di dicembre 2025, fra cui MCP, AGENTS.md, A2A e goose. Anthropic ha spiegato la donazione in un post sul suo blog.
DeepSeek raccoglie circa 15 miliardi di dollari
Secondo Bloomberg, ripreso da TechCrunch, DeepSeek ha chiuso un round da circa 15 miliardi di dollari (circa 100 miliardi di yuan), uno dei più grandi mai visti in Cina, con Tencent e il produttore di batterie CATL fra i possibili investitori. La notizia arriva due giorni dopo l’ordine del governo statunitense di eliminare la tecnologia di DeepSeek dalle agenzie federali civili, di cui avevamo parlato nella rassegna del 20 ottobre. A giugno l’azienda di Hangzhou aveva raccolto più di 7 miliardi a una valutazione di 50 miliardi, e si parla di una possibile quotazione in Cina già dal prossimo anno. DeepSeek non ha commentato.
Chiudiamo con la stessa opinione “controversa” sugli umani
ModelCompare ha chiesto a 12 modelli di testo, tre volte ciascuno e senza prompt di sistema, la loro opinione più controversa sugli esseri umani. Il risultato: 29 risposte su 35 dicono in sostanza la stessa cosa, cioè che le persone mettono l’appartenenza al gruppo, lo status o una storia lusinghiera su se stesse davanti alla verità. Fra le eccezioni c’è Claude Opus 5.5, secondo cui le persone sono più perbene di quanto credano, mentre Grok 4.7 una volta si è rifiutato di rispondere.
Anche sei modelli di immagini, con due disegni ciascuno, hanno mostrato poca fantasia: 10 vignette su 12 usano la stessa battuta, gli umani incollati al telefono mentre il pianeta va a rotoli. L’intero esperimento, 60 chiamate in tutto, è costato 1,54 dollari.
Dimostrazioni da 180 milioni di righe scritte da un modello e controllate da un verificatore automatico: vi fidereste di più di una libreria con una prova formale che di una con anni di test alle spalle? Ieri, sullo stesso filone, c’erano le falle PHP trovate dall’IA.
Lascia un commento