Can LLM Aid in Solving Constraints with Inductive Definitions?

Cet article propose une approche neuro-symbolique combinant les grands modèles de langage et les solveurs de contraintes pour générer itérativement des lemmes auxiliaires, améliorant ainsi de manière significative la résolution des contraintes impliquant des définitions inductives par rapport aux méthodes actuelles.

L'essentiel

Imagine que vous essayez de résoudre un casse-tête mathématique très complexe, comme prouver que l'ordre dans lequel vous multipliez deux nombres ne change pas le résultat (la commutativité de la multiplication). C'est ce que font les ordinateurs pour vérifier si des logiciels sont sûrs.

Le problème, c'est que ces preuves impliquent souvent des définitions "récursives" (des choses qui se définissent elles-mêmes, comme une poupée russe qui en contient une autre, et ainsi de suite). Les logiciels classiques de vérification (les "SMT" ou "CHC") sont très forts, mais ils ont un point faible : ils sont comme des robots très rigides. Ils peuvent suivre des règles strictes, mais s'ils ne voient pas le chemin direct, ils s'arrêtent et disent : "Je ne sais pas". Ils ont besoin d'un "pont" (une petite preuve intermédiaire ou un "lemme") pour franchir le fossé, mais ils ne savent pas toujours inventer ce pont eux-mêmes.

C'est là qu'intervient l'idée de cette recherche : donner un cerveau créatif (une IA générative) à ce robot rigide.

Voici comment cela fonctionne, expliqué avec des images simples :

1. Le Duo Gagnant : L'Architecte et l'Inspecteur

Les auteurs proposent une méthode "neuro-symbolique", ce qui est un mot compliqué pour dire : mélanger l'intuition d'une IA avec la rigueur d'un mathématicien.

• L'Architecte (L'IA / LLM) : Imaginez un architecte très imaginatif qui a lu tous les livres de mathématiques. Son travail est de proposer des idées de ponts (des lemmes). Il dit : "Et si on essayait de prouver que A + B = B + A avant de prouver la multiplication ?" ou "Peut-être que cette formule bizarre est la clé ?".
  • Le problème : L'architecte est parfois un peu rêveur. Il peut proposer des ponts qui n'existent pas, qui sont faux, ou qui ne mènent nulle part.
• L'Inspecteur (Le Solveur Logique) : C'est le robot rigide. Son travail est de vérifier chaque idée de l'architecte. Il dit : "Attends, ce pont est faux, il s'effondre" ou "Non, ce pont est vrai, mais il ne nous aide pas à traverser la rivière".

2. La Méthode en Trois Actes

Au lieu de laisser l'IA faire n'importe quoi, les chercheurs ont créé un processus en trois étapes, comme un atelier de fabrication de preuves :

• Étape 1 : Le Questionnement (La Stratégie)
  Au lieu de demander simplement à l'IA "Donne-moi une preuve", les chercheurs lui donnent des instructions précises, comme un chef d'orchestre.

  • Stratégie 1 (Le pas à pas) : Ils demandent à l'IA de raisonner comme un humain : "Regarde la première étape, puis la suivante. Où bloques-tu ? Invente une règle pour débloquer cette étape."
  • Stratégie 2 (La simplification) : Ils demandent à l'IA de simplifier le problème. "Si on enlève cette partie compliquée, qu'est-ce qui reste ? Trouve une règle qui relie la version simple à la version complexe."
  • Analogie : C'est comme si, au lieu de demander à un enfant de construire une tour de 100 étages d'un coup, on lui disait : "D'abord, construis une base solide. Ensuite, imagine comment on pourrait ajouter un étage de plus."

• Étape 2 : Le Filtre (Le Tamis)
  L'IA génère souvent des idées folles. Avant de perdre du temps à vérifier si elles sont utiles, un filtre rapide les élimine.

  • Si l'idée est mal écrite (faute de syntaxe) -> Poubelle.
  • Si l'idée est la même que le problème à résoudre (tricher) -> Poubelle.
  • Si l'idée contredit les règles de base (ex: dire que 2+2=5) -> Poubelle.
  • Analogie : C'est comme un tamis qui ne laisse passer que les cailloux de la bonne taille, en jetant la poussière et les gros rochers immédiatement.

• Étape 3 : La Validation (Le Test de Résistance)
  Les idées qui passent le filtre sont envoyées à l'Inspecteur (le solveur).

  • Est-ce que cette idée aide vraiment à prouver le problème final ?
  • Est-ce que cette idée est elle-même vraie ? (Parfois, l'IA propose un pont vrai, mais qu'on ne peut pas construire avec les outils dont on dispose. Dans ce cas, on doit prouver ce pont d'abord !).
  • Si tout passe, Boum ! La preuve est trouvée.

3. Les Résultats : Pourquoi c'est impressionnant

Les chercheurs ont testé cette méthode sur 706 problèmes mathématiques difficiles (des "casse-têtes" de logique).

• Le résultat : Leur méthode (nommée LLM4Ind) a réussi à résoudre 25 % de problèmes de plus que les meilleurs logiciels actuels qui fonctionnent seuls.
• La robustesse : Cela fonctionne même si on change l'IA utilisée (comme changer de modèle de voiture) ou si on la rend un peu plus "créative" ou "sérieuse". C'est comme si le système était capable de s'adapter à différents types d'architectes.

En résumé

Imaginez que vous essayez de traverser une rivière très large.

• Les logiciels classiques sont comme des ponts préfabriqués. Ils sont solides, mais s'il n'y a pas de pont exactement à l'endroit où vous êtes, vous êtes bloqué.
• Cette nouvelle méthode ajoute un ingénieur créatif (l'IA) qui peut imaginer des ponts temporaires, des passerelles ou des radeaux.
• Mais comme l'ingénieur peut se tromper, un inspecteur de génie civil (le solveur) vérifie immédiatement si chaque idée est solide et utile.

Le résultat ? On peut traverser des rivières (résoudre des problèmes) que l'on croyait infranchissables, en combinant l'imagination de l'IA avec la rigueur absolue des mathématiques. C'est une victoire pour la sécurité des logiciels et la vérification automatique.

Résumé technique

Voici un résumé technique détaillé de l'article "Can LLM Aid in Solving Constraints with Inductive Definitions?" (Les LLM peuvent-ils aider à résoudre des contraintes avec des définitions inductives ?).

1. Problème et Contexte

La vérification de programmes repose souvent sur le raisonnement inductif concernant des définitions inductives, telles que les types de données algébriques (ADT) et les fonctions définies récursivement (RDF).

• Défi actuel : Les solveurs de contraintes d'état de l'art (SMT comme cvc5, Z3) et les prouveurs de logique du premier ordre (comme Vampire) peinent à résoudre automatiquement des contraintes impliquant ces définitions, en particulier lorsqu'il faut déduire des lemmes auxiliaires complexes.
• Limites des méthodes existantes :
  • L'exploration de théorie (génération de conjectures par énumération) échoue sur des lemmes complexes.
  • Les méthodes de généralisation manquent d'expressivité.
  • Les méthodes basées sur les clauses de Horn contraintes (CHC) ont des difficultés avec les RDF.
• Opportunité : Les Grands Modèles de Langage (LLM) montrent des capacités prometteuses en génération de code et en raisonnement, mais ils souffrent de deux problèmes majeurs dans ce contexte :
  1. Ils ne sont pas naturellement efficaces pour le raisonnement inductif spécifique sans guidage.
  2. Leurs sorties sont aléatoires et peuvent contenir des "hallucinations" (conjectures fausses ou inutiles).

2. Méthodologie : Approche Neuro-Symbolique

Les auteurs proposent une approche hybride, LLM4Ind, qui intègre de manière synergique les LLM et les solveurs de contraintes dans un flux de travail itératif en trois étapes : Requête (Query), Filtrage (Filter) et Validation (Validate).

A. Workflow Global

L'algorithme principal (ProveRun) tente de prouver un objectif en utilisant une approche récursive :

1. Vérification initiale : Le solveur SMT tente de prouver l'objectif directement.
2. Génération de conjectures : Si échec, le système interroge le LLM avec des stratégies de prompts spécifiques pour générer des lemmes candidats.
3. Filtrage : Les conjectures sont rapidement rejetées si elles sont syntaxiquement incorrectes, identiques à l'objectif, ou contradictoires avec les axiomes.
4. Validation : Les conjectures restantes sont vérifiées pour voir si elles aident à prouver l'objectif. Si oui, elles deviennent de nouveaux sous-objectifs (récursivement traités).

B. Stratégies de Prompting (Clé de l'approche)

Pour surmonter le manque de stratégie des LLM, deux stratégies de prompts sont conçues :

1. Raisonnement Équationnel (Strategy 1) : Imitation du raisonnement humain pas à pas. Le LLM est invité à décomposer le cas inductif, appliquer les axiomes et l'hypothèse inductive, et identifier les étapes où une conjecture est nécessaire pour combler le vide.
2. Réécriture de Termes et Généralisation (Strategy 2) : Le LLM est guidé pour simplifier l'objectif en identifiant des termes communs, en renforçant la conclusion, ou en générant des lemmes "ponts" entre une forme simplifiée et l'objectif original.

C. Boucle de Validation

• Filtrage (isFiltered) : Utilise le solveur SMT avec un timeout court (1s) pour rejeter les conjectures fausses ($A \land L$ insatisfiable) ou inutiles.
• Validation (Verify) : Vérifie si l'ensemble des conjectures $C$ permet de prouver l'objectif ($A \land \bigwedge C \to P$). Si oui, chaque conjecture devient un nouveau problème de preuve à résoudre récursivement.

3. Contributions Clés

1. Première intégration systématique de LLM pour la génération automatique de lemmes dans le contexte du raisonnement inductif pur (SMT/Logique du premier ordre), au-delà de la simple assistance interactive.
2. Conception de stratégies de prompts spécifiques (raisonnement équationnel et généralisation) qui guident le LLM vers des conjectures structurellement pertinentes.
3. Architecture Neuro-Symbolique robuste qui combine la puissance générative des LLM avec la rigueur formelle des solveurs SMT pour éliminer les erreurs et les hallucinations.
4. Outil Open Source (LLM4Ind) et benchmark complet disponible publiquement.

4. Résultats Expérimentaux

L'évaluation a été menée sur 706 instances provenant de quatre benchmarks standards (StandardDT, StandardDTLIA, Autoproof, IndBen).

• Performance par rapport à l'état de l'art :
  • LLM4Ind résout environ 25 % de tâches de plus que les meilleurs solveurs existants (cvc5, Vampire, Racer).
  • Sur le benchmark total, LLM4Ind a résolu 525 tâches contre 293 pour cvc5 et 343 pour Vampire (avec une limite de temps de 1200s).
  • L'approche surpasse cvc5 de manière significative sur des tâches complexes (ex: +182 tâches de plus sur l'ensemble).
• Robustesse :
  • L'approche fonctionne bien avec différents modèles de LLM (Qwen, DeepSeek, Gemini, GPT-5).
  • Elle est robuste face aux variations de température d'échantillonnage (de 0.1 à 1.3), montrant une faible variance dans les résultats.
  • Elle fonctionne avec différents solveurs backend (cvc5 et Vampire).
• Analyse d'ablation :
  • Les stratégies de prompts avancées sont cruciales : une approche "naïve" (sans stratégie spécifique) résout beaucoup moins de tâches.
  • Le module de filtrage améliore l'efficacité en évitant de gaspiller du temps de calcul sur des conjectures fausses, réduisant également la consommation de tokens.

5. Signification et Impact

• Avancée Automatisation : Ce travail démontre que les LLM peuvent être intégrés de manière fiable dans des boucles de preuve entièrement automatisées, comblant le fossé entre la génération créative de conjectures et la vérification formelle rigoureuse.
• Dépassement des limites logiques : Il offre une solution aux limitations des méthodes purement logiques (heuristiques fixes) pour la découverte de lemmes complexes nécessaires à la preuve de propriétés inductives.
• Futur de la Vérification : L'approche suggère une nouvelle voie pour les vérificateurs de programmes, où l'IA assiste non pas seulement l'humain, mais agit comme un composant autonome capable de découvrir des preuves que les solveurs traditionnels ne peuvent pas trouver seuls.

En résumé, l'article prouve qu'une approche neuro-symbolique bien conçue, combinant des prompts stratégiques et une validation rigoureuse par solveur, permet de résoudre significativement plus de problèmes de vérification inductive que les méthodes actuelles.