webAI ra mắt TwIL-LM: Dòng mô hình logic hình thức 1,7 tỷ và 3 tỷ tham số cho tự động hình thức hóa trên phần cứng cục bộ

webAI đã phát hành TwIL-LM, một họ mô hình suy luận logic hình thức gồm hai phiên bản với 1,7 tỷ và 3 tỷ tham số. Phiên bản 3 tỷ tham số, TwIL-LM3, là một mô hình tinh chỉnh hợp nhất từ SmolLM3-3B; phiên bản 1,7 tỷ tham số là một bộ điều hợp PEFT LoRA cho SmolLM2-1.7B-Instruct. Cả hai đều hướng đến mục tiêu tự động hình thức hóa: dịch tiếng Anh sang logic bậc nhất và kiểm tra xem một kết luận có suy ra từ các tiền đề của nó hay không. Cả hai đều chạy cục bộ, với bản dựng lượng tử hóa 1,06 GB cho phiên bản 1,7 tỷ và 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 phát hành này xoay quanh việc đánh bại gpt-oss-120b trên bốn trong năm lĩnh vực suy luận hình thức. Có thể triển khai không? Một phần. Hiện tại chỉ dành cho mục đích phi thương mại. Cả hai điểm kiểm tra đề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 doanh thu yêu cầu một thỏa thuận riêng với webAI. Cấp độ công ty: mọi quy mô. GGUF Q4_K_M 3 tỷ tham số có dung lượng 1,78 GiB và chạy trên CPU hoặc 4 GB VRAM. Phiên bản Q4_K_M 1,7 tỷ tham số có dung lượng 1,06 GB. Các ngành: tuân thủ và RegTech (công nghệ quản lý), dịch vụ tài chính, chăm sóc sức khỏe và dược phẩm, hoạt động pháp lý và hợp đồng, nghiên cứu phương pháp hình thức. webAI định vị việc thực thi cục bộ cho các môi trường mà dữ liệu không thể rời khỏi thiết bị. Ứng dụng: dịch logic bậc nhất (FOL), phân loại suy luận dựa trên tập hợp tiền đề, chuyển đổi ngôn ngữ tự nhiên sang truy vấn có cấu trúc, soạn thảo và phê bình hình thức hóa Lean, và một lớp xác minh kiểm tra đầu ra của mô hình lớn hơn. TwIL-LM3 được xây dựng như thế nào? Bốn giai đoạn được xây dựng trên mô hình cơ sở. Tinh chỉnh có giám sát LoRA trên một kho ngữ liệu logic hình thức tổng hợp. Hợp nhất điểm kiểm tra, tính trung bình các điểm kiểm tra SFT trung gian trong không gian tham số. Nội suy WiSE-FT trở lại mô hình cơ sở đã được huấn luyện trước tại λ = 0,25. Sau đó là MGPO, một giai đoạn GRPO có trọng số entropy chạy với một trình xác minh lập trình. Điểm kiểm tra được công bố là bước 2071. Giá trị λ đó rất quan trọng: chỉ một phần tư delta đã được tinh chỉnh được giữ lại. Một nhánh song song bỏ qua nội suy đã đạt điểm cao hơn trong miền, tại cổng macro 0,515, nhưng đã mất khoảng mười hai điểm khả năng ngoài miền. webAI không công bố nhánh đó. Hiệu suất Thông báo của webAI liệt kê 96,4 về suy luận 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 định dạng chính xác và 68,7 về gán nhãn suy luận. Báo cáo hai đường đua. Trên Đường đua A, logic hình thức trong miền, TwIL-LM3 đạt 0,4488 trên mức trung bình sáu làn và 0,4218 trên cổng macro, chỉ số mà quy trình huấn luyện dựa vào. Nó dẫn đầu mọi nhánh cho đến và bao gồm LFM2.5-8B-A1B trên tất cả sáu làn mục tiêu, với 0,4218 so với 0,3757 với một phần ba số tham số. Nó không dẫn đầu hai nhánh lớn nhất. Qwen3-8B đạt cổng 0,5336 so với 0,4218, nhưng phần lớn là do điểm khớp lỏng lẻo; dưới điều kiện nghiêm ngặt-7, cả hai ở mức 0,2093 và 0,1971. gpt-oss-120b đạt mức trung bình sáu làn 0,5192 so với 0,4488. Hiệu quả là nơi thẻ mô hình rõ ràng. TwIL-LM3 tạo ra các thế hệ ngắn nhất trong số các nhánh, 482 token trên Đường đua B, và do đó có nhiều câu trả lời nhất mỗi giây ở mức 32,9 so với 4,2 của mô hình 120B. Chuyển giao ngoài miền TwIL-LM3 cải thiện trong miền thêm +26% tương đối, cổng macro từ 0,336 lên 0,422, đồng thời tăng thêm +0,022 trên mức trung bình cốt lõi ngoài miền. Thẻ mô hình gọi đây là nhánh duy nhất trong dự án đạt được trên cả hai đường đua. 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.7B là một giao dịch khác. Điểm chính vĩ mô của nó là 0,361 so với 0,185 của phiên bản cơ sở chưa điều chỉnh. Kết quả ngoài phân phối (out-of-distribution) có sự khác biệt: 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 TwIL-LM3 (3B) và TwIL-LM (1.7B) nhắm đến logic hình thức, cả hai đều theo giấy phép phi thương mại. TwIL-LM3 đang được triển khai có hiệu suất thấp hơn gpt-oss-120b trên mức trung bình sáu làn, từ 0,5192 xuống 0,4488. Ưu điểm thực sự của nó là hiệu quả: 32,9 câu trả lời/giây từ các thế hệ 482 token. WiSE-FT với λ = 0,25 là lý do tại sao các cải tiến trong miền không làm giảm hiệu suất trên tập dữ liệu giữ lại (held-out performance). Hãy xem các trọng số mô hình (Model weights) và chi tiết kỹ thuật (Technical details). Ngoài ra, bạn có thể theo dõi chúng tôi trên Twitter và đừng quên tham gia cộng đồng hơn 150 nghìn thành viên ML SubReddit của chúng tôi và đăng ký nhận bản tin (Newsletter). Bạn có dùng Telegram không? Giờ đây 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á kho lưu trữ GitHub HOẶC trang Hugging Face HOẶC phát hành sản phẩm HOẶC hội thảo trực tuyến (Webinar) của bạn? Hãy liên hệ với chúng tôi. Bài viết webAI ra mắt TwIL-LM: Dòng mô hình logic hình thức 1.7B và 3B cho tự động hình thức hóa trên phần cứng cục bộ xuất hiện lần đầu trên MarkTechPost.