webAI a publié TwIL-LM, une famille de deux raisonneurs en logique formelle avec 1,7B et 3B de paramètres conçus pour l'auto-formalisation sur du matériel local. Les modèles traduisent l'anglais en logique du premier ordre et vérifient la validité des conclusions, la variante 3B atteignant un score macro gate de 0,4218 sur des tâches de logique formelle dans le domaine.

  • TwIL-LM3 (3B) est un fine-tuning fusionné de SmolLM3-3B, tandis que le modèle 1,7B est un adaptateur PEFT LoRA pour SmolLM2-1.7B-Instruct.
  • Les deux modèles fonctionnent localement avec des versions quantifiées de 1,06 Go et 1,78 GiB respectivement, nécessitant seulement 4 Go de VRAM.
  • L'entraînement a impliqué un fine-tuning supervisé LoRA, une fusion de checkpoints, une interpolation WiSE-FT à λ = 0,25 et MGPO contre un vérificateur programmatique.
  • TwIL-LM3 devance tous les autres modèles jusqu'à LFM2.5-8B-A1B sur six voies objectives mais est inférieur à gpt-oss-120b sur la moyenne des six voies (0,4488 contre 0,5192).
  • Le modèle 3B produit les générations les plus courtes avec 482 tokens, offrant 32,9 réponses par seconde comparé aux 4,2 de gpt-oss-120b.

La publication permet l'exécution locale pour des environnements sensibles aux données comme la conformité et les opérations juridiques, offrant un équilibre entre performance dans le domaine et conservation des capacités hors domaine.