Mistral phát hành Leanstral 1.5 cho các chứng minh hình thức, giảm chi phí xuống còn ~$4 mỗi bài toán.

Theo OneMillion_AI, Mistral AI gần đây đã phát hành Leanstral 1.5, một mô hình chứng minh hình thức cho Lean 4 với tổng số 119 tỷ tham số và 65 tỷ tham số hoạt động. Mô hình được phát hành theo giấy phép Apache-2.0 với quyền truy cập API miễn phí. Trên PutnamBench, Leanstral 1.5 đạt chi phí trung bình khoảng $4 mỗi bài toán để giải, thấp hơn đáng kể so với các hệ thống trước đây có chi phí từ hàng chục đến hàng trăm USD mỗi bài toán.

Mô hình giải được 587 trong số 672 bài toán PutnamBench và đạt 87% trên benchmark đại số trừu tượng FATE-H và 34% trên FATE-X, thiết lập các kỷ lục hiệu suất mới cho hạng mục của nó. Ngoài các chứng minh toán học, Leanstral 1.5 còn được áp dụng vào xác minh mã, phát hiện 11 lỗi thực tế trên 57 kho lưu trữ Rust mã nguồn mở, trong đó có 5 lỗi chưa từng được báo cáo trước đây.