Mistral ra mắt Leanstral: tác nhân mã mã nguồn mở đầu tiên của Lean4, có khả năng tạo mã và xuất ra các bằng chứng hình thức cùng một lúc.

Theo 1M AI News , Mistral AI hôm nay đã phát hành Leanstral, tác nhân mã mã nguồn mở đầu tiên được thiết kế đặc biệt cho công cụ xác minh hình thức Lean 4. Nút thắt cổ chai cốt lõi trong việc tạo mã AI là việc xem xét của con người; Leanstral bỏ qua bước này bằng cách tạo mã và đồng thời xuất ra các bằng chứng hình thức có thể được Lean 4 tự động xác minh. Mô hình sử dụng kiến ​​trúc MoE thưa với tổng cộng 120 tỷ tham số và 6 tỷ tham số kích hoạt, mã nguồn mở Apache 2.0 và có các tối ưu hóa huấn luyện cụ thể cho lean-lsp-mcp. Nó có thể được khởi chạy mà không cần cấu hình trong Mistral Vibe (lệnh `/leanstall`) hoặc thông qua điểm cuối API miễn phí `labs-leanstral-2603`, hỗ trợ tự triển khai tỷ trọng đã tải xuống.

Mistral cũng đã phát hành một chuẩn đánh giá mới, FLTEval, sử dụng dự án hình thức hóa Định lý cuối cùng của Fermat từ cộng đồng Lean 4 làm nền tảng thử nghiệm. So sánh chi phí: Leanstral pass@2 đạt 26,3 điểm với giá 36 đô la, vượt qua Claude Sonnet 4.6 (23,7 điểm) với giá 549 đô la; pass@16 đạt 31,9 điểm với giá 290 đô la, dẫn trước Sonnet 8 điểm, trong khi Claude Opus 4.6 cần 1.650 đô la để đạt 39,6 điểm. Trong số các mô hình mã nguồn mở, Qwen3.5-397B-A17B cần 4 lần để đạt 25,4 điểm, vẫn thấp hơn Leanstral pass@2.