Schmieden und Suchen, das seinen Beweis verdient
Das alte Trick-Problem
Jedes ernsthafte Softwaresystem hat ein paar Codestellen, die weit wichtiger sind, als ihre Größe vermuten lässt. Eine Schleife, die millionenfach läuft. Eine Bitoperation in einem Komprimierungspfad. Eine kleine Matrixroutine. Ein Kernstück modularer Arithmetik. Die Art von Code, der im Review harmlos aussieht und dann stillschweigend über die Energierechnung, das Latenzbudget oder die Anzahl der benötigten Maschinen entscheidet. Sehr demokratisch, die Software. Eine winzige Funktion kann das Meeting für alle ruinieren.
Historisch gesehen werden solche Kernstücke von Menschen verbessert. Eine erfahrene Ingenieurin erinnert sich an einen Trick aus einem Paper. Jemand wühlt sich durch einen alten Forenbeitrag. Eine Benchmark-Suite wird geschrieben. Ein paar Kandidaten werden ausprobiert. Der schnellste gewinnt, wenn er noch korrekt erscheint. Dann friert die Organisation ihn ein, denn ihn erneut anzufassen fühlt sich an, als würde man einen schlafenden Transformator mit einer Gabel stochern.
Forge ist Forschung an einer besseren Version dieses Prozesses. Es ist eine Engine zur Programmsynthese für kleine, kritische Implementierungen: Gib ihr eine typisierte Spezifikation und Eigenschaften, lass sie Kandidatenprogramme durchsuchen, messe und vergleiche Abwägungen, verifiziere Äquivalenz und senke dann die entdeckte Implementierung auf relevante Zielplattformen ab. Das wichtige Wort ist nicht Suche. Das wichtige Wort ist immer noch. Es muss immer noch korrekt sein.
Deshalb lebt Forge in der Forschung. Es ist kein öffentlicher Produktknopf, bei dem jemand schneller machen eingibt und ein Wunder erhält. Es ist eine Synthese-Werkbank für Partnerexperimente, Kernel-Entdeckung und Forschung darüber, wie weit automatisierte Suche gehen kann, wenn sie an Verifikation gekoppelt ist statt an Benchmark-Theater.
Eine Spezifikation ist die Startlinie
Optimierung ohne Spezifikation ist nur Glücksspiel mit schöneren Variablennamen. Sobald ein cleverer Kandidat auftaucht, muss das Team wissen, was er bewahren soll. Behandelt er jede Eingabe oder nur die freundlichen aus der Benchmark? Respektiert er das Überlaufverhalten? Ist die algebraische Identität unter der tatsächlich verwendeten Darstellung gültig? Behält er dieselbe Semantik, wenn er auf ein anderes Backend abgesenkt wird?
Forge beginnt mit typisierten Ausdrücken und Eigenschaften, weil die Suche eine Grenze braucht. Die Grenze legt fest, was als äquivalent gilt. Ohne sie kann die Engine etwas Erstaunlich Schnelles finden, indem sie die Hälfte der Arbeit löscht. Computer sind hervorragend in bösartiger Compliance, wenn der Vertrag vage ist.
Die Suchseite ist bewusst plural. Enumerative Suche ist nützlich, wenn der Raum klein genug ist, um ihn abzudecken. CEGIS ist nützlich, wenn Gegenbeispiele die Verfeinerung leiten können. Genetische Programmierung und MCTS erkunden anders. ML-gestützte Suche kann Kostenmodelle lernen und vielversprechende Regionen priorisieren. Keine davon ist universell am besten. Das ist keine Schwäche. So verhält sich Suche in der realen Welt. Wenn ein Hammer jedes Kernel-Problem löste, wären Werkzeugkästen sehr langweilig und Hardware-Anbieter arbeitslos.
Die Forschungsfrage ist, wie man diese Engines mit genug Beweisdruck kombiniert, sodass das Ergebnis nicht nur clever ist. Ein synthetisierter Kernel muss sowohl die Happy-Path-Benchmark als auch den Unhappy-Path-Verifier überleben. Sonst ist die Verbesserung keine Technik. Sie ist ein Zaubertrick mit Wartungskosten.
Der Verifier ist der Erwachsene im Raum
Forge verwendet einen Verifikations-Stack, weil keine einzelne Prüfung für jede Domäne ausreicht. Schnelle Beispiele sind günstig und nützlich. Eigenschaftstests finden ganze Klassen von Fehlern und reduzieren Gegenbeispiele auf etwas, das ein Mensch lesen kann. SMT-Löser wie Z3 und CVC5 können Äquivalenz beweisen, wenn die Kodierung handhabbar ist. Vollständige Prüfung ist für kleine Domänen praktikabel. E-Graph-Gleichheitssättigung bietet einen weiteren Weg durch algebraische Äquivalenz.
Der Stack ist wichtig, weil Kernel auf ärgerliche Weise versagen. Ein Kandidat kann jeden gewöhnlichen Benchmark bestehen und trotzdem bei einem Randfall falsch sein. Er kann für vorzeichenlose Eingaben korrekt sein und für vorzeichenbehaftete falsch. Er kann in einem mathematischen Körper korrekt sein und nach dem Überlauf der gewählten Darstellung falsch. Er kann vor dem Lowering korrekt sein und nach einer Anweisungsauswahl-Entscheidung subtil falsch. Der Verifizierer existiert, weil Optimismus keine Teststrategie ist. Wir haben geprüft. Wiederholt. Es bleibt wahr.
Es gibt auch einen praktischen Grund, mehrere Beweiswege zu behalten. Formale Methoden sind mächtig, aber nicht kostenlos. Manche Kodierungen laufen in ein Timeout. Manche Domänen sind für vollständige Prüfung zu groß. Manche Eigenschaften lassen sich leichter zuerst probabilistisch testen und später beweisen. Forge behandelt Verifikation als Trichter, nicht als Reinheitsritual. Günstige Prüfungen verwerfen offensichtlichen Unsinn. Stärkere Prüfungen schützen den endgültigen Kandidaten.
Schnell ist nicht eine Zahl
Performance-Arbeit wird albern, wenn eine Metrik jedes Gespräch dominieren darf. Latenz zählt. Operationsanzahl zählt. Speichernutzung zählt. Registerdruck zählt. Kompilierzeit zählt manchmal. Portabilität zählt, wenn derselbe Kernel auf mehr als einem Backend leben muss. Ein Kandidat, der Latenz gewinnt, indem er Register wie ein kleines Lagerfeuer verbrennt, könnte für das eigentliche Ziel falsch sein. Ein Kandidat, der winzig, aber langsam ist, könnte woanders nützlich sein. Der Kontext bleibt ungeschlagen.
Forge formuliert Optimierung daher als Pareto-Problem. Die Engine kann über Ziele hinweg suchen, statt so zu tun, als gäbe es eine universelle Punktzahl, die von einer sehr selbstbewussten Tabellenkalkulation verkündet wird. Die nützliche Ausgabe ist nicht immer der einzelne schnellste Kandidat. Manchmal ist es eine Familie von Kandidaten mit sichtbaren Abwägungen, damit ein Ingenieur denjenigen wählen kann, der zur Bereitstellungsbeschränkung passt.
Deshalb mag ich auch keine nackten Speedup-Behauptungen in Blogbeiträgen. Die Forschungsseite kann interne Erwartungen und experimentelle Ziele beschreiben, aber öffentliche Behauptungen brauchen frische Läufe, aktuelle Hardware, aktuelle Compiler-Flags und genauen Workload-Kontext. Sonst wird die Zahl zu einem Souvenir. Souvenirs sind nett. Sie sind keine Architektur.
Die ehrliche Behauptung ist ohnehin stärker: Forge geht es darum, die Suche reproduzierbar, vergleichbar und prüfbar zu machen. Wenn ein Kandidat gewinnt, sollten wir wissen, welches Ziel er gewonnen hat, welche Kandidaten er geschlagen hat, welcher Verifizierer ihn akzeptiert hat und welches Backend er anvisiert. Das ist viel nützlicher als eine Zahl, die durch eine Slide-Deck schwebt und teuer aussieht.
Lowering ist, wo Beweise getestet werden
Eine entdeckte Implementierung ist nur dann nützlich, wenn sie den Weg zu echten Zielsystemen übersteht. Die Forge-Forschung umfasst das Absenken auf Backends wie x86-64, RISC-V, WASM, Vulkan-GPU-Pfade, C und Verilog. Diese Zielliste ist keine Dekoration. Jedes Backend hat seine eigenen Einschränkungen, Befehlsformen, Speicherverhalten und Fehlermodi. Dieselbe Spezifikation muss ihre Bedeutung behalten, während die Implementierung zu etwas wird, das das Zielsystem tatsächlich ausführen kann.
Hier verbindet sich die Synthese mit dem Rest des Dweve-Stacks. Core möchte effiziente innere Schleifen. Numerus kümmert sich um deterministische numerische Kernel. BitWeave möchte binäre Vektor- und Matrixoperationen, die die CPU nicht verschwenden. Kera kümmert sich darum, Berechnungsgraphen auf echte Hardware abzusenken. Forge kann diese Ebenen nur dann versorgen, wenn die erzeugte Implementierung mehr als nur schnell ist. Sie muss äquivalent sein, portabel genug für das gewählte Zielsystem und überprüfbar, wenn sich etwas ändert.
Was das für Teams ändert
Für ein Team ist die interessante Veränderung nicht, dass eine Maschine einen schnelleren Kernel entdecken könnte. Es ist, dass die Kernelarbeit weniger von Überlieferungen abhängt. Statt dass ein Experte sich den richtigen Trick merkt, wird der Prozess zu: den Vertrag festlegen, den Raum durchsuchen, Kandidaten messen, Äquivalenz beweisen, den Kompromiss dokumentieren und Zielcode erzeugen. Menschen entscheiden weiterhin. Sie hören nur auf, alle Entdeckungen von Hand zu machen.
Das ist für den Betrieb wichtig, weil Leistungsschulden auf eine Weise teuer sind, die Organisationen oft verbergen. Ein langsamer Kernel wird zu mehr Servern. Mehr Server werden zu mehr Kosten, mehr Energie, mehr Bereitstellungskomplexität und mehr Lärm in der Planung. Eine falsche Optimierung wird zu Vorfällen. Ein korrekter, aber undokumentierter Trick wird zu einem künftigen Migrationsrisiko. Forge ist Forschung zur Reduzierung dieses Haufens vermeidbaren Unsinns.
Es gibt auch einen kulturellen Wandel. Manuelle Leistungsarbeit belohnt oft Heldentaten. Jemand verschwindet in der Höhle und kehrt mit einem cleveren Bit-Hack zurück. Alle applaudieren, niemand versteht es vollständig, und das Unternehmen hat ein kleines heiliges Objekt erworben. Forge drängt den Prozess in Richtung Evidenz: hier ist die Spezifikation, hier ist der Suchpfad, hier sind die abgelehnten Kandidaten, hier ist der Verifizierer, hier ist das ausgewählte Backend. Weniger Mythologie. Mehr Belege.
Wo die Arbeit noch schwer ist
Nichts davon macht Synthese einfach. Spezifikationen sind schwer. Wenn die Spezifikation falsch ist, kann die Engine treu das Falsche entdecken. Suchräume können explodieren. Solver können eine Zeitüberschreitung haben. Kostenmodelle können irreführen. Backends können Details offenlegen, die der abstrakte Ausdruck nicht berücksichtigt hat. Verifikation kann in einem Bereich stark und in einem anderen umständlich sein. Wer Programmsynthese als Verkaufsautomaten für optimalen Code anpreist, überspringt entweder die schwierigen Teile oder verlangt extra für Enttäuschung.
Forge ist gerade deshalb interessant, weil es diese schwierigen Teile direkt angeht. Es kombiniert mehrere Suchstrategien. Es hält die Verifikation nahe. Es behandelt Ziele als Kompromisse. Es zielt auf echte Backends. Es bleibt ein Forschungsprogramm, weil wir noch lernen, wo die Grenze zwischen automatischer Entdeckung, menschlichem Urteil, Solver-Grenzen und Bereitstellungsrealität verläuft.
Diese Grenze ist es wert, erkundet zu werden. Die Softwarebranche hat zu viele kleine heiße Schleifen, zu viel duplizierte Leistungsüberlieferung und zu viele Optimierungen, die niemand wieder anfassen möchte. Wenn Forge auch nur einen Teil dieser Arbeit in einen wiederholbaren Evidenzprozess verwandeln kann, ist das Ergebnis nicht nur schnellerer Code. Es ist ruhigerer Code. Ruhigerer Code wird unterschätzt, meist von Menschen, die nicht um 02:17 Uhr angepiept wurden.
Was einen guten Forge-Lauf braucht
Ein ernsthaftes Forge-Experiment beginnt, bevor die Engine läuft. Das Team muss einen echten Kernel mitbringen, keine vage Beschwerde über die Leistung. Es braucht repräsentative Eingaben, bekannte Randfälle, Zielhardware, aktuelle Benchmarks und den geschäftlichen Grund, warum dieser Kernel wichtig ist. Andernfalls kann die Synthese-Engine viel Zeit damit verbringen, ein Problem zu lösen, das niemand tatsächlich hat. Forschungswerkzeuge sind nicht immun gegen Müll-Eingaben. Sie machen den Müll nur teurer in der Untersuchung.
Die nützlichste Eingabe ist ein kleiner, präziser Vertrag. Was soll die Funktion berechnen? Welche algebraischen Gesetze sind wichtig? Welches Überlaufverhalten ist beabsichtigt? Welche Bereiche sind konstruktionsbedingt unmöglich und welche sind nur im letzten Testlauf nicht aufgetreten? Welche Ausgaben können Näherung tolerieren und welche nicht? Ein Team, das diese Fragen nicht beantworten kann, hat wahrscheinlich noch kein Optimierungsproblem. Es hat ein Produktklärungsproblem, das einen Compiler-Hut trägt.
Ein guter Lauf braucht auch eine Zielhaltung. x86-64 und RISC-V sind nicht dasselbe. WASM hat andere Einschränkungen. Vulkan-GPU-Pfade kümmern sich um Formen und Speicherbewegungen. Verilog wirft Hardware-Fragen auf, die normale Anwendungsteams vor dem Kaffee selten genießen. Forge kann die Zielabsenkung erkunden, aber es kann keine organisatorischen Prioritäten festlegen. Wenn Portabilität wichtiger ist als Geschwindigkeit auf einem Ziel, sag das. Wenn Latenz wichtiger ist als Speicher, sag das. Wenn Registerdruck die praktische Grenze ist, sag auch das. Die Engine ist leistungsstark, nicht hellseherisch.
Die Ausgabe sollte wie ein Beweispaket behandelt werden. Kandidat, Ziel, Beweisweg, abgelehnte Gegenbeispiele, Backend, Benchmark-Kontext und offene Vorbehalte. Dieses Paket ist es, das Menschen eine vernünftige Entscheidung ermöglicht. Manchmal ist der Gewinnzug, den Kandidaten zu übernehmen. Manchmal ist es, den alten Kernel zu behalten, weil der Portabilitätskompromiss es nicht wert ist. Manchmal ist die Entdeckung, dass die Spezifikation zu locker war. Alle drei Ergebnisse sind nützlich. Nur eines davon sieht in einer Demo aufregend aus, weshalb Demos ein schlechter Ersatz für Engineering sind.
Die Lektion
Die Lektion von Forge ist einfach: Leistung sollte den Beweis nicht überholen. Suche ist mächtig, aber eine Suchmaschine ohne Verifikation ist nur eine sehr energische Art, Fehler zu erzeugen. Verifikation ist mächtig, aber ohne Suche wartet sie darauf, dass Menschen ihr Kandidaten bringen. Forge bringt beides zusammen und fragt, welche Kernel wir entdecken können, wenn die Maschine erkunden darf, aber nicht lügen darf.
Das ist die Forschung, die sich lohnt. Typisierte Spezifikationen, Kandidatensuche, Beweistrichter, Pareto-Ziele und Backend-Absenkung. Keine Magie. Keine Produktabkürzung. Ein Weg, besseren kleinen Code mit beigefügten Beweisen zu machen.