แอนโทรปิกใช้Claudeช่วยพิสูจน์ความปลอดภัยซอฟต์แวร์โอเพนซอร์สสเกลใหญ่
แอนโทรปิกเผยความสำเร็จในการใช้โมเดลปัญญาประดิษฐ์คลอดย์ร่วมกับทัวร์เอมเพื่อตรวจสอบความถูกต้องของไลบรารีโอเพนซอร์สในสเกลที่กว้างขึ้น
วันที่ 22 ตุลาคม 2026 บริษัท แอนโทรปิก (Anthropic) เผยแพร่ผลงานวิจัยที่ระบุว่าปัญญาประดิษฐ์เริ่มเข้ามาช่วยให้การพิสูจน์ความถูกต้องของซอฟต์แวร์ตามหลักคณิตศาสตร์ (Formal Software Verification) เป็นจริงได้ในสเกลที่ใหญ่ขึ้น โดยทำงานร่วมกับสตาร์ตอัป ทัวร์เอม (Theorem) ใช้โมเดล คลอดย์ (Claude) สร้างบทพิสูจน์ว่าจุดเข้าทดสอบ 239 จุด ใน 123 ไลบรารีโอเพนซอร์ส จะไม่เกิดการแครช (Crash) ภายใต้เงื่อนไขที่กำหนด ภายในระยะเวลาหลายสัปดาห์
กระบวนการดังกล่าวเริ่มต้นด้วยการแปลงการทดสอบแบบฟัซซิ่ง (Fuzz Tests) ให้เป็นข้อกำหนดทางคณิตศาสตร์ จากนั้นให้คลอดย์เขียนบทพิสูจน์ขึ้นมา แล้วใช้เครื่องมือร็อก (Rocq) ทำหน้าที่ตรวจสอบซ้ำว่าบทพิสูจน์นั้นตรงกับข้อกำหนดที่วางไว้จริงหรือไม่ แนวทางนี้ช่วยแก้ปัญหาความยุ่งยากและต้นทุนสูงของการทำบทพิสูจน์ทางคณิตศาสตร์แบบดั้งเดิมที่ต้องอาศัยผู้เชี่ยวชาญจำนวนมาก
อย่างไรก็ตาม แอนโทรปิกได้ระบุข้อจำกัดสำคัญไว้ชัดเจนว่า วิธีการนี้ยังคงจำกัดอยู่ภายใต้ขอบเขตเฉพาะ โดยครอบคลุมอินพุตขนาดต่ำกว่า 64 เมกะไบต์ (MB) สำหรับไบนารี อาร์ไอเอสซี-วี (RISC-V) แบบสแตติกและเธรดเดี่ยว (Single-thread) ภายใต้แบบจำลองลินุกซ์ (Linux) และหน่วยความจำที่กำหนดเท่านั้น ทั้งยังไม่ได้หมายความว่าตัวไลบรารีทั้งหมดจะปราศจากบั๊กโดยสิ้นเชิง
ความสำเร็จนี้แสดงให้เห็นแนวทางที่ปัญญาประดิษฐ์อาจช่วยยกระดับความปลอดภัยของโครงสร้างพื้นฐานซอฟต์แวร์โอเพนซอร์สทั่วโลกในอนาคต แต่ผู้พัฒนายังต้องระมัดระวังข้อจำกัดทางเทคนิคในการใช้งานจริง