Maxwell schreibt laufende Programme um und beweist jede Optimierung formal
Maxwell: A new kind of model that sits between code and hardware
doubleAI stellt Maxwell vor, ein „Code Execution Model“, das während der Laufzeit Binärcode analysiert und durch formal als semantisch äquivalent bewiesene, hardware- und datenspezifische Versionen ersetzt. Der Quellcode bleibt unangetastet. In Demos beschleunigt Maxwell die 4K-Videogenerierung von LTX-2.5 um das 1,87-Fache und Whisper-Transkriptionen auf einer RTX 4090 von 106 auf 50 Sekunden – bei identischen Ergebnissen.
Ein CEM lebt im laufenden Programm, beobachtet den Datenfluss und formt Algorithmen und Instruktionen im Betrieb um. Das Ergebnis ist eine Binärdatei, die direkt auf der Hardware läuft. Keine Menschen im Loop. Daher darf das Modell niemals irren.
- epsylon
Es gibt viele Behauptungen und so wenig technische Details auf dieser Seite.
Wie wurde die Formalisierung von Python bewerkstelligt? Welches formale Beweisframework verwendet ihr?
Wie reproduziert man die Optimierungen über mehrere Instanzen / Läufe des Programms hinweg? (da sich der Quellcode nicht ändert... vorausgesetzt, man macht nicht immer wieder die gleiche Arbeit?)
Welche Sichtbarkeit, Nachverfolgung und Protokollierung gibt es für den tatsächlich laufenden Code? Debugging ist ein extrem wichtiger Teil der Softwareentwicklung, besonders wenn ständig ein Dämon im Hintergrund den Binärcode austauscht. Selbst wenn der Recompiler perfekt wäre (was er nicht sein wird), ist Benutzercode es nie.
Warum werden die Superoptimierung und die Einsicht in die Daten nicht bis auf die Ebene des Quellcodes zurückgespielt? Das scheint eine Verschwendung zu sein.
- gavinray
Das war viel aufregender, als ich erwartet hatte.
Die Homepage erklärt nicht sehr gut, was wir da sehen:
Es scheint eine Kombination aus zwei Dingen zu sein:
1) Eine Formalisierung der Sprache Python
2) Ein LLM, das sich in laufende Programme einklinkt und Code mit nachweislich äquivalentem Verhalten, aber besserer Laufzeitleistung austauscht, gefunden durch Superoptimierung und dann verifiziert durch die Formalisierungsregeln
Das ist brillant, und im Nachhinein eines dieser Dinge, bei denen man denkt: "Ich kann nicht glauben, dass noch niemand darauf gekommen ist".
- mccoyb
Ich sage mal, mir gefällt die Idee:
- Verifikation
- Superoptimierung, spezialisiert auf eine bestimmte Hardware
- Patchen von Binärdateien während der Laufzeit
alles großartig
Allerdings bekomme ich von der Prosa auf dieser Seite ein seltsames Gefühl. Kleine Formulierungen und Behauptungen, die für Marketingzwecke gedacht zu sein scheinen, aber Dinge mit klarer technischer Bedeutung auf verwirrende Weise vermischen.
Zum Beispiel: Ich habe das Video gesehen ("ein Code-Ausführungsmodell muss jedes Mal richtig sein"), das implizit so etwas kommuniziert wie "das Modell kann nicht halluzinieren" ... natürlich ist das agentische LM immer noch probabilistisch, aber es ist mit Verifikationswerkzeugen umhüllt (um über semantische Äquivalenz zu schließen), und es ist wahrscheinlich nachtrainiert, um gut in der Nutzung dieser Werkzeuge zu sein.
Das erscheint mir als eine Vermischung zwischen dem Modell und dem Harness, die einen Marketingpunkt treffen soll (etwa: "es halluziniert nicht"), aber die eindeutig eine lächerliche Behauptung ist (den Abhang hinunterfallend: jeder Harness, der Fehlerkorrektur für unsachgemäße Werkzeugaufrufe durchführt, könnte auch ein "Modell sein, das keine Fehler macht")
Auch: "selbstverbessernder Code"
das ist es nicht wirklich, oder? Selbstverbessernder Code wäre Code, der sich selbst ausführt und sich selbst verbessert. Das hier ist Code, den ich ausführe, den Maxwell beobachtet und verbessert ... nicht wahr?
Verwandt: Ich mag die Verwendung des Wortes "Modell" in den obigen Diskussionen auf der Seite nicht. Wollen wir jetzt alles ein "Modell" nennen? Kann jeder ein neues Frontier-"Modell" erfinden, indem er ein agentisches LM mit Werkzeugen nachtrainiert?
Und sagen wir mal […]