Résumé technique : Les LLM s'appuient sur les a priori, et non sur la sémantique des langages de programmation

Énoncé du problème

Les modèles de langage de grande taille (LLM) actuels sont de plus en plus déployés pour résoudre des tâches de programmation qui nécessitent ostensiblement un raisonnement sur le comportement des programmes, comme la prédiction de sorties, la réparation de code ou la génération de nouveau code. Une question fondamentale demeure : ces modèles s'appuient-ils principalement sur des régularités statistiques acquises lors du pré-entraînement (a priori lexicaux), ou peuvent-ils conditionner de manière flexible leur raisonnement sur des règles comportementales explicitement fournies ?

Bien que les LLM soient souvent performants sur des tâches de programmation standards, il n'est pas clair s'ils peuvent adapter leur raisonnement à des systèmes formels spécifiés de l'extérieur lorsque ces derniers entrent en conflit avec des a priori ancrés dans les données. Par exemple, si le symbole '+' est explicitement défini pour effectuer une soustraction dans un ensemble de règles fourni, un modèle s'appuyant sur ses a priori produira probablement encore une addition, tandis qu'un modèle conditionné par les règles s'adaptera. Ce document examine si les LLM peuvent conditionner leur raisonnement sur des sémantiques formelles via l'exécution de programmes, en testant spécifiquement leur capacité à outrepasser les associations entre symboles et significations apprises.

Méthodologie

Les auteurs introduisent PLSEMANTICSBENCH, un benchmark piloté par la sémantique conçu pour sonder le raisonnement conditionné par des règles sous des changements de distribution contrôlés. La méthodologie comprend trois composantes centrales :

1. Formalisme et Langage

Le benchmark utilise un langage impératif léger, C⋆, dérivé du C mais simplifié pour éviter les ambiguïtés syntaxiques (par exemple, des délimiteurs de blocs explicites {} sont utilisés pour éviter les problèmes de sensibilité à l'indentation rencontrés en Python). Le langage est associé à deux systèmes de sémantique formelle distincts :

• Sémantique opérationnelle structurelle à petits pas (S) : Un système fin où chaque règle représente une étape de calcul atomique.
• Sémantique K (K) : Un système de réécriture plus grossier.

Ces formalismes permettent d'altérer systématiquement les définitions des règles sans changer la syntaxe de surface des programmes.

2. Décalages sémantiques et facteurs de stress

Pour découpler le raisonnement sémantique de la familiarité syntaxique, le benchmark introduit deux types de mutations sémantiques :

• KeywordSwap (Échange de mots-clés) : Des opérateurs syntaxiques sélectionnés (ex. : +, -) échangent leurs interprétations sémantiques. Par exemple, + est défini pour effectuer une soustraction. Cela crée un conflit direct avec les a priori du pré-entraînement tout en préservant la syntaxe de surface.
• KeywordObf (Obscurcissement de mots-clés) : Les mots-clés et opérateurs standards sont remplacés par des symboles nouveaux (tirés de l'alphabet caucasien-albanais) dont les significations sont définies uniquement par les règles fournies. Cela supprime tous les a priori syntaxiques.

Le benchmark évalue les modèles à travers trois divisions de jeux de données avec une complexité structurelle croissante :

• Écrit par l'humain (Human-Written) : Programmes adaptés de benchmarks de codage standards (LeetCode, HumanEval, etc.).
• Traduit par LLM (LLM-Translated) : Solutions C++ traduites en C⋆ par des LLM.
• Généré par Fuzzer (Fuzzer-Generated) : Programmes générés automatiquement par un fuzzer sensible à la sémantique et à contrôle de profondeur pour maximiser la complexité du flux de contrôle et de données.

3. Tâches d'évaluation

Le benchmark sonde quatre hypothèses concernant les capacités des modèles :

• H1 (Conditionnement de règle globale) : Les modèles peuvent-ils composer de nombreuses applications de règles pour prédire correctement les états finaux des programmes ? (Tâche : PredState)
• H2 (Conditionnement de règle sans état) : Les modèles peuvent-ils sélectionner les règles opérationnelles correctes lorsque l'état du programme ne mute pas ? (Tâche : PredRule)
• H3 (Conditionnement de règle à long horizon) : Les modèles peuvent-ils maintenir un raisonnement conditionné par des règles sur de longues traces d'exécution (boucles, flux de contrôle imbriqués) ? (Tâche : PredTrace)
• H4 (Conditionnement de règle sous décalage sémantique) : Les modèles continuent-ils de suivre les règles fournies sous des sémantiques nouvelles qui entrent en conflit avec les a priori ?

L'étude évalue 11 LLM de pointe, incluant des modèles de non-raisonnement (ex. : Llama-3.3, Qwen2.5-Inst) et des modèles orientés raisonnement (ex. : variantes de DeepSeek-R1, O3-mini, GPT-5-mini, Gemini-2.5-pro).

Contributions clés

1. PLSEMANTICSBENCH : Le premier benchmark à grande échelle explicitement conçu pour tester si les LLM conditionnent leur raisonnement sur des règles formelles plutôt que sur des a priori statistiques, en utilisant l'exécution de programmes comme une sonde contrôlée.
2. Décalages sémantiques formels : L'introduction des transformations KeywordSwap et KeywordObf qui perturbent systématiquement les correspondances entre symboles et significations tout en préservant la structure des règles, permettant d'isoler la dépendance aux associations lexicales versus les définitions formelles.
3. Analyse granulaire du raisonnement : Une décomposition du raisonnement d'exécution de programme en prédiction d'état global, sélection de règle locale et génération de trace à long horizon, révélant les modes de défaillance spécifiques des modèles actuels.
4. Évaluation empirique complète : Une évaluation systématique à travers 11 modèles, trois complexités de jeux de données et deux formalismes sémantiques, fournissant une carte détaillée des capacités et limites actuelles.

Résultats

Les expériences produisent plusieurs conclusions critiques :

• Dépendance aux a priori : Sous des sémantiques standards, de nombreux modèles atteignent une précision élevée (jusqu'à 90 %) sur des tâches simples. Cependant, sous des mutations sémantiques (KeywordSwap), la performance chute brutalement de 40 à 60 points de pourcentage. Cela indique que les modèles s'appuient principalement sur des associations lexicales pré-entraînées plutôt que sur les règles formelles fournies.
• Sensibilité au décalage sémantique : La mutation KeywordSwap provoque une dégradation de performance nettement plus importante que KeywordObf. Cela suggère que la présence d'une syntaxe familière (même avec un sens altéré) déclenche des réponses basées sur les a priori que les modèles ne parviennent pas à outrepasser.
• Fragilité du long horizon : Maintenir un raisonnement conditionné par des règles sur de longues traces d'exécution est extrêmement fragile. Seule une poignée de modèles atteint une précision non nulle sur la tâche PredTrace, et même les meilleurs systèmes n'atteignent que ~35 % de précision. La plupart des modèles s'effondrent vers une précision de zéro lorsqu'ils doivent suivre l'état et appliquer des règles de manière répétée sur des dizaines d'étapes.
• Impact de la complexité : La performance se détériore systématiquement avec l'augmentation de la complexité structurelle (profondeur du flux de contrôle, dépendances de flux de données). Bien que les modèles orientés raisonnement bénéficient de l'accès aux règles formelles sur des programmes simples écrits par l'humain, cet avantage disparaît ou s'inverse souvent sur des programmes complexes générés par fuzzer.
• Limitations de la Chaîne de Pensée (CoT) : Le prompting CoT améliore les performances sur les sémantiques standards pour les modèles de non-raisonnement, mais échoue à surmonter le biais introduit par les échanges sémantiques, indiquant que les traces de raisonnement seules ne permettent pas aux modèles d'outrepasser les a priori d'opérateurs ancrés.
• Compréhension de la notation : Les modèles démontrent généralement une haute compétence dans la compréhension de la notation formelle elle-même (tâches NL→Rule et Rule→NL), suggérant que les échecs dans les tâches d'exécution proviennent de limitations de raisonnement plutôt que d'une incapacité à parser le formalisme.

Signification et revendications

Le papier positionne le conditionnement par règle inférentielle comme un axe de capacité largement non résolu pour les systèmes d'apprentissage en matière de langages de programmation. Les auteurs affirment que les LLM contemporains échouent souvent à conditionner leur raisonnement sur des systèmes formels spécifiés de l'extérieur lorsque ceux-ci entrent en conflit avec les a priori dérivés des données.

La signification de ce travail réside dans :

1. Capacité de diagnostic : Fournir une méthode rigoureuse pour distinguer la reconnaissance de formes statistiques du véritable respect des règles dans les LLM.
2. Identification des limites : Souligner que les modèles actuels manquent de robustesse pour s'adapter à de nouvelles sémantiques formelles, une exigence critique pour les applications impliquant la surcharge d'opérateurs, les langages de domaines spécifiques (DSL) et la vérification formelle.
3. Direction future : Motiver le développement de modèles capables de raisonner plus fidèlement sur des spécifications formelles, en allant au-delà de la dépendance aux "associations lexicales ancrées" vers des systèmes capables d'un véritable raisonnement conditionnel basé sur les règles fournies.

Les auteurs concluent que bien que les LLM soient prometteurs dans les tâches d'exécution standards, leur capacité à conditionner leur raisonnement sur des règles formelles explicites reste un goulot d'étranglement important, particulièrement sous des décalages sémantiques et des horizons d'exécution longs.