Mistral AI Ra Mắt Leanstral - AI Agent Mã Nguồn Mở Cho Lean 4

Zach Anderson 16/03/2026 19:13 (Giờ VN)

Mistral phát hành Leanstral, một AI Agent 6B tham số cho xác minh chính thức Lean 4, vượt trội các mô hình lớn hơn với chi phí chỉ 1/15 theo giấy phép Apache 2.0.

Mistral AI đã phát hành Leanstral vào ngày 16 tháng 3 năm 2026 - AI Agent mã nguồn mở đầu tiên được xây dựng đặc biệt cho xác minh chính thức Lean 4. Mô hình 120B tham số hoạt động chỉ với 6B tham số hoạt động và được cung cấp theo giấy phép Apache 2.0, giúp chứng minh định lý cấp độ sản xuất trở nên dễ tiếp cận mà không cần ngân sách doanh nghiệp.

Tại sao điều này quan trọng đối với tiền mã hoá? Xác minh chính thức - bằng chứng toán học rằng mã thực hiện chính xác những gì nó tuyên bố - đã trở thành tiêu chuẩn vàng để bảo mật hợp đồng thông minh và các giao thức blockchain. Lỗi trong mã DeFi đã gây thiệt hại hàng tỷ đô la. Leanstral có thể giảm đáng kể rào cản cho các dự án tìm kiếm bảo mật đã được xác minh.

Đánh Đổi Hiệu Suất và Chi Phí

Mistral đã so sánh Leanstral với các đối thủ cạnh tranh độc quyền và mã nguồn mở bằng cách sử dụng FLTEval, một bộ đánh giá mới kiểm tra các tác vụ kỹ thuật chứng minh thực tế từ dự án chính thức hoá Định lý Cuối cùng của Fermat.

Con số rất ấn tượng. Leanstral ở pass@2 đạt 26,3 điểm với chi phí tính toán 36 đô la. Claude Sonnet 4.6 đạt 23,7 điểm nhưng tốn 549 đô la - gấp hơn 15 lần chi phí cho hiệu suất kém hơn. Ngay cả ở pass@16, nơi Leanstral đạt 31,9 điểm với 290 đô la, nó vẫn có chi phí thấp hơn một phần năm so với mức giá 1,650 đô la của Claude Opus 4.6 (mặc dù Opus dẫn đầu về chất lượng ở mức 39,6).

So với các lựa chọn mã nguồn mở, khoảng cách hiệu quả còn mở rộng hơn nữa. GLM5-744B-A40B và Kimi-K2.5-1T-A32B đạt ngưỡng khoảng 16-20 điểm mặc dù có gấp 6-8 lần tham số hoạt động hơn. Qwen3.5-397B-A17B cần bốn lần để đạt 25,4 điểm - Leanstral vượt qua con số đó chỉ với hai lần.

Kiến Trúc Kỹ Thuật

Leanstral sử dụng kiến trúc sparse mixture-of-experts được tối ưu hoá cho quy trình kỹ thuật chứng minh. Mô hình tích hợp với giao thức máy chủ ngôn ngữ của Lean thông qua MCP (Model Context Protocol), được huấn luyện đặc biệt để đạt hiệu suất tối đa với công cụ lean-lsp-mcp.

Bản thân Lean 4 đã ra mắt ổn định vào tháng 9 năm 2023 và đã có sự chấp nhận nhanh chóng để chính thức hoá toán học. Thư viện Mathlib - một bộ sưu tập đồ sộ các bằng chứng toán học - đã được chuyển đổi thành công sang Lean 4 trong cùng năm đó. Các dự án như bằng chứng chính thức của Định lý Cuối cùng của Fermat chứng minh khả năng của nền tảng cho công việc toán học nghiêm túc.

Ứng Dụng Thực Tế

Mistral đã giới thiệu Leanstral xử lý một câu hỏi gỡ lỗi thực tế trên Stack Exchange về các thay đổi gây hỏng trong Lean 4.29.0-rc6. AI Agent đã chẩn đoán vấn đề về đẳng thức định nghĩa với bí danh kiểu và xác định chính xác rằng việc thay thế def bằng abbrev sẽ khôi phục khớp chiến thuật.

Mô hình cũng đã chứng minh khả năng dịch đa ngôn ngữ, chuyển đổi các định nghĩa Rocq (trước đây là Coq) sang Lean 4 trong khi vẫn bảo toàn ngữ nghĩa chứng minh và triển khai ký hiệu tuỳ chỉnh.

Tuỳ Chọn Truy Cập

Có ba cách triển khai: tích hợp trực tiếp trong Mistral Vibe (sử dụng /leanstall để bắt đầu), một API endpoint miễn phí tại labs-leanstral-2603 để thu thập phản hồi trong thời gian giới hạn, hoặc triển khai tự lưu trữ với các trọng số Apache 2.0.

Đối với các dự án blockchain, tính toán rất đơn giản. Xác minh chính thức theo truyền thống yêu cầu các công ty kiểm toán đắt tiền hoặc chuyên môn sâu nội bộ. Một AI Agent mã nguồn mở có thể chứng minh tính chính xác của mã với chi phí 36-290 đô la mỗi tác vụ có thể định hình lại cách các giao thức tiếp cận bảo mật - giả sử các bằng chứng vẫn đứng vững trong điều kiện sản xuất.

• mistral ai
• leanstral
• lean 4
• xác minh chính thức
• mã nguồn mở