- Tác nhân mã nguồn mở đầu tiên được thiết kế cho Lean 4, nhằm tự động hóa chứng minh hình thức (formal proof) để giảm gánh nặng kiểm chứng thủ công của con người
- Công bố trọng số mô hình theo giấy phép Apache 2.0, và có thể sử dụng ngay thông qua môi trường Mistral Vibe cùng API endpoint miễn phí
- Sử dụng kiến trúc thưa với 6B tham số hoạt động để đạt hiệu quả và giảm chi phí, đồng thời hỗ trợ tích hợp MCP như lean-lsp-mcp
- Trên benchmark FLTEval, đạt điểm cao hơn các mô hình mã nguồn mở lớn như Qwen3.5, GLM5, Kimi-K2.5, đồng thời cho hiệu năng tương đương Claude Sonnet với chi phí rẻ hơn hơn 15 lần
- Đề xuất một cách tiếp cận mới kết hợp tự động hóa chứng minh hình thức và nâng cao độ tin cậy của mã, cho thấy tiềm năng ứng dụng trong cả toán học nghiên cứu lẫn phát triển phần mềm nhiệm vụ trọng yếu
Tổng quan về Leanstral
- Leanstral là tác nhân mã nguồn mở đầu tiên dành cho Lean 4, hoạt động trong môi trường trợ lý chứng minh (proof assistant)
- Lean 4 có thể biểu diễn các đối tượng toán học phức tạp (ví dụ: không gian perfectoid) và các đặc tả phần mềm
- Khác với các hệ thống chứng minh hiện có thường tập trung vào wrapper mô hình tổng quát hoặc các bài toán đơn lẻ, Leanstral được huấn luyện để hoạt động hiệu quả trong các kho lưu trữ hình thức thực tế (formal repositories)
- Áp dụng kiến trúc thưa với 6B tham số hoạt động, kết hợp suy luận song song (parallel inference) với khả năng kiểm chứng của Lean
- Hỗ trợ tích hợp MCP, tương thích với các giao thức thường dùng như lean-lsp-mcp
Công bố và khả năng tiếp cận
- Công bố trọng số mô hình theo giấy phép Apache 2.0, và được cung cấp ở chế độ tác nhân trong Mistral Vibe
- Bất kỳ ai cũng có thể truy cập qua API endpoint miễn phí (
labs-leanstral-2603), và phản hồi của người dùng sẽ được thu thập để cải thiện các phiên bản tiếp theo
- Đồng thời công bố báo cáo kỹ thuật và công cụ đánh giá FLTEval, nhằm đo lường hiệu năng kỹ nghệ chứng minh thực tế vượt ra ngoài các đánh giá vốn thiên về toán học trước đây
Đánh giá hiệu năng (Evaluation)
- Được đánh giá dựa trên khả năng hoàn thành toàn bộ chứng minh hình thức và định nghĩa các khái niệm toán học mới theo đơn vị Pull Request của dự án FLT
- Đối tượng so sánh: Claude Opus 4.6, Sonnet 4.6, Haiku 4.5, Qwen3.5 397B-A17B, Kimi-K2.5 1T-A32B, GLM5 744B-A40B
Leanstral so với các mô hình mã nguồn mở
- Leanstral-120B-A6B đạt 26.3 điểm(pass@2), cao hơn GLM5(16.6 điểm) và Kimi-K2.5(20.1 điểm)
- Trong khi Qwen3.5 đạt 25.4 điểm ở 4 lần chạy(pass@4), Leanstral đạt điểm cao hơn chỉ với một nửa số lần chạy
- Ở cùng mức chi phí, có thể mở rộng tuyến tính lên tới 29.3 điểm(pass@4)
Leanstral so với dòng Claude
- Cho thấy lợi thế 2.6 điểm so với Sonnet (26.3 điểm vs 23.7 điểm), trong khi chi phí chạy là $36 vs $549, rẻ hơn hơn 15 lần
- Theo tiêu chí pass@16, đạt 31.9 điểm, cao hơn Sonnet 8 điểm
- Claude Opus 4.6 có hiệu năng cao nhất với 39.6 điểm, nhưng chi phí là $1,650, cao hơn 92 lần so với Leanstral
- Tất cả benchmark đều được thực hiện trong môi trường Mistral Vibe mà không cần chỉnh sửa
| Mô hình |
Chi phí($) |
Điểm |
| Haiku |
184 |
23.0 |
| Sonnet |
549 |
23.7 |
| Opus |
1,650 |
39.6 |
| Leanstral |
18 |
21.9 |
| Leanstral pass@2 |
36 |
26.3 |
| Leanstral pass@4 |
72 |
29.3 |
| Leanstral pass@8 |
145 |
31.0 |
| Leanstral pass@16 |
290 |
31.9 |
Nghiên cứu tình huống (Case Studies)
Ứng phó với thay đổi phiên bản Lean
- Nhập vào một câu hỏi trên StackExchange xử lý lỗi liên quan đến type alias phát sinh trong Lean 4.29.0-rc6
- Leanstral tái hiện môi trường gây ra vấn đề, và chẩn đoán chính xác vấn đề đồng nhất định nghĩa (definitional equality)
- Đề xuất dùng
abbrev thay cho def, giúp chiến thuật rw (tactic) hoạt động bình thường trở lại
- Giải thích rõ cho người dùng nguyên nhân của vấn đề và lý do cách khắc phục có hiệu quả
Suy luận và chuyển đổi chương trình
- Chuyển định nghĩa chương trình của Rocq sang Lean, đồng thời triển khai cả ký pháp tùy biến do người dùng định nghĩa
- Ví dụ, chứng minh rằng lệnh
plus2 thực hiện thao tác cộng 2 vào biến X
- Chỉ từ đặc tả Rocq được cung cấp, hoàn thiện định lý (theorem) trong Lean và thực hiện chứng minh
Cách sử dụng
- Tích hợp Mistral Vibe: có thể dùng ngay bằng lệnh
/leanstall
- Labs API: có thể truy cập miễn phí hoặc với chi phí thấp
- Tải mô hình: có thể tự chạy trực tiếp theo giấy phép Apache 2.0
Ý nghĩa
- Leanstral là nỗ lực mã nguồn mở đầu tiên kết hợp tạo mã và tự động hóa chứng minh hình thức
- Cho thấy tiềm năng ứng dụng trong toán học nghiên cứu, phát triển phần mềm có thể kiểm chứng, thiết kế hệ thống độ tin cậy cao
- Được đánh giá là một hạ tầng kiểm chứng mã mới vừa hiệu quả về chi phí vừa mang tính mở
1 bình luận
Ý kiến trên Hacker News
Thật thú vị khi mọi người bắt đầu nhận ra một mô hình nơi đặc tả hành vi mong muốn cho agent, rồi để nó viết mã theo đúng đặc tả đó
Dù dùng TDD hay công cụ kiểm chứng nào đi nữa, theo thời gian các bộ kiểm chứng như vậy sẽ tích lũy thành một kho tài liệu có thể thực thi, cho thấy “nó phải hoạt động như thế nào”
Cách tiếp cận này mạnh hơn nhiều so với một đặc tả Markdown đơn thuần, vì nó ghi lại hành vi chi tiết bằng mã chứ không chỉ là ý định
Khi phần mềm ngày càng phức tạp, kiểu truyền miệng “cứ hỏi Jim ấy” rõ ràng có giới hạn
Độ chi tiết và ngữ cảnh sẽ bị mất đi trong quá trình thay đổi độ phân giải
Tôi đồng ý với TDD hay phát triển hướng kiểm chứng, nhưng viết nó bằng code không phải mục tiêu cuối cùng
Đã có hàng triệu dòng test tồn tại rồi, nên phát triển dựa trên đó có lẽ thực tế hơn
Tôi muốn biết Lean thực sự giúp gì ở đây.
Ví dụ là chứng minh một state machine bằng Lean rồi chuyển nó sang Dart sao?
Tôi không rành Lean nên khó hình dung đây có phải cách tiếp cận thực tế không
Như cũng đã được nhắc tới gần đây trong podcast của Jack Clark (đồng sáng lập Anthropic) và Ezra Klein, đang có nhiều thảo luận rằng alignment của mô hình là tương đối và tính đa dạng là quan trọng
Có ý kiến cho rằng mô hình của Mistral đang tụt lại so với các mô hình tiên phong khác, nhưng việc thử nghiệm nhiều kỹ thuật alignment và nhiều công ty khác nhau vẫn rất quan trọng với hệ sinh thái
Trường hợp thành công thực tế này khiến tôi nhớ tới Red Green TDD của Simon Willison
Tôi thấy ấn tượng với quá trình Leanstral tạo mã test để tái hiện môi trường thất bại và tìm ra vấn đề về definitional equality
Mô hình này được huấn luyện cho các tác vụ cụ thể nhưng hiệu năng vẫn thấp hơn Opus
Opus đắt hơn 6 lần, nhưng có vẻ xứng đáng với mức giá đó
Tôi hiểu vì sao một startup châu Âu ít vốn lại nhắm vào ngách này, nhưng có lẽ khó chuyển thành doanh thu lớn
Có lẽ so với các mô hình như Codex sẽ thú vị hơn
Tôi thích khái niệm “mã đáng tin cậy”
Nhưng tiêu chuẩn so sánh hơi khó hiểu. Họ nhấn mạnh là rẻ hơn Haiku, trong khi chính Haiku đã yếu ở tác vụ này và Leanstral còn yếu hơn nữa
Nếu mục tiêu là độ chính xác, tôi không hiểu vì sao “rẻ nhưng không tốt lắm” lại quan trọng
Dù vậy, Opus cũng không hoàn hảo, nên nếu tăng quy mô thì có thể cho kết quả tốt hơn
Ở 2 lần thì tốt hơn Haiku và Sonnet, còn ở 16 lần thì tiệm cận Opus trong khi vẫn hiệu quả chi phí hơn
Với người không biết Lean như tôi, tôi muốn hiểu liệu thứ này có giá trị trực tiếp không
Nó có tự động gắn chứng minh vào code ngôn ngữ như Go không, hay đơn giản là mình chỉ nên ủng hộ sự đa dạng của các mô hình mở?
Nhưng rồi chính đặc tả Lean4 đó lại trở thành một software artifact
Khi ấy ta lại quay về câu hỏi làm sao xác minh đặc tả đó là đúng — tức là cuối cùng vẫn cần con người rà soát
Tôi đã dự đoán xu hướng này từ vài tuần trước, nên rất vui vì nó thực sự xảy ra
Trong thời đại LLM, có lẽ tính thân thiện với con người của code sẽ kém quan trọng hơn khả năng chứng minh và hiệu quả token
Có thể sẽ đến một thế giới kết hợp Lean và Rust, nơi “chỉ mã đã được chứng minh mới biên dịch được”
Tôi đã tổng hợp thảo luận liên quan trong bình luận trước đó
Nó chỉ đảm bảo rằng nó hợp lệ về mặt logic
Việc hiểu đầy đủ một chứng minh đang chứng minh điều gì cũng khó chẳng kém gì hiểu một chương trình, nhưng điểm lợi là quá trình đó buộc tư duy đi sâu hơn
Thật mừng khi họ nói “mã nguồn mở” không chỉ bằng lời, mà thực sự phát hành trọng số theo giấy phép Apache-2.0
Theo tin tức chính thức của Mistral
Claude Opus có chi phí 1.650 USD với điểm số 39.6,
Leanstral pass@8 là 145 USD với 31.0, còn pass@16 là 290 USD với 31.9,
nên hiệu quả hiệu năng trên chi phí là khá cao