Anthropic เผย Claude ตรวจสอบอย่างเป็นทางการระดับใหญ่ของไลบรารีโอเพนซอร์สสำเร็จ

เมื่อวันที่ 22 ตุลาคม ทีม Frontier Red Team ของบริษัทปัญญาประดิษฐ์ Anthropic เผยแพร่งานวิจัยระบุว่าโมเดลภาษาขนาดใหญ่สามารถเขียนการพิสูจน์อย่างเป็นทางการได้ในวงกว้างขึ้น ทีมงานร่วมมือกับ Theorem ใช้ Claude พิสูจน์คุณสมบัติด้านความปลอดภัยบนไลบรารีโอเพนซอร์สจริงกว่า 100 แห่งในระดับแอสเซมบลี RISC-V โดยอ้างว่านี่เป็นครั้งแรกที่ทราบกันว่ามีการใช้ AI สำหรับการตรวจสอบอย่างเป็นทางการระดับใหญ่ของซอฟต์แวร์ที่ใช้งานจริงในระดับแอสเซมบลี ในระหว่างกระบวนการเขียนการพิสูจน์ ยังค้นพบช่องโหว่ที่ตรวจไม่พบมาเป็นเวลาหลายปีอีกด้วย การทดลองแปลงฟัซซ์เทสต์ที่คอมไพล์ได้ซึ่งมีอยู่แล้วจาก Google OSS-Fuzz ให้เป็นข้อกำหนด: ภายใต้สมมติฐานของไบนารีแบบสแตติกแบบเธรดเดียว งบประมาณหน่วยความจำคงที่ ซีพียู RISC-V และ Linux สำหรับอินพุตใดๆ ที่น้อยกว่า 64 MB โปรแกรมควรออกตามปกติโดยไม่ทำให้เกิดข้อผิดพลาดด้านความปลอดภัยของหน่วยความจำหรือการยืนยันล้มเหลว ภายในไม่กี่สัปดาห์ Claude พิสูจน์คุณสมบัติดังกล่าวสำหรับจุดเข้า 239 จุดในไลบรารี OSS-Fuzz 123 แห่งหลังจากแพตช์ปัญหาที่ตรวจพบ การพิสูจน์มุ่งเป้าไปที่คำสั่ง RISC-V ที่คอมไพล์แล้ว ประมาณ 180 ล้านบรรทัดของ Rocq และได้รับการตรวจสอบโดยเคอร์เนล Rocq หน้าเว็บระบุว่าสิ่งนี้ไม่ได้หมายความว่าไลบรารีเหล่านี้ปลอดช่องโหว่ เนื่องจากปัญหาที่เหลืออยู่อาจอยู่นอกส่วนประกอบที่เชื่อถือได้หรือขอบเขตของการพิสูจน์ หน้าเว็บยังกล่าวถึงว่าทีมให้ Claude ทำให้ RFC 1950 เป็นทางการและพิสูจน์ว่าการใช้งาน zlib ในเคอร์เนล Linux สอดคล้องกับข้อกำหนดนั้นในระดับไบนารี x86 อินเทอร์พรีเตอร์ที่เขียนด้วย Rust ซึ่งครอบคลุมชุดย่อยขนาดใหญ่ของ Python แสดงความสอดคล้อง 99.95% กับพฤติกรรมของ CPython ในโปรแกรมที่สร้างแบบสุ่มกว่า 1.7 ล้านโปรแกรม ในงานตรวจสอบขนาดเล็ก 36 งาน Opus 5.5 พิสูจน์ว่าประมาณครึ่งหนึ่งใช้โทเค็นน้อยลงประมาณ 40% เมื่อเทียบกับ Opus 5 ทีมยังชี้ให้เห็นว่าการพิสูจน์มุ่งเป้าไปที่ไบนารี RISC-V แบบเธรดเดียวที่ลิงก์แบบสแตติก และตัวตรวจสอบการพิสูจน์ไม่สามารถระบุได้ว่าข้อกำหนดสอดคล้องกับความเป็นจริงหรือไม่