Agentified Assessment of Logical Reasoning Agents

Cet article présente un cadre d'évaluation agentifié pour les agents de raisonnement logique, démontré par un agent de formalisation automatique qui atteint 86,70 % de précision sur le jeu de données FOLIO, surpassant ainsi une baseline de type « chaîne de pensée ».

L'essentiel

🌟 Le Concept de Base : Un Nouveau Système de Contrôle Qualité

Imaginez que vous voulez tester la logique d'un robot très intelligent. Dans le passé, pour le tester, on lui donnait un exercice, on regardait sa réponse, et on notait "Juste" ou "Faux". Mais il y avait un gros problème : si le robot avait un bug informatique (un plantage, un temps d'attente trop long, une erreur d'impression), on le notait souvent comme "Faux" sur le fond, alors qu'en réalité, il avait juste eu un problème technique. C'est comme si un étudiant ratait son examen parce que son stylo s'est cassé, et qu'on lui mettait une mauvaise note en mathématiques.

Ce papier propose une nouvelle façon de faire, qu'ils appellent "l'évaluation par des agents".

Au lieu d'avoir un simple correcteur automatique (un script rigide), ils ont créé un Agent Examinateur. C'est un robot "professeur" qui a deux missions :

1. Gérer l'examen : Il donne le sujet, surveille le temps, et s'assure que le robot étudiant ne triche pas ou ne plante pas.
2. Analyser les erreurs : Si le robot étudiant plante, le Professeur ne dit pas juste "Échec". Il dit : "Ah, il a eu une erreur de syntaxe" ou "Il a mis trop de temps". Il classe les erreurs pour qu'on puisse les réparer plus tard.

C'est comme passer d'un examen écrit où l'on rature tout si on a un faux pas, à un examen oral où le professeur comprend si vous avez bégayé à cause du stress ou si vous ne saviez vraiment pas la réponse.

---

🧹 Partie 1 : Le Nettoyage de la "Banque de Questions" (Les Données)

Avant de tester les robots, les auteurs ont dû nettoyer leur banque de questions (appelée FOLIO).
Imaginez que vous avez un livre de logique, mais que certaines pages ont été mal traduites par une machine. Certaines phrases sont contradictoires ou illisibles. Si vous posez ces questions à vos robots, ils vont échouer non pas parce qu'ils sont bêtes, mais parce que la question est nulle.

Ce qu'ils ont fait :
Ils ont créé une chaîne de montage automatisée (un pipeline) avec deux "ouvriers" intelligents :

• Le Critique : Il lit la question et la réponse attendue. S'il voit une incohérence (ex: "Tous les chats sont des chiens" vs "Ce chat est un chien"), il dit : "Hé, il y a une erreur ici !"
• Le Réparateur : Il essaie de corriger l'erreur automatiquement.
• L'Expert Humain : Si les robots ne peuvent pas se mettre d'accord, un humain intervient pour trancher.

Résultat : Ils ont créé une version "propre" et fiable du test, où chaque question a été vérifiée par un mathématicien virtuel (un solveur) pour s'assurer qu'elle est logique.

---

🤖 Partie 2 : Les Deux Robots en Compétition

Sur ce test nettoyé, ils ont mis aux prises deux types de robots pour voir qui est le meilleur en logique :

1. Le Robot "Penseur" (Chain-of-Thought)

C'est le robot classique. On lui dit : "Réfléchis étape par étape comme un humain, puis donne-moi la réponse."

• Analogie : C'est comme un élève qui écrit tout son raisonnement sur une copie. Il essaie de déduire la réponse en parlant à voix haute.
• Résultat : Il a eu 73,9 % de bonnes réponses. C'est bien, mais il se trompe souvent quand la logique est très tordue.

2. Le Robot "Traducteur-Ingénieur" (Auto-Formalization)

C'est le robot innovant. Au lieu de juste "réfléchir" en langage naturel, il traduit le problème en code informatique (un langage que les ordinateurs comprennent parfaitement, appelé Z3Py) et le lance dans un moteur de calcul.

• Analogie : Imaginez que vous avez un problème de logique complexe. Au lieu de l'expliquer à un ami, vous le transformez en équation mathématique précise, vous le donnez à une calculatrice ultra-puissante, et la calculatrice vous dit la réponse exacte.
• Sécurité : Si le code plante (erreur de frappe), le robot se dit : "Oh, j'ai fait une faute de frappe", il corrige le code, et réessaie jusqu'à 3 fois.

---

🏆 Les Résultats : Qui a gagné ?

Le robot "Traducteur-Ingénieur" a gagné haut la main avec 86,7 % de réussite, contre 73,9 % pour l'autre.

Pourquoi cette différence ?

• Sur les contradictions (Faux) : C'est là que le robot "Ingénieur" a brillé. Il a passé de 44 % à 77 % de réussite. Pourquoi ? Parce que quand on traduit un problème en code, l'ordinateur peut prouver mathématiquement qu'une chose est impossible. Le robot "Penseur", lui, peut se perdre dans ses propres mots et se tromper.
• Sur les cas incertains : Le robot "Ingénieur" a aussi mieux géré les situations où la réponse n'est pas claire, car le moteur de calcul lui dit exactement ce qui est déterminé et ce qui ne l'est pas.

💡 En Résumé

Ce papier nous dit deux choses importantes :

1. Pour bien tester l'intelligence artificielle, il faut un système d'évaluation intelligent qui ne confond pas les bugs techniques avec les erreurs de logique. C'est comme avoir un juge qui comprend la différence entre un accident de voiture et une conduite dangereuse.
2. La meilleure façon de faire de la logique pour un robot n'est pas toujours de "penser" comme un humain, mais de traduire le problème en un langage mathématique rigide que l'ordinateur peut vérifier sans erreur.

C'est une victoire pour la rigueur mathématique appliquée à l'intelligence artificielle ! 🧠✨

Résumé technique

1. Problématique

L'évaluation des agents de raisonnement logique rencontre plusieurs obstacles majeurs :

• Confusion des échecs : Les harness d'évaluation statiques traditionnels ont tendance à confondre les erreurs d'opération (délais d'attente, erreurs d'exécution, échecs d'analyse de sortie) avec les erreurs de raisonnement réel, masquant ainsi les modes d'échec sous un seul chiffre de précision.
• Couplage fort : Les architectures traditionnelles lient étroitement la logique du benchmark à l'implémentation de l'agent, ce qui rend l'intégration coûteuse et complexe à mesure que le nombre de benchmarks augmente.
• Fiabilité des données : Les jeux de données existants, comme FOLIO, contiennent des erreurs d'étiquetage et des incohérences entre les annotations en langage naturel et les formalisations logiques, compromettant la fiabilité des évaluations.

2. Méthodologie

Le papier propose une approche en deux volets : un nettoyage rigoureux des données et un nouveau cadre d'évaluation basé sur des agents.

A. Nettoyage et Réparation des Données (Pipeline FOLIO)

Les auteurs ont mis en place un pipeline systématique pour nettoyer le jeu de données FOLIO (First-Order Logic Inference) :

1. Vérification Symbolique : Utilisation du prouveur de théorèmes Vampire pour vérifier la consistance des prémisses et les relations d'implication.
   • VRAI (TRUE) : Les prémisses impliquent la conclusion ($\bigwedge \phi_i \to \phi$ est valide).
   • FAUX (FALSE) : Les prémisses contredisent la conclusion.
   • INCERTAIN : Aucune relation ne peut être déduite.
2. Identification et Réparation : Lorsqu'une divergence est détectée entre la vérification symbolique et l'étiquette originale, deux agents LLM interviennent :
   • Un agent critique diagnostique les erreurs de traduction (parenthèses déséquilibrées, fautes de frappe, incohérences de nommage).
   • Un agent raffineur applique des corrections ciblées.
3. Boucle itérative : Le processus de réparation se répète jusqu'à ce que l'étiquette attendue soit atteinte. Les cas non résolus après un seuil d'itérations sont envoyés à une revue humaine.

• Résultat du nettoyage : Sur l'ensemble de validation (203 exemples), 75,9 % ont été vérifiés directement, 4,9 % réparés automatiquement, et 19,2 % marqués comme problématiques. Cela a permis d'identifier et de corriger environ 1,5 % d'erreurs d'étiquetage dans l'ensemble de validation.

B. Cadre d'Évaluation « Agentifiée » (Agentified Assessment)

Au lieu d'un script d'évaluation statique, les auteurs utilisent une évaluation d'agent par agent (AAA) :

• L'Agent Évaluateur (Assessor Agent) : Il contrôle l'exécution des tâches, impose des budgets (délais, nombre de tentatives), analyse les sorties et enregistre les types d'échecs structurés (ex: TIMEOUT, RUNTIMEERROR, PARSEERROR). Il communique via une interface standardisée Agent-to-Agent (A2A).
• L'Agent à Tester : Il n'a besoin que d'exposer une interface A2A standardisée, ce qui permet une évaluation « plug-and-play » et réduit le coût d'intégration de $O(n)$ à $O(1)$ par agent.
• Agents comparés :
  1. Baseline Chain-of-Thought (CoT) : L'agent raisonne étape par étape et doit sortir l'étiquette finale sur la dernière ligne.
  2. Agent de Formalisation Automatique : Il traduit les prémisses et conclusions en code Z3Py (Python pour le solveur Z3) et utilise un solveur SMT (Satisfiability Modulo Theories) pour déterminer la validité logique. Il inclut une boucle d'auto-réparation (jusqu'à 3 tentatives) pour corriger les erreurs de syntaxe ou de quantificateurs.

3. Contributions Clés

1. Cadre d'évaluation robuste : Introduction d'un protocole où l'évaluation elle-même est un agent, permettant une traçabilité complète, une auditabilité et une gestion structurée des échecs d'exécution.
2. Jeu de données FOLIO révisé : Publication d'une version nettoyée et réparée de FOLIO avec des étiquettes vérifiées par des prouveurs de théorèmes, augmentant la fiabilité du benchmark.
3. Preuve de concept de l'approche hybride : Démonstration qu'un agent combinant la génération de code et l'exécution par solveur (formalisation automatique) surpasse les méthodes purement basées sur le raisonnement textuel (CoT) pour la logique du premier ordre.

4. Résultats Expérimentaux

L'évaluation a été menée sur l'ensemble de validation nettoyé de FOLIO (203 exemples) en utilisant le modèle Gemini 2.5 Flash.

• Précision Globale :
  • Chain-of-Thought (Baseline) : 73,89 % (150/203).
  • Agent de Formalisation Automatique : 86,70 % (176/203).
• Analyse par catégorie :
  • VRAI (TRUE) : Les deux méthodes performent bien, avec une légère avance pour l'agent formalisé (90,41 % vs 89,04 %).
  • FAUX (FALSE) : C'est ici que l'amélioration est la plus spectaculaire. L'agent formalisé atteint 77,05 % contre seulement 44,26 % pour le CoT. Cela suggère que le raisonnement par solveur est bien plus efficace pour détecter les contradictions.
  • INCERTAIN : L'agent formalisé améliore également la détection des cas indéterminés (91,30 % vs 84,06 %).

5. Signification et Conclusion

Ce travail démontre que l'intégration de la vérification formelle (via des solveurs SMT comme Z3) dans les agents de raisonnement est cruciale pour la robustesse, en particulier pour les tâches de logique du premier ordre où les erreurs de raisonnement implicite sont fréquentes.

L'approche Agentified Assessment offre un nouveau standard pour l'évaluation des agents : elle découple la logique de test de l'implémentation de l'agent, rendant les benchmarks plus reproductibles, auditable et résilients aux pannes d'exécution. Les auteurs suggèrent que cette méthodologie pourrait être étendue à des environnements d'agents utilisant des outils plus complexes, au-delà de la simple logique formelle.