การพิสูจน์ทฤษฎีก็เริ่มแข่งขันเรื่องต้นทุน: Mistral เปิดซอร์ส Leanstral 1.5, แต่ละข้อประมาณ 4 ดอลลาร์สหรัฐ

จาก การติดตามของ Movee Beating ระบุว่า Mistral AI ได้เปิดตัว Leanstral 1.5 ซึ่งเป็นโมเดลสำหรับการพิสูจน์เชิงรูปนัยใน Lean 4 โมเดลมีพารามิเตอร์ทั้งหมด 119,000 ล้าน พารามิเตอร์ที่ถูกเปิดใช้งานประมาณ 6,500 ล้าน ใช้สัญญาอนุญาต Apache-2.0 และให้บริการ API ฟรี

การประเมินอย่างเป็นทางการแสดงให้เห็นว่า Leanstral 1.5 สามารถแก้ปัญหา PutnamBench 587 ข้อจากทั้งหมด 672 ข้อ ในเกณฑ์มาตรฐานพีชคณิตนามธรรม FATE-H และ FATE-X ทำคะแนนได้ 87% และ 34% ตามลำดับ สร้างสถิติที่ดีที่สุดในกลุ่มโมเดลประเภทเดียวกัน

ต้นทุนการแก้ปัญหาเฉลี่ยของ Leanstral 1.5 ใน PutnamBench อยู่ที่ประมาณ 4 ดอลลาร์สหรัฐ ซึ่งต่ำกว่าระบบก่อนหน้านี้หลายสิบถึงหลายร้อยดอลลาร์ เมื่อเพิ่มงบประมาณ token ต่อข้อ จำนวนข้อที่แก้ได้เพิ่มขึ้นอย่างต่อเนื่อง ในการพิสูจน์ความซับซ้อนของ AVL tree โมเดลใช้การอนุมาน token มากกว่า 2.7 ล้านครั้งและการบีบอัดบริบท 22 ครั้ง ก่อนจะเสร็จสิ้นการพิสูจน์ที่เกี่ยวข้อง

นอกเหนือจากการพิสูจน์ทางคณิตศาสตร์แล้ว Leanstral 1.5 ยังถูกใช้ในการตรวจสอบโค้ด ทีมงานค้นพบข้อบกพร่องจริง 11 รายการในคลัง Rust แบบโอเพนซอร์ส 57 แห่ง ซึ่งในจำนวนนี้ 5 รายการไม่เคยถูกรายงานมาก่อน
news.article.disclaimer
แสดงความคิดเห็น
0/400
ไม่มีความคิดเห็น