Aller au contenu

Apple GSM-Symbolic : les LLM font du pattern matching, pas du raisonnement mathematique

Resume

Des chercheurs Apple publient GSM-Symbolic, un benchmark qui demontre que les LLM ne raisonnent pas en mathematiques. En modifiant les valeurs numeriques ou en ajoutant une phrase non pertinente aux problemes de maths de primaire (GSM8K), les performances chutent jusqu'a 65%. Meme o1-preview (le modele de raisonnement avance d'OpenAI) passe de 92.7% a 77.4%. Les modeles font du pattern matching sur les mots-cles ("discount" -> multiplier, "smaller" -> soustraire), pas du raisonnement logique.

Analyse critique

Ce qui est juste :

Le papier est methodologiquement solide. Le protocole est simple et devastateur : 1. Prendre un probleme GSM8K (maths primaire) 2. Changer uniquement les valeurs numeriques -> les resultats varient jusqu'a 15 points de pourcentage 3. Ajouter 1 phrase non pertinente ("cinq d'entre eux etaient plus petits que la moyenne") -> chute jusqu'a 65% 4. Donner 8 exemples resolus du meme probleme PUIS poser la question -> le modele echoue quand meme

Le "probleme des kiwis" est emblematique : le modele voit "five of them were a bit smaller than average" et soustrait 5 du total. Il ne comprend pas que la taille est irrelevante pour un comptage.

Ce qui est exagere :

  • Le titre viral "AI models cannot do math" simplifie. Les LLM sont mauvais sur les maths avec distracteurs. Sur les problemes standard, les scores sont corrects — c'est le delta qui est revelateur.
  • Le papier date d'octobre 2024 (arxiv 2410.05229). Les modeles plus recents (Claude Opus 4.6, GPT-5) pourraient performer differemment. Mais le mecanisme sous-jacent (pattern matching vs raisonnement) reste valide.

Le vrai signal :

Les benchmarks de maths mesurent la memorisation du corpus d'entrainement, pas la capacite de raisonnement. Si on change juste les nombres, les resultats changent. C'est une faille fondamentale de l'architecture transformer pour le raisonnement formel.

Pertinence ProbatioVault

Impact modere — Renforce nos choix architecturaux :

  1. Verification formelle quad-moteur (TLA+/Alloy/Z/Prolog) : les LLM ne remplaceront JAMAIS les prouveurs formels pour verifier les invariants mathematiques. Ce papier le confirme. Notre investissement dans ProbatioVault-formal est justifie.

  2. Article II (validation croisee) : un LLM qui "raisonne" sur une spec fait du pattern matching. La validation croisee par un deuxieme LLM ne corrige pas le probleme — il faut des mecanismes formels (Prolog, TLA+).

  3. TODO #23 (generation adversariale contre-exemples) : les contre-exemples formels (L-System / Prime Radiant) sont encore plus importants si les LLM ne font que pattern-matcher. Un faux positif LLM sur un invariant crypto/eIDAS serait catastrophique.

  4. Gates PMO : le scoring des gates par ChatGPT (temperature 0.1) est fiable pour la structure et la completude, mais pas pour la verification logique. Renforce le choix de garder les checks formels separement.