Mistral phát hành Leanstral: Agent mã nguồn mở đầu tiên cho Lean4, tạo mã đồng thời xuất ra chứng minh hình thức

Thông tin từ CoinWorld, theo theo dõi của 1M AI News, Mistral AI hôm nay đã phát hành Leanstral, agent mã nguồn mở đầu tiên được thiết kế dành riêng cho công cụ xác minh hình thức Lean 4. Thủ phạm chính gây ra trở ngại trong việc tạo mã AI là kiểm tra thủ công, Leanstral cho phép AI tạo mã đồng thời xuất ra các chứng minh hình thức có thể tự động xác minh bởi Lean 4, bỏ qua bước này. Mô hình sử dụng kiến trúc MoE thưa, tổng tham số 120B, tham số kích hoạt 6B, mã nguồn mở Apache 2.0, đã được tối ưu hóa huấn luyện đặc biệt cho lean-lsp-mcp. Có thể khởi động không cấu hình trong Mistral Vibe (lệnh /leanstall), hoặc gọi qua API miễn phí tại điểm cuối labs-leanstral-2603, hỗ trợ tải trọng số để tự triển khai. Mistral cũng đồng thời phát hành chuẩn đánh giá mới FLTEval, dựa trên dự án hình thức của định lý Fermat trong cộng đồng Lean 4 để thử nghiệm. So sánh chi phí: Leanstral pass@2 đạt điểm 26.3 với $36, vượt xa Claude Sonnet 4.6 với 23.7 điểm và chi phí $549; pass@16 đạt điểm 31.9 với $290, dẫn trước Sonnet 8 điểm, trong khi Claude Opus 4.6 cần tới $1,650 mới đạt 39.6 điểm. Trong các mô hình mã nguồn mở, Qwen3.5-397B-A17B phải chạy 4 lần mới đạt 25.4 điểm, vẫn thấp hơn Leanstral pass@2.