Mistral เปิดตัว Leanstral: Code Agent โอเพนซอร์สตัวแรกสำหรับ Lean4 ที่สามารถสร้างโค้ดพร้อมกับผลลัพธ์การพิสูจน์ที่เป็นทางการ

ข่าวจากเว็บไซต์币界网 โดยอ้างอิงข้อมูลจาก 1M AI News รายงานว่า Mistral AI ได้เปิดตัว Leanstral ซึ่งเป็นเอเจนโอเพนซอร์สตัวแรกที่ออกแบบมาเพื่อเครื่องมือการตรวจสอบเชิงฟอร์มาลาโดยเฉพาะสำหรับ Lean 4 ในวันนี้ จุดสำคัญของการสร้างโค้ดด้วย AI คือการตรวจสอบโดยมนุษย์ ซึ่ง Leanstral ช่วยให้ AI สร้างโค้ดพร้อมกับแสดงหลักฐานเชิงฟอร์มาลาที่สามารถตรวจสอบโดยอัตโนมัติด้วย Lean 4 ได้โดยไม่ต้องพึ่งพาการตรวจสอบด้วยมนุษย์ โมเดลใช้สถาปัตยกรรม MoE แบบ sparse มีพารามิเตอร์รวม 120B และพารามิเตอร์เปิดใช้งาน 6B เปิดให้ใช้งานแบบ Apache 2.0 และได้รับการฝึกฝนและปรับแต่งเฉพาะสำหรับ lean-lsp-mcp สามารถเริ่มต้นใช้งานใน Mistral Vibe ได้โดยไม่ต้องตั้งค่าใด ๆ (คำสั่ง /leanstall) หรือเรียกผ่าน API ฟรีที่ปลายทาง labs-leanstral-2603 รองรับการดาวน์โหลดและติดตั้งเอง สำหรับโมเดลที่เปิดเผย โครงสร้าง Qwen3.5-397B-A17B ต้องรัน 4 ครั้งจึงจะได้คะแนน 25.4 ซึ่งยังต่ำกว่า Leanstral pass@2 ที่ได้ 26.3 ด้วยค่าใช้จ่ายเพียง $36 เท่านั้น ขณะที่ Claude Sonnet 4.6 ทำได้ 23.7 คะแนนในราคา $549 และ pass@16 ได้ 31.9 คะแนนในราคา $290 ซึ่งนำหน้า Sonnet 8 คะแนน ส่วน Claude Opus 4.6 ต้องใช้เงินถึง $1,650 จึงจะได้คะแนน 39.6