- Trong xu hướng đưa kiểm chứng hình thức đến gần hơn với công việc phát triển thực tế, Mistral AI đã công bố Leanstral 1.5, một mô hình theo giấy phép Apache-2.0 dành cho Lean 4
- Mô hình chỉ kích hoạt 6B trong tổng số 119B tham số, được huấn luyện để cùng xử lý viết chứng minh và làm việc với kho mã thông qua tiền huấn luyện trung gian, tinh chỉnh có giám sát và học tăng cường CISPO
- Đạt miniF2F 100%, PutnamBench 587/672, FATE-H 87%, FATE-X 34%, cho thấy hiệu năng mạnh trên các benchmark chứng minh toán học và đánh giá kỹ thuật chứng minh thực tế
- Trong kiểm chứng mã thực tế, mô hình chứng minh độ phức tạp thời gian O(log n) của cây AVL và tìm ra 11 lỗi thực sự trong 57 kho mã thông qua pipeline Rust-to-Lean
- Trọng số và API miễn phí
leanstral-1-5đã được công bố, có thể áp dụng ngay cho kỹ thuật chứng minh thực dụng như chứng minh định lý, gỡ lỗi chứng minh và đóng góp vào kho mã
Công bố Leanstral 1.5 và đặc tính mô hình
- Leanstral 1.5 là mô hình được tạo ra để thực hiện kỹ thuật chứng minh trong Lean 4
- Giấy phép là Apache-2.0, quy mô mô hình gồm tổng cộng 119B tham số và 6B tham số kích hoạt
- Mô hình nâng cao hiệu năng kiểm chứng hình thức, có thể dùng không chỉ cho benchmark toán học mà cả kiểm chứng thuộc tính trong mã thực tế
- Mô hình bão hòa miniF2F, giải được 587 trong 672 bài của PutnamBench, và đạt FATE-H 87%, FATE-X 34%
Huấn luyện 3 giai đoạn học từ phản hồi chứng minh
- Quá trình huấn luyện gồm 3 giai đoạn: huấn luyện trung gian, tinh chỉnh có giám sát và học tăng cường dựa trên CISPO
- Hai môi trường được dùng cho học tăng cường
- Môi trường nhiều lượt: mô hình nhận mệnh đề định lý để chứng minh hoặc phản chứng, rồi lặp lại việc sửa chứng minh dựa trên phản hồi từ trình biên dịch Lean
- Khi chứng minh biên dịch được thì thành công; nếu không, vòng lặp tiếp tục cho đến khi giải được bài hoặc dùng hết ngân sách
- Môi trường tác nhân mã: mô hình chỉnh sửa tệp trên hệ thống tệp thô như một lập trình viên, chạy lệnh bash và kiểm tra mục tiêu, lỗi, thông tin kiểu theo thời gian thực bằng Lean language server
- Môi trường tác nhân mã xử lý các tác vụ dài như hoàn thiện chứng minh một phần trong kho mã, viết bổ đề phụ trợ, và tiếp tục công việc ngay cả sau nhiều lần nén ngữ cảnh
- Tính đúng đắn cuối cùng được kiểm chứng trong fork SafeVerify của Mistral dựa trên danh sách định lý mục tiêu
Benchmark toán học và kỹ thuật chứng minh
- Đánh giá sử dụng miniF2F, PutnamBench, FATE-H/FATE-X và FLTEval
- miniF2F là benchmark toán học hình thức gồm các bài từ mức tiểu học đến mức IMO
- PutnamBench gồm 672 bài từ Putnam Mathematical Competition
- FATE-H và FATE-X lần lượt là benchmark đại số trừu tượng ở cấp sau đại học và tiến sĩ
- FLTEval đánh giá độ khó kỹ thuật chứng minh dựa trên các pull request thực tế của kho Fermat’s Last Theorem
- Trên miniF2F, mô hình đạt 100% ở cả tập kiểm chứng và tập kiểm thử
- Trên PutnamBench và FATE-H/X, mô hình được so sánh với Goedel-Architect, Seed-Prover 1.5 high và AxProverBase mà không có hướng dẫn chứng minh bằng ngôn ngữ tự nhiên
- Hiệu năng FATE-H/X:
- FATE-H đạt 87%, FATE-X đạt 34%, lập mức cao nhất mới
- Trên PutnamBench, mô hình giải nhiều hơn Seed-Prover 1.5 high 7 bài, với chi phí khoảng 4 USD mỗi bài
- Thiết lập high của Seed-Prover dùng ngân sách 10 H20-days mỗi bài, chi phí ước tính hơn 300 USD
- Một số prover xếp hạng cao hơn nhận hướng dẫn chứng minh bằng ngôn ngữ tự nhiên, hoặc hoạt động trong điều kiện khác như Aleph Prover, vốn tốn 54–68 USD mỗi bài
Khả năng mở rộng với ngân sách suy luận dài và FLTEval
- Trên PutnamBench, khi tăng ngân sách token, hiệu năng Pass@8 của Leanstral 1.5 tăng mượt và đơn điệu
- Trong thí nghiệm tăng ngân sách token mỗi lần thử từ 25k lên 4M, số bài giải được tăng như sau
- 50k token: 44 bài
- 200k token: 244 bài
- 1M token: 493 bài
- 4M token: 587 bài
- Việc tiếp tục suy luận, chỉnh sửa tệp và sửa lỗi qua hàng triệu token mà không dừng lại trong các chứng minh dài đã dẫn đến cải thiện hiệu năng
- FLTEval cũng được phát hành hoàn toàn dưới dạng mã nguồn mở
- Trên FLTEval, Leanstral 1.5 nâng pass@1 từ 21.9 lên 28.9, và pass@8 từ 31.9 lên 43.2
- pass@8 43.2 vượt mức 39.6 của Opus 4.6, trong khi chi phí chỉ bằng khoảng một phần bảy
- Mô hình cũng có hiệu năng vượt các mô hình mã nguồn mở lớn hơn 3–10 lần
Các trường hợp kiểm chứng mã thực tế
-
Chứng minh độ phức tạp thời gian của cây AVL
- Cây AVL là cây tìm kiếm nhị phân tự cân bằng, duy trì chiều cao O(log n) thông qua tái cân bằng khi chèn và xóa
- Leanstral 1.5 kiểm chứng rằng thao tác chèn và xóa trên triển khai thực tế có độ phức tạp O(log n)
- Tác vụ này đòi hỏi quy nạp cấu trúc phản ánh cấu trúc đệ quy của cây, xử lý theo dõi thời gian dựa trên monad, và phân tích vét cạn các trường hợp trên đường tái cân bằng
- Chứng minh được thực hiện qua hơn 2,7 triệu token và 22 lần nén ngữ cảnh
- Leanstral mở rộng có hệ thống từng tầng của monad TimeM để bộc lộ các phép tính đan xen với luồng điều khiển
- Với thao tác chèn, mô hình thiết lập ràng buộc 48 bước cho mỗi đơn vị chiều cao cùng một hạng gần như hằng số, rồi liên kết chiều cao và kích thước cây bằng quan hệ logarit
-
Tìm lỗi trong mã Rust
- Thí nghiệm phát hiện lỗi gồm một pipeline trong đó Aeneas chuyển mã Rust sang Lean, còn Leanstral suy luận ý định người dùng từ mã và tạo các thuộc tính nhất quán
- Leanstral thử chứng minh mỗi thuộc tính 4 lần; nếu tất cả đều thất bại, mô hình thử chứng minh phủ định của thuộc tính đó thêm 4 lần
- Trong 57 kho mã, 47 thuộc tính vi phạm được đánh dấu, trong đó 11 thuộc tính chỉ ra lỗi thực sự
- 5 trong số các lỗi thực sự là lỗi chưa từng được báo cáo trên GitHub trước đó
- Một trường hợp được phát hiện trong hàm sign của zigzag decoding thuộc thư viện datrs/varinteger
- Khi đầu vào là
Std.U64.MAX, biểu thức(value + 1)bị tràn số - Ở chế độ debug, chương trình crash; ở chế độ release, xảy ra hỏng dữ liệu âm thầm
- Edge case này là trường hợp mà kiểm thử và fuzzing thông thường dễ bỏ sót
Phân phối và cách sử dụng
- Trọng số được công bố trên Hugging Face
- Endpoint API miễn phí được cung cấp với tên
leanstral-1-5trong model card - Mistral Vibe là môi trường sử dụng được khuyến nghị
- Quy trình bắt đầu gồm thiết lập Mistral Vibe, cài đặt Leanstral 1.5, chạy tác nhân, tùy chọn cài đặt Lean LSP MCP, rồi bắt đầu tác vụ chứng minh
- Lean LSP MCP được khuyến nghị cài đặt bằng cách thêm vào
~/.vibe/config.toml - Nếu không có máy chủ MCP hiện có, có thể cần xóa
mcp_servers = [] - Leanstral có thể dùng cho giải định lý, gỡ lỗi chứng minh và đóng góp vào kho mã
1 bình luận
Ý kiến trên Hacker News
Phê phán rằng Mistral khó cạnh tranh với các mô hình lớn là có lý, nhưng thực tế có vẻ họ đang tập trung vào việc cung cấp một số tính năng cụ thể với chất lượng cao trên các mô hình nhỏ
Tôi dùng Mistral cho các tác vụ như OCR hay phân tích tệp, và nếu nạp 100 USD vào tài khoản thì có thể chạy suốt 1 năm mà không phải lo về lượng request
Chi phí cực nhỏ, nên ngay cả khi không thể cạnh tranh với Opus 4.8 thì vẫn hoàn toàn đáng giá
Chất lượng ổn với giá rẻ có vẻ là một thị trường ngách hơn là trả giá cao gấp 10 lần để lấy chất lượng tốt nhất nhằm giảm sai sót về sau
OCR giờ gần như đã là hàng hóa phổ thông, và các mô hình mã nguồn mở hay những nơi như AWS cũng cung cấp sẵn như một tính năng cơ bản
Hơn nữa, với mức giá 100 USD/năm thì khó tạo được lòng trung thành, lại không có chi phí chuyển đổi, nên chỉ cần có giá thấp hơn là khách hàng có thể rời đi ngay
Nếu một công cụ giá rẻ dễ bị sao chép mà không có lock-in khách hàng, thì nó gần giống một tính năng hơn là một doanh nghiệp
Với người mua thì điều đó là tốt, nhưng nếu muốn các công ty châu Âu về dài hạn cạnh tranh với đối thủ toàn cầu bằng năng lực sản phẩm, thì đây có vẻ là một chiến lược tệ
Bản thân công việc này thì tốt, nhưng ví dụ phát hiện bug lại cho cảm giác hơi kỳ
Họ nói trong hàm sign của zigzag decoding, khi đầu vào là
Std.U64.MAXthì(value + 1)bị overflow, dẫn tới crash ở debug mode và hỏng dữ liệu âm thầm ở release mode; tôi không chắc có thể gọi đây là kiểu điều kiện biên mà test “thường bỏ sót” hay khôngTest tệ thì có thể bỏ sót, nhưng người cẩn thận hoặc các hệ thống coding dựa trên machine learning thường làm khá tốt việc nghĩ ra “phải test giá trị cực hạn”. Nhất là với code parse input từ người dùng thì lại càng thế
Tôi tự hỏi có phải họ còn tìm thấy những bug thú vị hơn nhưng khó giải thích nhanh, nên mới đưa ví dụ này ra không
Với một thư viện encoding như thế này, kỳ vọng cơ bản đối với code tử tế là có fuzzing, và gần như chắc chắn nó sẽ bị bắt trong vài giây
Thực tế, tôi viết một bài test round-trip cực đơn giản bằng
proptestthì chưa đến 1 giây đã ra hàng chục lỗi cùng kết quả dưới đây:thread 'signed_round_trip' (50528) panicked at tests/test.rs:72:1:Test failed: attempt to multiply with overflow.minimal failing input: value = 4611686018427387904successes: 2local rejects: 0global rejects: 0Dùng Lean cho thấy lợi thế là ta ít phải khôn khéo trong việc chọn ví dụ để test hơn
Điều đó khiến tôi tò mò về xuất thân của các tác giả
Mọi hệ thống kiểm thử dựa trên thuộc tính được phát minh từ khoảng năm 1980 đều khám phá giá trị biên
Có thể việc test thực tế khó khăn do ngữ nghĩa của C và C++, hoặc vì thiếu ngữ nghĩa, bởi compiler vẫn được phép coi mọi đầu vào dẫn đến undefined behavior là “test passed”
Ở giữa bài có phần so sánh với nhiều LLM hàng đầu, nhưng tất cả đều là các mô hình từ nửa năm trước
Kiểu “mô hình mới của chúng tôi tốt hơn các mô hình Trung Quốc từ 3 thế hệ trước” nên khá buồn cười
Thư viện đó là https://github.com/datrs/varinteger
Có vẻ đúng, vì cùng vấn đề này đã được đăng trong repo đó từ một tuần trước khi bài báo được công bố: https://github.com/datrs/varinteger/issues/8
Tôi không rõ người này có phải nhân viên Leanstral không, hay Leanstral chỉ lấy issue này mang vào
Thư viện này nhỏ, test thì yếu đến mức đáng ngạc nhiên, và gần như không được đụng tới trong 8 năm: https://github.com/datrs/varinteger/blob/master/tests/test.r...
Số lượt tải có vẻ thấp, khoảng 1 nghìn lượt mỗi ngày: https://crates.io/crates/varinteger
Vì vậy khó xem đây là một thành công nổi bật đến mức đáng đem ra làm ví dụ duy nhất. Việc phát hiện tự động rõ ràng là hữu ích, nhưng tôi không chắc đây có phải thành tựu đáng chú ý trong phân ngành này không
Tôi chưa dùng LLM viết chứng minh bao giờ, nhưng vì dữ liệu huấn luyện khá khan hiếm nên nếu nó thô hơn các mô hình coding thông thường thì cũng không có gì đáng ngạc nhiên
Nhân tiện, https://crates.io/crates/varinteger hiển thị là https://github.com/mafintosh/varinteger-rs, nhưng URL này redirect sang https://github.com/datrs/varinteger, nên có vẻ đây là cùng một thư viện dù nhìn bề ngoài không phải vậy
Mấu chốt không phải là tìm ra bug, mà là chứng minh rằng một số loại bug nhất định không tồn tại dưới những giả định nhất định
Nhưng câu chuyện này khó bán, nên marketing thường hay trôi sang hướng “chúng tôi đã tìm ra bug này”
Liệu điều này có hữu ích ngay cả với người hoàn toàn không biết gì về Lean không? Muốn kiểm chứng phần mềm đang phát triển nhưng không có kinh nghiệm về kiểm chứng hình thức
Tò mò không biết chỉ với đặc tả, mã nguồn và thời gian học hạn chế thì có thể đạt được kết quả đủ dùng hay không
Nó giống đọc kiểu của Haskell hơn là toán học, chỉ là cảm giác như mượn khá nhiều từ vựng từ toán học
Có thể cũng nhận được hỗ trợ theo kiểu hội thoại để viết mã Lean phục vụ kiểm chứng ứng dụng, nhưng điều đó thì chưa chắc
Nếu không thì bạn sẽ không thể xác minh đầu ra
Về mặt máy móc, có thể bạn đã chứng minh một mệnh đề nào đó được kiểm tra là đúng, nhưng nếu không biết mệnh đề ấy có nghĩa gì và liệu nó có bao quát điều bạn thực sự muốn kiểm chứng hay không, thì việc đó không có ý nghĩa
Thật ngạc nhiên khi các mô hình lại thông thạo Lean4 một cách ổn định đến vậy. Không chỉ các mô hình hàng đầu mà cả các mô hình cục bộ nhỏ cũng vậy, có cảm giác như LLM đơn giản là hiểu Lean4 rất tốt
Vẫn còn khá xa mới có thể tự gọi mình là chuyên gia Lean4, nhưng giờ thì không còn nhất thiết phải cần hỗ trợ để tạo ra các chương trình hữu ích
Việc có thể tin cậy những phần mình chưa hoàn toàn hiểu, ngay cả khi gần như chưa có kiến thức, giúp tốc độ học tăng lên rất nhiều. Có được các chương trình đáng tin cậy dù kiến thức còn chưa đầy đủ vừa thực tế vừa tạo động lực
Có cảm giác giới hạn nằm ở phần ngôn ngữ dùng để mô tả các tiên đề và bề mặt mệnh đề của mình, chứ không phải toàn bộ các bước chứng minh trung gian. Theo thời gian, nếu muốn làm được nhiều hơn thì vẫn phải hiểu nhiều hơn, nhưng theo một nghĩa nào đó, bạn có thể làm việc an toàn ở mức N+1
Lean4 cũng là một ngôn ngữ lập trình thú vị ngay cả khi tách khỏi vai trò chứng minh định lý, và tốc độ của nó nhanh một cách đáng ngạc nhiên
Tôi đang dùng nó gắn với
io_uring, và trong nhiều trường hợp nó nhanh hơn rất nhiều so với C++/libuv hoặc Rust/TokioThỉnh thoảng nếu thấy đuôi lớn ở các chỉ số như độ trễ p99.99 thì cần tinh chỉnh kiểu như đổi số sang fixed-width, nhưng C++ và Rust cũng phải tinh chỉnh thôi
Việc họ thúc đẩy Lean 4 cho kiểm chứng hình thức khá thú vị
Tôi cứ nghĩ lĩnh vực này thuộc về Isabelle/HOL và TLA+
Ít nhất tôi đã kỳ vọng vào các mô hình được huấn luyện để dùng cả ba. Với suy diễn tiến trong đại số tuyến tính thì Isabelle/Isar thậm chí còn có vẻ tốt hơn, ai có thể giải thích không?
Trong lĩnh vực này, ngay cả Agda cũng từng được dùng nhiều hơn
Tuy vậy, Lean hiện đang có được đà phát triển đáng kể như một lựa chọn thay thế, đặc biệt nhờ năng lực như một ngôn ngữ lập trình hàm đa dụng
Cá nhân tôi thấy các cách tiếp cận dựa trên logic Hoare hoặc separation logic thực tế hơn vì dễ khớp yêu cầu với đặc tả. Tôi thích Dafny và F*
Khá buồn cười khi trong thông báo trên Twitter, các nhà phát triển lại lấp ló nhắc đến Le Chaton Fat
Bất kể họ có thực sự liên quan đến Le Chaton Fat hay không, có vẻ sắp xuất hiện một mô hình thật sự “mới, lớn, đa dụng”
Sau cả đợt ồn ào truyền thông mà họ vẫn nhắc trực tiếp thì cũng đáng để mong đợi. Hy vọng cái tên sẽ sáng tạo hơn “Large 4”
Có thể thử Leanstral 1.5 trong OpenATP mới nhất
OpenATP là một gói Python mã nguồn mở kiêm CLI cho các bộ chứng minh định lý tự động kiểu tác nhân, hỗ trợ sẵn cả chạy cục bộ trên Docker lẫn chạy từ xa trong sandbox của Modal
GitHub: https://github.com/henryrobbins/open-atp
Docs: https://open-atp.henryrobbins.com