Mô hình 4B QED-Nano tiến sát model đóng trong chứng minh toán học khó
Điểm nổi bật
- Quy mô mô hình: nhóm tác giả xây dựng QED-Nano 4B, nhỏ hơn rất nhiều so với nhiều model mở và model đóng đang dẫn đầu ở tác vụ suy luận toán học.
- Pipeline 3 bước: công trình dùng SFT → RL theo rubric → reasoning cache, tức không chỉ fine-tune mà còn tối ưu cách mô hình chia nhỏ và tinh luyện chứng minh.
- So sánh hiệu năng: paper khẳng định QED-Nano vượt một số model mở lớn hơn như Nomos-1 và GPT-OSS-120B ở bài toán proof generation.
- Hàm ý chi phí: nhóm tác giả nhấn mạnh mô hình đạt kết quả ở mức cạnh tranh với chi phí inference thấp hơn đáng kể, tạo ý nghĩa thực tế cho giáo dục, kiểm chứng hình thức và trợ lý toán học.
- Tính mở: tác giả công bố model, dataset FineProofs-SFT/FineProofs-RL, mã huấn luyện và đánh giá, giúp cộng đồng tái lập thay vì chỉ xem benchmark đóng.
Biểu đồ
Tóm tắt
Paper “Teaching a Tiny Model to Prove Hard Theorems” là một tín hiệu đáng chú ý cho hạng mục con người và AI, vì nó chạm trực tiếp vào câu hỏi vốn bị chi phối bởi các công ty frontier: liệu năng lực suy luận khó có bắt buộc phải đi cùng mô hình rất lớn, pipeline kín và chi phí khổng lồ hay không. Nhóm tác giả trả lời bằng một hướng đi ngược: dùng model 4B, nhưng huấn luyện theo pipeline có cấu trúc để cải thiện khả năng viết chứng minh hình thức ở mức cạnh tranh.
Điểm chiến lược không nằm ở việc QED-Nano đã “đánh bại” hoàn toàn các hệ thống độc quyền, mà ở việc paper kéo cuộc thảo luận sang một mặt trận khác: hiệu quả phương pháp. Nếu mô hình nhỏ hơn nhiều nhưng được huấn luyện đúng cách vẫn có thể tiến sát model lớn trong bài toán hẹp nhưng giá trị cao, thì lợi thế của AI tương lai có thể nằm không chỉ ở quy mô compute tuyệt đối, mà ở thiết kế dữ liệu, reward và cơ chế suy luận lặp.
Chi tiết
Từ bản abstract trên arXiv, nhóm tác giả đặt vấn đề rất đúng vào trọng tâm của giai đoạn AI hiện nay. Năm 2025, thị trường chứng kiến các hệ thống độc quyền công bố thành tích ấn tượng ở bài toán chứng minh và toán olympic, nhưng phần lớn pipeline đứng sau vẫn là “hộp đen”: dữ liệu nào được dùng, scaffold nào điều phối, chi phí suy luận ra sao và đâu là phần đóng góp thật của mô hình cốt lõi. Điều đó khiến giới nghiên cứu và người làm ứng dụng khó tái lập, khó kiểm chứng và càng khó tối ưu cho các use case thực tiễn. QED-Nano vì vậy có ý nghĩa như một nỗ lực kéo bài toán reasoning quay lại quỹ đạo khoa học mở.
Công thức huấn luyện mà paper mô tả gồm ba lớp. Thứ nhất là supervised fine-tuning để hấp thụ “proof-writing styles” từ một model mạnh hơn, ở đây là DeepSeek-Math-V2. Đây là bước truyền đạt kỹ năng nền tảng: không chỉ ra đáp án, mà học cách trình bày chứng minh đúng ngữ pháp và logic của miền toán học hình thức. Thứ hai là reinforcement learning với rubric-based rewards. Cách tiếp cận này quan trọng vì nó chuyển đánh giá từ kiểu đúng/sai đơn giản sang một thang đo giàu cấu trúc hơn, phù hợp với bản chất nhiều bước của chứng minh. Thứ ba là reasoning cache, nơi những chứng minh dài được tách thành các chu kỳ summarize-and-refine. Đây là điểm có giá trị lớn, vì nó hàm ý một hướng khác ngoài việc chỉ kéo dài context hoặc tăng tham số: dùng bộ nhớ và vòng lặp suy luận để làm dày chất lượng lập luận.
Nếu tuyên bố của paper đứng vững khi cộng đồng tái lập, tác động sẽ vượt ra ngoài một benchmark toán học. Với giáo dục, một model 4B đủ mạnh mở đường cho công cụ hỗ trợ học sinh, sinh viên hoặc nhà nghiên cứu ở mức chi phí thấp hơn nhiều so với dùng hệ đóng cỡ lớn. Với kỹ nghệ phần mềm và formal verification, đây là tín hiệu rằng các tác vụ cần lập luận hình thức có thể được hỗ trợ bởi stack mở, chạy cục bộ hoặc trên hạ tầng doanh nghiệp nhỏ hơn. Với nghiên cứu AI, paper này tiếp thêm lập luận rằng scaling law không phải con đường duy nhất; kiến trúc huấn luyện, reward design và cơ chế suy luận hậu huấn luyện có thể tạo ra bước nhảy đáng kể.
Tuy nhiên, cần giữ một mức thận trọng. Bản hiện có mới là phiên bản đầu tiên trên arXiv, và phần nội dung mà ta thấy qua abstract chưa đủ để khẳng định toàn bộ mức độ khái quát. QED-Nano có thể rất mạnh ở một tập benchmark proof generation, nhưng chưa chắc chuyển hóa tương ứng sang các miền suy luận mở hơn, kém cấu trúc hơn hoặc giàu mơ hồ hơn. Hơn nữa, “chi phí inference thấp hơn” là tuyên bố có sức hấp dẫn thương mại lớn, song doanh nghiệp vẫn cần nhìn vào tổng chi phí sở hữu: dữ liệu, đánh giá, hạ tầng và năng lực tích hợp. Dù vậy, ngay cả với các giới hạn đó, paper vẫn là một tín hiệu mạnh cho thấy giai đoạn tới của AI reasoning có thể được định hình không chỉ bởi ai có model lớn nhất, mà bởi ai biết thiết kế pipeline huấn luyện hiệu quả nhất.