Mistral AI vừa chính thức phát hành Leanstral 1.5, một mô hình trí tuệ nhân tạo nguồn mở chuyên biệt cho việc xác thực chính thức (formal verification) sử dụng ngôn ngữ Lean 4. Đây là một bước đi đáng chú ý của startup công nghệ Pháp trong việc tối ưu hóa AI cho các tác vụ tư duy logic và toán học chuyên sâu.
Diễn biến
Theo thông tin từ The Decoder, Leanstral 1.5 được thiết kế để vượt qua các bài kiểm tra toán học chính thức một cách xuất sắc. Không chỉ dừng lại ở lý thuyết toán học, mô hình này đã chứng minh tính thực tiễn cao khi quét qua 57 kho lưu trữ nguồn mở (repositories) khác nhau. Trong quá trình quét này, Leanstral 1.5 đã phát hiện ra 5 lỗi lập trình (bugs) thực tế chưa từng được biết đến trước đó.
Bối cảnh
Việc ứng dụng AI vào xác thực mã nguồn và toán học chính thức đang là một xu hướng lớn trong ngành công nghệ. Thay vì chỉ tạo ra mã nguồn dựa trên phán đoán xác suất, các mô hình như Leanstral 1.5 sử dụng ngôn ngữ chứng minh định lý như Lean 4 để đảm bảo tính chính xác tuyệt đối về mặt logic toán học, giảm thiểu tối đa các lỗi bảo mật và vận hành.
Vì sao đáng chú ý
Đối với cộng đồng phát triển phần mềm và nghiên cứu AI tại Việt Nam, sự xuất hiện của một mô hình nguồn mở như Leanstral 1.5 mang lại công cụ mạnh mẽ để nâng cao chất lượng code. Khả năng phát hiện lỗi thực tế của mô hình cho thấy AI đang dần chuyển từ vai trò hỗ trợ viết code thông thường sang kiểm thử và bảo mật hệ thống ở cấp độ chuyên sâu.