Leanstral 1.5

 (docs.mistral.ai)
1 คะแนน โดย GN⁺ 3 시간 전 | 1 ความคิดเห็น | แชร์ทาง WhatsApp
  • Leanstral 1.5 เป็นโมเดลอัปเดตที่ปรับให้เหมาะกับงานวิศวกรรมการพิสูจน์เชิงรูปนัยของ Lean 4 โดยมุ่งเน้นการพิสูจน์ทฤษฎีบทอัตโนมัติและการจัดรูปแบบเชิงรูปนัยอัตโนมัติ
  • ขนาดโมเดลประกอบด้วย พารามิเตอร์รวม 119B และ พารามิเตอร์ที่ทำงานอยู่ 6.5B โดยออกแบบมาสำหรับการจัดการบริบทของการพิสูจน์และเอกสารที่ยาว
  • ตัวระบุที่ให้ใช้งานคือ labs-leanstral-1-5 และในเอกสารถูกระบุเป็นโมเดล Labs v1.5
  • ความยาวคอนเท็กซ์คือ 256k และรายการราคาแสดงเป็น $0 เพื่อเน้นการเข้าถึงสำหรับการทดลองและการประเมินผล
  • สามารถใช้งานร่วมกับ Chat Completions, Function Calling, Agents, Structured Outputs, OCR, Document QnA, FIM, Embeddings, Moderations, Audio และ Batch Processing API

โมเดลที่ออกแบบมาสำหรับการพิสูจน์เชิงรูปนัยของ Lean 4

  • Leanstral 1.5 เป็นเวอร์ชันอัปเดตของโมเดลงานวิศวกรรมการพิสูจน์เชิงรูปนัยของ Lean 4
  • เป้าหมายการปรับแต่งหลักคือ การพิสูจน์ทฤษฎีบทอัตโนมัติ และ การจัดรูปแบบเชิงรูปนัยอัตโนมัติ
  • โมเดลนี้ให้ใช้งานด้วยตัวระบุ labs-leanstral-1-5

ขนาดโมเดลและคุณสมบัติพื้นฐาน

  • โครงสร้างพารามิเตอร์ระบุเป็น 119B total parameters, 6.5B active
  • ความยาวคอนเท็กซ์คือ 256k
  • รายการราคาแสดงเป็น $0
  • การจัดหมวดหมู่รีลีสคือ Labs v1.5

API สำหรับบทสนทนา เอเจนต์ และ Structured Output

การประมวลผลเอกสาร การเติมโค้ด และ Embeddings

ความปลอดภัย เสียง และการประมวลผลแบบแบตช์

บทความที่เกี่ยวข้อง

1 ความคิดเห็น

 
GN⁺ 3 시간 전
ความคิดเห็นจาก Hacker News

  • สงสัยเลยสมัคร ใส่เงินเข้าบัญชี แล้วลองใช้ดู แต่ใช้ไม่ได้ เห็นบอกว่าเป็นโมเดล Labs เลยพยายามเปิด Labs คราวนี้กลับขึ้น ข้อผิดพลาดที่ไม่ทราบสาเหตุ พอจะติดต่อฝ่ายสนับสนุนตามคำแนะนำ ก็ไม่มีฝ่ายสนับสนุน มีแต่ FAQ ที่ทำมาแบบลวก ๆ
    FAQ ดูเหมือนเขียนด้วย vibe coding และระบบค้นหาก็แย่มาก ไม่ว่าจะใส่คำถามอะไร ก็ได้แต่คำตอบที่ไม่เกี่ยวข้องเลย แล้วผมก็นึกได้ว่า ถ้า AI เก่งเรื่องบริการลูกค้าจริง ทำไม บริษัท AI ถึงไม่ใช้ AI ของตัวเองให้บริการลูกค้าล่ะ?

    • จริง ๆ ก็มีใช้นะ ตัวอย่างเช่น Cursor ลองดูการถกเถียงเก่าที่ชื่อ “Cursor IDE support hallucinates lockout policy, causes user cancellations” ได้[1]
      [1]: https://news.ycombinator.com/item?id=43683012
    • ไม่มีใครคิดว่า AI ให้บริการลูกค้าได้ดีหรอก มันแค่ทำให้ได้ ฝ่ายสนับสนุนราคาถูก เท่านั้น และหลายบริษัทก็ไม่ได้สนใจคุณภาพงานซัพพอร์ตอยู่แล้ว ให้บริการห่วย ๆ กันมานาน จึงชอบที่มันช่วยลดต้นทุนได้อีก
      จากมุมมองของบริษัทที่รำคาญว่าต้องเสียเงินไปแก้ปัญหาจริง ๆ นี่ก็ถือเป็นบริการลูกค้าที่ “ดี” แล้ว
    • อ่านคอมเมนต์นี้แล้วทั้งขำทั้งจุก รู้สึกว่า ช่าง EU มาก ผมใช้เวลา 18 เดือนกว่าจะปิดสัญญากับองค์กรใน EU ได้รายหนึ่ง วันนี้เซ็นแล้วส่งกลับไป ก็ได้อีเมลตอบกลับอัตโนมัติว่า “ขออภัย แต่เราลาพักร้อนจนถึงปลายเดือนกรกฎาคม...”
      ตลอด 1 ปีที่ติดต่อกับผู้รับผิดชอบคนนี้ นี่เป็นอีเมลตอบกลับอัตโนมัติเรื่องลาพักร้อนครั้งที่สี่แล้ว
    • แปลกและน่าหงุดหงิด แต่ผมใช้โมเดลนี้ได้ ฟรี ทั้งที่ไม่เคยผูกวิธีชำระเงินเลย
    • คนพวกนี้ไม่ตอบอีเมล qwant ก็เหมือนกัน
      ตัวอย่างมีแค่สองรายก็จริง แต่ทำให้ผมสันนิษฐานว่าบริษัทฝรั่งเศสไม่ค่อยชอบให้ติดต่อเป็นภาษาอังกฤษ

  • ออกนอกเรื่องนิดหน่อย แต่ค่อนข้างเศร้าที่ EU แทบไม่มีอะไรในตลาด LLM ระดับ frontier จริง ๆ โดยเฉพาะเมื่อคิดถึงเรื่องล่าสุดที่สหรัฐฯ จำกัดการเข้าถึงโมเดลระดับล้ำหน้าจริง ๆ อย่างสิ้นเชิง
    นี่เป็นเพราะขาดเงินทุนและโครงสร้างพื้นฐานล้วน ๆ หรือเปล่า?

    • Mistral โดยมากกำลังชนะในสนามที่พวกเขาเลือกจะสู้ และตอนนี้เราต้องการแบบนั้น
      แทนที่จะดูว่าเศรษฐกิจ EU ทั้งหมดจะมีส่วนกับโมเดลระดับ frontier ได้แค่ไหน การดูว่า เศรษฐกิจฝรั่งเศส จะมีส่วนได้แค่ไหนแล้วเทียบกับสหรัฐฯ หรือจีนจะถูกต้องกว่า ขนาดมันไม่พอ แต่ควรดูว่าพวกเขาทำอะไรได้บ้างจากขนาดที่เล็กกว่านั้น และ ผลิตภัณฑ์เฉพาะทาง อย่าง Leanstral, Voxtral ก็คือผลลัพธ์แบบนั้น
    • โดยรวมก็ถูก
      ฝรั่งเศสและเยอรมนีเป็นเศรษฐกิจที่ใหญ่ที่สุดใน EU ฝรั่งเศสมี Mistral ส่วนเยอรมนีมีหน่วยงานลักษณะเวนเจอร์แคปิตอลที่ได้รับการสนับสนุนจากรัฐ หน่วยงานนั้นภูมิใจมากที่ประกาศเงินถึง 125 ล้านยูโร (<150 ล้านดอลลาร์) เพื่อช่วยให้นักวิจัยยุโรปสร้าง frontier ใหม่ในโมเดลอธิปไตย[1]
      เงินนั้นก็ไม่ได้ให้ผู้ชนะรายเดียว แต่แบ่งให้ผู้รับหลายราย เป็นก้าวแรกที่ดี แต่ถ้าพูดให้ตรง น่าจะเป็นก้าวแรกที่เหมาะเมื่อ 3–4 ปีก่อน น่าเสียดายจริง ๆ
      [1] (ภาษาเยอรมัน) https://www.sprind.org/worte/magazin/verkuendung-next-fronti...
    • ทั้งซอฟต์แวร์โดยรวมและ AI ต่างก็เป็นตลาดแบบ คนรวยยิ่งรวย คนจนยิ่งจน บริษัทใหญ่ของสหรัฐฯ มีกำลังและก็ทำจริงในการกวาดซื้อคนเก่งยุโรปกับบริษัทยุโรปที่กำลังมาแรง ถ้าไม่อยากซื้อ ก็ทุ่มราคากดจนอีกฝ่ายล้มละลายได้
      เราอยู่ใน เศรษฐกิจอาณานิคม ที่ใช้ทุนมนุษย์เป็นวัตถุดิบ และทุกอย่างไหลไปสหรัฐฯ ถ้าจะหลีกเลี่ยง ก็ต้องเลิกเล่นเกมแบบปัจจุบัน แล้วสร้างอุตสาหกรรมที่แข่งขันได้ด้วยนโยบายอุตสาหกรรมจริงจังแบบจีน ตลอดหลายทศวรรษที่ผ่านมาไม่มีเจตจำนงแบบนั้น แต่ Trump ได้แสดงให้เห็นอย่างชัดเจนถึงการกลับมาของรัฐ และยุโรปก็ค่อย ๆ ยอมรับเรื่องนี้อยู่
    • Mistral ระดมทุนได้ มากกว่า 4 พันล้านดอลลาร์ ก็ถือว่าเป็นเงินก้อนใหญ่ แต่ยังไม่ใช่ระดับ OpenAI/Anthropic/xAI
      ส่วนที่ยากคือการอธิบายความคุ้มค่าทางการเงินของการพัฒนา LLM ล้วน ๆ โมเดลต่าง ๆ คล้ายกันมาก OpenAI ตอนแรกอธิบายตัวเองว่าเป็น “องค์กรการกุศล” เพื่อการวิจัยล้วน ๆ ส่วน Anthropic แยกออกมาโดยบอกว่า OpenAI ไม่ใส่ใจเรื่องความปลอดภัยมากพอ Elon บอกว่าถ้าเขาไม่สร้าง Grok ขึ้นมา AI ก็จะแกล้งตื่นรู้และไม่ซื่อสัตย์ต่อความจริง ส่วน Google สร้าง Gemini เพราะเดิมทีพวกเขาเป็นจุดเริ่มต้น และงานวิจัย AI เป็นภารกิจหลักที่ Larry กับ Sergey มอบไว้ตั้งแต่ก่อตั้งบริษัท เพียงแต่ถูกพักไว้ช่วงหนึ่งด้วยเหตุผลทางการเงิน
      แรงจูงใจของโมเดลจีนพูดตรง ๆ คือไม่ชัดเจน ผมยังไม่เคยเห็นคำอธิบายที่ดี มีแต่สมมติฐาน แต่ดูจากการปล่อยฟรีหรือขายถูกเกินไป แรงจูงใจก็คงไม่ใช่เรื่องการเงิน
      ในทางกลับกัน Mistral เป็นบริษัททั่วไป ไม่มีผู้สนับสนุนมหาเศรษฐีที่เชื่อในเรื่องเล่าระดับชะตากรรมจักรวาลแล้วเทเงินให้ ดังนั้นสิ่งที่ทำต้องอธิบายได้ด้วย ผลตอบแทนจากการลงทุน และนั่นแทบจะตัดการฝึก LLM ขนาดใหญ่ออกไป
      ต้องพิจารณากฎระเบียบของ EU ด้วย เมื่อก่อนผมเคยลองค้นดู มีข้อบังคับแปลก ๆ มากมายที่ทำลายความเป็นไปได้ของอุตสาหกรรมเทคโนโลยียุโรป ในสหราชอาณาจักรมีกฎว่าการ crawl อินเทอร์เน็ตทำได้เฉพาะเพื่อการวิจัยเท่านั้นด้วย
      https://knowledgerights21.org/news-story/the-uks-copyright-l...
      และถ้าไม่มี First Amendment ความเสี่ยงที่จะถูกดำเนินคดีเพราะสิ่งที่โมเดลพูดก็สูงกว่ามาก ดูกรณีที่เยอรมนีพา Google ขึ้นศาลเพราะเนื้อหาที่โมเดลใส่ไว้ในหน้าผลการค้นหาก็ได้
      ดังนั้นผลประโยชน์ไม่ชัดเจน แต่ความเสี่ยงทางกฎหมายสูงมาก
    • EU ไม่มี ตลาดร่วม ที่แท้จริง โดยเฉพาะในตลาดทุน ต่อให้มีประชากรมากกว่าสหรัฐฯ และขนาดเศรษฐกิจรวมใหญ่กว่า ถ้าไม่สามารถรวบรวมทรัพยากรได้อย่างมีประสิทธิภาพ ก็ไม่มีความหมายมากนัก
      ในยุโรปจะระดมทุน 100 พันล้านดอลลาร์ ให้แล็บวิจัยใหม่แห่งเดียวได้ไหม? ถ้าไม่ได้ ก็จบแล้ว และยอมแพ้ได้เลย

  • บังเอิญจัง เช้านี้เพิ่งปล่อย OpenATP พอดี OpenATP เป็นแพ็กเกจ Python แบบโอเพนซอร์สและ CLI สำหรับ automated theorem prover แบบเอเจนต์
    รวมถึงรองรับ Leanstral ผ่าน Vibe harness ของ Mistral ด้วย โมเดล Leanstral สำหรับโปรดักชันตัวก่อนถูกเลิกใช้ไปเมื่อวันที่ 22 พฤษภาคม และจะอัปเดตแพ็กเกจให้ชี้ไปที่ Leanstral 1.5 ให้เร็วที่สุด
    GitHub: https://github.com/henryrobbins/open-atp
    Docs: https://open-atp.henryrobbins.com

  • 404 หรือเปล่า?
    https://web.archive.org/web/20260630223430/https://docs.mist...

  • ยังไม่ค่อยเข้าใจ นโยบายเรื่อง weights เท่าไร เว็บไซต์นี้บอกว่า weights ใช้ไลเซนส์ Apache เลยดูเหมือนเป็น weights แบบเปิด แต่หาลิงก์ดาวน์โหลดไม่เจอ
    โปรไฟล์ Hugging Face ดูเหมือนจะมีแค่สแนปช็อตก่อนหน้าเท่านั้น[0] มีใครรู้ไหมว่า weights ดาวน์โหลดได้หรือไม่ และถ้าได้ ดาวน์โหลดจากที่ไหน?
    [0] https://huggingface.co/mistralai/Leanstral-2603

  • ผมก็ขึ้น “Page not found” เหมือนกัน เข้าถึงได้แล้วเหรอ? เนื้อหาเกี่ยวกับอะไร?

    • ตามเว็บอาร์ไคฟ์: Leanstral 1.5 - 30 มิถุนายน 2026
      เป็น โมเดลวิศวกรรมพิสูจน์เชิงรูปแบบ Lean 4 ที่อัปเดตแล้ว และปรับแต่งมาเพื่อ automated theorem proving กับ autoformalization รวมพารามิเตอร์ทั้งหมด 119B ใช้งานจริง 6.5B
      https://web.archive.org/web/20260630223430/https://docs.mist...

  • การสนทนาเกี่ยวกับ Leanstral 1: https://news.ycombinator.com/item?id=47404796

  • Lean 4 และ Idris 2 ถูกประเมินค่าต่ำเกินไป และเพราะให้การรับประกันเพิ่มเติม จึงน่าจะเหมาะมากให้ LLM ใช้เขียนโค้ด

  • ตอนนี้ขึ้น 404

  • สมัครมาเพราะข่าวนี้เลย แต่ถ้าจะใช้ “Code” ต้อง เชื่อมต่อ GitHub ด้วยเหรอ? ดูจำกัดเกินไปมาก