webAI ra mắt TwIL-LM: Dòng mô hình logic hình thức để tự động hình thức hóa cục bộ

webAI đã phát hành TwIL-LM, một nhóm gồm hai mô hình suy luận logic hình thức với 1,7B và 3B tham số. Thành viên 3B, TwIL-LM3, là một bản tinh chỉnh hợp nhất của SmolLM3-3B; thành viên 1,7B là một adapter LoRA PEFT cho SmolLM2-1.7B-Instruct. Cả hai đều hướng đến mục tiêu tự động hóa hình thức: dịch tiếng Anh sang logic bậc nhất và kiểm tra xem một kết luận có được suy ra từ các tiền đề hay không. Cả hai đều chạy cục bộ, với bản lượng tử hóa 1,06 GB cho mô hình 1,7B và GGUF Q4_K_M 1,78 GiB cho mô hình 3B. Thông báo của webAI nhấn mạnh việc phát hành xoay quanh việc đánh bại gpt-oss-120b trên bốn trong năm hạng mục suy luận hình thức. Việc triển khai là một phần, vì cả hai checkpoint được phát hành theo Giấy phép Phi thương mại webAI phiên bản 1.0; triển khai tạo doanh thu yêu cầu một thỏa thuận riêng. Các mô hình nhắm đến nhiều ngành công nghiệp khác nhau bao gồm tuân thủ và RegTech, dịch vụ tài chính, chăm sóc sức khỏe và dược phẩm, vận hành pháp lý và hợp đồng, và nghiên cứu phương pháp hình thức. Các ứng dụng bao gồm dịch logic bậc nhất (FOL), phân loại hệ quả logic, truy vấn có cấu trúc từ ngôn ngữ tự nhiên, soạn thảo và phê bình hình thức hóa Lean, và một lớp xác minh. TwIL-LM3 được xây dựng qua bốn giai đoạn: tinh chỉnh có giám sát LoRA, hợp nhất checkpoint, nội suy WiSE-FT trở lại cơ sở được tiền huấn luyện với λ = 0.25, và MGPO, một giai đoạn GRPO có trọng số entropy chạy với một bộ xác minh theo chương trình. Checkpoint được công bố là bước 2071. TwIL-LM3 đạt 96,4 điểm về quy nạp quy tắc, 87,6 về phân tích cú pháp 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 hệ quả logic. Trên Track A, nó đạt 0,4488 về trung bình sáu hạng mục và 0,4218 về cổng vĩ mô, dẫn đầu mọi nhánh lên đến LFM2.5-8B-A1B nhưng không vượt qua hai nhánh lớn nhất (Qwen3-8B và gpt-oss-120b). Hiệu quả là một lợi thế chính: TwIL-LM3 tạo ra các câu trả lời ngắn nhất (482 token) và nhiều câu trả lời mỗi giây nhất (32,9 so với 4,2 đối với mô hình 120B). TwIL-LM3 cải thiện trong miền +26% tương đối trong khi cũng tăng +0,022 về trung bình lõi giữ lại, là nhánh duy nhất tăng ở cả hai track. Mô hình 1,7B cung cấp một sự đánh đổi khác với kết quả phân phối ngoài miền hỗn hợp. Điểm chính: TwIL-LM3 và TwIL-LM dành cho logic hình thức dưới giấy phép phi thương mại; TwIL-LM3 xếp sau gpt-oss-120b về trung bình sáu hạng mục; lợi thế thực sự của nó là hiệu quả; WiSE-FT với λ=0.25 là lý do tại sao các lợi ích trong miền không làm sụp đổ hiệu suất giữ lại.