Leanstral 1.5: ความอุดมสมบูรณ์ของการพิสูจน์สำหรับทุกคน

 (mistral.ai)
1 คะแนน โดย GN⁺ 4 시간 전 | 1 ความคิดเห็น | แชร์ทาง WhatsApp
  • ท่ามกลางแนวโน้มที่ต้องการนำการตรวจพิสูจน์เชิงรูปแบบมาใช้ให้ใกล้กับงานพัฒนาจริงมากขึ้น Mistral AI ได้เปิดตัว Leanstral 1.5 โมเดลภายใต้ Apache-2.0 สำหรับ Lean 4
  • โมเดลนี้มีพารามิเตอร์รวม 119B โดยเปิดใช้งานเพียง 6B และผ่านการฝึกช่วงกลาง, supervised fine-tuning และ reinforcement learning แบบ CISPO เพื่อเรียนรู้ทั้งการเขียนบทพิสูจน์และงานกับโค้ดรีโพซิทอรี
  • ทำสถิติ miniF2F 100%, PutnamBench 587/672, FATE-H 87%, FATE-X 34% แสดงให้เห็นประสิทธิภาพที่แข็งแกร่งทั้งในเบนช์มาร์กการพิสูจน์ทางคณิตศาสตร์และการประเมินวิศวกรรมการพิสูจน์ในโลกจริง
  • ในการตรวจสอบโค้ดจริง โมเดลพิสูจน์เวลาเชิงซับซ้อน O(log n) ของ AVL tree ได้ และผ่าน Rust-to-Lean pipeline สามารถพบบั๊กจริง 11 รายการจาก 57 รีโพซิทอรี
  • มีการเผยแพร่น้ำหนักโมเดลและ API ฟรี leanstral-1-5 ทำให้นำไปใช้กับ วิศวกรรมการพิสูจน์เชิงปฏิบัติ เช่น theorem proving, proof debugging และการมีส่วนร่วมกับรีโพซิทอรีได้ทันที

การเปิดตัว Leanstral 1.5 และคุณลักษณะของโมเดล

  • Leanstral 1.5 เป็นโมเดลที่สร้างขึ้นเพื่อทำงานด้านวิศวกรรมการพิสูจน์บน Lean 4
  • ใช้ไลเซนส์ Apache-2.0 และมีขนาดรวม 119B พารามิเตอร์ โดยมี 6B active parameters
  • ยกระดับความสามารถด้าน formal verification ให้ใช้งานได้ไม่เพียงกับเบนช์มาร์กคณิตศาสตร์ แต่ยังรวมถึงการตรวจสอบคุณสมบัติของโค้ดจริง
  • โมเดลทำ miniF2F ได้เต็ม, แก้ PutnamBench ได้ 587 ข้อจาก 672 ข้อ และทำ FATE-H 87%, FATE-X 34%

การฝึก 3 ขั้นที่เรียนรู้จากฟีดแบ็กของการพิสูจน์

  • การฝึกประกอบด้วย 3 ขั้น ได้แก่ การฝึกช่วงกลาง, supervised fine-tuning และ reinforcement learning แบบ CISPO
  • ในการเสริมกำลังใช้สภาพแวดล้อม 2 แบบ
    • สภาพแวดล้อมแบบหลายเทิร์น: โมเดลรับข้อความทฤษฎีบทแล้วทำการพิสูจน์หรือหักล้าง จากนั้นปรับแก้บทพิสูจน์ซ้ำโดยอิงจากฟีดแบ็กของ Lean compiler
    • หากบทพิสูจน์คอมไพล์ผ่านจะถือว่าสำเร็จ หากไม่สำเร็จลูปจะทำต่อไปจนกว่าจะแก้โจทย์ได้หรือใช้งบประมาณหมด
    • สภาพแวดล้อม code agent: แก้ไขไฟล์ใน raw filesystem เหมือนนักพัฒนา รันคำสั่ง bash และตรวจดูเป้าหมาย, ข้อผิดพลาด และข้อมูล type แบบเรียลไทม์ผ่าน Lean language server
  • สภาพแวดล้อม code agent รองรับงานยาว เช่น การเติมบทพิสูจน์บางส่วนในรีโพซิทอรี การเขียน lemma ช่วย และการทำงานต่อเนื่องแม้ผ่านการบีบอัดบริบทหลายครั้ง
  • ความถูกต้องสุดท้ายของคำตอบจะตรวจเทียบกับรายการทฤษฎีบทเป้าหมายใน SafeVerify fork ของ Mistral

เบนช์มาร์กด้านคณิตศาสตร์และวิศวกรรมการพิสูจน์

  • การประเมินใช้ miniF2F, PutnamBench, FATE-H/FATE-X และ FLTEval
    • miniF2F เป็นเบนช์มาร์กคณิตศาสตร์เชิงรูปแบบที่ครอบคลุมตั้งแต่โจทย์พื้นฐานไปจนถึงระดับ IMO
    • PutnamBench ประกอบด้วยโจทย์ 672 ข้อจากการแข่งขัน Putnam Mathematical Competition
    • FATE-H และ FATE-X เป็นเบนช์มาร์กพีชคณิตนามธรรมระดับบัณฑิตศึกษาและปริญญาเอกตามลำดับ
    • FLTEval ใช้ pull request จริงจากรีโพซิทอรี Fermat’s Last Theorem เพื่อวัดความยากของงานวิศวกรรมการพิสูจน์
  • บน miniF2F โมเดลทำได้ 100% ทั้งใน validation set และ test set
  • สำหรับ PutnamBench และ FATE-H/X มีการเปรียบเทียบกับ Goedel-Architect, Seed-Prover 1.5 high และ AxProverBase โดยไม่มี natural language proof guide
  • ประสิทธิภาพบน FATE-H/X: {b:87,34}
  • FATE-H ทำได้ 87% และ FATE-X ทำได้ 34% ซึ่งเป็นสถิติสูงสุดใหม่
  • บน PutnamBench โมเดลแก้โจทย์ได้มากกว่า Seed-Prover 1.5 high อยู่ 7 ข้อ โดยมีต้นทุนราว 4 ดอลลาร์ ต่อข้อ
    • การตั้งค่า high ของ Seed-Prover ใช้งบประมาณ 10 H20-days ต่อข้อ และคาดว่ามีต้นทุนเกิน 300 ดอลลาร์
    • ตัวพิสูจน์บางตัวที่อยู่อันดับสูงกว่าทำงานภายใต้เงื่อนไขอื่น เช่น ได้รับ natural language proof guide หรือมีต้นทุน 54–68 ดอลลาร์ต่อข้อแบบ Aleph Prover

การขยายตัวภายใต้งบประมาณการให้เหตุผลระยะยาวและ FLTEval

  • Leanstral 1.5 บน PutnamBench มี Pass@8 ที่เพิ่มขึ้นอย่างราบรื่นและเป็นทิศทางเดียวเมื่อเพิ่มงบประมาณโทเคน
  • ในการทดลองที่เพิ่มงบประมาณโทเคนต่อความพยายามจาก 25k เป็น 4M จำนวนโจทย์ที่แก้ได้เพิ่มขึ้นดังนี้
    • 50k โทเคน: 44 ข้อ
    • 200k โทเคน: 244 ข้อ
    • 1M โทเคน: 493 ข้อ
    • 4M โทเคน: 587 ข้อ
  • ความสามารถในการให้เหตุผล แก้ไขไฟล์ และปรับแก้อย่างต่อเนื่องข้ามหลายล้านโทเคนโดยไม่หยุดกลางทาง เป็นปัจจัยที่ช่วยยกระดับประสิทธิภาพ
  • FLTEval ก็ถูกเปิดซอร์สเต็มรูปแบบเช่นกัน
  • บน FLTEval, Leanstral 1.5 ยกระดับ pass@1 จาก 21.9 เป็น 28.9 และ pass@8 จาก 31.9 เป็น 43.2
  • ค่า pass@8 ที่ 43.2 สูงกว่า 39.6 ของ Opus 4.6 ขณะที่ต้นทุนอยู่เพียงประมาณหนึ่งในเจ็ด
  • โมเดลนี้ยังทำได้ดีกว่าโมเดลโอเพนซอร์สบางตัวที่มีขนาดใหญ่กว่า 3–10 เท่า

กรณีศึกษาการตรวจสอบโค้ดจริง

  • การพิสูจน์เวลาเชิงซับซ้อนของ AVL tree

    • AVL tree เป็น self-balancing binary search tree ที่รักษาความสูง O(log n) ผ่านการ rebalance ระหว่างการแทรกและการลบ
    • Leanstral 1.5 ตรวจพิสูจน์ได้ว่าการแทรกและการลบใน implementation จริงมีความซับซ้อน O(log n)
    • งานนี้ต้องใช้ structural induction ที่สะท้อนโครงสร้างรีเคอร์ซีฟของต้นไม้, การติดตามเวลาด้วย monad และการวิเคราะห์กรณีทั้งหมดของเส้นทางการ rebalance
    • บทพิสูจน์ดำเนินไปผ่านโทเคนมากกว่า 2.7 ล้านรายการและ การบีบอัดบริบท 22 ครั้ง
    • Leanstral คลี่แต่ละชั้นของ TimeM monad อย่างเป็นระบบเพื่อเผยให้เห็นการคำนวณที่ผสมอยู่กับ control flow
    • สำหรับการแทรก โมเดลตั้งขอบเขตไว้ที่ 48 สเต็ปต่อหน่วยความสูง พร้อมเทอมคงที่ที่ใกล้เคียง และเชื่อมความสูงของต้นไม้เข้ากับขนาดต้นไม้ในความสัมพันธ์แบบลอการิทึม

  • การหาบั๊กในโค้ด Rust

    • การทดลองตรวจจับบั๊กประกอบด้วย pipeline ที่ Aeneas แปลงโค้ด Rust เป็น Lean แล้วให้ Leanstral อนุมานเจตนาของผู้ใช้จากโค้ดเพื่อสร้างคุณสมบัติด้านความถูกต้อง
    • Leanstral พยายามพิสูจน์แต่ละคุณสมบัติ 4 ครั้ง และหากล้มเหลวทั้งหมดจะพยายามพิสูจน์ปฏิเสธของมันอีก 4 ครั้ง
    • จาก 57 รีโพซิทอรี พบคุณสมบัติที่ละเมิด 47 รายการ และในนั้น 11 รายการเป็นบั๊กจริง
    • ในบรรดาบั๊กจริง มี 5 รายการที่ไม่เคยถูกรายงานบน GitHub มาก่อน
    • พบกรณีหนึ่งในฟังก์ชัน sign ของ zigzag decoding ในไลบรารี datrs/varinteger
    • เมื่ออินพุตเป็น Std.U64.MAX นิพจน์ (value + 1) จะเกิด overflow
    • ในโหมดดีบักจะเกิดแครช และในโหมดรีลีสจะเกิดความเสียหายของข้อมูลแบบเงียบ
    • edge case นี้เป็นกรณีที่การทดสอบทั่วไปและการทำ fuzzing มักพลาดได้ง่าย

การเผยแพร่และวิธีใช้งาน

  • น้ำหนักโมเดลเผยแพร่บน Hugging Face
  • API endpoint ฟรีมีให้ใน model card ภายใต้ชื่อ leanstral-1-5
  • สภาพแวดล้อมที่แนะนำสำหรับการใช้งานคือ Mistral Vibe
  • ขั้นตอนเริ่มต้นคือ ตั้งค่า Mistral Vibe, ติดตั้ง Leanstral 1.5, รัน agent, ติดตั้ง Lean LSP MCP เพิ่มเติมถ้าต้องการ แล้วเริ่มงานพิสูจน์
  • แนะนำให้ติดตั้ง Lean LSP MCP โดยเพิ่มลงใน ~/.vibe/config.toml
  • หากยังไม่มี MCP server เดิม อาจต้องลบบรรทัด mcp_servers = []
  • Leanstral สามารถใช้กับงานแก้ theorem, proof debugging และการมีส่วนร่วมกับรีโพซิทอรี

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

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

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

  • คำวิจารณ์ที่ว่า Mistral แข่งขันกับโมเดลขนาดใหญ่ได้ยากนั้นสมเหตุสมผล แต่ในความเป็นจริง ผมมองว่าพวกเขากำลังโฟกัสกับการ ให้ความสามารถเฉพาะบางอย่างในโมเดลขนาดเล็กด้วยคุณภาพสูง
    ผมใช้ Mistral กับงานอย่าง OCR หรือการวิเคราะห์ไฟล์ และถ้าเติมเงินไว้ในบัญชี 100 ดอลลาร์ ก็ใช้งานได้เป็นปีโดยไม่ต้องกังวลเรื่องปริมาณคำขอ
    ต้นทุนต่ำมาก จึงยังมีคุณค่ามากพอ แม้จะแข่งขันกับ Opus 4.8 ไม่ได้ก็ตาม

    • อยากรู้ว่าในงาน OCR จริง ๆ แล้วแข่งขันได้แค่ไหน
      คุณภาพพอใช้ในราคาถูก ดูเหมือนเป็นตลาดเฉพาะทางมากกว่า เมื่อเทียบกับการยอมจ่ายแพงกว่า 10 เท่าเพื่อใช้คุณภาพสูงสุดเพื่อลดความผิดพลาดในภายหลัง
    • พวกคนยุโรปโง่ ๆ กำลัง optimize เพื่อ สร้างผลิตภัณฑ์ที่ดี แทนที่จะ optimize เพื่อหาเงินให้ได้มากที่สุดสินะ /s
    • ผมไม่แน่ใจว่า “ประมวลผลเอกสารได้หนึ่งปีในราคาต่ำกว่า 100 ดอลลาร์ต่อปี” จะยอดเยี่ยมอย่างที่คิดหรือไม่ อย่างน้อยในมุมของ ความสามารถในการแข่งขันของยุโรป ก็เท่ากับว่า Mistral ตั้งเพดานรายได้ไว้ต่ำเกินไป
      OCR แทบจะกลายเป็นสินค้าโภคภัณฑ์ไปแล้ว และก็มีให้เป็นพื้นฐานทั้งในโมเดลโอเพนซอร์สหรือบริการอย่าง AWS
      อีกทั้งป้ายราคา 100 ดอลลาร์ต่อปีทำให้สร้างความภักดีได้ยาก และไม่มีต้นทุนในการย้ายแพลตฟอร์ม ถ้ามีราคาที่ต่ำกว่านี้ ลูกค้าก็อาจย้ายออกทันที
      ถ้าเป็นเครื่องมือราคาถูกที่ลอกเลียนได้ง่ายและไม่มีการล็อกอินลูกค้า มันก็ใกล้เคียงกับฟีเจอร์มากกว่าธุรกิจ
      จากมุมของผู้ซื้อก็ดีอยู่ แต่ถ้าต้องการให้บริษัทยุโรปแข่งขันกับคู่แข่งทั่วโลกในระยะยาวด้วยขีดความสามารถของผลิตภัณฑ์ นี่ดูเป็นกลยุทธ์ที่แย่

  • ตัวงานเองดี แต่ ตัวอย่างการพบบั๊ก รู้สึกแปลก ๆ
    เขาบอกว่าในฟังก์ชัน sign ของการถอดรหัส zigzag เมื่ออินพุตเป็น Std.U64.MAX แล้ว (value + 1) จะ overflow ทำให้โหมด debug แครช ส่วนโหมด release เกิดความเสียหายแบบเงียบ ๆ แต่ผมไม่แน่ใจว่าจะเรียกสิ่งนี้ว่าเงื่อนไขขอบเขตที่การทดสอบ “มักพลาด” ได้ไหม
    ถ้าเป็นเทสต์แย่ ๆ ก็อาจพลาด แต่คนที่รอบคอบหรือระบบเขียนโค้ดที่ใช้ machine learning มักทำเรื่อง “ควรทดสอบค่าขีดสุด” ได้ค่อนข้างดี โดยเฉพาะถ้าเป็นโค้ดที่ parse อินพุตจากผู้ใช้
    เลยสงสัยว่าพวกเขาเจอบั๊กที่น่าสนใจกว่านี้ด้วยหรือเปล่า แต่หยิบตัวอย่างนี้มาเพราะอธิบายอย่างรวดเร็วได้ยาก

    • โดยเฉพาะส่วนที่บอกว่า “แม้แต่ fuzzing ก็พลาด” นั้นแปลกมาก fuzzing ที่ผมเห็นโดยทั่วไปมักสำรวจค่าขอบเขตอย่างตั้งใจ
      ถ้าเป็นไลบรารี encoding แบบนี้ การคาดหวังพื้นฐานของโค้ดที่ดีคือควรทำ fuzzing และแทบจะแน่นอนว่าน่าจะจับได้ภายในไม่กี่วินาที
      ผมลองทำเทสต์ round-trip ง่าย ๆ ด้วย proptest ก็เจอความล้มเหลวหลายสิบรายการภายในไม่ถึง 1 วินาที และได้ผลลัพธ์ด้านล่าง:
      thread 'signed_round_trip' (50528) panicked at tests/test.rs:72:1:
      Test failed: attempt to multiply with overflow.
      minimal failing input: value = 4611686018427387904
      successes: 2
      local rejects: 0
      global rejects: 0
    • คงพูดยากว่า “มักพลาด” แต่ในเมื่อมันมีอยู่จริง ก็ถือเป็น บั๊กที่บางครั้งถูกพลาด ได้เหมือนกัน
      ข้อดีที่เห็นได้คือเมื่อใช้ Lean ก็ลดความจำเป็นในการต้องเลือกอย่างชาญฉลาดว่าจะทดสอบตัวอย่างใด
    • นี่คือ การประกันคุณภาพ ขั้นพื้นฐาน ถ้าเทสต์พลาดเรื่องแบบนี้ ประโยชน์ของมันก็คงจำกัดกว่าที่เราคาดหวังกันตามปกติมาก
      เริ่มสงสัยภูมิหลังของผู้เขียน
    • นี่ก็แค่การประชาสัมพันธ์ขยะ ๆ
      ระบบ property-based testing ทุกตัวที่ถูกคิดค้นมาตั้งแต่ราวปี 1980 ล้วนสำรวจค่าขอบเขต
      การทดสอบจริงอาจยากเพราะความหมายเชิง semantics ของ C และ C++ หรือการไม่มี semantics ที่ชัดเจน เพราะคอมไพเลอร์สามารถถือว่า “ทดสอบผ่าน” สำหรับอินพุตทุกอย่างที่นำไปสู่พฤติกรรมที่ไม่ได้กำหนดได้

  • กลางบทความมีการเปรียบเทียบกับ LLM ระดับแนวหน้าหลายตัว แต่ทั้งหมดเป็นโมเดลเมื่อครึ่งปีก่อน
    ฟังดูค่อนข้างตลกในทำนองว่า “โมเดลใหม่ของเราดีกว่า โมเดลจีนเมื่อ 3 รุ่นก่อน”

    • นี่เป็น โมเดลพารามิเตอร์ 6 พันล้านตัว จึงเป็นคนละระดับกันเลย กลับกัน ผมยิ่งคาดหวังกับ “โมเดลภาษาขนาดเล็กระดับแนวหน้า” มากกว่า
    • เห็นด้วย แต่แค่เป็น open weights และมีขนาดค่อนข้างเล็กก็พอเป็นข่าวพาดหัวได้แล้ว โมเดลนี้รันได้ค่อนข้างดี

  • ไลบรารีนั้นคือ https://github.com/datrs/varinteger
    ปัญหาเดียวกันถูกโพสต์ใน repository นี้ไว้แล้วหนึ่งสัปดาห์ก่อนที่ paper จะเผยแพร่ ดังนั้นน่าจะใช่: https://github.com/datrs/varinteger/issues/8
    ไม่รู้ว่าคนนี้เป็นพนักงานของ Leanstral หรือว่า Leanstral แค่หยิบ issue นี้มาใช้
    ไลบรารีนี้เล็ก เทสต์แย่อย่างน่าประหลาดใจ และแทบไม่ได้ถูกแตะต้องมา 8 ปีแล้ว: https://github.com/datrs/varinteger/blob/master/tests/test.r...
    ยอดดาวน์โหลดดูค่อนข้างต่ำ ประมาณวันละ 1,000 ครั้ง: https://crates.io/crates/varinteger
    ดังนั้นจึงมองยากว่านี่เป็นความสำเร็จที่ยิ่งใหญ่พอจะยกมาเป็นตัวอย่างเดียวได้ การตรวจจับอัตโนมัติมีประโยชน์จริง แต่ไม่แน่ใจว่านี่ถือเป็นผลงานที่น่าจับตาในสาขาย่อยนี้หรือไม่
    ผมไม่เคยใช้ LLM สำหรับเขียน proof แต่ข้อมูลฝึกดูจะมีค่อนข้างน้อย จึงไม่น่าแปลกใจถ้ามันจะหยาบกว่าโมเดลเขียนโค้ดทั่วไป
    อนึ่ง https://crates.io/crates/varinteger แสดงเป็น https://github.com/mafintosh/varinteger-rs แต่ URL นี้ redirect ไปยัง https://github.com/datrs/varinteger ดังนั้นดูเหมือนจะเป็นไลบรารีเดียวกันแม้ภายนอกจะดูต่างกัน

    • ปัญหาของ proof คือบางครั้งการสื่อสารคุณค่านั้นทำได้ยาก
      ประเด็นหลักไม่ใช่การหาบั๊ก แต่คือการพิสูจน์ว่าไม่มีบั๊กบางชนิดภายใต้สมมติฐานบางอย่าง
      แต่เรื่องนี้ขายยาก ฝ่ายการตลาดจึงมักไหลไปทาง “เราพบบั๊กนี้”

  • จะมีประโยชน์กับคนที่ไม่รู้จัก Lean เลยไหม? อยากตรวจสอบซอฟต์แวร์ที่กำลังทำอยู่ แต่ไม่มีประสบการณ์ด้าน formal verification
    สงสัยว่ามีแค่สเปก โค้ด และเวลาเรียนรู้ที่จำกัด จะได้ผลลัพธ์ที่พอใช้ได้หรือไม่

    • ต้องเข้าใจส่วนที่ต้องการพิสูจน์เอง แต่ไม่จำเป็นต้องเข้าใจกระบวนการพิสูจน์ทั้งหมด
      ให้ความรู้สึกใกล้กับการอ่าน type ของ Haskell มากกว่าคณิตศาสตร์ และเหมือนแค่ยืมคำศัพท์จากคณิตศาสตร์มาใช้เยอะ
    • ถ้าอ่านส่วน “Bug Discovery: Finding Hidden Flaws” ในบทความ ดูเหมือนว่าเริ่มจากมีแค่โค้ด Rust แล้วใช้โมเดลช่วยค้นหาปัญหาใน Rust แบบโอเพนซอร์ส
      อาจคุยให้ช่วยเขียน โค้ด Lean สำหรับตรวจสอบแอปพลิเคชันได้ด้วย แต่ก็ยังไม่แน่ใจ
    • อย่างน้อยต้องเข้าใจว่าอยากพิสูจน์ theorem อะไรเกี่ยวกับโค้ด และจะสื่อมันใน Lean อย่างไร
      ไม่เช่นนั้นก็ตรวจสอบเอาต์พุตไม่ได้
      ในเชิงกลไก อาจพิสูจน์ proposition บางอย่างที่ถูกตรวจแล้วว่าถูกต้องได้ แต่ถ้าไม่รู้ว่า proposition นั้นหมายถึงอะไร หรือครอบคลุมสิ่งที่ต้องการตรวจสอบจริงหรือไม่ ก็ไม่มีความหมาย
    • จากที่ไม่รู้จัก Lean4 เลย ใช้เวลาราว 6 เดือนจนมาถึงระดับที่เขียนโค้ดส่วนใหญ่ด้วย Lean4 ได้ และกระบวนการนี้เร็วขึ้นมากเพราะ AI ช่วย
      น่าทึ่งมากที่โมเดลต่าง ๆ ใช้ Lean4 ได้คล่องและสม่ำเสมอขนาดไหน ไม่ใช่แค่โมเดลระดับแนวหน้าเท่านั้น แต่โมเดล local ขนาดเล็กก็เช่นกัน รู้สึกว่า LLM เข้าใจ Lean4 ได้ดีโดยธรรมชาติ
      ยังเหลือทางอีกไกลกว่าจะเรียกตัวเองว่าเป็นผู้เชี่ยวชาญ Lean4 ได้ แต่ตอนนี้ไม่จำเป็นต้องพึ่งตัวช่วยเพื่อสร้างโปรแกรมที่มีประโยชน์แล้ว
      แม้มีความรู้แทบไม่มีเลย การที่สามารถเชื่อถือส่วนที่ยังไม่เข้าใจทั้งหมดได้ช่วยเร่งความเร็วในการเรียนรู้ขึ้นมาก การได้โปรแกรมที่พึ่งพาได้แม้มีความรู้ไม่สมบูรณ์นั้นใช้งานได้จริงและช่วยสร้างแรงจูงใจด้วย
      รู้สึกเหมือนขีดจำกัดไม่ได้อยู่ที่ขั้นตอนพิสูจน์ระหว่างทางทั้งหมด แต่อยู่ที่ส่วนของภาษาที่ใช้อธิบาย axioms และผิวหน้าของ proposition ของตัวเอง เมื่อเวลาผ่านไป หากจะทำได้มากขึ้นก็ต้องเข้าใจมากขึ้น แต่ในอีกความหมายหนึ่ง เราสามารถทำงานได้อย่างปลอดภัยในระดับ N+1
      Lean4 เป็นภาษาโปรแกรมที่สนุกแม้แยกจากบทบาท theorem prover และยังเร็วอย่างน่าประหลาดใจด้วย
      ใช้เชื่อมกับ io_uring อยู่ และในหลายกรณีเร็วกกว่า C++/libuv หรือ Rust/Tokio มาก
      บางครั้งถ้าเห็นหางยาวมากในค่าอย่าง latency p99.99 ก็ต้องจูน เช่นเปลี่ยนตัวเลขเป็นความกว้างคงที่ แต่ C++ กับ Rust ก็ต้องจูนเหมือนกัน

  • น่าสนใจที่ผลักดัน Lean 4 เพื่อใช้กับ formal verification
    คิดว่าโดเมนนี้เป็นของ Isabelle/HOL กับ TLA+ เสียอีก
    อย่างน้อยก็น่าจะคาดหวังโมเดลที่ฝึกให้ใช้ทั้งสามอย่างได้ สำหรับการอนุมานไปข้างหน้าในพีชคณิตเชิงเส้น Isabelle/Isar ก็ดูดีกว่าด้วย ใครอธิบายได้ไหม?

    • เป็นความจริงที่ Lean ถูกนำไปใช้ในการตรวจสอบซอฟต์แวร์น้อยกว่า Isabelle หรือ Rocq ซึ่งเป็น Coq แบบเดิม
      ในสาขานี้ แม้แต่ Agda ก็ถูกใช้มากกว่า
      อย่างไรก็ตาม ตอนนี้ Lean กำลังได้รับแรงส่งมากในฐานะทางเลือก โดยเฉพาะความสามารถในฐานะภาษาโปรแกรมเชิงฟังก์ชันแบบทั่วไป
      ส่วนตัวมองว่าแนวทางที่อิง Hoare logic หรือ separation logic ซึ่งทำให้จับคู่ requirement กับ specification ได้ง่ายนั้นใช้งานได้จริงกว่า ชอบ Dafny กับ F*

  • ในประกาศบน Twitter น่าสนุกดีที่นักพัฒนาแอบพูดถึง Le Chaton Fat
    ไม่ว่าพวกเขาจะเกี่ยวข้องกับ Le Chaton Fat จริงหรือไม่ ก็ดูเหมือนว่าโมเดล “general-purpose ขนาดใหญ่ใหม่” ตัวจริงกำลังจะมาในไม่ช้า
    หลังจากกระแสสื่อแล้วยังเอ่ยถึงโดยตรงแบบนี้ก็เลยน่าคาดหวัง หวังว่าชื่อจะสร้างสรรค์กว่า “Large 4”

  • สามารถลองใช้ Leanstral 1.5 ได้ใน OpenATP เวอร์ชันล่าสุด
    OpenATP เป็นแพ็กเกจ Python และ CLI แบบโอเพนซอร์สสำหรับ agentic automated theorem prover และรองรับโดยค่าเริ่มต้นทั้งการรัน local ใน Docker หรือรันระยะไกลใน Modal sandbox
    GitHub: https://github.com/henryrobbins/open-atp
    Docs: https://open-atp.henryrobbins.com