Leanstral: เอเจนต์โอเพนซอร์สสำหรับวิศวกรรมโค้ดและการพิสูจน์เชิงรูปนัยที่เชื่อถือได้

 (mistral.ai)
1 คะแนน โดย GN⁺ 2026-03-17 | 1 ความคิดเห็น | แชร์ทาง WhatsApp
  • เอเจนต์โค้ดโอเพนซอร์สตัวแรกที่ออกแบบมาสำหรับ Lean 4 โดยมีเป้าหมายเพื่อทำให้ การพิสูจน์เชิงรูปนัย (formal proof) เป็นอัตโนมัติ เพื่อลดภาระการตรวจสอบของมนุษย์
  • เปิดเผยน้ำหนักโมเดลภายใต้ Apache 2.0 License และพร้อมใช้งานได้ทันทีผ่านสภาพแวดล้อม Mistral Vibe และ API endpoint ฟรี
  • ใช้สถาปัตยกรรมแบบ sparse ที่มี 6B active parameters เพื่อให้ได้ทั้งประสิทธิภาพและการลดต้นทุน พร้อมรองรับการเชื่อมต่อ MCP เช่น lean-lsp-mcp
  • บน FLTEval benchmark ทำคะแนนได้สูงกว่าโมเดลโอเพนซอร์สขนาดใหญ่อย่าง Qwen3.5, GLM5 และ Kimi-K2.5 และให้ประสิทธิภาพใกล้เคียงกับ Claude Sonnet ที่ต้นทุนถูกกว่ามากกว่า 15 เท่า
  • นำเสนอแนวทางใหม่ที่ผสาน ระบบอัตโนมัติของการพิสูจน์เชิงรูปนัยและการเพิ่มความน่าเชื่อถือของโค้ด ซึ่งมีศักยภาพทั้งในคณิตศาสตร์เชิงวิจัยและการพัฒนาซอฟต์แวร์ mission-critical

ภาพรวมของ Leanstral

  • Leanstral คือเอเจนต์โค้ดโอเพนซอร์สตัวแรกสำหรับ Lean 4 ที่ทำงานในสภาพแวดล้อม proof assistant สำหรับการพิสูจน์เชิงรูปนัย
    • Lean 4 สามารถใช้แสดงวัตถุทางคณิตศาสตร์ที่ซับซ้อน (เช่น perfectoid spaces) และข้อกำหนดของซอฟต์แวร์ได้
    • ต่างจากระบบพิสูจน์เดิมที่มักเน้นเพียง wrapper ของโมเดลทั่วไปหรือโจทย์เดี่ยว Leanstral ถูกฝึกมาให้ทำงานได้อย่างมีประสิทธิภาพใน formal repositories ที่ใกล้เคียงการใช้งานจริง
  • ใช้สถาปัตยกรรมแบบ sparse ที่มี 6B active parameters โดยผสาน parallel inference เข้ากับความสามารถในการตรวจสอบของ Lean
  • รองรับ MCP integration จึงเข้ากันได้กับโปรโตคอลที่ใช้บ่อยอย่าง lean-lsp-mcp

การเปิดเผยและการเข้าถึง

  • เปิดเผยน้ำหนักโมเดลภายใต้ Apache 2.0 License และให้ใช้งานในโหมดเอเจนต์ภายใน Mistral Vibe
  • ทุกคนสามารถเข้าถึงได้ผ่าน API endpoint ฟรี (labs-leanstral-2603) และมีแผนจะนำ feedback จากผู้ใช้ไปใช้ปรับปรุงโมเดลรุ่นถัดไป
  • เปิดเผยทั้ง technical report และ เครื่องมือประเมิน FLTEval เพื่อวัดประสิทธิภาพด้านวิศวกรรมการพิสูจน์จริง นอกเหนือจากการประเมินที่เน้นคณิตศาสตร์แบบเดิม

การประเมินประสิทธิภาพ (Evaluation)

  • ประเมินจากความสามารถในการทำการพิสูจน์เชิงรูปนัยทั้งหมดและนิยามแนวคิดทางคณิตศาสตร์ใหม่ให้เสร็จสิ้นในระดับ Pull Request ของโครงการ FLT
  • โมเดลที่ใช้เปรียบเทียบ: Claude Opus 4.6, Sonnet 4.6, Haiku 4.5, Qwen3.5 397B-A17B, Kimi-K2.5 1T-A32B, GLM5 744B-A40B

Leanstral เทียบกับโมเดลโอเพนซอร์ส

  • Leanstral-120B-A6B ทำได้ 26.3 คะแนน (pass@2) สูงกว่า GLM5 (16.6 คะแนน) และ Kimi-K2.5 (20.1 คะแนน)
  • ขณะที่ Qwen3.5 ได้ 25.4 คะแนนจากการรัน 4 ครั้ง (pass@4) Leanstral กลับทำคะแนนได้สูงกว่าโดยใช้จำนวนการรันเพียงครึ่งเดียว
  • สามารถสเกลแบบเชิงเส้นได้ถึง 29.3 คะแนน (pass@4) ที่ระดับต้นทุนเดียวกัน

Leanstral เทียบกับตระกูล Claude

  • มีคะแนนนำ Sonnet อยู่ 2.6 คะแนน (26.3 เทียบกับ 23.7) โดยมีต้นทุนการรันเพียง $36 เทียบกับ $549 หรือถูกกว่ามากกว่า 15 เท่า
  • ที่ระดับ pass@16 ทำได้ 31.9 คะแนน สูงกว่า Sonnet อยู่ 8 คะแนน
  • Claude Opus 4.6 ซึ่งเป็นรุ่นที่ทำผลงานดีที่สุด ได้ 39.6 คะแนน แต่มีต้นทุนสูงถึง $1,650 หรือสูงกว่า Leanstral 92 เท่า
  • benchmark ทั้งหมดรันในสภาพแวดล้อม Mistral Vibe โดยไม่มีการแก้ไขใด ๆ
โมเดล ต้นทุน($) คะแนน
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

กรณีศึกษา (Case Studies)

การรับมือกับการเปลี่ยนเวอร์ชันของ Lean

  • ป้อนคำถามจาก StackExchange ที่เกี่ยวกับข้อผิดพลาดจาก type alias ใน Lean 4.29.0-rc6
  • Leanstral สามารถจำลองสภาพแวดล้อมของปัญหาและวินิจฉัยปัญหาเรื่อง definitional equality ได้อย่างถูกต้อง
  • เสนอให้ใช้ abbrev แทน def เพื่อให้ rw tactic กลับมาทำงานได้ตามปกติ
  • อธิบายสาเหตุของปัญหาและเหตุผลของแนวทางแก้ไขให้ผู้ใช้อย่างชัดเจน

การให้เหตุผลเกี่ยวกับโปรแกรมและการแปลง

  • แปลงนิยามโปรแกรมของ Rocq ไปเป็น Lean พร้อมทั้งสร้าง user-defined notation
  • ตัวอย่างเช่น พิสูจน์ได้ว่าคำสั่ง plus2 ทำหน้าที่เพิ่มค่า 2 ให้กับตัวแปร X
  • ทำ theorem ใน Lean ให้สมบูรณ์และดำเนินการพิสูจน์โดยอาศัยเพียงข้อกำหนด Rocq ที่ให้มา

วิธีใช้งาน

  • Mistral Vibe integration: ใช้งานได้ทันทีด้วยคำสั่ง /leanstall
  • Labs API: เข้าถึงได้ฟรีหรือมีต้นทุนต่ำ
  • ดาวน์โหลดโมเดล: นำไปรันเองได้ภายใต้ Apache 2.0 License

ความสำคัญ

  • Leanstral คือความพยายามแบบโอเพนซอร์สครั้งแรกที่ผสาน การสร้างโค้ดและระบบอัตโนมัติของการพิสูจน์เชิงรูปนัย เข้าด้วยกัน
  • แสดงศักยภาพในการใช้งานกับ คณิตศาสตร์เชิงวิจัย การพัฒนาซอฟต์แวร์ที่ตรวจสอบได้ และการออกแบบระบบที่ต้องการความน่าเชื่อถือสูง
  • ถูกประเมินว่าเป็นโครงสร้างพื้นฐานใหม่สำหรับการตรวจสอบโค้ดที่ให้ทั้ง ความคุ้มค่าด้านต้นทุนและความเปิดกว้าง

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

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

 
GN⁺ 2026-03-17
ความคิดเห็นจาก Hacker News

  • น่าสนใจที่ตอนนี้ผู้คนเริ่มมองเห็นแพตเทิร์นที่ ระบุพฤติกรรมที่ต้องการให้เอเจนต์ทำ แล้วให้เขียนโค้ดให้ตรงกับสเปกนั้น
    ไม่ว่าจะใช้ TDD หรือเครื่องมือตรวจสอบแบบไหน เมื่อเวลาผ่านไป ชุดการตรวจสอบเหล่านี้ก็จะสะสมกลายเป็น คลังเอกสาร ที่รันได้และแสดงให้เห็นว่า “มันควรทำงานอย่างไร”
    แนวทางนี้ทรงพลังยิ่งกว่าสเปก Markdown ธรรมดามาก เพราะมันบันทึก พฤติกรรมในรายละเอียด เป็นโค้ด ไม่ใช่แค่เจตนา
    ยิ่งซอฟต์แวร์ซับซ้อนขึ้น การถ่ายทอดปากต่อปากแบบ “ไปถาม Jim สิ” ก็ยิ่งมีข้อจำกัด

    • รู้สึกว่าความต่างไม่ได้มากนัก ท้ายที่สุดโค้ดก็เป็นแค่อีกรูปแบบหนึ่งของข้อมูลที่อาจเขียนลงในไฟล์ .md ได้อยู่ดี
      ความละเอียดและบริบทมักหายไประหว่างการเปลี่ยนระดับความละเอียด
      ผมเห็นด้วยกับ TDD หรือการพัฒนาแบบยึดการตรวจสอบเป็นศูนย์กลาง แต่การเขียนสิ่งนั้นเป็นโค้ดไม่ใช่เป้าหมายสุดท้าย
      ตอนนี้มีชุดทดสอบอยู่แล้วหลายล้านบรรทัด ดังนั้นการ ต่อยอดจากสิ่งนั้น น่าจะเป็นทางที่สมจริงกว่า
    • พอมี AI ขึ้นมา ผมคิดว่าในที่สุด ความจริงที่ TDD เคยฝันไว้ ก็เริ่มเป็นไปได้
    • แนวทางนี้น่าสนใจ แต่โพสต์ในบล็อกทำให้งง
      อยากรู้ว่า Lean ช่วยอะไรได้จริง ๆ
      เช่นพิสูจน์ state machine ด้วย Lean แล้วค่อยย้ายไป Dart อะไรทำนองนั้นหรือเปล่า?
      ผมไม่ค่อยรู้จัก Lean เลยยังจับไม่ค่อยได้ว่านี่เป็นแนวทางที่ใช้งานได้จริงไหม

  • อย่างที่ถูกพูดถึงในพอดแคสต์ของ Jack Clark (ผู้ร่วมก่อตั้ง Anthropic) กับ Ezra Klein เมื่อไม่นานนี้ มีการพูดกันมากขึ้นว่า alignment ของโมเดล เป็นเรื่องสัมพัทธ์และความหลากหลายมีความสำคัญ
    แม้จะมีความเห็นว่าโมเดลของ Mistral ยังตามหลังโมเดลแนวหน้าตัวอื่น แต่การทดลองทั้งวิธี alignment และบริษัทที่หลากหลายก็สำคัญต่อระบบนิเวศ

    • ท้ายที่สุดผมคิดว่า เวลา จะเป็นตัวคลี่คลายเอง

  • กรณีความสำเร็จจริงนี้ทำให้นึกถึง Red Green TDD ของ Simon Willison
    ผมประทับใจกระบวนการที่ Leanstral สร้างโค้ดทดสอบเพื่อจำลองสภาพแวดล้อมที่ล้มเหลว และค้นพบปัญหา definitional equality

    • ถ้าเอเจนต์เขียนเทสต์ด้วยตัวเอง ความสามารถในการ รับประกันความถูกต้อง จะสูงกว่าการเขียนโค้ดกับเทสต์แยกกันหรือเปล่า ก็น่าสงสัย
    • ท้ายที่สุดแล้ว TDD ก็เหมือน prompt engineering เพราะมันคือกระบวนการให้เป้าหมายที่ชัดเจนกับเอเจนต์

  • โมเดลนี้ถูกฝึกมาให้เหมาะกับงานเฉพาะทาง แต่ ประสิทธิภาพยังด้อยกว่า Opus
    Opus แพงกว่า 6 เท่า แต่ก็ดูเหมือนจะคุ้มค่านั้น

    • ไอเดียดี แต่สุดท้าย คุณภาพสำคัญกว่าความน่าเชื่อถือ
      เข้าใจได้ที่สตาร์ตอัปยุโรปซึ่งมีทุนน้อยกว่าจะเจาะตลาดเฉพาะแบบนี้ แต่ก็ดูยากที่จะต่อยอดเป็นรายได้ก้อนใหญ่
    • ความน่าเชื่อถือของ benchmark อาจกำกวม แต่พอดูผล pass@2 หรือ pass@3 แล้วความประทับใจก็เปลี่ยนไป
      น่าจะน่าสนใจกว่าถ้าเทียบกับโมเดลอย่าง Codex
    • โมเดลนี้เป็น โอเพนซอร์ส จึงสามารถรันบนเครื่องโลคัลได้ นี่ไม่ใช่จุดสำคัญมากเลยหรือ?

  • ผมชอบคอนเซปต์เรื่อง “โค้ดที่เชื่อถือได้”
    แต่เกณฑ์เปรียบเทียบยังชวนสับสน พวกเขาเน้นว่าถูกกว่า Haiku แต่ Haiku เองก็ไม่ค่อยเก่งกับงานนี้ และ Leanstral ก็ยังแย่กว่านั้น
    ถ้าเป้าคือความแม่นยำ ผมไม่เข้าใจว่าการ “ถูกแต่ไม่ค่อยดี” จะสำคัญทำไม
    อย่างไรก็ดี Opus เองก็ไม่ได้สมบูรณ์แบบ ดังนั้นถ้าขยายสเกลได้ ผลลัพธ์อาจดีขึ้นก็ได้

    • จากกราฟจะเห็นว่ายิ่งเพิ่มจำนวน pass ประสิทธิภาพก็ยิ่งดีขึ้น
      ที่ 2 รอบมันดีกว่า Haiku และ Sonnet และที่ 16 รอบก็เข้าใกล้ Opus พร้อมกับมี ความคุ้มค่าต่อราคา สูงกว่า
    • จริง ๆ ก็ง่ายมาก — แค่ใส่ในพรอมป์ต์ว่า “เอาเฉพาะเอาต์พุตที่เชื่อถือได้” ก็พอ

  • สำหรับคนที่ไม่รู้จัก Lean ผมสงสัยว่ามันมีคุณค่าโดยตรงหรือเปล่า
    มันคือการแนบการพิสูจน์เข้ากับโค้ดภาษาอย่าง Go แบบอัตโนมัติ หรือแค่เป็นเรื่องของการสนับสนุน ความหลากหลายของโมเดลแบบเปิด เท่านั้น?

    • น่าจะเป็นโครงสร้างที่เอเจนต์สร้างสเปก Lean4 แล้วใช้สเปกนั้นเป็นเกณฑ์ประเมินซอฟต์แวร์
      แต่สุดท้ายสเปก Lean4 เองก็กลายเป็น ซอฟต์แวร์อาร์ติแฟกต์
      ถ้าอย่างนั้นก็ย้อนกลับไปสู่ปัญหาว่าสเปกนั้นถูกต้องหรือไม่ — สุดท้ายก็ยังต้องมี การตรวจทานโดยมนุษย์

  • ผมคาดกระแสแบบนี้ไว้ตั้งแต่หลายสัปดาห์ก่อน และก็ดีใจที่มันเป็นจริง
    ในยุค LLM ความเป็นมิตรต่อมนุษย์ของโค้ดอาจสำคัญน้อยกว่า ความสามารถในการพิสูจน์และประสิทธิภาพด้านโทเค็น
    Lean กับ Rust อาจถูกผสานเข้าด้วยกันจนเกิดโลกที่ “คอมไพล์ได้เฉพาะโค้ดที่พิสูจน์แล้ว”
    มีสรุปการถกเถียงที่เกี่ยวข้องไว้ในคอมเมนต์ก่อนหน้า

    • แต่ระบบพิสูจน์ใด ๆ ก็ไม่ได้รับประกันว่าเป็น “การพิสูจน์ที่ถูกต้อง”
      มันเพียงรับประกันว่า ใช้ตรรกะได้อย่างถูกต้อง (valid) เท่านั้น
      การเข้าใจอย่างถ่องแท้ว่าการพิสูจน์นั้นกำลังพิสูจน์อะไร ยากพอ ๆ กับการทำความเข้าใจโปรแกรม แต่กระบวนการนี้ก็มีข้อดีตรงที่ช่วยให้คิดได้ลึกขึ้น

  • น่ายินดีที่พวกเขาไม่ได้แค่พูดคำว่า “โอเพนซอร์ส” แต่ปล่อย weights ภายใต้ไลเซนส์ Apache-2.0 ออกมาจริง

    • แต่ถ้าวัดตามมาตรฐานของชุมชน ถ้ายังสร้างโมเดลขึ้นมาใหม่ซ้ำไม่ได้ มันก็เป็นแค่ “open weights” ไม่ใช่ “open source”

  • ตาม ข่าวอย่างเป็นทางการของ Mistral
    Claude Opus มีต้นทุน 1,650 ดอลลาร์และได้คะแนน 39.6,
    Leanstral pass@8 อยู่ที่ 145 ดอลลาร์และได้ 31.0, pass@16 อยู่ที่ 290 ดอลลาร์และได้ 31.9
    ดังนั้น ประสิทธิภาพต่อราคาที่จ่าย จึงค่อนข้างสูง