Leanstral: Nền tảng nguồn mở để vibe-code đáng tin cậy

Các tác nhân AI đã được chứng minh là công cụ có khả năng tạo mã cao. Tuy nhiên, khi chúng tôi đẩy các mô hình này sang các lĩnh vực có tính đặt cược cao, từ toán học nghiên cứu cơ bản đến phần mềm quan trọng, chúng tôi gặp phải một nút thắt về quy mô: đánh giá của con người. Thời gian và chuyên môn chuyên môn cần thiết để xác minh thủ công trở thành trở ngại chính cho tốc độ kỹ thuật.

Chúng tôi hình dung ra một thế hệ tác nhân mã hóa hữu ích hơn để vừa thực hiện nhiệm vụ vừa chính thức chứng minh việc triển khai của mình dựa trên các thông số kỹ thuật nghiêm ngặt. Thay vì gỡ lỗi logic do máy tạo ra, con người ra lệnh cho những gì họ muốn. Hôm nay, chúng tôi đang thực hiện bước quan trọng đầu tiên hướng tới tầm nhìn đó.

Giới thiệu Leanstral

Chúng tôi phát hành Leanstral, tác nhân mã nguồn mở đầu tiên được thiết kế cho Lean 4. Lean4 là một trợ lý chứng minh có khả năng biểu diễn các đối tượng toán học phức tạp như không gian hoàn hảo và các thông số kỹ thuật phần mềm như thuộc tính của các mảnh Rust(Rust fragments). Không giống như các hệ thống chứng minh hiện có đóng vai trò bao quanh các mô hình tổng quát lớn hoặc tập trung vào các bài toán đơn lẻ, Leanstral được thiết kế để đạt hiệu quả cao (với các tham số hoạt động 6B) và được đào tạo để vận hành trong các kho lưu trữ hình thức thực tế.

• Mở và có thể truy cập: Chúng tôi phát hành trọng số Leanstral theo giấy phép Apache 2.0, ở chế độ tác nhân trong phạm vi Mistral và thông qua điểm cuối API miễn phí. Chúng tôi cũng sẽ phát hành một báo cáo công nghệ trình bày chi tiết về phương pháp đào tạo của chúng tôi và bộ đánh giá FLTEval mới để đưa các đánh giá vượt ra ngoài phạm vi tập trung vào môn toán cạnh tranh.

• Hiệu quả và mạnh mẽ: Chúng tôi sử dụng kiến trúc rất thưa thớt cho Leanstral và tối ưu hóa kiến trúc đó cho các nhiệm vụ kỹ thuật kiểm chứng. Tận dụng khả năng suy luận song song với Lean như một công cụ xác minh hoàn hảo, Leanstral vừa mang lại hiệu quả vừa tiết kiệm chi phí so với các đối thủ cạnh tranh nguồn đóng hiện có.

• Có thể nâng cấp thông qua MCP: Leanstral hỗ trợ các MCP tùy ý thông qua Vibe và được đào tạo đặc biệt để đạt được hiệu suất tối đa với Lean-lsp-mcp thường được sử dụng. 

Đánh giá

Để phản ánh tính hữu ích trong các kịch bản kỹ thuật chứng minh thực tế, chúng tôi đánh giá Leanstral về việc hoàn thành tất cả các bằng chứng chính thức và xác định chính xác các khái niệm toán học mới trong mỗi PR cho dự án FLT, thay vì các vấn đề toán học riêng lẻ. Chúng tôi so sánh Leanstral với các tác nhân mã hóa hàng đầu (Claude Opus 4.6, Sonnet 4.6, Haiku 4.5) và các mô hình nguồn mở (Qwen3.5 397B-A17B, Kimi-K2.5 1T-A32B, GLM5 744B-A40B).

Leanstral vs. Các mô hình OSS

Leanstral-120B-A6B thể hiện lợi thế hiệu quả đáng kể so với các sản phẩm nguồn mở ngang hàng lớn hơn nhiều. Trong khi các mẫu như GLM5-744B-A40B và Kimi-K2.5-1T-32B gặp khó khăn trong việc mở rộng quy mô, giới hạn điểm FLTEval lần lượt là khoảng 16,6 và 20,1 thì Leanstral vượt trội hơn cả hai chỉ với một lần vượt qua.

Ngay cả Qwen3.5-397B-A17B, đối thủ cạnh tranh OSS mạnh nhất được thể hiện, cũng cần 4 đường chuyền để đạt được số điểm 25,4. Ngược lại, Leanstral đạt được số điểm vượt trội là 26,3 với một nửa khoản đầu tư đó (pass@2) và tiếp tục mở rộng quy mô tuyến tính, đạt 29,3 ở cùng mức chi phí.

Leanstral vs. Gia đình Claude

Leanstral đóng vai trò là giải pháp thay thế có giá trị cao cho bộ Claude, mang lại hiệu suất cạnh tranh với mức giá chỉ bằng một phần nhỏ: Leanstral pass@2 đạt số điểm 26,3, đánh bại Sonnet 2,6 điểm, trong khi chỉ tốn 36 USD để chạy, so với 549 USD của Sonnet. Ở pass@16, Leanstral đạt số điểm 31,9, dễ dàng đánh bại Sonnet 8 điểm. Mặc dù Claude Opus 4.6 vẫn dẫn đầu về chất lượng nhưng nó có mức giá đáng kinh ngạc là 1.650 USD, cao gấp 92 lần so với Leanstral.

Trong quá trình đo điểm chuẩn, chúng tôi đã sử dụng Mistral Vibe làm nền tảng mà không có sửa đổi cụ thể nào cho việc đánh giá.

Mẫu	Chi phí ($)	Điểm
Haiku	184	23,0
Sonnet	549	23,7
Opus	1.650	39,6
Leanstral	18	21,9
Leanstral pass@2	36	26,3
Leanstral pass@4	72	29,3
Leanstral pass@8	145	31,0
Leanstral pass@16	290	31,9

Nghiên cứu điển hình

Trả lời các bài đăng trên stackexchange về những thay đổi trong phiên bản Lean mới nhất

Khi các thay đổi nhỏ xảy ra với bản phát hành Lean mới, việc di chuyển mã có thể là một vấn đề đau đầu. Chúng tôi đã cung cấp cho Leanstral một câu hỏi thực tế từ Proof Assistants Stack Exchange về một tập lệnh đã ngừng biên dịch một cách bí ẩn trong Lean 4.29.0-rc6 (mà chúng tôi không đào tạo do nó mới xuất hiện). Thủ phạm là một chiến thuật viết lại (rw) đột nhiên không khớp với các mẫu liên quan đến bí danh loại đơn giản, ban đầu được viết là def T2 := List Bool.

Thay vì lao vào bóng tối, Leanstral đã xắn tay áo lên. Nó đã xây dựng thành công mã kiểm tra để tạo lại môi trường bị lỗi và chẩn đoán vấn đề cơ bản bằng sự bình đẳng về mặt định nghĩa. Mô hình đã xác định chính xác rằng vì def tạo ra một định nghĩa cứng nhắc đòi hỏi phải trình bày rõ ràng nên nó đã chủ động ngăn chiến thuật rw nhìn thấy cấu trúc cơ bản mà nó cần phải khớp.

Cách khắc phục được đề xuất rất đơn giản: chỉ cần hoán đổi def thành abbrev. Bởi vì abbrev tạo ra một bí danh trong suốt được xác định ngay lập tức bằng loại ban đầu, nên chiến thuật rw một lần nữa có thể khớp hoàn hảo với mẫu (L2 n).length trong bằng chứng. Leanstral hoàn thành công việc và giải thích lý do một cách hoàn hảo cho người dùng. 

Lý luận về chương trình

Chúng tôi đã sao chép các định nghĩa trong Rocq từ https://www.cs.princeton.edu/courses/archive/fall10/cos441/sf/Imp.html và yêu cầu Leanstral chuyển đổi sang Lean. Nó đã thực hiện thành công, thậm chí còn triển khai cả ký hiệu tùy chỉnh. Đoạn ví dụ:

Nó cũng có thể dịch sang Lean và sau đó chứng minh một số đặc tính về chương trình bằng ngôn ngữ này khi chỉ đưa ra câu lệnh Rocq (không có bằng chứng):

Bằng chứng về nhu cầu. Hãy thử Leanstral ngay hôm nay.

Leanstral hiện đã có sẵn cho mọi người sử dụng.

• Không thiết lập trong Mistral Vibe: Chúng tôi đã tích hợp Leanstral trực tiếp vào Mistral Vibe để mã hóa và chứng minh cảm xúc ngay lập tức, không cần thiết lập. Sử dụng /leanstall để bắt đầu.

• API Labs: Truy cập mô hình thông qua điểm cuối API miễn phí/gần miễn phí labs-leanstral-2603 của chúng tôi. Chúng tôi đang duy trì khả năng truy cập cao của điểm cuối này trong một khoảng thời gian giới hạn để thu thập phản hồi thực tế và dữ liệu có thể quan sát nhằm thúc đẩy thế hệ mô hình mã đã xác minh tiếp theo.

• Sở hữu trọng lượng: Tải xuống mô hình được cấp phép Apache 2.0 và chạy mô hình đó trên kim loại của riêng bạn.

Tài liệu - Đăng ký Mistral Vibe