webAI, une startup d'IA d'entreprise basée à Austin, a lancé aujourd'hui TwiL-LM : deux petits modèles — 1,7 Md et 3 Md de paramètres — conçus spécifiquement pour l'autoformalisation, la tâche consistant à traduire de l'anglais courant en logique formelle et à vérifier si des conclusions découlent bien de leurs prémisses. L'affirmation phare : TwiL-LM3, à 3 milliards de paramètres, bat GPT-OSS-120B d'OpenAI — quarante fois plus gros — sur quatre des cinq benchmarks de raisonnement formel de son propre panel.
L'arithmétique tient. Ce qui mérite d'être lu au-delà du titre, c'est le cinquième benchmark, et quelques éléments que la publication elle-même ne concilie pas tout à fait.
Les cinq benchmarks
| Benchmark | TwiL-LM3 (3 Md) | GPT-OSS-120B | Résultat |
|---|---|---|---|
| Induction de règles (dériver des règles à partir de données) | 96,4 | 65,2 | TwiL gagne de 31 points |
| Analyse sémantique (langage → requête structurée, F1 token) | 87,6 | 43,3 | TwiL gagne, plus de 2× |
| Formalisation Lean (énoncés de théorèmes → code formel, F1 token) | 64,6 | 63,1 | TwiL gagne de 1,5 point |
| Réponse au format exact | 52,0 | 7,0 | TwiL gagne, 7,4× |
| Étiquetage d'implication (la conclusion découle-t-elle ?) | 68,7 | 77,5 | GPT-OSS-120B gagne |
Quatre vraies victoires, dont une d'un cheveu (formalisation Lean, 1,5 point), et deux énormes (analyse sémantique, réponse au format exact). Tout est auto-déclaré, sur le propre panel de benchmarks de webAI — la réserve habituelle s'applique. Mais les victoires sont précises et orientées plutôt que vagues, et un vendeur qui publie le benchmark qu'il perd adopte le bon comportement, à saluer comme ce blog a salué Prime Intellect pour avoir publié le résultat faible de GLM 5.2 plutôt que de le dissimuler.
Voici la partie qui mérite qu'on s'y attarde. TwiL-LM est présenté explicitement pour « les règles de conformité, les conditions contractuelles, la recherche, et la prise de décision quotidienne » — et l'implication logique est l'opération sous-jacente à ces quatre usages. Une règle de conformité qui s'applique correctement, c'est vérifier qu'un ensemble de faits donné implique une conséquence donnée. Une clause contractuelle qui s'applique, c'est vérifier que les conditions déclenchantes impliquent l'obligation. Ce n'est pas un benchmark parmi cinq pour cet usage-là — c'est sans doute le benchmark. Le modèle conçu pour faire du raisonnement déductif en périphérie perd face au géant sur l'acte même de déduire si quelque chose découle d'autre chose.
Rien de tout cela ne rend la sortie inintéressante — un 96,4 contre 65,2 sur l'induction de règles et un 87,6 contre 43,3 sur l'analyse sémantique sont des écarts réels et importants à 1/40e des paramètres. Cela signifie simplement que le cadrage (« bat un modèle de 120 Md sur 4 benchmarks sur 5 ») et l'aptitude réelle à l'usage revendiqué ne sont pas tout à fait la même affirmation, et qu'il vaut mieux savoir laquelle des deux on évalue avant de déployer ceci pour quoi que ce soit où se tromper sur l'implication a des conséquences.
Ce qu'il y a réellement à l'intérieur
Pour la variante 1,7 Md, webAI divulgue la recette : une base SmolLM2-1,7B plus un adaptateur LoRA de 72 millions de paramètres (289 Mo), entraîné via ce que la publication appelle un « moteur de données de raisonnement propriétaire construit à partir de sources ouvertes » — un adaptateur, pas un fine-tuning complet, qui fait le travail. La précision de raisonnement agrégée passe de 0,185 (SmolLM2-1,7B seul) à 0,361 avec l'adaptateur — environ le double. Sur le test spécifique de LogicBench en réserve, en revanche, le gain est bien plus modeste : de 0,563 à 0,590, soit environ 5%. « Double environ son modèle de base » est vrai en agrégat et nettement plus faible sur au moins une des composantes de cet agrégat.
L'architecture et le modèle de base de TwiL-LM3 lui-même ne sont divulgués nulle part dans la publication — seul le 1,7 Md reçoit une recette documentée. À noter comme une asymétrie plutôt qu'un défaut : c'est le petit modèle, celui ciblant le téléphone, que webAI a choisi de rendre transparent.
Les deux variantes font aussi des arbitrages différents sur le contexte : le modèle 1,7 Md tourne avec une fenêtre de 8 192 tokens, le modèle 3 Md avec environ 65 000. La recommandation de webAI elle-même est d'associer TwiL-LM à un solveur symbolique pour le travail formel à enjeux élevés, précisément à cause du contexte court du petit modèle — une limite énoncée et sensée plutôt qu'une note de bas de page marketing, dans l'esprit des limites énoncées par Pokee-Isaac ou d'Antares qui admet ne faire que du triage.
Les chiffres de la publication ne s'accordent pas tout à fait entre eux
Une affirmation ne résiste pas à une lecture attentive : le modèle 1,7 Md est décrit comme ayant « devancé tous les modèles sub-2 Md évalués par webAI », et la même phrase nomme l'ensemble de comparaison — Phi-4-mini, SmolLM-3B, Qwen2.5-3B, Llama-3.2-3B — comme des « modèles de la classe 3 à 4 milliards de paramètres ». Phi-4-mini à lui seul fait 3,8 Md. Ce n'est pas un ensemble de comparaison sub-2 Md ; c'est une comparaison face à des modèles à peu près deux fois plus gros que TwiL-LM 1,7B, décrits dans la même phrase comme « sub-2 Md ». Soit l'étiquette de catégorie est fausse, soit la liste de modèles l'est, et la publication ne précise pas laquelle — le résultat réel, et toujours respectable, enfoui dessous, est qu'un modèle de 1,7 Md doté d'un adaptateur de 289 Mo est compétitif face à des modèles de 3 à 4 Md, près du double de sa taille, ce qui n'avait pas besoin du cadrage « sub-2 Md » pour mériter d'être rapporté honnêtement.
« Sortie open source » porte beaucoup de poids
Les deux variantes de TwiL-LM sont publiées aujourd'hui sur Hugging Face, aux formats Transformers et llama.cpp — sous la licence webAI Non-Commercial License v1.0. L'annonce qualifie cela de « notre première sortie open source du webAI Intelligence Lab ». Une licence non commerciale n'est pas de l'open source, selon aucune définition que ce blog n'ait utilisée de façon cohérente — ce n'est même pas l'échelon le plus faible de l'échelle à six niveaux que ce blog a cartographiée en juillet, c'est un cran en dessous de toute l'échelle, puisque chaque échelon de celle-ci permet encore un certain usage commercial. Des poids gratuits, téléchargeables et exécutables à des fins personnelles ou de recherche uniquement, c'est une chose réelle et utile à publier. C'est une chose différente de l'open source, et confondre les deux est exactement le geste que ce blog a déjà signalé quand un vendeur veut la bienveillance associée à « ouvert » sans les obligations qui vont avec.
À surveiller ensuite
- Voir si un « TwiL-LM2 » émerge. Le nommage (TwiL-LM 1,7B, TwiL-LM3) laisse entendre une famille avec un échelon intermédiaire manquant, ou un schéma de versionnage pas encore expliqué.
- L'écart sur l'implication est le chiffre à suivre dans les prochaines sorties. Si webAI le comble tout en conservant l'avantage de paramètres, « petit modèle, vrai raisonnement déductif » devient une affirmation véritablement disruptive pour l'outillage de conformité et de legal-tech, plutôt qu'un résultat solide assorti d'un astérisque.
- Attendre une vérification indépendante du panel de raisonnement formel. C'est le propre benchmark de webAI, pas un benchmark tiers — la même réserve que ce blog applique à tout graphique auto-noté, et l'affirmation « 4 sur 5 » mérite les 5 benchmarks de quelqu'un d'autre avant d'être tenue pour acquise.
Références : webAI — sortie de TwiL-LM · TwiL-LM3 — Hugging Face · couverture liée : Ouvert jusqu'où ? Petit guide des licences de modèles d'IA · Les limites énoncées de Pokee-Isaac · Prime Agent et la troisième théorie de la mémoire