webAI ra mắt TwIL-LM: Dòng mô hình logic hình thức 1.7B và 3B chạy mượt trên thiết bị cá nhân

webAI vừa phát hành TwIL-LM, một dòng mô hình gồm hai phiên bản chuyên về suy luận logic hình thức với quy mô 1,7 tỷ và 3 tỷ tham số. Phiên bản 3 tỷ tham số, TwIL-LM3, là kết quả tinh chỉnh hợp nhất (merged fine-tune) từ SmolLM3-3B; phiên bản 1,7 tỷ tham số là một adapter PEFT LoRA dành cho SmolLM2-1.7B-Instruct. Cả hai đều hướng tới mục tiêu tự động hóa hình thức (autoformalization): dịch tiếng Anh sang logic bậc nhất và kiểm tra xem một kết luận có được rút ra từ các tiền đề hay không. Cả hai đều có thể chạy cục bộ, với bản dựng định lượng (quantized build) 1,06 GB cho phiên bản 1,7 tỷ và tệp GGUF Q4_K_M 1,78 GiB cho phiên bản 3 tỷ. Thông báo của webAI nhấn mạnh việc vượt qua gpt-oss-120b trên bốn trong số năm lĩnh vực suy luận hình thức.

Liệu mô hình có thể triển khai được không?

Một phần. Hiện tại chỉ dành cho mục đích phi thương mại.

Cả hai checkpoint đều được phát hành theo Giấy phép Phi thương mại webAI phiên bản 1.0. Việc triển khai tạo ra doanh thu yêu cầu một thỏa thuận riêng với webAI.

TwIL-LM3 được xây dựng như thế nào?

Có bốn giai đoạn được thực hiện trên mô hình cơ sở. Tinh chỉnh có giám sát (SFT) bằng LoRA trên tập dữ liệu logic hình thức tổng hợp. Hợp nhất checkpoint (Checkpoint fusion), lấy trung bình các checkpoint SFT trung gian trong không gian tham số. Nội suy WiSE-FT quay trở lại mô hình cơ sở đã được huấn luyện trước với λ = 0,25. Sau đó là MGPO, một giai đoạn GRPO có trọng số entropy được chạy đối chiếu với một trình xác minh theo chương trình. Checkpoint được công bố là bước 2071.

Giá trị λ đó đóng vai trò then chốt: chỉ một phần tư độ lệch (delta) sau tinh chỉnh được giữ lại. Một nhánh phụ bỏ qua bước nội suy đạt điểm cao hơn trong miền (in-domain) với macro gate là 0,515, nhưng lại mất đi khoảng 12 điểm về khả năng suy rộng (held-out capability). webAI đã không công bố nhánh đó.

Hiệu suất

Thông báo của webAI liệt kê điểm số 96,4 về quy nạp quy tắc, 87,6 về phân tích ngữ nghĩa, 64,6 về hình thức hóa Lean, 52,0 về trả lời theo định dạng chính xác và 68,7 về dán nhãn kéo theo (entailment labeling).

Báo cáo đưa ra hai lộ trình. Ở Lộ trình A (logic hình thức trong miền), TwIL-LM3 đạt điểm trung bình 0,4488 trên sáu lĩnh vực và 0,4218 trên macro gate – chỉ số mà quy trình huấn luyện dựa vào để kiểm soát. Nó dẫn trước mọi nhánh cho đến và bao gồm cả LFM2.5-8B-A1B trên cả sáu lĩnh vực mục tiêu, với tỷ số 0,4218 so với 0,3757 dù chỉ bằng một phần ba số tham số. Nó không dẫn trước hai nhánh lớn nhất. Qwen3-8B đạt macro gate 0,5336 so với 0,4218 của TwIL-LM3, nhưng phần lớn là nhờ điểm khớp lỏng (loose-match); theo tiêu chuẩn strict-7, cả hai đạt lần lượt 0,2093 và 0,1971. gpt-oss-120b dẫn trước với điểm trung bình sáu lĩnh vực là 0,5192 so với 0,4488.

Hiệu quả là điểm mà thẻ mô hình (model card) thể hiện rõ ràng nhất. TwIL-LM3 tạo ra các thế hệ văn bản ngắn nhất trong tất cả các nhánh, 482 token trên Lộ trình B, và nhờ đó đạt số câu trả lời mỗi giây cao nhất với 32,9 so với 4,2 của mô hình 120B.

Khả năng chuyển đổi (Held-out transfer)

TwIL-LM3 cải thiện hiệu suất trong miền thêm +26% tương đối, macro gate từ 0,336 lên 0,422, đồng thời tăng +0,022 trên điểm trung bình cốt lõi (held-out core average). Thẻ mô hình gọi đây là nhánh duy nhất trong dự án đạt được sự cải thiện trên cả hai lộ trình. LogicBench tăng từ 0,6467 lên 0,7167. GSM8K giảm nhẹ từ 0,8833 xuống 0,8733 và IFEval giảm từ 0,6767 xuống 0,6433.

Phiên bản 1,7 tỷ tham số là một sự đánh đổi khác. Điểm macro-primary của nó là 0,361 so với 0,185 của mô hình cơ sở chưa tinh chỉnh. Kết quả ngoài phân phối (out-of-distribution) khá hỗn hợp: LogicBench BQA cải thiện từ 0,563 lên 0,590, trong khi GSM8K giảm từ 0,413 xuống 0,380 và ARC-C chain-of-thought giảm từ 0,587 xuống 0,463.

Những điểm chính cần lưu ý

Hãy xem Trọng số mô hình và Chi tiết kỹ thuật. Ngoài ra, đừng ngần ngại theo dõi chúng tôi trên Twitter, tham gia cộng đồng ML SubReddit với hơn 150 nghìn thành viên và đăng ký nhận Bản tin của chúng tôi. Khoan đã! Bạn có dùng Telegram không? Bây giờ bạn cũng có thể tham gia cùng chúng tôi trên Telegram.

Cần hợp tác với chúng tôi để quảng bá GitHub Repo, Trang Hugging Face, Sản phẩm mới hoặc Hội thảo trực tuyến của bạn? Hãy kết nối với chúng tôi.

Michal Sutter là một chuyên gia khoa học dữ liệu với bằng Thạc sĩ Khoa học Dữ liệu từ Đại học Padova. Với nền tảng vững chắc về phân tích thống kê, học máy và kỹ thuật dữ liệu, Michal xuất sắc trong việc chuyển đổi các tập dữ liệu phức tạp thành những thông tin chi tiết có giá trị thực tiễn.