Nghiên cứu · The Decoder：AI News（RSS）
Mistral AI ra mắt Leanstral 1.5: Mô hình chuyên biệt cho kiểm chứng toán học và phát hiện lỗi code
Mistral AI phát hành Leanstral 1.5, mô hình mã nguồn mở tối ưu cho ngôn ngữ Lean 4, đạt hiệu suất ấn tượng trong các bài toán chứng minh hình thức và phát hiện lỗ hổng bảo mật thực tế trong các thư vi
Mistral AI phát hành Leanstral 1.5, mô hình mã nguồn mở tối ưu cho ngôn ngữ Lean 4, đạt hiệu suất ấn tượng trong các bài toán chứng minh hình thức và phát hiện lỗ hổng bảo mật thực tế trong các thư viện mã nguồn mở.
Đây là bước tiến quan trọng trong việc ứng dụng AI vào kiểm chứng toán học và bảo mật phần mềm, với kết quả benchmark thực tế rất thuyết phục.
Nội dung dịch chi tiết
Mistral AI đã chính thức phát hành Leanstral 1.5, một mô hình mã nguồn mở miễn phí (giấy phép Apache 2.0) được xây dựng chuyên biệt cho việc xác minh hình thức trong ngôn ngữ lập trình Lean 4. Ngôn ngữ này được thiết kế để kiểm chứng các chứng minh toán học và tính đúng đắn của phần mềm.
Theo Mistral, mô hình đạt tỷ lệ chính xác 100% trên miniF2F, một bộ tiêu chuẩn toán học hình thức bao gồm các bài toán từ cấp trung học đến trình độ Olympic. Đối với PutnamBench, bao gồm 672 bài toán từ cuộc thi toán Putnam, mô hình giải được 587 bài. Trong các bài kiểm tra đại số FATE-H và FATE-X ở trình độ thạc sĩ và tiến sĩ, Leanstral 1.5 đạt kết quả lần lượt là 87% và 34%.
Leanstral 1.5 hiện dẫn đầu các mô hình mã nguồn mở trên PutnamBench, FATE-H và FATE-X. Chỉ có mô hình đóng Aleph Prover mới vượt qua được Leanstral 1.5 trên PutnamBench.
Mặc dù được đào tạo chủ yếu cho toán học, Mistral cho biết mô hình này cũng thể hiện khả năng tốt trong việc xác minh mã nguồn. Trong một thử nghiệm thực tế, Leanstral 1.5 đã quét 57 kho lưu trữ mã nguồn mở và phát hiện 5 lỗi chưa từng được biết đến trước đó, bao gồm một lỗi tràn số trong thư viện Rust có tên là varinteger.
Hiện tại, mô hình đã có sẵn trên Hugging Face và thông qua API miễn phí. Quá trình đào tạo mô hình bao gồm các giai đoạn đào tạo trung gian, tinh chỉnh có giám sát và học tăng cường.
Ý chính từ bài gốc
- Mistral AI phát hành Leanstral 1.5, mô hình mã nguồn mở chuyên biệt cho xác minh hình thức trong Lean 4.
- Mô hình đạt kết quả xuất sắc trên các bộ tiêu chuẩn toán học như miniF2F, PutnamBench, FATE-H và FATE-X.
- Leanstral 1.5 dẫn đầu các mô hình mã nguồn mở trong các bài kiểm tra toán học cấp cao.
- Mô hình đã phát hiện 5 lỗi phần mềm chưa từng được biết đến trong 57 kho lưu trữ mã nguồn mở.
- Người dùng có thể tiếp cận mô hình thông qua Hugging Face và API miễn phí.