Cunxi Yu Rongjian Liang Chia-Tung Ho Haoxing Ren

Résumé

Les grands modèles linguistiques (LLM) ont récemment démontré des capacités prometteuses en matière de programmation, permettant non seulement la génération statique de code, mais aussi l’évolution itérative du code lui-même grâce à des cadres agencés. Récemment, AlphaEvolve \cite{novikov2025alphaevolve} a montré que des agents de programmation basés sur les LLM peuvent améliorer de manière autonome des algorithmes et dépasser les experts humains, bien que cette capacité soit actuellement limitée à des noyaux isolés s’étendant sur quelques centaines de lignes de code. Inspirés par AlphaEvolve, nous présentons SATLUTION, le premier cadre permettant d’étendre l’évolution du code basée sur les LLM à l’échelle complète d’un dépôt logiciel, couvrant des centaines de fichiers et des dizaines de milliers de lignes de code C/C++. Axé sur le problème classique de satisfiabilité booléenne (SAT), problème NP-complet fondamental tant en théorie qu’en applications pratiques, SATLUTION orchestre des agents LLM pour évoluer directement des dépôts de solveurs sous des garanties strictes de correction et en s’appuyant sur des retours d’exécution distribués, tout en auto-évoluant simultanément ses propres politiques et règles d’évolution. À partir des bases de code et des benchmarks du SAT Competition 2024, SATLUTION a conçu des solveurs qui ont nettement surpassé les gagnants conçus par des humains lors du SAT Competition 2025, et ont également dépassé à la fois les champions 2024 et 2025 sur les benchmarks 2024.