webAI prezentuje TwIL-LM: modele logiki formalnej 1.7B i 3B do autoformalizacji

WebAI udostępniła TwIL-LM, rodzinę dwóch modeli specjalizujących się w logice formalnej i autoformalizacji. Mniejsza wersja o rozmiarze 1.7B parametrów to adapter LoRA PEFT dla SmolLM2, a większa 3B to merged fine-tune SmolLM3-3B. Oba modele zostały wytrenowane do tłumaczenia tekstu angielskiego na logikę pierwszego rzędu oraz sprawdzania, czy wniosek wynika z przesłanek - zadania fundamentalne dla systemów wnioskowania formalnego.

Oszczędność zasobów to główna zaleta TwIL-LM. Wersja 1.7B zajmuje zaledwie 1.06 GB w skwantyzowanej formie, a model 3B to 1.78 GB w formacie Q4_K_M GGUF. Oba działają lokalnie na CPU lub z minimalnym VRAM, co otwiera możliwości wdrażania w środowiskach, gdzie dane nie mogą opuszczać urządzenia. WebAI podkreśla, że TwIL-LM3 osiąga lepsze wyniki niż gpt-oss-120b w czterech z pięciu testów formalnego rozumowania, co stanowi znaczący wynik dla tak małych modeli.

Zagodka pozostaje kwestia licencji. Oba modele wydano pod licencją webAI Non-Commercial ver. 1.0, co oznacza, że mogą być używane wyłącznie do celów niekomercyjnych bez dodatkowej umowy. Wdrożenie generujące przychody wymaga osobnego porozumienia z webAI. Aplikacje obejmują tłumaczenie na logikę pierwszego rzędu, klasyfikację wynikania logicznego, formalizację Lean, oraz weryfikację wyników większych modeli - szczególnie cenne dla branż compliance, RegTech, usług finansowych, ochrony zdrowia i operacji prawnych.