ข่าว 
ข้อมูลเหรียญ 
แนะนำสื่อ 
Anthropic ใช้ Claude พิสูจน์ทางคณิตศาสตร์ว่าไลบรารีโอเพนซอร์ส 123 รายการปลอดภัยตามเงื่อนไขที่กำหนดในจุดเริ่มต้นการทดสอบ 239 จุด
Frontier Red Team ของ Anthropic ระบุในงานวิจัยที่เผยแพร่เมื่อวันที่ 22 ว่าได้ร่วมงานกับ Theorem บริษัทด้านการตรวจสอบ ทีมวิจัยแปลงการทดสอบเดิมให้เป็นเงื่อนไขสำหรับพิสูจน์ และใช้เครื่องมือแยกต่างหากตรวจสอบข้อพิสูจน์ที่ Claude เขียนขึ้น
ไลบรารีที่นำมาตรวจสอบอยู่ใน OSS-Fuzz โครงการตรวจจับข้อผิดพลาดโอเพนซอร์สของ Google ทีมวิจัยปรับการทดสอบแบบ fuzzing ที่มีอยู่ให้เป็นข้อความว่า “สำหรับอินพุตใด ๆ ที่มีขนาดต่ำกว่า 64MB โปรแกรมจะไม่หยุดทำงานผิดปกติ ไม่เกิดข้อผิดพลาดด้านความปลอดภัยของหน่วยความจำ และไม่ละเมิดเงื่อนไขการตรวจสอบ” Claude เป็นผู้เขียนข้อพิสูจน์ ส่วน Rocq เป็นเครื่องมือตรวจสอบ
ทีมวิจัยกล่าวว่า หลังใช้เวลาหลายสัปดาห์แก้ข้อผิดพลาดที่ Claude ตรวจพบ พวกเขาได้ตรวจสอบจุดเริ่มต้นการทดสอบ 239 จุดในไลบรารี 123 รายการ จุดเริ่มต้นเหล่านี้เป็นเส้นทางอินพุตที่ใช้ทดสอบฟังก์ชันเฉพาะของโปรแกรม ข้อพิสูจน์ตรวจสอบคำสั่ง RISC-V ที่คอมไพล์แล้ว ไม่ใช่ซอร์สโค้ดต้นฉบับที่มนุษย์อ่านได้ โดยข้อพิสูจน์ Rocq ที่เขียนขึ้นมีความยาวประมาณ 180 ล้านบรรทัด
การตรวจสอบแบบ formal verification คือการพิสูจน์ทางคณิตศาสตร์ว่าโปรแกรมทำตามกฎที่ระบุไว้ ต่างจากการทดสอบทั่วไปที่ป้อนข้อมูลเพื่อค้นหาข้อผิดพลาด วิธีนี้พิสูจน์ข้อความที่กำหนดให้ครอบคลุมอินพุตทุกค่าที่อยู่ภายใต้เงื่อนไขนั้น ระหว่างเขียนข้อพิสูจน์ ทีมวิจัยยังพบข้อผิดพลาดที่การทดสอบเดิมตรวจไม่พบ และสร้างเงื่อนไขการตรวจสอบขึ้นใหม่ให้สอดคล้องกับโค้ดหลังแก้ไข
ผลการตรวจสอบครั้งนี้จำกัดอยู่ที่โปรแกรม RISC-V แบบ single-threaded และ static-linked ซึ่งทำงานบน Linux และใช้หน่วยความจำขนาดคงที่ ไม่ได้ครอบคลุมทุกฟังก์ชันของแต่ละไลบรารีหรือสภาพแวดล้อมการใช้งานจริงทั้งหมด Anthropic อธิบายว่าเครื่องมือพิสูจน์ตรวจได้ว่าข้อความที่กำหนดเป็นจริงหรือไม่ แต่ไม่อาจตัดสินได้ว่าเงื่อนไขนั้นครอบคลุมการใช้งานจริงครบถ้วนหรือไม่
ทีมวิจัยยังรายงานการทดลองแยกต่างหากว่า Claude ตรวจสอบการทำงานของ zlib ในเคอร์เนล Linux ได้ในระดับไฟล์ปฏิบัติการ x86 นอกจากนี้ เมื่อนำตัวแปลภาษา Python ที่เขียนด้วย Rust ไปทดสอบด้วยโปรแกรมที่สร้างแบบสุ่มมากกว่า 1.7 ล้านโปรแกรม ผลการทำงานตรงกับ CPython ในสัดส่วน 99.95% การทดลองทั้งสองมีขอบเขตและวิธีการต่างจากการตรวจสอบไลบรารี 123 รายการด้วย RISC-V ในครั้งนี้
Anthropic เปิดเผยผลเปรียบเทียบงานตรวจสอบขนาดเล็ก 36 งานด้วย โดย Claude Opus 5.5 ใช้โทเคนในการพิสูจน์งานครึ่งหนึ่งน้อยกว่า Opus 5 ราว 40% ทีมวิจัยเปิดเผยข้อพิสูจน์บางส่วนเพื่อให้นักพัฒนารายอื่นตรวจสอบและนำไปใช้ซ้ำได้
ความคิดเห็น 0