webAI anunció el lanzamiento de TwIL-LM, una familia de dos modelos de razonamiento lógico con 1,7 mil millones y 3 mil millones de parámetros, orientados a la autoformalización: la traducción de lenguaje natural a lógica de primer orden y la verificación de si una conclusión se deduce de las premisas. La empresa afirma que los modelos se ejecutan en hardware local, con versiones cuantizadas de 1,06 GB para el más pequeño y 1,78 GiB para el más grande.
TwIL-LM3, de 3 mil millones de parámetros, es un fine-tune fusionado de SmolLM3-3B. La versión de 1,7 mil millones, llamada TwIL-LM, usa un adaptador LoRA sobre SmolLM2-1.7B-Instruct. webAI distribuye los dos checkpoints bajo la licencia no comercial versión 1.0, y la implementación para generar ingresos requiere un acuerdo separado con la empresa.
Desempeño
En las evaluaciones de webAI, TwIL-LM3 alcanza un promedio de 0,4488 en seis pistas de lógica formal y 0,4218 en el macro gate, métrica utilizada para orientar el entrenamiento. El modelo queda por detrás de gpt-oss-120b, que registra 0,5192 en el promedio de las seis pistas, y de Qwen3-8B en el macro gate, pero produce las respuestas más cortas entre todos los brazos evaluados: 482 tokens por respuesta, con 32,9 respuestas por segundo, frente a 4,2 de gpt-oss-120b.
Según webAI, TwIL-LM3 mejora el desempeño en el dominio en un 26% y también gana 0,022 puntos en el promedio de un conjunto de transferencia, convirtiéndose en el único brazo del proyecto en avanzar en ambos frentes. En LogicBench, el modelo pasa de 0,6467 a 0,7167; en GSM8K, cae de 0,8833 a 0,8733; y en IFEval, retrocede de 0,6767 a 0,6433. El entrenamiento usó interpolación WiSE-FT con λ = 0,25, que preserva solo una cuarta parte del delta del fine-tune; un brazo sin esta etapa obtuvo 0,515 en el macro gate, pero perdió unos 12 puntos en capacidad fuera del dominio, y webAI no publicó ese brazo.
La versión de 1,7 mil millones eleva la nota macro-primary de 0,185 a 0,361 en comparación con la base sin adaptación. En las pruebas de transferencia, LogicBench BQA sube de 0,563 a 0,590, mientras que GSM8K cae de 0,413 a 0,380 y ARC-C con cadena de pensamiento cae de 0,587 a 0,463.
Aplicaciones
La empresa posiciona los modelos para sectores como cumplimiento, servicios financieros, salud, operaciones jurídicas e investigación en métodos formales, especialmente en entornos donde los datos no pueden salir del dispositivo. Las aplicaciones incluyen traducción a lógica de primer orden, clasificación de implicación, generación de consultas estructuradas, elaboración y crítica de formalizaciones en Lean y una capa verificadora de la salida de modelos más grandes.
