Vers l'Autoformalization des Sorties Générées par LLM pour la Vérification des Exigences

Informations Fondamentales

• ID de l'article: 2511.11829
• Titre: Towards Autoformalization of LLM-generated Outputs for Requirement Verification
• Auteurs: Mihir Gupte, Ramesh S. (General Motors)
• Classification: cs.CL, cs.AI, cs.FL, cs.LO
• Date de publication: 18 novembre 2025 (prépublication arXiv)
• Lien de l'article: https://arxiv.org/abs/2511.11829

Résumé

Cet article explore la faisabilité d'utiliser des techniques d'autoformalization pour vérifier l'exactitude des sorties générées par les grands modèles de langage (LLM). Avec le potentiel démontré par les LLM dans la conversion des exigences en langage naturel en sorties structurées (comme les scénarios Gherkin), la vérification formelle de l'exactitude de ces sorties devient une question cruciale. L'équipe de recherche a mené deux séries d'expériences : la première a identifié avec succès l'équivalence logique entre deux exigences en langage naturel formulées différemment ; la deuxième a identifié les incohérences logiques entre les sorties générées par LLM et les exigences originales. Bien que la portée de la recherche soit limitée, les résultats démontrent un potentiel significatif de l'autoformalization pour assurer la fidélité et la cohérence logique des sorties générées par LLM.

Contexte de Recherche et Motivation

1. Problème Central

Avec la prolifération des applications LLM, particulièrement dans les tâches d'ingénierie telles que la génération automatique de scénarios de test, existe un défi clé : l'absence de méthodes formelles pour vérifier que les sorties générées par LLM reflètent fidèlement les exigences originales en langage naturel. Par exemple, après la génération d'un scénario Gherkin à partir d'une exigence telle que « Lorsque la vitesse du véhicule ≥ 10 et la ceinture de sécurité n'est pas attachée, activer l'alerte de ceinture de sécurité », il est impossible de garantir l'exactitude logique du contenu généré.

2. Importance du Problème

Dans les domaines critiques pour la sécurité, tels que l'ingénierie automobile, la vérification des exigences est cruciale. Une conversion incorrecte des exigences peut entraîner :

• Des cas de test incomplets ou erronés
• Un comportement du système non conforme aux attentes
• Des risques de sécurité potentiels

3. Limitations des Approches Existantes

• Méthodes formelles traditionnelles : principalement appliquées à la preuve de théorèmes mathématiques, manquent d'applications spécifiques à la vérification des exigences d'ingénierie
• Méthodes d'évaluation des LLM : dépendent de l'inspection manuelle ou de méthodes heuristiques, manquent de vérification logique rigoureuse
• Recherche en autoformalization : se concentrent principalement sur la construction de jeux de données et l'entraînement de modèles, peu d'applications en ingénierie pratique

4. Motivation de la Recherche

Cet article propose d'appliquer les techniques d'autoformalization à un nouveau scénario : la vérification des sorties générées par LLM. En convertissant à la fois les exigences en langage naturel et les sorties générées par LLM en représentations logiques formelles (Lean 4), il utilise des vérificateurs de théorèmes pour valider l'équivalence logique.

Contributions Principales

1. Proposition du premier pipeline d'autoformalization dédié à la vérification des sorties générées par LLM : convertit les exigences en langage naturel et les sorties LLM en représentations formalisées Lean 4, et vérifie la cohérence logique par la preuve d'équivalence biconditionnelle
2. Validation de deux scénarios d'application concrets :
   • Identification de l'équivalence logique entre des exigences en langage naturel formulées différemment
   • Détection d'incohérences logiques entre les sorties générées par LLM et les exigences originales
3. Identification des défis techniques clés :
   • Nécessité et difficulté d'automatisation de l'ancrage des variables (variable grounding)
   • Impact du non-déterminisme des LLM sur la formalisation
   • Traitement de l'ambiguïté du langage naturel
4. Proposition de directions de recherche futures : établit les fondations pour construire un cadre fiable de vérification des sorties LLM

Explication Détaillée de la Méthode

Définition de la Tâche

Entrées :

• Une paire de déclarations dont la relation logique doit être vérifiée (S₁, S₂), pouvant être :
  • Deux exigences en langage naturel
  • Une exigence en langage naturel et un scénario Gherkin généré par LLM

Sorties :

• Jugement d'équivalence logique : équivalent (S₁ ↔ S₂ peut être prouvé) ou non équivalent (preuve échouée)

Contraintes :

• Les déclarations doivent être formalisables en logique propositionnelle
• Les informations de contexte du système sont nécessaires pour l'ancrage des variables

Architecture du Modèle

Le pipeline global comprend quatre étapes clés (voir figure 9) :

Étape 1 : Autoformalization

Utilise DeepSeek-Prover-v2 (modèle 7B) pour convertir les déclarations en langage naturel en propositions Lean 4 :

-- Exemple : formalisation de l'exigence R1
variable (vehicle_speed_avg : ℝ)
variable (calibratable_speed : ℝ)
variable (seatbelt_active : Bool)
variable (initiate_chime : Bool)

def seatbelt_chime_condition : Prop :=
  (vehicle_speed_avg ≥ calibratable_speed ∨ ¬seatbelt_active) → initiate_chime

Modèle de prompt (voir annexe A.1) :

• Demande explicitement la génération d'énoncés def Lean 4
• Spécifie l'utilisation de logique propositionnelle (type Prop)
• Demande la représentation des conditions comme des implications (A ∧ B → C)

Étape 2 : Ancrage des Variables (Variable Grounding)

Implémentation actuelle : identification manuelle et unification des variables pointant vers le même concept dans différentes formalisations

Exemple de problème :

• vehicle_speed_avg dans R1 et mean_vehicle_speed dans R2 pointent vers la même grandeur physique
• Il est nécessaire d'informer explicitement le compilateur Lean de cette équivalence

-- Exemple d'ancrage manuel
(h_speed : vehicle_speed_avg = mean_vehicle_speed)
(h_belt : seatbelt_active = seatbelt_plugged_in)

Étape 3 : Construction de Théorème d'Équivalence Biconditionnelle

Construit un théorème formalisé pour vérifier l'équivalence logique :

theorem req1_eq_req2 
  (h_grounding : <hypothèses d'ancrage>) :
  (Proposition_A) ↔ (Proposition_B) := by
  <processus de preuve>

Étape 4 : Preuve Automatique de Théorème

Utilise à nouveau DeepSeek-Prover-v2 pour générer le code de preuve Lean :

• Preuve réussie → les deux déclarations sont logiquement équivalentes
• Échec de la preuve → existence d'incohérence logique

Points d'Innovation Technique

1. Innovation d'application interdisciplinaire : première application des techniques d'autoformalization du domaine de la preuve de théorèmes mathématiques à la vérification des exigences d'ingénierie logicielle
2. Utilisation LLM à deux niveaux :
   • Premier niveau : traduction de formalisation (LN → Lean)
   • Deuxième niveau : preuve de théorème (vérification d'équivalence)
3. Mécanisme de vérification basé sur l'échec : utilise l'échec du vérificateur de théorème comme indicateur d'incohérence logique, constituant une méthode de vérification négative innovante
4. Identification de l'ancrage des variables : met explicitement en avant que l'ancrage des variables est une étape indispensable du pipeline d'autoformalization, ce qui n'a pas été suffisamment souligné dans les recherches antérieures

Configuration Expérimentale

Ensemble de Données

Expérience 1 : Vérification d'Équivalence d'Exigences

• R1: « If Vehicle Speed Average Driven ≥ CALIBRATABLE Seatbelt Reminder Speed OR Seatbelt is inactive then initiate SeatBelt Chime »
• R2: « If mean vehicle speed is greater than CALIBRATABLE Seatbelt Reminder Speed OR Seatbelt is not plugged in then initiate chime for seatbelt »

Expérience 2 : Vérification de Sortie LLM

• R3: « When Front Passenger Seat Belt Status changes to 'Fastened' then the Front Passenger Seat Belt Reminder Indication On shall be set to FALSE. »
• G3: Scénario Gherkin généré par LLM (contenant 4 lignes d'exemple, introduisant des variables supplémentaires telles que seat_occupancy)

Métriques d'Évaluation

Métriques qualitatives :

• Succès/échec de la compilation Lean 4
• Succès/échec de la preuve de théorème

Critères de Vérification :

• Équivalence logique : le théorème PA ↔ PB peut être prouvé
• Incohérence logique : échec de la preuve du théorème ou impossibilité de compiler le code Lean

Détails d'Implémentation

Sélection du Modèle :

• DeepSeek-Prover-v2 (7B)
• Raisons du choix :
  1. Entraîné sur Lean 4
  2. Capacités de compréhension du langage naturel
  3. Adoption d'une stratégie de décomposition de sous-objectifs

Langage de Formalisation : Lean 4

• Puissantes capacités de preuve de théorème
• Expression logique précise
• Compatibilité avec DeepSeek-Prover-v2

Intervention Manuelle :

• Étape d'ancrage des variables entièrement manuelle
• Vérification des sorties de formalisation dépendant du compilateur Lean

Résultats Expérimentaux

Résultats Principaux

Expérience 1 : Vérification d'Équivalence d'Exigences (Cas de Succès)

Sorties de Formalisation :

• R1 et R2 ont été convertis avec succès en propositions Lean (figures 3, 4)
• Les mappages de variables ont été établis manuellement :
  • vehicle_speed_avg ≡ mean_vehicle_speed
  • seatbelt_active ≡ seatbelt_plugged_in

Résultats de Vérification (figure 5) :

• ✅ Compilation Lean réussie
• ✅ Preuve du théorème req1_eq_req2 réussie
• Conclusion : R1 et R2 sont logiquement équivalents

Signification : Démontre que le pipeline peut identifier les exigences sémantiquement identiques mais formulées différemment, facilitant la vérification de la cohérence des exigences.

Expérience 2 : Vérification de Sortie LLM (Cas d'Échec)

Sorties de Formalisation :

• R3 : proposition simple contenant uniquement les conditions de changement d'état de la ceinture de sécurité (figure 6)
• G3 : proposition complexe contenant des variables supplémentaires (seat_occupancy, initial_seatbelt_status) (figure 7)

Découvertes Clés :

• G3 introduit des variables non mentionnées dans R3
• Structure logique plus complexe (contenant 4 exemples de scénarios)

Résultats de Vérification (figure 8) :

• ❌ Compilation du code Lean échouée ou preuve échouée
• Conclusion : G3 est logiquement incohérent avec R3

Signification : Détecte avec succès le problème de « sur-génération » des sorties LLM — ajout de conditions de contrainte non présentes dans l'exigence originale.

Analyse de Cas

Cas : Problème d'Ambiguïté (R4)

Exigence :

« When the seatbelt is Unfastened and the vehicle is in motion then the Front Passenger Seat Belt Reminder Indication On shall be set to TRUE. »

Problème : L'ambiguïté de la formalisation de « vehicle in motion »

Deux formalisations Possibles (figure 10) :

1. pass@1 : variable booléenne vehicle_in_motion : Bool
2. pass@2 : variable numérique vehicle_speed > 0

Analyse :

• Les deux formalisations peuvent être sémantiquement correctes dans le système
• Cependant, elles ne sont pas équivalentes en logique formelle (types différents)
• Souligne l'impact de l'ambiguïté du langage naturel sur la formalisation

Découvertes Expérimentales

1. La formalisation dépend de l'interprétabilité : le non-déterminisme des LLM entraîne que la même exigence peut produire différentes formalisations, toutes « raisonnables »
2. L'ancrage des variables est un goulot d'étranglement :
   • Étape la plus chronophage
   • Nécessite des connaissances spécialisées du domaine
   • Actuellement réalisable uniquement manuellement
3. Le contexte du système est crucial : l'absence de définition explicite du système (comme un dictionnaire de données) entraîne des incohérences de formalisation
4. La vérification négative est efficace : l'échec de la preuve peut efficacement indiquer une incohérence logique

Travaux Connexes

Construction de Jeux de Données pour Autoformalization

• ProofNet : autoformalization mathématique de niveau premier cycle
• MiniF2F : benchmark mathématique de niveau olympiade
• Jeux de données multilingues : entraînement combiné sur Lean, Isabelle, Coq améliore les performances

Stratégies d'Entraînement des LLM

• Méthode « brouillon-esquisse-preuve » (Jiang et al.) : génération d'esquisses de preuve guidant la formalisation
• Décomposition de sous-objectifs : stratégie de recherche récursive adoptée par DeepSeek-Prover
• Apprentissage par renforcement : améliore le taux de succès de la preuve de théorème

Traitement du Non-Déterminisme

• Cadre d'équivalence symbolique : traite les différences entre pass@1 et pass@k
• Méthodes RAG : récupère les définitions formelles précises pour fournir du contexte

Extension aux Domaines d'Application

• Résolution de problèmes mathématiques : mathématiques du secondaire au premier cycle
• Vérification de code : vérification de la correction des programmes
• Biomédical : vérification de faits

Contribution de cet article : première application de l'autoformalization à la vérification des exigences d'ingénierie et à la vérification des sorties LLM, ouvrant une nouvelle direction de recherche.

Conclusions et Discussion

Conclusions Principales

1. Vérification de Faisabilité : le pipeline d'autoformalization peut efficacement vérifier la cohérence logique entre les sorties générées par LLM et les exigences originales
2. Valeur d'Application Double :
   • Vérification de la cohérence des exigences (identification des exigences équivalentes)
   • Contrôle de qualité des sorties LLM (détection des erreurs logiques)
3. Preuve de Concept : bien que l'échantillon soit limité, démontre avec succès le potentiel d'application des techniques de preuve de théorème à l'ingénierie logicielle

Limitations

1. Limitation d'Échelle :
   • Seulement 3 paires d'exigences testées
   • Manque d'évaluation à grande échelle
   • Absence d'analyse de signification statistique
2. Dépendance Manuelle :
   • Ancrage des variables entièrement manuel
   • Chronophage et sujet aux erreurs
   • Limite la scalabilité
3. Limitations du Modèle :
   • Utilisation d'un modèle 7B (ressources limitées)
   • Les modèles plus grands (671B) pourraient avoir de meilleures performances
   • La qualité de formalisation dépend des capacités du modèle
4. Ambiguïté Non Résolue :
   • Ambiguïté inhérente du langage naturel
   • Manque de support ontologique du système
   • Peut produire plusieurs formalisations « correctes » mais non équivalentes
5. Spécificité du Domaine :
   • Les expériences se limitent aux exigences de sécurité automobile
   • Capacité de généralisation inconnue

Directions Futures

L'article propose trois questions de recherche clés (RQ) :

RQ1 : Meilleure Méthode de Formalisation

• Explorer les stratégies k-pass (générer plusieurs formalisations, sélectionner la plus probable)
• Comparer la précision entre conversion unique et échantillonnage multiple

RQ2 : Automatisation de l'Ancrage des Variables

• Méthode 1 : formalisation contextuelle unique (traiter toutes les déclarations dans un seul appel)
• Méthode 2 : ancrage basé sur la similarité (utiliser les embeddings pour correspondre à l'ontologie du système)
• Défi : comment vérifier que les hypothèses d'ancrage du LLM lui-même sont correctes

RQ3 : Vérification LLM dans les Systèmes Contraints

• Construire des graphes de connaissances des actions du système
• Développer des mécanismes de traversée pour LLM
• Utiliser l'autoformalization pour garantir la cohérence logique des sorties
• Scénarios d'application : maisons intelligentes, assistants embarqués et autres systèmes avec espace d'action limité

Autres Directions :

• Développer des techniques automatisées de normalisation des variables
• Intégrer des ontologies spécifiques au domaine (comme les dictionnaires de données des systèmes automobiles)
• Étendre à des représentations logiques plus complexes (comme la logique temporelle)

Évaluation Approfondie

Points Forts

1. Définition du Problème Novatrice :
   • Première application systématique de l'autoformalization à la vérification des sorties LLM
   • Résout un vrai problème douloureux de la pratique d'ingénierie
   • Ouvre une nouvelle direction de recherche
2. Méthodologie Claire :
   • Conception du pipeline simple et compréhensible
   • Utilise des outils matures (Lean 4, DeepSeek-Prover)
   • Forte reproductibilité
3. Identification Profonde des Problèmes :
   • Met explicitement en avant la criticité de l'ancrage des variables
   • Analyse approfondie du problème d'ambiguïté
   • Discussion honnête de l'impact du non-déterminisme des LLM
4. Valeur Pratique Élevée :
   • Ciblant les domaines critiques pour la sécurité (ingénierie automobile)
   • Applicable directement aux processus d'ingénierie des exigences
   • Contribue à améliorer la fiabilité des applications LLM
5. Qualité d'Écriture Excellente :
   • Structure claire, logique rigoureuse
   • Fournit des modèles de prompt détaillés (annexe)
   • Figures riches, faciles à comprendre

Insuffisances

1. Échelle Expérimentale Gravement Insuffisante :
   • Seulement 3 échantillons : impossible de tirer des conclusions statistiques
   • Manque de tests sur des exigences de différents domaines et complexités
   • Pas d'évaluation des performances sur des ensembles de données plus grands
   • Recommandation : au minimum 50-100 paires d'exigences pour une évaluation suffisante
2. Manque d'Évaluation Quantitative :
   • Pas de métriques de précision, rappel, etc.
   • Pas de rapport du taux de succès de formalisation
   • Manque de comparaison avec la vérification manuelle
   • Recommandation : construire un ensemble de données annotées, calculer les métriques de précision
3. Intervention Manuelle Excessive :
   • Ancrage des variables entièrement manuel, affaiblissant la revendication d'automatisation
   • Pas de solution d'automatisation concrète fournie
   • Scalabilité douteuse
   • Recommandation : implémenter au moins un système prototype d'ancrage automatique
4. Choix du Modèle Limité :
   • Utilisation d'un modèle 7B uniquement en raison de limitations de ressources
   • Pas d'exploration du modèle 671B ou d'alternatives
   • Manque d'analyse de l'impact de la taille du modèle sur les résultats
   • Recommandation : au minimum comparer différents modèles sur un petit nombre d'échantillons
5. Manque d'Analyse des Cas d'Échec :
   • Pas d'analyse détaillée des raisons de l'échec de la preuve de théorème
   • Pas de distinction entre erreur de formalisation et véritable incohérence logique
   • Manque d'analyse des faux positifs/faux négatifs
   • Recommandation : établir une taxonomie des erreurs
6. Critères d'Évaluation Uniques :
   • Dépend uniquement du succès/échec de la compilation Lean
   • Ne considère pas les cas partiellement corrects
   • Manque d'analyse granulaire des types d'erreurs
7. Capacité de Généralisation Inconnue :
   • Teste uniquement les exigences de sécurité automobile
   • N'a pas validé l'applicabilité dans d'autres domaines (médical, financier, etc.)
   • La spécificité des scénarios Gherkin peut limiter la généralité de la méthode

Impact

Contribution au Domaine :

• ⭐⭐⭐⭐ Contribution Conceptuelle Élevée : propose une nouvelle direction de recherche et un scénario d'application
• ⭐⭐ Contribution Technique Modérée : principalement une combinaison de technologies existantes
• ⭐⭐⭐ Valeur Pratique Relativement Élevée : résout un vrai problème de la pratique d'ingénierie

Valeur Pratique :

• Court terme : fournit aux ingénieurs des exigences une approche de vérification
• Moyen terme : peut catalyser le développement d'outils de vérification spécialisés
• Long terme : peut devenir un processus standard d'assurance qualité pour les applications LLM

Reproductibilité :

• ✅ Utilise des outils open-source (Lean 4, DeepSeek-Prover)
• ✅ Fournit des modèles de prompt détaillés
• ❌ N'a pas publié le code ou les données
• ❌ Les étapes manuelles sont difficiles à reproduire
• Évaluation : ⭐⭐⭐ (modéré)

Impact Attendu :

• Peut déclencher plus de recherches sur la vérification formelle des sorties LLM
• Peut promouvoir l'intégration de l'ingénierie des exigences et des méthodes formelles
• Le problème d'ancrage des variables peut devenir un nouveau point chaud de recherche

Scénarios Applicables

Hautement Applicable :

• ✅ Vérification des exigences des systèmes critiques pour la sécurité (automobile, aéronautique, médical)
• ✅ Vérification de la cohérence des exigences et dédoublonnage
• ✅ Contrôle de qualité des cas de test générés par LLM

Modérément Applicable :

• ⚠️ Vérification de logiques métier complexes (nécessite l'extension des capacités de formalisation)
• ⚠️ Exigences multimodales (comme les exigences contenant des diagrammes)
• ⚠️ Systèmes temps réel (nécessite l'extension à la logique temporelle)

Non Applicable :

• ❌ Textes en langage naturel hautement ambigus
• ❌ Scénarios manquant de définition explicite du système
• ❌ Scénarios nécessitant une réponse en temps réel (les étapes manuelles actuelles sont trop lentes)

Recommandations d'Amélioration

1. Immédiatement Réalisable :
   • Étendre à au minimum 50 paires d'exigences
   • Implémenter un prototype d'ancrage automatique des variables basique
   • Établir une taxonomie des erreurs
2. Améliorations à Court Terme :
   • Comparer différentes tailles de modèles
   • Introduire des métriques d'évaluation quantitatives
   • Tester sur plusieurs domaines
3. Objectifs à Long Terme :
   • Pipeline entièrement automatisé
   • Intégration de graphes de connaissances du domaine
   • Support de la logique temporelle et des contraintes complexes

Références Clés

1. Weng et al. (2025) : Autoformalization in the era of large language models: A survey - littérature de synthèse
2. Wu et al. (2022) : Autoformalization with large language models - travail fondamental
3. Ren et al. (2025) : DeepSeek-Prover-v2 - modèle central utilisé dans cet article
4. Jiang et al. (2022) : Draft, sketch, and prove - méthode de décomposition de sous-objectifs
5. de Moura & Ullrich (2021) : The Lean 4 theorem prover - langage de formalisation

Évaluation Globale : Ceci est un article de preuve de concept de nature exploratoire qui propose une nouvelle direction de recherche précieuse, mais avec une vérification expérimentale gravement insuffisante. En tant que prépublication et recherche préliminaire, il réussit à identifier les problèmes clés et à fournir un chemin technique viable, mais il reste loin d'une solution mature. La valeur principale de l'article réside dans la définition du problème et l'orientation de la direction, plutôt que dans les percées technologiques. Les travaux ultérieurs sont recommandés pour se concentrer sur la résolution de l'automatisation de l'ancrage des variables et de l'évaluation à grande échelle.