Maxwell is een innovatief Code Execution Model (CEM) ontwikkeld door doubleAI. In tegenstelling tot traditionele compilers, analyseert Maxwell software terwijl deze wordt uitgevoerd. Het observeert de datastroom en de specifieke hardware om de onderliggende binaries in real-time te herschrijven en te optimaliseren.
De belangrijkste kenmerken en resultaten zijn:
- Formele Verificatie: Om fouten te voorkomen, maakt Maxwell gebruik van wiskundige bewijzen van semantische equivalentie. Dit garandeert dat de geoptimaliseerde code exact hetzelfde resultaat geeft als het origineel.
- Prestatieverbeteringen: Het model realiseert significante snelheidswinsten, zoals 38× snellere dataprocessing-pipelines en 4,25× snellere AI-inference kernels. Concrete voorbeelden zijn de versnelling van 4K-videogeneratie in LTX-2.5, Whisper-transcripties en Pandas-kernels.
- Hardware-agnostisch: Maxwell optimaliseert zowel CPU-code (via SIMD-implementaties) als GPU-code (via gespecialiseerde kernels).
- Filosofische basis: Geïnspireerd door Alan Turing, streeft Maxwell ernaar de strikte scheiding tussen het 'denkloze' uitvoeren van code en het beslissen over optimalisaties op te heffen.
Kortom, Maxwell fungeert als een agent voor de machine die code zelf-verbeterend maakt zonder de broncode aan te passen, wat leidt tot een veel efficiënter gebruik van schaarse rekenkracht.
Maxwell: Het eerste Code Execution Model (door doubleAI)
Prestaties
- 38× snellere dataprocessing-pipelines.
- 4,25× snellere AI-inference kernels.
Wat is een code execution model?
De meeste code "ziet" de hardware waarop hij draait of de data die hij verwerkt nooit. Een code execution model (CEM) kijkt naar een programma terwijl het draait, herschrijft de onderliggende binary om deze exact aan die machine en data aan te passen, en bewijst formeel dat elke verbetering equivalent is aan het origineel. Maxwell werkt op zowel CPU's als GPU's en versnelt hiermee datapipe-lines en AI-inference kernels.
Maxwell in de praktijk
Zodra Maxwell voldoende runtime-data heeft verzameld, vervangt het stukken code door formeel bewezen optimalisaties die zijn afgestemd op de specifieke machine, terwijl het programma blijft draaien.
LTX-2.5: 4K-videogeneratie in de helft van de tijd
LTX-2.5 is een state-of-the-art open world model dat video, audio en de fysieke wereld genereert en simuleert. Hoewel de pipeline al door experts was geoptimaliseerd (gecompileerd end-to-end, sequence-parallel over GPU's en met een handgeschreven attention kernel), wist Maxwell de generatie van 4K-video bijna twee keer zo snel te maken.
- Resultaat: 1,87× snellere 4K-videogeneratie.
- Tijd: Van 250 seconden naar 134 seconden per 4K-clip op twee B200's.
- Kwaliteit: De video's zijn visueel onscheidbaar van het origineel.
Maxwell voerde meer dan een dozijn significante wijzigingen door, variërend van algoritmische aanpassingen tot edits in individuele GPU-kernels, waaronder:
- Attention over twee GPU's.
- Dunnere tiling-naden (tiling seams).
- Wijzigingen binnen de decoder.
GPU-gebaseerde spraak-naar-tekst (Whisper)
Bij het uitvoeren van 180 transcripties met Whisper-small op een RTX 4090 vanaf een koude start, waren de resultaten als volgt:
- Zonder Maxwell: 106,23 seconden.
- Met Maxwell: 49,82 seconden.
- Resultaat: Identieke transcripties.
CPU-gebaseerde graafalgoritmen
Bij het uitvoeren van NetworkX betweenness centrality (15 runs) op dezelfde machine:
- Zonder Maxwell: 61,44 seconden.
- Met Maxwell: 17,50 seconden.
- Resultaat: Identieke resultaten.
Onderzoek achter Maxwell
- Speed of Light op Blackwell: Na één dag zoeken verslaat Maxwell de PyTorch-baselines van NVIDIA op 90% van de SOL-ExecBench Blackwell-kernels.
- NVIDIA cuGraph: Maxwell genereerde en verifieerde onafhankelijk een hyper-geoptimaliseerde drop-in versie van NVIDIA cuGraph, die gemiddeld 3,6× sneller is.
- Pandas: Maxwell heeft de kernels van pandas volledig vanaf nul herschreven, gespecialiseerd voor moderne hardware, zonder dat er een regel broncode hoefde te worden aangepast.
---
De filosofie: All Thinking Things
"Wat we willen is een machine die kan leren van ervaring. De mogelijkheid om de machine zijn eigen instructies te laten wijzigen, biedt het mechanisme hiervoor." — Alan Turing, London Mathematical Society, februari 1947.
In 1952 speelde Alan Turing een schaakpartij tegen zijn collega Alick Glennie. Turing nam de rol van een computer aan: hij had een schaakprogramma op papier geschreven en volgde bij elke zet de instructies letterlijk op. Elke zet kostte hem ongeveer een half uur. Hij verloor.
Tijdens dat spel deed Turing precies wat een computer doet: hij voerde het programma trouw uit, zonder een enkele regel te verbeteren, hoe voor de hand liggend die verbeteringen soms ook waren.
Sinds de komst van computers is er een strikte arbeidsverdeling: mensen beslissen en schrijven precies wat een programma moet doen, en de computer voert dit mechanisch, deterministisch en "denkloos" uit. Zelfs moderne AI-modellen die code schrijven, leveren code die uiteindelijk op dezezelfde manier mechanisch wordt uitgevoerd.
De noodzaak voor CEMs
Als Turing vrij geweest zou zijn om te handelen naar wat hij op het bord zag, had hij zijn programma bij elke zet kunnen verbeteren. Analoog hieraan zou elke regel computercode versneld of verbeterd kunnen worden als deze gekoppeld zou zijn aan volledige "contextuele kennis" van de omgeving, de hardware en de datastroom.
Bij doubleAI zijn Code Execution Models (CEMs) ontwikkeld om dit te realiseren. Een CEM bevindt zich tussen de code en het silicium. Het leeft binnen het draaiende programma, observeert de datastroom en hervormt de algoritmen en instructies terwijl het programma draait. De output is een binary die direct op de hardware wordt uitgevoerd. Omdat er geen mens in de loop is, mag het model nooit een fout maken.
Bewijzen, Wiskunde en Code
Om veiligheid te garanderen, maakt Maxwell gebruik van formele verificatie¹: het schrijven van een bewijs in een taal die precies genoeg is voor een computer om elke stap te controleren.
Superoptimalisatie
Maxwell's doel is superoptimalisatie: het vinden van de allersnelste manier om een stuk code uit te voeren op de specifieke machine waar hij op draait. Terwijl het programma draait, identificeert Maxwell bottlenecks en creëert hij een nieuwe versie van de machine-instructies (vergelijkbaar met een just-in-time compiler, maar met veel meer vrijheid in de vorm van het algoritme⁴).
Cruciaal is dat de broncode ongewijzigd blijft. Alleen de onderliggende binaries worden vervangen door versies die bewezen exact equivalent zijn.
Semantische Equivalentie
Twee programma's zijn semantisch equivalent wanneer ze, bij dezelfde input, altijd hetzelfde resultaat produceren en hetzelfde effect hebben op de wereld om hen heen. Een formeel bewijs van equivalentie stelt dit vast voor elke mogelijke input en elk scenario tegelijk.
Voorbeeld van equivalentie:
``python def original(n): s = 0 for i in range(n): for j in range(i): s += 1 return s ``
``rust fn replacement(n: i64) -> i64 { n * (n - 1) / 2 } ``
Vereist $n : \text{int}$ en $0 \le n \le 3037000500$. Theorem: original(n) = replacement(n) Door inductie op $n$:
- Case 0:
original(0) = 0 = replacement(0)
- Case $n + 1$:
original(n + 1) = original(n) + n = n(n − 1)/2 + n = (n + 1)n/2 = replacement(n + 1) $\blacksquare$
De Curry-Howard correspondentie
Er bestaat een diepe verbinding tussen programma's en bewijzen, bekend als de Curry-Howard correspondentie. In essentie is een bewijs een programma, en het controleren van een bewijs komt overeen met het controleren of het programma correct is opgebouwd. Type-checking is hierbij het mechanisme waarmee het bewijs wordt geverifieerd.
Doorbraken in Python-formalisering
Een van de grootste uitdagingen was de formalisering van de programmeertaal Python, omdat deze zeer dynamisch is (waarden kunnen van type veranderen terwijl het programma draait). doubleAI heeft Python volledig geformaliseerd, inclusief communicatie en bestandsgebruik. Hierdoor kan Maxwell nieuwe code schrijven samen met een formeel bewijs van semantische equivalentie.
Maxwell maakt gebruik van herbruikbare "proof gadgets" om deze bewijzen efficiënt op te bouwen, een taak waar AI superieur is aan mensen.
Hardware-optimalisatie
Maxwell optimaliseert zowel CPU- als GPU-code:
- CPU: Python-code wordt vervangen door low-level, bare-metal geoptimaliseerde code (zoals directe SIMD-implementaties).
- GPU: PyTorch-code wordt vervangen door hooggeoptimaliseerde kernels voor de specifieke GPU in de machine.
Omdat elke versnelling gepaard gaat met een machine-gecontroleerd bewijs, kan Maxwell transformaties durven uitvoeren die een menselijke engineer of een standaard compiler nooit zou riskeren.
Maxwell: Een Agent voor de Machine
AI in software heeft tot nu toe gewerkt voor programmeurs. Maxwell werkt voor de machine. Hij observeert de hardware en de data en past de code hierop aan.
Zodra Maxwell een snellere versie van code heeft bewezen, wordt die versie het startpunt voor de volgende poging. De code is daarmee zelf-verbeterend, terwijl de broncode exact blijft zoals de auteur deze heeft achtergelaten.
In een wereld waar rekenkracht een schaars middel is, kan Maxwell helpen om code efficiënter uit te voeren. Zoals Turing in 1952 zijn programma exact moest volgen, hoeven onze machines dat nu niet meer.
***
Voetnoten: ¹ Formele verificatie is de praktijk van het schrijven van een bewijs in een taal die precies genoeg is voor een computer om elke stap te controleren. ² Het bewijs van de Laatste Stelling van Fermat werd door AI-agents van Anthropic in elf dagen geschreven, waar een team van menselijke wiskundigen in 2024 vijf jaar voor had gepland. ³ Maxwell is vernoemd naar het wezen dat James Clerk Maxwell in 1867 imagineerde, dat de entropie van een gas verlaagde door moleculen te sorteren. ⁴ Compilers en JIT-compilers (zoals torch.compile en PyPy) zijn beperkt tot transformaties die vooraf door ingenieurs zijn geschreven. Superoptimaliseerders zoals STOKE zijn beperkt tot korte, lus-vrije fragmenten. Maxwell herschrijft volledige functies en algoritmen in real-world programma's tijdens de uitvoering. ⁵ De stelling van Rice stelt dat geen enkel algoritme semantische equivalentie voor elk paar programma's kan beslissen. Dit is een limiet voor een universele procedure, maar niet voor een specifiek paar programma's.
Maxwell: Het eerste Code Execution Model (door doubleAI)
Prestaties
- 38× snellere dataprocessing-pipelines.
- 4,25× snellere AI-inference kernels.
Wat is een code execution model?
De meeste code "ziet" de hardware waarop hij draait of de data die hij verwerkt nooit. Een code execution model (CEM) kijkt naar een programma terwijl het draait, herschrijft de onderliggende binary om deze exact aan die machine en data aan te passen, en bewijst formeel dat elke verbetering equivalent is aan het origineel. Maxwell werkt op zowel CPU's als GPU's en versnelt hiermee datapipe-lines en AI-inference kernels.
Maxwell in de praktijk
Zodra Maxwell voldoende runtime-data heeft verzameld, vervangt het stukken code door formeel bewezen optimalisaties die zijn afgestemd op de specifieke machine, terwijl het programma blijft draaien.
LTX-2.5: 4K-videogeneratie in de helft van de tijd
LTX-2.5 is een state-of-the-art open world model dat video, audio en de fysieke wereld genereert en simuleert. Hoewel de pipeline al door experts was geoptimaliseerd (gecompileerd end-to-end, sequence-parallel over GPU's en met een handgeschreven attention kernel), wist Maxwell de generatie van 4K-video bijna twee keer zo snel te maken.
- Resultaat: 1,87× snellere 4K-videogeneratie.
- Tijd: Van 250 seconden naar 134 seconden per 4K-clip op twee B200's.
- Kwaliteit: De video's zijn visueel onscheidbaar van het origineel.
Maxwell voerde meer dan een dozijn significante wijzigingen door, variërend van algoritmische aanpassingen tot edits in individuele GPU-kernels, waaronder:
- Attention over twee GPU's.
- Dunnere tiling-naden (tiling seams).
- Wijzigingen binnen de decoder.
GPU-gebaseerde spraak-naar-tekst (Whisper)
Bij het uitvoeren van 180 transcripties met Whisper-small op een RTX 4090 vanaf een koude start, waren de resultaten als volgt:
- Zonder Maxwell: 106,23 seconden.
- Met Maxwell: 49,82 seconden.
- Resultaat: Identieke transcripties.
CPU-gebaseerde graafalgoritmen
Bij het uitvoeren van NetworkX betweenness centrality (15 runs) op dezelfde machine:
- Zonder Maxwell: 61,44 seconden.
- Met Maxwell: 17,50 seconden.
- Resultaat: Identieke resultaten.
Onderzoek achter Maxwell
- Speed of Light op Blackwell: Na één dag zoeken verslaat Maxwell de PyTorch-baselines van NVIDIA op 90% van de SOL-ExecBench Blackwell-kernels.
- NVIDIA cuGraph: Maxwell genereerde en verifieerde onafhankelijk een hyper-geoptimaliseerde drop-in versie van NVIDIA cuGraph, die gemiddeld 3,6× sneller is.
- Pandas: Maxwell heeft de kernels van pandas volledig vanaf nul herschreven, gespecialiseerd voor moderne hardware, zonder dat er een regel broncode hoefde te worden aangepast.
---
De filosofie: All Thinking Things
"Wat we willen is een machine die kan leren van ervaring. De mogelijkheid om de machine zijn eigen instructies te laten wijzigen, biedt het mechanisme hiervoor." — Alan Turing, London Mathematical Society, februari 1947.
In 1952 speelde Alan Turing een schaakpartij tegen zijn collega Alick Glennie. Turing nam de rol van een computer aan: hij had een schaakprogramma op papier geschreven en volgde bij elke zet de instructies letterlijk op. Elke zet kostte hem ongeveer een half uur. Hij verloor.
Tijdens dat spel deed Turing precies wat een computer doet: hij voerde het programma trouw uit, zonder een enkele regel te verbeteren, hoe voor de hand liggend die verbeteringen soms ook waren.
Sinds de komst van computers is er een strikte arbeidsverdeling: mensen beslissen en schrijven precies wat een programma moet doen, en de computer voert dit mechanisch, deterministisch en "denkloos" uit. Zelfs moderne AI-modellen die code schrijven, leveren code die uiteindelijk op dezezelfde manier mechanisch wordt uitgevoerd.
De noodzaak voor CEMs
Als Turing vrij geweest zou zijn om te handelen naar wat hij op het bord zag, had hij zijn programma bij elke zet kunnen verbeteren. Analoog hieraan zou elke regel computercode versneld of verbeterd kunnen worden als deze gekoppeld zou zijn aan volledige "contextuele kennis" van de omgeving, de hardware en de datastroom.
Bij doubleAI zijn Code Execution Models (CEMs) ontwikkeld om dit te realiseren. Een CEM bevindt zich tussen de code en het silicium. Het leeft binnen het draaiende programma, observeert de datastroom en hervormt de algoritmen en instructies terwijl het programma draait. De output is een binary die direct op de hardware wordt uitgevoerd. Omdat er geen mens in de loop is, mag het model nooit een fout maken.
Bewijzen, Wiskunde en Code
Om veiligheid te garanderen, maakt Maxwell gebruik van formele verificatie¹: het schrijven van een bewijs in een taal die precies genoeg is voor een computer om elke stap te controleren.
Superoptimalisatie
Maxwell's doel is superoptimalisatie: het vinden van de allersnelste manier om een stuk code uit te voeren op de specifieke machine waar hij op draait. Terwijl het programma draait, identificeert Maxwell bottlenecks en creëert hij een nieuwe versie van de machine-instructies (vergelijkbaar met een just-in-time compiler, maar met veel meer vrijheid in de vorm van het algoritme⁴).
Cruciaal is dat de broncode ongewijzigd blijft. Alleen de onderliggende binaries worden vervangen door versies die bewezen exact equivalent zijn.
Semantische Equivalentie
Twee programma's zijn semantisch equivalent wanneer ze, bij dezelfde input, altijd hetzelfde resultaat produceren en hetzelfde effect hebben op de wereld om hen heen. Een formeel bewijs van equivalentie stelt dit vast voor elke mogelijke input en elk scenario tegelijk.
Voorbeeld van equivalentie:
``python def original(n): s = 0 for i in range(n): for j in range(i): s += 1 return s ``
``rust fn replacement(n: i64) -> i64 { n * (n - 1) / 2 } ``
Vereist $n : \text{int}$ en $0 \le n \le 3037000500$. Theorem: original(n) = replacement(n) Door inductie op $n$:
- Case 0:
original(0) = 0 = replacement(0)
- Case $n + 1$:
original(n + 1) = original(n) + n = n(n − 1)/2 + n = (n + 1)n/2 = replacement(n + 1) $\blacksquare$
De Curry-Howard correspondentie
Er bestaat een diepe verbinding tussen programma's en bewijzen, bekend als de Curry-Howard correspondentie. In essentie is een bewijs een programma, en het controleren van een bewijs komt overeen met het controleren of het programma correct is opgebouwd. Type-checking is hierbij het mechanisme waarmee het bewijs wordt geverifieerd.
Doorbraken in Python-formalisering
Een van de grootste uitdagingen was de formalisering van de programmeertaal Python, omdat deze zeer dynamisch is (waarden kunnen van type veranderen terwijl het programma draait). doubleAI heeft Python volledig geformaliseerd, inclusief communicatie en bestandsgebruik. Hierdoor kan Maxwell nieuwe code schrijven samen met een formeel bewijs van semantische equivalentie.
Maxwell maakt gebruik van herbruikbare "proof gadgets" om deze bewijzen efficiënt op te bouwen, een taak waar AI superieur is aan mensen.
Hardware-optimalisatie
Maxwell optimaliseert zowel CPU- als GPU-code:
- CPU: Python-code wordt vervangen door low-level, bare-metal geoptimaliseerde code (zoals directe SIMD-implementaties).
- GPU: PyTorch-code wordt vervangen door hooggeoptimaliseerde kernels voor de specifieke GPU in de machine.
Omdat elke versnelling gepaard gaat met een machine-gecontroleerd bewijs, kan Maxwell transformaties durven uitvoeren die een menselijke engineer of een standaard compiler nooit zou riskeren.
Maxwell: Een Agent voor de Machine
AI in software heeft tot nu toe gewerkt voor programmeurs. Maxwell werkt voor de machine. Hij observeert de hardware en de data en past de code hierop aan.
Zodra Maxwell een snellere versie van code heeft bewezen, wordt die versie het startpunt voor de volgende poging. De code is daarmee zelf-verbeterend, terwijl de broncode exact blijft zoals de auteur deze heeft achtergelaten.
In een wereld waar rekenkracht een schaars middel is, kan Maxwell helpen om code efficiënter uit te voeren. Zoals Turing in 1952 zijn programma exact moest volgen, hoeven onze machines dat nu niet meer.
***
Voetnoten: ¹ Formele verificatie is de praktijk van het schrijven van een bewijs in een taal die precies genoeg is voor een computer om elke stap te controleren. ² Het bewijs van de Laatste Stelling van Fermat werd door AI-agents van Anthropic in elf dagen geschreven, waar een team van menselijke wiskundigen in 2024 vijf jaar voor had gepland. ³ Maxwell is vernoemd naar het wezen dat James Clerk Maxwell in 1867 imagineerde, dat de entropie van een gas verlaagde door moleculen te sorteren. ⁴ Compilers en JIT-compilers (zoals torch.compile en PyPy) zijn beperkt tot transformaties die vooraf door ingenieurs zijn geschreven. Superoptimaliseerders zoals STOKE zijn beperkt tot korte, lus-vrije fragmenten. Maxwell herschrijft volledige functies en algoritmen in real-world programma's tijdens de uitvoering. ⁵ De stelling van Rice stelt dat geen enkel algoritme semantische equivalentie voor elk paar programma's kan beslissen. Dit is een limiet voor een universele procedure, maar niet voor een specifiek paar programma's.
Groetjes,