Leanstral 1.5

 (docs.mistral.ai)
1 điểm bởi GN⁺ 3 giờ trước | 1 bình luận | Chia sẻ qua WhatsApp
  • Leanstral 1.5 là mô hình cập nhật được tinh chỉnh cho kỹ thuật chứng minh hình thức Lean 4, hướng đến chứng minh định lý tự động và tự động hình thức hóa
  • Quy mô mô hình gồm tổng 119B tham số và 6.5B tham số hoạt động, giả định xử lý ngữ cảnh dài cho chứng minh và tài liệu
  • Định danh được cung cấp là labs-leanstral-1-5, và trong tài liệu được hiển thị là mô hình Labs v1.5
  • Độ dài ngữ cảnh là 256k, mục giá được hiển thị là $0, nhấn mạnh khả năng tiếp cận cho mục đích thử nghiệm và đánh giá
  • Có thể sử dụng cùng với Chat Completions, gọi hàm, agent, đầu ra có cấu trúc, OCR, Document QnA, FIM, embeddings, moderation, audio và API xử lý theo lô

Mô hình tối ưu cho chứng minh hình thức Lean 4

  • Leanstral 1.5 là phiên bản cập nhật của mô hình kỹ thuật chứng minh hình thức Lean 4
  • Các mục tiêu tối ưu hóa cốt lõi là chứng minh định lý tự động và tự động hình thức hóa
  • Định danh mô hình được cung cấp là labs-leanstral-1-5

Quy mô mô hình và thuộc tính cơ bản

  • Cấu hình tham số được hiển thị là 119B total parameters, 6.5B active
  • Độ dài ngữ cảnh là 256k
  • Mục giá được hiển thị là $0
  • Phân loại phát hành là Labs v1.5

API hội thoại, agent và đầu ra có cấu trúc

Xử lý tài liệu, hoàn thiện mã và embeddings

An toàn, audio và xử lý theo lô

Bài viết liên quan

1 bình luận

 
GN⁺ 3 giờ trước
Ý kiến trên Hacker News

  • Tôi tò mò nên đăng ký, nạp tiền vào tài khoản và định dùng thử thì không được. Vì thấy nói là model Labs nên tôi định bật Labs, nhưng lần này lại hiện lỗi không xác định. Tôi định liên hệ hỗ trợ khách hàng theo hướng dẫn thì chẳng có hỗ trợ khách hàng, chỉ có một FAQ làm qua loa
    FAQ trông như được vibe coding, tìm kiếm cũng tệ hại, nhập truy vấn nào cũng chỉ ra câu trả lời hoàn toàn không liên quan. Rồi tôi nhận ra: nếu AI làm hỗ trợ khách hàng tốt, tại sao các công ty AI lại không dùng AI của chính họ để cung cấp hỗ trợ khách hàng?

    • Thực ra họ có dùng. Ví dụ có Cursor. Xem cuộc thảo luận cũ “Cursor IDE support hallucinates lockout policy, causes user cancellations”[1]
      [1]: https://news.ycombinator.com/item?id=43683012
    • Chưa từng có ai nghĩ AI làm hỗ trợ khách hàng tốt cả. Nó chỉ tạo ra hỗ trợ khách hàng rẻ, và vì nhiều công ty vốn đã không quan tâm đến chất lượng hỗ trợ khách hàng nên đã cung cấp hỗ trợ tồi tệ từ trước, họ thích việc có thể cắt giảm chi phí thêm nữa
      Với những công ty thấy bực vì phải chi tiền để sửa vấn đề thực sự, đó có thể coi là hỗ trợ khách hàng “tốt”
    • Đọc bình luận này vừa buồn cười vừa nghẹn. Cảm giác quá kiểu EU. Mất 18 tháng mới giành được một hợp đồng doanh nghiệp ở EU, hôm nay ký xong gửi lại thì nhận được trả lời tự động: “Xin lỗi, nhưng tôi đang nghỉ phép đến cuối tháng 7...”
      Trong một năm qua liên lạc với người phụ trách này, đây đã là lần thứ tư tôi nhận được trả lời tự động báo nghỉ phép
    • Lạ và khó chịu thật, nhưng tôi có thể dùng miễn phí model này dù chưa từng liên kết bất kỳ phương thức thanh toán nào
    • Những người này không trả lời email. qwant cũng vậy
      Mẫu chỉ có hai trường hợp, nhưng khiến tôi mặc định rằng các công ty Pháp không thích được liên hệ bằng tiếng Anh cho lắm

  • Hơi lạc đề một chút, nhưng khá buồn khi EU thực sự chẳng có gì trong thị trường LLM tuyến đầu. Nhất là khi nghĩ đến việc gần đây Mỹ đã hạn chế hoàn toàn quyền tiếp cận các model thật sự tiên tiến
    Đây có phải thuần túy là do thiếu vốn và hạ tầng không?

    • Mistral nhìn chung đang thắng trong những mảng họ chọn để chiến đấu, và hiện giờ đó là điều cần thiết
      Thay vì nhìn xem toàn bộ nền kinh tế EU có thể đóng góp bao nhiêu cho các model tuyến đầu, sẽ chính xác hơn nếu nhìn xem nền kinh tế Pháp có thể đóng góp bao nhiêu rồi so với Mỹ hoặc Trung Quốc. Quy mô không đủ lớn. Thay vào đó nên nhìn xem họ làm được gì với quy mô thấp đó, và các sản phẩm ngách như Leanstral, Voxtral là kết quả như vậy
    • Nhìn chung là đúng
      Pháp và Đức là hai nền kinh tế lớn nhất EU; Pháp có Mistral, còn Đức có một tổ chức mang tính quỹ đầu tư mạo hiểm được chính phủ hỗ trợ. Tổ chức đó rất tự hào khi đưa ra tận 125 triệu euro (<150 triệu USD) để giúp các nhà nghiên cứu châu Âu đạt mốc tiên tiến mới với các model có chủ quyền[1]
      Số tiền đó cũng không dành cho một người thắng duy nhất mà được chia cho nhiều bên nhận. Là bước đầu thì tuyệt, nhưng chính xác hơn là nếu diễn ra 3–4 năm trước thì mới đáng là bước đầu. Thật đáng tiếc
      [1] (tiếng Đức) https://www.sprind.org/worte/magazin/verkuendung-next-fronti...
    • Phần mềm nói chung và AI nói riêng đều là thị trường kẻ giàu càng giàu, kẻ nghèo càng nghèo. Các tập đoàn lớn của Mỹ có đủ khả năng gom sạch nhân tài châu Âu và các công ty châu Âu đang nổi, và thực tế họ làm vậy. Nếu không muốn mua, họ cũng có thể dùng giá để đè cho phá sản
      Chúng ta đang sống trong một nền kinh tế thuộc địa lấy vốn con người làm nguyên liệu thô, và tất cả đều chảy về Mỹ. Muốn tránh điều đó thì phải ngừng chơi trò chơi hiện tại và nuôi dưỡng các ngành công nghiệp có sức cạnh tranh bằng chính sách công nghiệp đúng nghĩa như Trung Quốc. Suốt nhiều thập kỷ qua không hề có ý chí đó, nhưng Trump đang cho thấy rất rõ sự trở lại của nhà nước, và châu Âu cũng đang dần thừa nhận
    • Mistral đã huy động được hơn 4 tỷ USD, nên đó cũng là số tiền khá lớn, nhưng không ở tầm OpenAI/Anthropic/xAI
      Phần khó là biện minh về mặt tài chính cho việc phát triển LLM thuần túy. Các model rất giống nhau. OpenAI ban đầu biện minh bằng danh nghĩa một “tổ chức từ thiện” cho nghiên cứu thuần túy, Anthropic thì tách ra với lý do OpenAI không đủ quan tâm đến an toàn. Elon nói rằng nếu ông không tạo ra Grok thì AI sẽ giả vờ thức tỉnh và không trung thực, còn Google tạo Gemini vì ban đầu chính họ là điểm xuất phát và nghiên cứu AI là sứ mệnh cốt lõi Larry và Sergey đặt ra khi thành lập công ty. Chỉ là vì lý do tài chính nên họ đã để nó nằm im một thời gian
      Động cơ của các model Trung Quốc thì nói thật là không rõ. Tôi chưa thấy lời giải thích hay nào, chỉ thấy các giả thuyết. Nhưng nhìn việc họ phát miễn phí hoặc đưa ra với giá rẻ quá mức, động cơ đó dường như cũng không phải là tài chính
      Ngược lại, Mistral là một công ty bình thường. Không có nhà tài trợ giàu có tin vào kiểu tự sự định mệnh vũ trụ và đổ tiền vào, nên họ phải biện minh việc mình làm bằng tỷ suất hoàn vốn đầu tư. Khi đó, huấn luyện LLM quy mô lớn gần như bị loại trừ
      Cũng phải tính đến quy định của EU. Trước đây khi tìm hiểu, tôi thấy có nhiều quy tắc kỳ lạ làm mất khả năng tồn tại của ngành công nghệ châu Âu. Ở Anh còn có quy định chỉ được crawl Internet cho mục đích nghiên cứu
      https://knowledgerights21.org/news-story/the-uks-copyright-l...
      Và nếu không có Tu chính án thứ nhất, nguy cơ bị truy tố vì những gì model nói ra cao hơn nhiều. Cứ nhìn trường hợp Đức đưa Google ra tòa vì nội dung model đưa vào trang kết quả tìm kiếm là thấy
      Vì vậy lợi ích thì không rõ ràng, còn rủi ro pháp lý thì rất lớn
    • EU không có một thị trường chung đúng nghĩa, đặc biệt là trong thị trường vốn. Dù dân số đông hơn Mỹ và tổng quy mô kinh tế lớn hơn, nếu không thể gom nguồn lực một cách hiệu quả thì cũng chẳng có nhiều ý nghĩa
      Ở châu Âu liệu có thể huy động 100 tỷ USD cho một phòng thí nghiệm mới không? Nếu không thì coi như xong, có thể bỏ cuộc được rồi

  • Thật trùng hợp. Sáng nay tôi vừa công bố OpenATP. OpenATP là một gói Python mã nguồn mở kiêm CLI dành cho các trình chứng minh định lý tự động dạng tác tử
    Nó cũng bao gồm hỗ trợ Leanstral thông qua Vibe harness của Mistral. Mô hình Leanstral production trước đó đã bị ngừng vào ngày 22 tháng 5, và tôi sẽ cập nhật gói để trỏ tới Leanstral 1.5 sớm nhất có thể
    GitHub: https://github.com/henryrobbins/open-atp
    Docs: https://open-atp.henryrobbins.com

  • 404 à?
    https://web.archive.org/web/20260630223430/https://docs.mist...

  • Tôi không hiểu rõ chính sách trọng số. Trang này nói trọng số theo giấy phép Apache nên trông như trọng số mở, nhưng tôi không tìm thấy liên kết tải xuống
    Hồ sơ Hugging Face có vẻ chỉ cung cấp snapshot trước đó[0]. Có ai biết có thể tải trọng số xuống không, và nếu có thì tải ở đâu?
    [0] https://huggingface.co/mistralai/Leanstral-2603

  • Tôi cũng thấy “Page not found”. Bạn truy cập được à? Nội dung là gì vậy?

    • Theo Web Archive: Leanstral 1.5 - ngày 30 tháng 6 năm 2026
      Đây là mô hình kỹ thuật chứng minh hình thức Lean 4 được cập nhật, tối ưu cho chứng minh định lý tự động và hình thức hóa tự động. Tổng cộng 119B tham số, 6.5B tham số hoạt động
      https://web.archive.org/web/20260630223430/https://docs.mist...

  • Thảo luận về Leanstral 1: https://news.ycombinator.com/item?id=47404796

  • Lean 4 và Idris 2 đang bị đánh giá thấp, và vì cung cấp thêm các bảo đảm nên rất có khả năng sẽ cực kỳ phù hợp để LLM viết code

  • Hiện đang bị 404

  • Tôi đăng ký vì tin này, nhưng để dùng “Code” thì có phải kết nối GitHub không? Trông quá hạn chế