💻 computer science

Theory Under Construction: Orchestrating Language Models for Research Software Where the Specification Evolves

Ce papier présente Comet-H, un automate de prompts itératif qui orchestre le développement couplé du code, de la théorie et de la documentation pour prévenir les hallucinations et la désynchronisation dans les logiciels de recherche, en démontrant son efficacité grâce à un outil d'analyse statique Python qui surpasse nettement les références sur un benchmark de 90 cas.

Auteurs originaux : Halley Young, Nikolaj Björner

Publié 2026-05-01

📖 7 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Halley Young, Nikolaj Björner

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez que vous essayez de construire un nouveau type de voiture, mais que vous ne disposez pas d'un plan achevé. À la place, vous avez une équipe d'ingénieurs incroyablement talentueux et à la pensée rapide (l'IA) capables de dessiner des pièces, de construire des moteurs et de rédiger le manuel du propriétaire, le tout simultanément.

Le problème est que ces ingénieurs sont enclins à deux erreurs spécifiques :

Le piège du « Fake It Till You Make It » (Fais semblant jusqu'à ce que tu y arrives) : Ils pourraient écrire dans le manuel : « Cette voiture atteint 200 mph », avant même d'avoir construit le moteur pour le prouver. Ensuite, le prochain ingénieur lit cette affirmation, suppose qu'elle est vraie, et construit un châssis conçu pour 200 mph. Si le moteur ne peut pas réellement le faire, tout le projet est bâti sur un mensonge.
Le piège de la « Perte dans la traduction » : L'ingénieur qui a conçu le moteur pourrait changer d'avis sur son fonctionnement, mais la personne rédigeant le manuel ne le sait pas. Désormais, le manuel décrit un ancien moteur, le plan en montre un nouveau, et la voiture réelle sur la chaîne de montage est quelque chose d'entièrement différent. Ils dérivent tous les uns par rapport aux autres.

Ce papier, « Orchestrating Language Models for Research Software Where the Specification Evolves », introduit un nouveau système appelé Comet-H pour résoudre ces problèmes. Il traite la recherche non pas comme une ligne droite, mais comme une danse où la musique, les pas et les danseurs doivent constamment s'ajuster les uns aux autres.

L'idée centrale : Un « Chef d'orchestre » pour l'IA

Au lieu de simplement demander à l'IA de « écrire du code », les auteurs ont construit un Chef d'orchestre (un contrôleur) qui gère l'ensemble de l'orchestre. Ce Chef d'orchestre ne se contente pas de dire à l'IA quoi faire ; il vérifie constamment l'« espace de travail » (le code, la théorie mathématique, les benchmarks et le papier) pour voir ce qui manque ou ce qui est désynchronisé.

Voici comment Comet-H fonctionne, en utilisant des analogies simples :

1. La « Liste de tâches qui s'estompe » (Déclin de l'obligation)

Imaginez que vous écrivez un livre. Vous avez un post-it qui dit : « Je dois vérifier les faits de ce chapitre ».

L'ancienne méthode : Si vous oubliez de le vérifier, le post-it reste là pour toujours, encombrant votre bureau, ou vous l'ignorez et passez à autre chose.
La méthode Comet-H : Le post-it a une demi-vie. Chaque fois que vous faites un pas en avant dans le projet, le post-it devient légèrement plus pâle. Si vous ne le traitez pas bientôt, il s'efface. Mais s'il est très récent, il brille d'un rouge vif.
Pourquoi cela compte : Cela force l'IA à régler les affaires inachevées (comme « prouver cette affirmation ») tant qu'elles sont fraîches. Si l'IA tente d'ignorer la dette, la « lueur » devient plus intense, et le Chef d'orchestre force l'IA à s'arrêter et à corriger le tir avant de continuer.

2. La « Vérification de la réalité » (Ancrage réactif)

Chaque fois que l'IA modifie la « face publique » du projet (comme le fichier README ou le papier de recherche), Comet-H appuie sur le bouton Pause.

La règle : Vous ne pouvez pas changer l'histoire sans vérifier les faits.
Le processus : Si l'IA écrit : « Notre outil est 10 fois plus rapide », le système s'arrête immédiatement et dit : « D'accord, montrez-moi les résultats de la course ». Il force l'IA à exécuter le code et à générer un « registre d'ancrage » (un reçu lisible par machine) prouvant l'affirmation.
Le résultat : Cela empêche le piège du « Fake It Till You Make It ». Un mensonge ne peut survivre qu'un seul pas avant d'être attrapé et corrigé.

3. Le « Pas sûr » (Contraintes d'adjacence)

Parfois, une IA s'enthousiasme et veut passer de « construire un vélo » à « construire un vaisseau spatial ».

La règle : Comet-H n'autorise que des mouvements adjacents. L'IA peut faire un petit pas en avant (par exemple : « ajouter un engrenage au vélo »), mais elle ne peut pas sauter vers un univers complètement différent.
Pourquoi cela compte : Cela maintient le projet ancré. Si l'IA veut changer la théorie de base, elle doit le faire d'une manière qui reste connectée à ce qui a été construit hier. Cela empêche l'équipe de dériver si loin les uns des autres qu'elles oublient ce qu'elles essayaient de construire à l'origine.

Les résultats : L'étude de cas « a3 »

Les auteurs ont testé ce système en construisant un portefeuille de 46 projets différents de logiciels de recherche. La star du spectacle est un outil appelé a3, un programme conçu pour trouver des bugs dans le code Python.

Le défi : Habituellement, les outils de détection de bugs sont comme des voisins bruyants ; ils crient « BUG ! » à tout, même quand tout va bien. Cela crée beaucoup de fausses alertes.
L'approche Comet-H : Le système n'a pas seulement construit l'outil ; il a fait évoluer la théorie derrière celui-ci. Il a commencé par une idée simple, a réalisé qu'elle était trop difficile à calculer, et le Chef d'orchestre a permis à l'équipe de pivoter vers une nouvelle approche mathématique (utilisant des « certificats de sécurité ») qui fonctionnait réellement.
Le résultat : L'outil final était incroyablement précis. Il a détecté de vrais bugs (haute précision) sans crier pour des choses qui n'étaient pas cassées. Il a obtenu un score de 0,768 sur une échelle de test, tandis que le prochain meilleur outil n'obtenait que 0,364.

Ce que nous avons appris sur le comportement de l'IA

En observant l'IA travailler sur ces 46 projets, les auteurs ont remarqué certains schémas intéressants :

L'« Équipe de nettoyage » est réelle : Au début, l'IA est occupée à construire de nouvelles fonctionnalités. Mais à mesure que le projet approche de la fin, l'IA passe la majeure partie de son temps à auditer et réparer. C'est comme une équipe de construction qui passe la dernière semaine d'un projet à vérifier simplement que la peinture est sèche et que les portes s'ouvrent, plutôt qu'à construire de nouveaux murs.
L'honnêteté émerge : Contrainte de prouver ses affirmations, l'IA est devenue étonnamment honnête. Au lieu de cacher les échecs, elle a commencé à déclarer explicitement : « Nous ne pouvons pas résoudre ce type spécifique de problème pour l'instant ». Le système n'avait pas programmé cette honnêteté ; elle est apparue parce que la « Vérification de la réalité » rendait le mensonge trop difficile.
Auto-organisation : Avec le temps, l'IA a commencé à organiser son propre code en structures plus propres et plus logiques, même si personne ne lui avait explicitement demandé de le faire.

La grande image

Le papier soutient que construire des logiciels de recherche est différent de corriger une faute de frappe dans un document. C'est un processus de co-évolution. La théorie, le code, les tests et l'histoire doivent croître ensemble.

Si vous demandez simplement à une IA de « écrire un papier et du code », elle risque de dériver, d'halluciner et de perdre la synchronisation. Mais si vous lui donnez un Chef d'orchestre qui vérifie constamment la partition, force les vérifications de réalité et s'assure que les pas restent connectés, vous pouvez construire des outils de recherche complexes et fiables qui fonctionnent réellement.

En bref : Comet-H est un système qui empêche l'IA de rêvasser et la force à tenir ses promesses, garantissant que l'histoire qu'elle raconte correspond au code qu'elle écrit.

1. Énoncé du problème : Le défi de la co-évolution

Le papier comble une lacune critique dans le développement automatisé de logiciels de recherche : le problème de la co-évolution. Contrairement aux tâches d'ingénierie logicielle standard où la spécification est fixe, le logiciel de recherche implique une spécification qui est en cours de construction. La thèse mathématique, le code exécutable, les surfaces de benchmark et les affirmations publiques doivent mûrir ensemble.

Les agents actuels basés sur les grands modèles de langage (LM) échouent dans ce régime en raison de deux modes d'échec spécifiques :

Accumulation d'hallucinations : Des affirmations non étayées ou des données fabriquées introduites à une étape (par exemple, dans un brouillon de papier) sont traitées comme une vérité fondamentale dans les étapes suivantes, propageant ainsi les erreurs à travers la boucle de développement.
Désynchronisation : Le code, la théorie ou le modèle du monde interne du LM divergent. Par exemple, le code peut être optimisé pour une spécification obsolète, ou la représentation interne du LM du dépôt peut devenir périmée à mesure que les fichiers s'accumulent, entraînant une incohérence globale même si une cohérence par paires existe.

Les cadres existants (par exemple, SWE-agent, AI Scientist) supposent des tâches fixes ou des cadres d'évaluation fixes, ce qui les rend inadaptés à la recherche où l'objectif lui-même évolue.

2. Méthodologie : Comet-H

Les auteurs proposent Comet-H, un automate de prompt itératif conçu pour orchestrer l'évolution couplée de la théorie, du code, des preuves et des affirmations.

Architecture de base

Comet-H fonctionne comme une Machine d'État de Co-évolution qui gère un espace de travail $W$ composé de six composants :

$T$ (Théorie) : La thèse mathématique mutable.
$R$ (Dépôt) : L'implémentation du code.
$P$ (Projection Publique) : Le papier et le README.
$E$ (Preuve) : Les benchmarks et les registres d'ancrage.
$U$ (Hypothèse d'utilité) : Le « pourquoi » du logiciel.
$Q$ (Obligations Ouvertes) : Une file d'attente d'affirmations non vérifiées ou de tâches en attente.

Mécanismes clés

Déclencheurs d'ancrage réactifs :
- Tout changement sur les artefacts destinés au public ( $P$ : papier/README) déclenche immédiatement une Création d'ancrage suivie d'un Audit sceptique.
- Cela force le système à vérifier les affirmations par rapport au code exécutable et aux benchmarks avant qu'elles ne puissent se propager, limitant la propagation des hallucinations à une seule étape.
Contraintes d'adjacence :
- Le contrôleur empêche le système de dériver arbitrairement. Toute expansion ou pivot doit être « adjacente » à l'état actuel (atteignable en une étape conceptuelle unique) et doit renforcer les benchmarks ou la théorie existants. Cela empêche le modèle de sauter vers des problèmes sans rapport qui manquent de surfaces d'évaluation.
Sélection de prompt comme bandit contextuel :
- Le contrôleur sélectionne le prochain prompt parmi un alphabet fixe de 17 familles de prompts (par exemple, Idéation, Génération de graines, Renforcement du papier, Audit sceptique).
- Notation : Un scoreur linéaire transparent et défini à la main calcule un score basé sur un vecteur de caractéristiques des déficits de l'espace de travail (par exemple, « faible couverture de tests », « affirmations non vérifiées »).
- Décayance des obligations : Le travail de suivi inachevé est stocké dans un vecteur d'obligations $o_t$ qui décroît exponentiellement (demi-vie de 8 étapes). Cela garantit que le contrôleur se concentre sur les dettes récentes et prioritaires sans être submergé par un historique périmé, mimant les stratégies de bandits non stationnaires.
Phases de la boucle de développement :
- Graine : Sélectionne une question de recherche différenciée et un noyau formel.
- Itération réactive : Génère du code/des papiers, puis les renforce itérativement en fonction de la surface la plus faible (par exemple, si les benchmarks sont faibles, il exécute un Resserrement des benchmarks).
- Queue : Une séquence fixe d'étapes d'audit et de polissage pour garantir que la sortie finale est ancrée, indépendamment du budget restant.

3. Contributions clés

Définition des modes d'échec de la co-évolution : Le papier identifie formellement l'accumulation d'hallucinations et la désynchronisation comme les causes principales d'échec dans la recherche automatisée, distinctes des erreurs de codage standard.
Machine d'État de Co-évolution : Un cadre formel (Définition 4.1) qui traite la théorie comme une variable d'état mutable et impose une synchronisation inter-artefacts via un mode de contrôle fini et une mémoire d'obligations en déclin.
Orchestration transparente : Une conception de contrôleur novatrice associant un scoreur linéaire défini à la main à un registre en déclin du travail inachevé. Cela évite les politiques apprises (boîtes noires) au profit d'une prise de décision auditable et interprétable.
Portefeuille empirique : La création de 46 dépôts de logiciels de recherche répartis sur plus de 12 domaines, démontrant l'évolutivité de l'approche.

4. Résultats et étude de cas (a3)

Les auteurs plongent en profondeur dans a3, un outil d'analyse statique Python développé entièrement dans la boucle Comet-H.

Performance : Sur un benchmark de 90 cas, a3 a obtenu un score F1 de 0,768, surpassant significativement la meilleure baseline suivante de 0,364.
Gains monotones : Les études d'ablation ont montré que chaque couche ajoutée de couplage théorie/pratique (par exemple, analyse interprocédurale, exécution symbolique dynamique) améliorait les performances sans dégradation.
Évolution de la théorie : Le système a réussi à réviser sa théorie sous-jacente deux fois au cours du développement (passant d'un cadre de « distance à la frontière » à des « certificats de sécurité » et intégrant des solveurs SMT) sans casser la base de code, démontrant la capacité du contrôleur à gérer les pivots de spécification.
Observations comportementales :
- Dominance de l'audit : Dans les phases ultérieures du développement, la majorité des commits concernaient l'ancrage, l'audit et la réparation des affirmations plutôt que l'ajout de fonctionnalités.
- Échec visible : Le système a appris à signaler ouvertement les limitations (par exemple, des verdicts « INCONNU » pour les cas récursifs) plutôt que de les cacher, un comportement piloté par le prompt Audit sceptique.
- Auto-organisation : Sur de longs horizons, le LM a naturellement réorganisé le code en structures plus compositionnelles (par exemple, conversion en sous-modules) sans prompt explicite.

5. Signification

Ce papier déplace le paradigme des agents de recherche en IA de l'achèvement de tâches (résoudre un problème fixe) vers la gestion d'état (maintenir l'intégrité d'un système en co-évolution).

Gouvernance sur génération : Il soutient que la partie la plus difficile de l'automatisation de la recherche n'est pas de générer du code, mais de s'assurer que la thèse mathématique, le code et les affirmations restent synchronisés.
Nouvelles métriques d'évaluation : Il suggère que les futures évaluations des agents de recherche devraient mesurer la stabilité, la récupérabilité après dérive et la latence de réparation de l'intégrité, plutôt que simplement les scores finaux de benchmark.
Impact pratique : En prouvant que les LM peuvent gérer le cycle de vie complet du logiciel de recherche — y compris la révision de la théorie et l'audit rigoureux — Comet-H fournit un modèle pour construire des systèmes de découverte scientifique autonomes et dignes de confiance.

En résumé, Comet-H démontre qu'en traitant la recherche comme un processus co-évolutif avec des mécanismes explicites pour l'ancrage, l'audit et la dérive bornée, les LM peuvent naviguer avec succès dans la voie complexe et non linéaire de la création de logiciels de recherche novateurs.