Can LLMs Build a MaxSAT Solver from Papers? The CoreForge Experience
Das Papier berichtet über CoreForge, ein Experiment, das demonstriert, dass große Sprachmodelle erfolgreich dabei unterstützen können, direkt aus Forschungspapieren durch einen iterativen Workflow einen funktionalen ungewichteten MaxSAT-Solver zu erstellen, obwohl das resultierende System noch menschliche Anleitung und Validierung erfordert und hinter der Leistung handgefertigter Solver zurückbleibt.
Originalarbeit lizenziert unter CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). Dies ist eine KI-generierte Erklärung des untenstehenden Papers. Sie wurde nicht von den Autoren verfasst oder gebilligt. Für technische Genauigkeit konsultieren Sie das Originalpaper. Vollständigen Haftungsausschluss lesen
Stellen Sie sich vor, Sie sind ein Detektiv, der versucht, einen riesigen, verhedderten Knoten aus Hinweisen zu lösen. In der Welt der Informatik wird dieser Knoten als „Constraint-Problem“ bezeichnet. Sie haben eine Liste von Regeln (wie „der rote Ball muss links liegen“ oder „der blaue Ball darf nicht neben dem grünen liegen“) und Ihre Aufgabe ist es, eine Möglichkeit zu finden, alles so anzuordnen, dass jede einzelne Regel zufrieden ist. Manchmal ist es unmöglich, alle zufrieden zu stellen, daher verschiebt sich das Ziel dahin, die Anordnung zu finden, die die meisten Menschen glücklich macht. Dies ist die Aufgabe eines „MaxSAT-Solvers“ – eines superintelligenten Computerprogramms, das als Meister-Rätsellöser fungiert und die bestmögliche Lösung findet, wenn eine perfekte Lösung nicht existiert.
Jahrzehntelang war der Bau dieser Rätsellöser eine Aufgabe für menschliche Experten. Sie mussten komplexe Forschungspapiere lesen, tiefe mathematische Theorien verstehen und jahrelang Millionen von Codezeilen schreiben sowie winzige Details anpassen, um den Solver schnell genug nützlich zu machen. Doch vor kurzem ist ein neuer Typ digitaler Assistent angekommen: Large Language Models (LLMs). Dies sind die KI-Gehirne hinter Werkzeugen wie ChatGPT, die in der Lage sind, Geschichten, Gedichte und sogar Computercode zu schreiben. Die große Frage ist: Kann eine KI ein Forschungspapier lesen und von Grund auf einen funktionierenden Rätsellöser bauen, ohne dass ein Mensch auch nur eine einzige Zeile des Codes schreibt? Das ist das Rätsel, das das Projekt „CoreForge“ zu lösen versucht.
Das CoreForge-Experiment: Eine KI lehren, einen Rätsellöser zu bauen
In einem Projekt namens CoreForge beschloss ein Forscher namens Ruben Martins von der Carnegie Mellon University, die Grenzen der KI zu testen. Anstatt eine KI zu bitten, einen bereits existierenden, fehlerhaften Rätsellöser zu reparieren, forderte er sie heraus, einen von Grund auf neu zu bauen, wobei Forschungspapiere als einzige Bedienungsanleitung dienten. Stellen Sie sich das so vor, als würde man einem Roboter einen Stapel Kochbücher berühmter Köche überreichen und ihn bitten, eine Fünf-Sterne-Küche aufzubauen und ein Gourmetmenü zu kochen, ohne jemals zuvor einen Herd gesehen zu zu haben.
Der Prozess war kein „One-Shot“-Zaubertrick, bei dem die KI einfach ein perfektes Programm ausspuckte. Stattdessen war es ein langer, iterativer Tanz zwischen Mensch und Maschine. Der menschliche Forscher wählte ein Forschungspapier aus, diskutierte die Kernideen mit der KI und bat die KI (speziell ein Codierungswerkzeug namens Codex), den Code zu schreiben. Aber die KI hatte keinen Freifahrtschein. Der Mensch führte dann Tests durch, prüfte auf Bugs und bat die KI, ihre Fehler zu korrigieren. Sie wiederholten diesen Zyklus immer und immer wieder, wie ein Schüler und ein Tutor, die gemeinsam eine schwierige Matheaufgabe durcharbeiten, bis sie einen funktionierenden Solver hatten.
Was haben sie gebaut?
Das Ergebnis war eine massive Codebasis von über 25.000 Zeilen C++-Code. Die KI schaffte es erfolgreich, komplexe mathematische Ideen aus Papieren in funktionierende Software zu übersetzen. Sie implementierte mehrere fortgeschrittene Strategien, darunter:
- Core-guided Optimization: Eine Methode, bei der der Solver aus seinen Fehlern (den sogenannten „Cores“) lernt, um diese nicht zu wiederholen.
- Preprocessing: Das Bereinigen des Rätsels, bevor man versucht, es zu lösen, um es einfacher zu machen.
- Lookahead: Ein neues Feature, das die KI mitentwickelte, bei dem der Solver einige schnelle „Übungsrunden“ macht, um die beste Strategie vorherzusagen, bevor er sich auf die echte Lösung festlegt.
Hat es funktioniert?
Der überraschendste Teil der Geschichte ist, dass die KI nicht geschummelt hat. Die Forscher führten Tausende von Tests durch, einschließlich „Fuzzing“ (das Werfen von zufälligen, chaotischen Daten auf den Solver, um zu sehen, ob er zusammenbricht) und dem Vergleich mit offiziellen Wettbewerbs-Benchmarks. Sie fanden null falsche Antworten in den getesteten Konfigurationen. Der Solver war mathematisch korrekt. Er hat nicht nur geraten; er hat die Rätsel tatsächlich korrekt gelöst.
Aber ist er schnell genug?
Hier liegt der Haken. Obwohl die KI einen korrekten Solver gebaut hat, war sie nicht der schnellste. Im Vergleich zu den von Menschen entwickelten Top-Solvern, die seit Jahren verfeinert werden, war CoreForge langsamer und löste weniger Rätsel. Es ist, als hätte die KI ein Auto gebaut, das perfekt fährt und niemals abstürzt, aber es fährt nur 40 Meilen pro Stunde, während die besten menschengebauten Autos 120 Meilen pro Stunde erreichen.
Die Forscher fanden heraus, dass die KI sehr gut darin war, die hochgradigen Ideen zu verstehen und sie in Code zu übersetzen. Sie hatte jedoch Schwierigkeiten mit den Details des „Fine-Tunings“ – jenen winzigen, aggressiven Optimierungen, die einen Solver blitzschnell machen. Die KI fügte auch manchmal zusätzliche Schritte hinzu, die den Prozess verlangsamten, so als würde man einen Umweg nehmen, wenn eine gerade Straße besser wäre.
Das Urteil
Die CoreForge-Erfahrung legt nahe, dass KI definitiv dabei helfen kann, komplefxe Software aus Forschungspapieren zu bauen, aber sie ist noch nicht bereit, menschliche Ingenieure zu ersetzen. Die KI benötigt einen menschlichen Führer, der ihre Arbeit überprüft, entscheidet, welche Ideen beibehalten werden sollen, und ihr hilft, nicht in langsamen Schleifen stecken zu bleiben.
Das Paper kommt zu dem Schluss, dass wir zwar noch nicht an dem Punkt sind, an dem eine KI autonom einen Weltklasse-Solver bauen kann, wir aber sehr nah dran sind. Die KI hat bewiesen, dass sie die „Kochbücher“ lesen und die „Küche“ bauen kann. Der nächste Schritt besteht darin, sie zu einem Meisterkoch zu lehren, der genau weiß, wie man Hitze und Timing abstimmt, um den Wettbewerb zu gewinnen. Vorerst erzielen die besten Ergebnisse durch ein Team: ein Mensch, der die Strategie vorgibt, und die KI, die die schwere Arbeit des Codierens übernimmt.
Ertrinken Sie in Arbeiten in Ihrem Fachgebiet?
Erhalten Sie tägliche Digests der neuesten Arbeiten passend zu Ihren Forschungsbegriffen — mit technischen Zusammenfassungen, in Ihrer Sprache.