webAI, Yerel Otomatik Formalizasyon için TwIL-LM Model Ailesini Tanıttı

webAI, 1.7B ve 3B parametre boyutlarında iki modelden oluşan TwIL-LM adlı biçimsel mantık akıl yürütme model ailesini yayınladı. 3B'lik üye TwIL-LM3, SmolLM3-3B'nin birleştirilmiş ince ayarıdır; 1.7B'lik üye ise SmolLM2-1.7B-Instruct için bir PEFT LoRA adaptörüdür. Her iki model de otomatik biçimselleştirmeyi hedefler: İngilizceyi birinci dereceden mantığa çevirmek ve bir sonucun öncüllerinden çıkıp çıkmadığını kontrol etmek. Her ikisi de yerel olarak çalışır; 1.7B için 1.06 GB nicelenmiş derleme ve 3B için 1.78 GiB Q4_K_M GGUF bulunur. webAI'ın duyurusu, sürümü beş biçimsel akıl yürütme kulvarının dördünde gpt-oss-120b'yi geçme etrafında çerçeveliyor. Dağıtım kısmi çünkü her iki kontrol noktası da webAI Ticari Olmayan Lisans sürüm 1.0 altında sunuluyor; gelir getiren dağıtım ayrı bir anlaşma gerektirir. Modeller, uyumluluk ve RegTech, finansal hizmetler, sağlık ve ilaç, hukuk ve sözleşme operasyonları ve biçimsel yöntemler araştırması dahil olmak üzere çeşitli sektörleri hedefler. Uygulamalar arasında birinci dereceden mantık (FOL) çevirisi, gerektirme sınıflandırması, doğal dilden yapılandırılmış sorguya, Lean biçimselleştirme taslağı ve eleştirisi ve bir doğrulayıcı katmanı yer alır. TwIL-LM3 dört aşamayla oluşturuldu: LoRA denetimli ince ayar, kontrol noktası füzyonu, λ = 0.25'te önceden eğitilmiş tabana doğru WiSE-FT interpolasyonu ve programlı bir doğrulayıcıya karşı çalıştırılan entropi ağırlıklı bir GRPO aşaması olan MGPO. Yayınlanan kontrol noktası 2071. adımdır. TwIL-LM3, kural türetmede 96.4, anlamsal ayrıştırmada 87.6, Lean biçimselleştirmede 64.6, tam biçim yanıtlamada 52.0 ve gerektirme etiketlemede 68.7 puan alır. Track A'da altı kulvar ortalamasında 0.4488 ve makro kapıda 0.4218 puan alarak LFM2.5-8B-A1B'ye kadar her kolu önde götürür ancak en büyük iki kolu (Qwen3-8B ve gpt-oss-120b) geçemez. Verimlilik önemli bir avantajdır: TwIL-LM3 en kısa üretimleri (482 jeton) ve saniyede en fazla yanıtı üretir (32.9'a karşı 120B için 4.2). TwIL-LM3, alan içinde göreli olarak %+26 iyileşirken aynı zamanda tutulan çekirdek ortalamada +0.022 kazanç elde eder ve her iki kulvarda da kazanç sağlayan tek koldur. 1.7B model, karışık dağılım dışı sonuçlarla farklı bir denge sunar. Ana çıkarımlar: TwIL-LM3 ve TwIL-LM, ticari olmayan lisans altında biçimsel mantık içindir; TwIL-LM3, altı kulvar ortalamasında gpt-oss-120b'nin gerisindedir; gerçek avantajı verimliliktir; λ=0.25'teki WiSE-FT, alan içi kazanımların tutulan performansı çökertmemesinin nedenidir.