TwIL-LM od webAI: rodzina małych modeli logiki formalnej, które rywalizują z modelami 120B
W skrócie
- webAI udostępniło rodzinę dwóch modeli TwIL-LM o rozmiarach 1,7B i 3B parametrów, zdolnych do automatycznej formalizacji logicznej i działających lokalnie na zwykłym sprzęcie.
- Model TwIL-LM3 (3B) osiąga wynik 0,4218 na metryce macro gate, przewyższając modele do rozmiaru LFM2.5-8B-A1B przy zaledwie jednej trzeciej ich parametrów.
- Oba modele dostępne są wyłącznie na licencji niekomercyjnej, a wdrożenie w celach zarobkowych wymaga odrębnej umowy z webAI.
Firma webAI opublikowała rodzinę modeli TwIL-LM — dwa wyspecjalizowane systemy do wnioskowania w logice formalnej, liczące odpowiednio 1,7 miliarda i 3 miliardy parametrów marktechpost.com.
Ich głównym zadaniem jest automatyczna formalizacja: przekształcanie zdań w języku naturalnym na logikę pierwszego rzędu oraz weryfikowanie, czy wniosek wynika z podanych przesłanek. Co istotne, oba modele zaprojektowano z myślą o uruchamianiu lokalnie — bez potrzeby dostępu do chmury obliczeniowej marktechpost.com.
Budowa i architektura
Większy z modeli, TwIL-LM3, to dostrojona wersja SmolLM3-3B, natomiast wariant 1,7B stanowi adapter PEFT LoRA dla SmolLM2-1.7B-Instruct marktechpost.com.
Rozmiary skwantyzowanych plików są skromne: 1,06 GB dla wariantu 1,7B oraz 1,78 GiB w formacie Q4_K_M dla modelu 3B, co umożliwia uruchomienie nawet na urządzeniach mobilnych marktechpost.com.
Proces trenowania TwIL-LM3 składał się z czterech etapów marktechpost.com:
- Nadzorowane dostrajanie z użyciem LoRA na syntetycznym zbiorze danych z zakresu logiki formalnej
- Fuzja punktów kontrolnych — uśrednianie pośrednich punktów kontrolnych w przestrzeni parametrów
- Interpolacja WiSE-FT z powrotem w kierunku wstępnie wytrenowanego modelu bazowego przy współczynniku λ = 0,25
- Etap MGPO — ważona entropią odmiana GRPO, uruchamiana względem programowego weryfikatora
Wartość λ = 0,25 jest tu kluczowa: zachowuje jedynie jedną czwartą delty uzyskanej podczas dostrajania. Alternatywna wersja bez tej interpolacji osiągała wyższy wynik w domenie (macro gate 0,515), lecz traciła około dwunastu punktów na danych spoza domeny — webAI zdecydowało się jej nie publikować marktechpost.com.
Wyniki i porównania
Na tle konkurencji TwIL-LM3 wypada przekonująco w swojej klasie rozmiarowej. W ramach Track A (logika formalna w domenie) model osiąga wynik 0,4488 na średniej sześciu kategorii oraz 0,4218 na metryce macro gate marktechpost.com.
Przewyższa wszystkie modele do rozmiaru LFM2.5-8B-A1B — przy zaledwie jednej trzeciej ich parametrów uzyskuje 0,4218 wobec 0,3757 marktechpost.com.
Dwa większe modele pozostają jednak poza jego zasięgiem. Qwen3-8B osiąga macro gate 0,5336 wobec 0,4218 TwIL-LM3, choć webAI zaznacza, że większość tej przewagi pochodzi z punktacji za częściowe dopasowania — przy rygorystycznej metryce strict-7 różnica zaciera się (0,2093 wobec 0,1971) marktechpost.com.
Model gpt-oss-120B z kolei prowadzi na średniej sześciu kategorii wynikiem 0,5192 do 0,4488 marktechpost.com.
Szczegółowe wyniki TwIL-LM3 w poszczególnych kategoriach prezentują się następująco marktechpost.com:
- Indukcja reguł: 96,4
- Parsowanie semantyczne: 87,6
- Formalizacja w Lean: 64,6
- Odpowiedzi w ścisłym formacie: 52,0
- Etykietowanie wynikania: 68,7
Wyraźną przewagą modelu jest efektywność obliczeniowa. TwIL-LM3 generuje najkrótsze odpowiedzi spośród wszystkich testowanych modeli — średnio 482 tokeny na Track B — i osiąga przepustowość 32,9 odpowiedzi na sekundę, podczas gdy model 120B uzyskuje jedynie 4,2 marktechpost.com.
Transfer wiedzy poza domenę
Interesującym wynikiem jest zachowanie modelu poza domeną trenowania. TwIL-LM3 poprawia wynik w domenie o +26% względnie (macro gate z 0,336 do 0,422), jednocześnie zyskując +0,022 na średniej dla danych spoza domeny — webAI opisuje go jako jedyny model w projekcie, który poprawia wyniki na obu ścieżkach jednocześnie marktechpost.com.
Wynik na LogicBench wzrósł z 0,6467 do 0,7167. Nieznacznie pogorszyły się natomiast GSM8K (z 0,8833 do 0,8733) oraz IFEval (z 0,6767 do 0,6433) marktechpost.com.
Wariant 1,7B prezentuje inny profil kompromisów: macro-primary score wynosi 0,361 wobec 0,185 dla nieadaptowanego modelu bazowego, jednak wyniki poza domeną są niejednoznaczne — LogicBench BQA poprawia się z 0,563 do 0,590, natomiast GSM8K spada z 0,413 do 0,380, a ARC-C z łańcuchem myślenia — z 0,587 do 0,463 marktechpost.com.
Licencja i dostępność
Oba modele opublikowano na platformie Hugging Face pod licencją webAI Non-Commercial License ver. 1.0, która wyklucza zastosowania komercyjne. Wdrożenie generujące przychody wymaga zawarcia odrębnej umowy z webAI marktechpost.com.
Co to oznacza
Publikacja TwIL-LM wpisuje się w rosnący trend tworzenia wyspecjalizowanych, małych modeli językowych zdolnych do działania lokalnie — bez zależności od infrastruktury chmurowej. Dla polskich organizacji i deweloperów oznacza to realną możliwość wdrożenia narzędzi do wnioskowania logicznego na własnym sprzęcie, z zachowaniem pełnej kontroli nad danymi i bez kosztów API.
Szczególnie istotny jest kontekst efektywności: model o 3 miliardach parametrów, mieszczący się w pliku poniżej 2 GB, osiąga przepustowość prawie ośmiokrotnie wyższą niż model 120-miliardowy. Dla zastosowań wymagających szybkiego przetwarzania dużej liczby zapytań logicznych — np. w systemach weryfikacji faktów, automatycznej analizie dokumentów prawnych czy asystentach do nauki matematyki — taka różnica w szybkości może być decydująca.
Ograniczenie licencji do zastosowań niekomercyjnych to jednak istotna bariera dla firm chcących wdrożyć TwIL-LM w produktach. Konieczność negocjowania odrębnej umowy z webAI wprowadza niepewność prawną i operacyjną, która może skłonić część deweloperów do sięgnięcia po alternatywy z bardziej otwartymi licencjami — takie jak sam Qwen3-8B, który w testach osiąga wyższe wyniki absolutne. Wybór między TwIL-LM a większymi modelami otwartymi sprowadza się więc do konkretnego przypadku użycia: tam, gdzie liczy się szybkość i praca offline, mały model webAI ma realne argumenty; tam, gdzie priorytetem jest maksymalna dokładność lub swoboda komercyjna — przewaga jest po stronie konkurencji.
Szerszy kontekst
TwiL-LM3, model 3B, pokonuje gpt-oss-120b, model 40 razy większy, w czterech z pięciu benchmarków w pakiecie testów rozumowania formalnego webAI.
Wydajność TwiL-LM nie wymagała trenowania od zera. Zamiast tego jego mały, ukierunkowany etap dostrajania pochodził z adaptera LoRA o wielkości 289 MB i około 72 milionach parametrów, wytrenowanego na celowo zaprojektowanym, zastrzeżonym silniku danych z logiki formalnej, zbudowanym z otwartych źródeł.
Porównanie z modelem 120B nie jest jedynie historią o rozmiarze; to dowód, że ograniczone, ustrukturyzowane rozumowanie może przewyższać brutalne skalowanie w określonych klasach zadań.
Analiza
Najważniejszy wniosek jest taki, że webAI nie próbuje konkurować skalą, tylko wąskim wyspecjalizowaniem. Firma przedstawia TwiL-LM jako przeciwwagę dla kierunku wyznaczanego przez laboratoria graniczne, które budują coraz większe modele serwowane z centrów danych. Według komunikatu prasowego TwiL-LM3 „pokonuje gpt-oss-120b, model czterdziestokrotnie większy, w czterech z pięciu testów w pakiecie formalnego rozumowania webAI” (wg prnewswire.com). Warto jednak pamiętać, że to wynik w zestawie testów autorstwa samej firmy, a nie w ogólnych benchmarkach. Komentujący na LinkedIn zwracają uwagę, że porównanie dotyczy konkretnych zadań, a nie ogólnych zdolności AI (wg linkedin.com). Różnica między „lepszy w logice formalnej” a „lepszy” jest tu zasadnicza.
Drugi wątek to tryb wdrożenia. Model TwiL-LM3 ma być na tyle mały, by działać lokalnie, a według komunikatu webAI może zostać pobrany na telefon i zajmuje około jednego gigabajta (wg webai.com; wg prnewswire.com). Jego dostrojenie opiera się na adapterze LoRA o wielkości 289 MB i około 72 milionach parametrów, bez trenowania od zera (wg prnewswire.com). Z tego punktu widzenia ciekawsza od samego wyniku jest sama architektura: wąski adapter na istniejącym modelu bazowym, a nie osobny, pełny model. Dla przedsiębiorstw, które chcą mieć kontrolę nad danymi i nie płacić za API, taki wzorzec może być tańszy i prostszy do utrzymania niż wdrażanie dużych modeli.
Najwięcej napięcia wiąże się z licencją. Materiały prasowe opisują model jako otwarty (wg linkedin.com), a artykuł wskazuje, że licencja webAI Non-Commercial wyklucza zastosowania komercyjne. Dla firm, które miały wdrażać model w produktach, ta różnica jest zasadnicza. W praktyce oznacza to, że mały model ma przewagę techniczną w zadaniach wymagających szybkości i pracy offline, ale jego przydatność biznesowa zależy od negocjacji z webAI. Dopóki ten warunek nie zostanie wyjaśniony, konkurencyjne modele o bardziej przejrzystych licencjach pozostaną realną alternatywą.