Cunxi Yu Rongjian Liang Chia-Tung Ho Haoxing Ren

Abstract

Große Sprachmodelle (LLMs) haben in letzter Zeit starke Fähigkeiten im Codieren gezeigt, was nicht nur die statische Codegenerierung, sondern auch die iterative, selbstständige Verbesserung von Code durch agente-basierte Frameworks ermöglicht. Kürzlich hat AlphaEvolve \cite{novikov2025alphaevolve} gezeigt, dass LLM-basierte Code-Agenten Algorithmen autonom verbessern und sogar menschliche Experten übertreffen können – allerdings mit einem Fokus auf isolierte Kerne von Hunderten von Codezeilen. Inspiriert durch AlphaEvolve präsentieren wir SATLUTION, den ersten Framework, der die evolutionäre Weiterentwicklung von LLM-basiertem Code auf das volle Repository-Niveau erweitert und dabei Hunderte von Dateien sowie Zehntausende von Zeilen C/C++-Code umfasst. Ziel ist die Erfüllbarkeitsprüfung (SAT), das klassische NP-vollständige Problem und eine zentrale Grundlage sowohl in der Theorie als auch in praktischen Anwendungen. SATLUTION koordiniert LLM-Agenten, um Solver-Repositorys unter strikten Korrektheitsgarantien und mit Hilfe verteilter Laufzeitfeedbacks direkt zu evolutionären Verbesserungen zu führen, während gleichzeitig die eigenen Evolutionsrichtlinien und -regeln selbstständig weiterentwickelt werden. Ausgehend von den Codebasen und Benchmarks der SAT Competition 2024 entwickelte SATLUTION Solver, die die menschlich konzipierten Sieger der SAT Competition 2025 entscheidend übertrafen und zudem sowohl die Sieger von 2024 als auch die von 2025 auf den 2024-Benchmarks übertreffen konnten.