OpenBMB đã mở mã nguồn toàn bộ hệ thống MathForm dùng để hình thức hóa toán học tự động: trọng số mô hình 8B, bộ dữ liệu khoảng 367.000 mẫu Lean 4 đã được xác minh, mã đánh giá và các script Pass@k. Mô hình được đăng trên Hugging Face, cấp phép Apache 2.0, xây dựng trên nền Qwen3-8B, trọng số ở độ chính xác BF16. Dự án do đội ngũ OpenBMB thực hiện, với sự hỗ trợ của Phòng thí nghiệm Xử lý Ngôn ngữ Tự nhiên Đại học Thanh Hoa và ModelBest; bài báo cùng tên với 10 tác giả đã được nộp lên arXiv vào giữa tháng này.
Hình thức hóa tự động là việc dịch các mệnh đề toán học viết bằng ngôn ngữ tự nhiên sang ngôn ngữ hình thức mà máy có thể kiểm chứng như Lean 4. Khó khăn không nằm ở việc dịch từng chữ. Hệ thống phân cấp kiểu và bộ định nghĩa của Mathlib cực kỳ đồ sộ: các khái niệm như "hàm liên tục", "nhóm hữu hạn" trong một mệnh đề phải khớp chính xác với đúng định nghĩa tương ứng trong thư viện, đồng thời mệnh đề sau khi hình thức hóa vẫn phải nói đúng điều mà mệnh đề gốc nói. Chỉ cần lệch một trong hai điểm đó, trình biên dịch vẫn có thể gật đầu thông qua như thường.
Dữ liệu được tạo ra như thế nào
Quy trình của MathForm gồm bốn bước. Đầu tiên bộ lập kế hoạch tra cứu Mathlib theo các khái niệm toán học có trong mệnh đề, công cụ truy xuất LeanExplore mỗi lần trả về 22 kết quả hàng đầu; mô hình sau đó sinh ra mệnh đề Lean 4 dựa trên ngữ cảnh truy xuất này. Các ứng viên lần lượt qua kiểm tra định dạng, kiểm tra biên dịch, rồi được một mô hình lớn đóng vai giám khảo đánh giá tính nhất quán ngữ nghĩa. Những đường đi thành công được tái cấu trúc ngược lại thành các quỹ đạo huấn luyện sạch.
Một con số trong bài báo cho thấy vì sao việc lặp lại là cần thiết: các vòng sau đóng góp thêm 31,0% mẫu được giữ lại tính trên tổng số mẫu cuối cùng. Nói cách khác, nếu chỉ sinh một lượt duy nhất rồi loại bỏ những mẫu không đạt, gần một phần ba lượng dữ liệu khả dụng sẽ bị mất trắng.
Bước truy xuất là thiết kế tiết kiệm nhất trong toàn bộ hệ thống. Bắt mô hình nhớ chính xác tên và chữ ký của một định nghĩa trong Mathlib từ trí nhớ, về bản chất là kiểm tra xem nó có thuộc lòng một thư viện vẫn đang liên tục cập nhật hay không. Khi giao thư viện cho công cụ truy xuất và chỉ để mô hình chịu trách nhiệm lắp ráp kết quả, lượng tham số cần thiết tự nhiên giảm xuống. Điều này cũng giải thích vì sao một mô hình 8B có thể đọ sức với mô hình 32B: hai bên vốn không giải cùng một bài toán.
Bộ dữ liệu tạo ra có tên FormalVerse, khoảng 367.000 mẫu đã xác minh, lấy từ DeepTheorem, NuminaMath, AceReason-Math, Lean Workbook, Principia-Collection, DeepMath, OpenR1-Math, bổ sung thêm nội dung từ các giáo trình kinh điển. Bộ dữ liệu này đã nhận được 358 lượt thích trên Hugging Face.
Bảng thành tích và hai thước đo của nó
Đường huấn luyện là tinh chỉnh có giám sát rồi tiếp đến học tăng cường. Đánh giá trải rộng trên sáu benchmark: FormalMATH-Lite và DeepSeek-ProverBench về toán thi đấu, CombiBench kiểm tra tổ hợp, còn dòng FATE chia theo độ khó đại số thành ba mức M, H, X.
MathForm-8B đạt Pass@8 trung bình cho kiểm tra cú pháp là 88,06%, kiểm tra nhất quán là 72,37%; tỷ lệ nhất quán ở ba mức của FATE lần lượt là 97,33%, 63,00% và 37,00%. Nhóm đối chứng gồm Herald Translator-7B, Kimina-Autoformalizer-7B, Mathesis-HPO-7B, cùng các phiên bản 7B/8B và 32B của StepFun-Formalizer, Goedel-Formalizer-V2 và ReForm. Mô hình 8B vượt qua các mô hình hình thức hóa chuyên dụng 32B trên nhiều bộ kiểm tra.
Khoảng cách giữa hai thước đo này nói lên nhiều điều hơn là điểm số tuyệt đối. Kiểm tra cú pháp chỉ hỏi mã có biên dịch được không; kiểm tra nhất quán hỏi mệnh đề sau hình thức hóa có còn cùng nghĩa với đề gốc hay không — 88% so với 72%, khoảng chênh hơn chục điểm phần trăm đó chính là nút thắt cổ chai thực sự của quy trình hiện nay. Thứ biên dịch được chưa chắc đã là định lý mà người ta muốn chứng minh.
Ngưỡng phần cứng hạ xuống mức một trạm làm việc
Trang này mới đây từng viết về lời cảnh báo của Terence Tao rằng các chứng minh do AI tạo ra sẽ nhiều đến mức không ai đọc hết nổi. Hình thức hóa chính là nửa còn lại của câu trả lời cho vấn đề đó — chỉ cần chứng minh qua được trình biên dịch Lean, việc đọc hiểu nó không còn là điều kiện để chấp nhận nữa. Nhưng điều kiện vẫn còn đó là mệnh đề gốc phải được dịch đúng, và con số 37% trên FATE-X cho thấy vẫn còn một khoảng cách khá xa để đạt được điều đó.
Tính sơ bộ, một mô hình 8B nạp ở BF16 cần khoảng 16GB VRAM, còn mô hình 32B cùng độ chính xác cần khoảng 64GB. Mô hình đầu chạy được trên một card đồ họa phổ thông 24GB, mô hình sau cần nhiều card hoặc card chuyên dụng. Với các khoa toán ở trường đại học, cộng đồng trợ lý chứng minh và các nhóm nhỏ, ngưỡng phần cứng để chạy một quy trình hình thức hóa nhờ vậy hạ từ cấp cụm máy chủ xuống cấp một máy đơn. Bộ dữ liệu và mã đánh giá được mở cùng lúc cũng làm giảm chi phí để người khác tái lập và kiểm chứng.
Danh sách các mô hình đối chứng cũng cho thấy sân chơi này hiện đông đúc đến mức nào: Herald, Kimina, Mathesis, StepFun-Formalizer, Goedel-Formalizer-V2, ReForm, toàn là các mô hình hình thức hóa chuyên dụng xuất hiện trong một hai năm gần đây, và đều mã nguồn mở. Hình thức hóa không giống hội thoại tổng quát vốn dựa vào việc đốt sức tính toán để tạo khoảng cách, mà cạnh tranh bằng kỹ thuật xây dựng dữ liệu và vòng lặp xác minh; quy mô tham số ở đây lại trở thành biến số phụ. Một quy trình đi từ minh họa trong bài báo đến mức có thể mở mã nguồn giao hàng được, với nhịp độ này, nhanh hơn phần lớn người ta hình dung.
Nguồn tham khảo: kho dự án và model card của OpenBMB, CocoLoop, bản in trước arXiv 2608.14221, trang bộ dữ liệu trên Hugging Face; đã kiểm chứng quy mô tham số, giấy phép, số lượng mẫu FormalVerse và các số liệu Pass@8 của từng bộ kiểm tra.