webAI prezentuje TwIL-LM: Nowa rodzina modeli logiki formalnej do autoformalizacji

Firma webAI zaprezentowała TwIL-LM, rodzinę dwóch modeli do rozumowania w logice formalnej, o parametrach 1.7 miliarda i 3 miliardów. Modele te, przeznaczone do autoformalizacji, czyli tłumaczenia języka angielskiego na logikę pierwszego rzędu oraz weryfikacji wniosków, działają lokalnie. Wersja 1.7B dostępna jest w skwantyzowanej kompilacji o rozmiarze 1.06 GB, natomiast wersja 3B jako plik GGUF Q4_K_M o rozmiarze 1.78 GiB. webAI podkreśla, że ich nowe modele przewyższają gpt-oss-120b w czterech z pięciu zadań rozumowania formalnego.

Architektura i licencjonowanie TwIL-LM

Model TwIL-LM3 (3B parametrów) powstał poprzez scalenie i dostrojenie modelu SmolLM3-3B, natomiast wersja 1.7B to adapter PEFT LoRA dla SmolLM2-1.7B-Instruct. Oba modele są obecnie dostępne wyłącznie do użytku niekomercyjnego, zgodnie z licencją webAI Non-Commercial License ver. 1.0. Wdrożenie generujące przychody wymaga odrębnej umowy z webAI.

Proces tworzenia modeli obejmował cztery etapy. Na początku zastosowano nadzorowane dostrajanie LoRA na syntetycznym korpusie logiki formalnej. Następnie przeprowadzono fuzję punktów kontrolnych, uśredniając pośrednie punkty SFT w przestrzeni parametrów. Kolejnym krokiem była interpolacja WiSE-FT w kierunku wstępnie wytrenowanej bazy z parametrem λ = 0.25. Ostatnim etapem był MGPO, czyli etap GRPO ważony entropią, uruchomiony w oparciu o programowy weryfikator. Opublikowany punkt kontrolny to krok 2071.

Warto zaznaczyć, że parametr λ = 0.25 jest kluczowy – oznacza to, że zachowano tylko jedną czwartą dostrojonej delty. Alternatywna wersja, która pominęła interpolację, osiągnęła wyższe wyniki w domenie (makrobramka 0.515), ale straciła około dwunastu punktów zdolności na danych odłożonych. webAI nie opublikowało tej wersji.

Wyniki wydajności i porównania

webAI podaje imponujące wyniki dla swoich modeli. Na przykład, w indukcji reguł osiągnięto 96.4%, w analizie semantycznej 87.6%, w formalizacji Lean 64.6%, w odpowiadaniu w dokładnym formacie 52.0%, a w etykietowaniu implikacji 68.7%.

W teście Track A, dotyczącym logiki formalnej w domenie, TwIL-LM3 uzyskał średni wynik 0.4488 na sześciu torach oraz 0.4218 na makrobramce, która jest kluczową metryką w procesie treningowym. Model ten przewyższa wszystkie konkurencyjne rozwiązania, w tym LFM2.5-8B-A1B, na wszystkich sześciu torach, osiągając 0.4218 w porównaniu do 0.3757, przy czym TwIL-LM3 ma jedną trzecią parametrów. Nie przewodzi jednak dwóm największym modelom: Qwen3-8B osiąga 0.5336 na makrobramce (głównie dzięki luźnemu dopasowaniu), podczas gdy w ścisłym dopasowaniu (strict-7) oba modele uzyskują odpowiednio 0.2093 i 0.1971. gpt-oss-120b osiąga średnią sześciotorową 0.5192 w porównaniu do 0.4488 TwIL-LM3.

Model TwIL-LM3 wyróżnia się również efektywnością. Generuje najkrótsze odpowiedzi spośród wszystkich testowanych modeli (482 tokeny na Track B), co przekłada się na największą liczbę odpowiedzi na sekundę – 32.9 w porównaniu do 4.2 dla modelu 120B.

Wpływ na różne metryki i wersja 1.7B

TwIL-LM3 odnotowuje 26% względny wzrost w domenie (makrobramka z 0.336 do 0.422), jednocześnie zyskując +0.022 na średniej danych odłożonych. Karta modelu określa go jako jedyny projekt, który zyskał na obu torach. Wyniki na LogicBench poprawiły się z 0.6467 do 0.7167. Odnotowano jednak niewielkie spadki na GSM8K (z 0.8833 do 0.8733) oraz IFEval (z 0.6767 do 0.6433).

Wersja 1.7B modelu prezentuje inne kompromisy. Jej wynik makro-podstawowy wynosi 0.361 w porównaniu do 0.185 dla nieprzystosowanej bazy. Wyniki poza dystrybucją są mieszane: LogicBench BQA poprawia się z 0.563 do 0.590, podczas gdy GSM8K spada z 0.413 do 0.380, a ARC-C chain-of-thought z 0.587 do 0.463.

Premiera TwIL-LM przez webAI stanowi znaczący krok w rozwoju modeli AI zdolnych do rozumowania formalnego, szczególnie w kontekście ich zdolności do działania na lokalnym sprzęcie. Wysoka efektywność i konkurencyjne wyniki, zwłaszcza w stosunku do znacznie większych modeli, wskazują na potencjał tych rozwiązań w zadaniach wymagających precyzyjnej logiki i autoformalizacji, otwierając nowe możliwości dla zastosowań AI w dziedzinach takich jak weryfikacja oprogramowania czy automatyczne dowodzenie twierdzeń.

Źródło: marktechpost.com