A webAI divulgou o lançamento do TwIL-LM, uma família de dois modelos de raciocínio lógico com 1,7 bilhão e 3 bilhões de parâmetros, voltados à autoformalização: a tradução de linguagem natural para lógica de primeira ordem e a verificação de se uma conclusão decorre das premissas. A empresa afirma que os modelos rodam em hardware local, com versões quantizadas de 1,06 GB para o menor e 1,78 GiB para o maior.
O TwIL-LM3, de 3 bilhões de parâmetros, é um fine-tune mesclado do SmolLM3-3B. Já a versão de 1,7 bilhão, chamada TwIL-LM, usa um adaptador LoRA sobre o SmolLM2-1.7B-Instruct. A webAI distribui os dois checkpoints sob a licença não comercial versão 1.0, e a implantação para gerar receita exige acordo separado com a empresa.
Desempenho
Em avaliações da webAI, o TwIL-LM3 atinge média de 0,4488 em seis pistas de lógica formal e 0,4218 no macro gate, métrica usada para orientar o treinamento. O modelo fica atrás do gpt-oss-120b, que registra 0,5192 na média das seis pistas, e do Qwen3-8B no macro gate, mas produz as respostas mais curtas entre todos os braços avaliados: 482 tokens por resposta, com 32,9 respostas por segundo, ante 4,2 do gpt-oss-120b.
Segundo a webAI, o TwIL-LM3 melhora o desempenho no domínio em 26% e também ganha 0,022 ponto na média de um conjunto de transferência, tornando-se o único braço do projeto a avançar nas duas frentes. No LogicBench, o modelo passa de 0,6467 para 0,7167; no GSM8K, cai de 0,8833 para 0,8733; e no IFEval, recua de 0,6767 para 0,6433. O treinamento usou interpolação WiSE-FT com λ = 0,25, que preserva apenas um quarto do delta do fine-tune; um braço sem essa etapa obteve 0,515 no macro gate, mas perdeu cerca de 12 pontos em capacidade fora do domínio, e a webAI não publicou esse braço.
A versão de 1,7 bilhão eleva a nota macro-primary de 0,185 para 0,361 em relação à base sem adaptação. Nos testes de transferência, o LogicBench BQA sobe de 0,563 para 0,590, enquanto GSM8K cai de 0,413 para 0,380 e ARC-C com cadeia de pensamento cai de 0,587 para 0,463.
Aplicações
A companhia posiciona os modelos para setores como conformidade, serviços financeiros, saúde, operações jurídicas e pesquisa em métodos formais, especialmente em ambientes em que os dados não podem sair do dispositivo. As aplicações incluem tradução para lógica de primeira ordem, classificação de implicação, geração de consultas estruturadas, elaboração e crítica de formalizações em Lean e uma camada verificadora da saída de modelos maiores.
