Đừng cho model mới làm thủ khoa

Đừng cho model mới làm thủ khoa

Leanstral 1.5 đáng chú ý, nhưng không phải vì benchmark đẹp. Câu hỏi thật là team bạn có cần một lớp kiểm chứng riêng cho code rủi ro cao không.

Một bạn tech lead nhắn mình lúc gần nửa đêm: team đang phân vân có nên kéo ngay Leanstral 1.5 vào pipeline không, vì model này vừa ghi điểm rất mạnh trên formal math benchmark, lại còn bắt được bug thật trong repo open-source.

Mình đọc xong thì phản xạ đầu tiên không phải là: dùng ngay đi. Phản xạ đầu tiên là: đừng cho nó làm thủ khoa của cả lớp chỉ vì bảng điểm môn toán đẹp.

Leanstral 1.5 của Mistral là một tín hiệu đáng chú ý: open-source, Apache 2.0, tập trung vào Lean 4, tức ngôn ngữ dùng để kiểm chứng hình thức cho chứng minh toán và tính đúng đắn phần mềm. Nhưng quyết định hay cho builder không nằm ở chuyện nó có mới không. Quyết định nằm ở việc bạn có bài toán nào đủ nghiêm túc để cần một lớp kiểm chứng riêng hay không.

Sơ đồ minh họa cho bài Đừng cho model mới làm thủ khoa

Sơ đồ tóm tắt ý chính của bài viết.

Thứ đang diễn ra: model đang tách chuyên ngành

Trong vài tuần gần đây, các release AI có một mẫu số chung khá rõ: không còn chỉ khoe model lớn hơn, mà bắt đầu khoe vai trò trong workflow.

Leanstral 1.5 nhắm vào formal verification — kiểm chứng hình thức, tức mô tả điều cần đúng bằng logic rồi để hệ thống kiểm tra chặt chẽ. OpenScience đi theo hướng workbench nghiên cứu mở, model-agnostic — nghĩa là đổi model theo từng request, không khóa vào một vendor. Hugging Face và Cerebras đẩy stack voice AI mở, tập trung vào latency — độ trễ phản hồi. LongCat-2.0 khoe native 1M context và kiến trúc MoE — Mixture-of-Experts, tức mỗi token chỉ gọi một phần chuyên gia của model. Astryx thì làm design system mà agent có thể đọc qua CLI và MCP server.

Điểm chung không phải là tất cả đều nên dùng. Điểm chung là: AI stack đang chuyển từ cuộc thi điểm số sang cuộc thi tích hợp đúng chỗ.

Với Leanstral, Mistral nói model đạt 100% trên miniF2F, giải được 587 bài trên PutnamBench, và có kết quả cao trên FATE-H, FATE-X. Ấn tượng, nhưng với team build production, benchmark giống bài kiểm tra cuối kỳ: hữu ích để biết năng lực nền, chưa nói em học sinh đó có làm tốt trong lớp của bạn không.

Mổ xẻ Leanstral: nó không phải coding assistant thường

Lean 4 không giống Python, TypeScript hay Rust mà bạn viết hằng ngày. Nó giống một ngôn ngữ để buộc máy kiểm tra lập luận: nếu bạn khẳng định hàm này không overflow, hoặc thuật toán này giữ invariant nào đó, bạn phải biểu diễn điều đó theo cách formal.

Nói thẳng ra thì, Leanstral không nên được hiểu là model viết code nhanh hơn. Nó nên được hiểu là model hỗ trợ tạo, sửa, hoặc kiểm tra chứng minh hình thức quanh code và toán.

Nguồn chính có chi tiết thú vị: dù được train chủ yếu cho toán, Leanstral 1.5 được Mistral nói là có khả năng code verification. Trong một thử nghiệm thực tế, nó quét 57 repo open-source và phát hiện 5 bug chưa biết trước, gồm một lỗi overflow trong thư viện Rust varinteger.

Đây là phần đáng giữ. Không phải vì 5 bug là con số thần kỳ. Mà vì nó chỉ ra một hướng dùng rất khác với autocomplete: cho model đi qua những đoạn logic có rủi ro cao, rồi biến nghi ngờ thành thứ có thể kiểm chứng.

Ví dụ cụ thể: team bạn đang viết module tính hạn mức tín dụng, xử lý số nguyên, làm rounding, hoặc encode dữ liệu nhị phân. Coding assistant thường có thể giúp viết test case. Nhưng với formal verification, câu hỏi đổi thành: có thể phát biểu invariant nào bắt buộc luôn đúng không? Có thể chứng minh nhánh này không overflow không? Có thể mô tả điều kiện đầu vào khiến parser không rơi vào trạng thái sai không?

Đây là khác biệt lớn. Test hỏi: với vài input mẫu, code có chạy đúng không. Verification hỏi: với một lớp input được định nghĩa rõ, điều kiện này có luôn đúng không.

Framework quyết định: ai nên dùng, ai nên đứng ngoài

Nếu là tech lead, mình sẽ không hỏi: Leanstral có giỏi không? Mình sẽ hỏi 4 câu này trước.

| Câu hỏi | Nếu câu trả lời là có | Nếu câu trả lời là không |
|---|---|---|
| Code của bạn có vùng lỗi gây hậu quả lớn không? | Cân nhắc verification lane | Dùng static analysis và test trước |
| Team có người đọc được Lean 4 hoặc sẵn sàng học không? | Có thể pilot nghiêm túc | Dễ thành demo bỏ xó |
| Bạn có spec rõ không? | Model có đất làm việc | Model sẽ đoán điều cần chứng minh |
| CI có chỗ cho bước kiểm chứng chậm hơn không? | Tích hợp được theo gate | Chỉ nên chạy thủ công theo case |

Mình gọi đây là verification lane: một làn riêng trong quy trình build, dành cho những phần code cần độ tin cậy cao hơn mức test thông thường. Nó không thay thế unit test, fuzzing, static analyzer hay review. Nó ngồi cạnh những thứ đó.

Ba nhóm nên thử:

  1. Team làm infrastructure, crypto, compiler, parser, payment, tài chính, dữ liệu nhị phân — nơi bug nhỏ có thể thành sự cố lớn.
  2. Nhóm nghiên cứu hoặc R&D có bài toán toán học rõ — nơi Lean 4 đã nằm gần workflow.
  3. Team platform muốn xây internal quality gate cho thư viện lõi — không phải mọi service, chỉ các package nền.

Ba nhóm nên bỏ qua, ít nhất lúc này:

  1. Team CRUD app bình thường, chưa có test coverage tử tế.
  2. Team không có spec, chỉ có ticket kiểu làm cho đúng như app cũ.
  3. Team cần tốc độ feature hơn độ chắc của logic lõi, vì verification sẽ thêm chi phí học, viết spec, debug proof.

Đổi cách nghĩ ở đây là: model chuyên formal verification không phải món nâng cấp mặc định cho dev productivity; nó là công cụ giảm rủi ro cho vùng code có giá trị kiểm chứng cao.

Điều đáng giữ: open-source làm thay đổi quyền thử nghiệm

Leanstral 1.5 có license Apache 2.0 và được cung cấp qua Hugging Face cùng API miễn phí. Với builder, điểm này quan trọng hơn headline benchmark.

Open-source ở đây cho bạn ba quyền:

Điểm này khớp với tín hiệu từ OpenScience: workbench nghiên cứu model-agnostic, chạy trên hạ tầng của bạn, dùng key của bạn. Astryx cũng cùng hướng: agent không chỉ nhìn UI bằng ảnh, mà đọc được component, CLI, MCP server. Hugging Face và Cerebras thì nhấn vào stack voice modular, từng lớp thay được. LongCat đặt cược vào kiến trúc dài hơi cho agentic coding, nhưng quyết định vẫn là chi phí vận hành và độ ổn định khi phục vụ.

Nói cách khác, release đáng chú ý hiện nay không chỉ trả lời: model làm được gì? Nó phải trả lời thêm: model nằm ở đâu trong giáo án kỹ thuật của team bạn?

Điều nên bỏ qua: leaderboard không phải roadmap

Mình không hạ thấp benchmark. miniF2F, PutnamBench, FATE-H, FATE-X đều có giá trị riêng. Nhưng builder dễ mắc một lỗi: thấy điểm cao ở bài toán formal math rồi suy ra nó sẽ tự động làm codebase của mình an toàn hơn.

Không nhanh vậy.

Bạn vẫn cần spec. Bạn vẫn cần chọn module nào đáng formalize. Bạn vẫn cần người review proof. Bạn vẫn cần quyết định failure policy: nếu Leanstral đề xuất proof không compile thì sao? Nếu proof compile nhưng spec viết thiếu thì sao? Nếu CI chậm lên thì ai chịu?

Một pilot hợp lý trong một buổi chiều có thể như sau:

  1. Chọn một hàm nhỏ nhưng quan trọng, ví dụ encode/decode, arithmetic boundary, parser state transition.
  2. Viết ra 2-3 invariant bằng tiếng Việt trước, rồi mới chuyển sang Lean 4 hoặc pseudo-spec.
  3. Dùng Leanstral để gợi ý formal statement và proof skeleton — khung chứng minh ban đầu.
  4. Chạy Lean 4 compiler để kiểm tra, không chấp nhận output chỉ vì model nói ổn.
  5. Ghi lại thời gian mất cho spec, proof, sửa lỗi, và so với cách viết test/fuzzing thông thường.

Nếu sau pilot, bạn chỉ có một demo đẹp nhưng không ai hiểu proof, dừng lại. Nếu bạn phát hiện spec bị mơ hồ, đó vẫn là kết quả tốt: model đã ép team làm bài tập về nhà mà trước giờ né.

Khuyến nghị của mình

Nếu team bạn đang build hệ thống AI bình thường, Leanstral 1.5 chưa phải ưu tiên số một. Hãy lo observability, eval, test data, rollback, cost guard trước.

Nếu team bạn có một lớp logic lõi mà sai là đau thật, mình sẽ thử Leanstral như một assistant cho verification lane, không phải thay thế reviewer. Bắt đầu nhỏ, đo bằng số bug hoặc spec ambiguity phát hiện được, không đo bằng cảm giác model thông minh.

Còn nếu bạn đang chọn giữa các release ồn ào — Leanstral cho verification, OpenScience cho research workflow, stack voice của Hugging Face/Cerebras cho latency, LongCat cho agentic coding dài ngữ cảnh, Astryx cho UI agent-readiness — câu hỏi lọc nên là:

Release này giúp mình ra quyết định production nào rõ hơn không?

Nếu không, nó chỉ là một dòng đẹp trong tab bookmark.

Takeaway gọn: model mới không cần làm thủ khoa toàn trường; chỉ cần đúng môn, đúng lớp, đúng bài kiểm tra là đã đáng tiền cà phê đêm nay rồi.

---
Bụi Wire — nghiện đọc release notes lúc 2 giờ sáng

Nguồn tham khảo