Claude โชว์เหนือ! เขียนโค้ดพร้อมพิสูจน์ความปลอดภัยอัตโนมัติ

ประเด็นสำคัญ

• Anthropic และพันธมิตรอย่าง Theorem ใช้ Claude ตรวจสอบความถูกต้องของโค้ดซอฟต์แวร์ด้วยหลักการทางคณิตศาสตร์ พร้อมสร้างข้อพิสูจน์อย่างเป็นทางการ (formal proofs) เพื่อยืนยันความแม่นยำ

• ภายในเวลาเพียงไม่กี่สัปดาห์ โมเดลสามารถสร้างโค้ดพิสูจน์ได้ถึง 180 ล้านบรรทัดสำหรับ 123 ไลบรารีโอเพนซอร์ส และตรวจพบจุดบกพร่องหลายร้อยจุดที่การทดสอบแบบดั้งเดิมตรวจไม่พบ

• การที่ AI สามารถเขียนโค้ดและพิสูจน์ความถูกต้องได้เอง ถือเป็นการก้าวกระโดดครั้งใหญ่ของระบบอัตโนมัติ โดย Anthropic ตั้งเป้าให้การตรวจสอบอย่างเป็นทางการด้วย AI กลายเป็นมาตรฐานทั่วไปในอุตสาหกรรม

Anthropic ใช้ Claude เพื่อพิสูจน์ทางคณิตศาสตร์ว่าโค้ดทำงานถูกต้อง ซึ่งเป็นทางออกสำคัญสำหรับซอฟต์แวร์ที่สร้างโดย AI แม้ว่าในปัจจุบันจะยังมีข้อจำกัดด้านเทคนิคที่เข้มงวดก็ตาม

ที่ผ่านมา การพิสูจน์ว่าซอฟต์แวร์ปราศจากข้อผิดพลาดในทุกสภาวะมีค่าใช้จ่ายสูงมหาศาล ตัวอย่างเช่น การตรวจสอบความถูกต้องของ seL4 ซึ่งเป็นเคอร์เนลระบบปฏิบัติการขนาดเล็ก ต้องใช้ผู้เชี่ยวชาญทำงานเทียบเท่ากับ 20 person-years วิธีนี้จึงมักถูกจำกัดไว้ใช้กับงานวิกฤตเท่านั้น เช่น ซอฟต์แวร์การบินของ Airbus

Frontier Red Team ของ Anthropic ร่วมกับ Theorem จึงได้มอบหมายให้ Claude เข้ามาจัดการงานนี้แทน โดยโมเดลได้สร้างโค้ดพิสูจน์ทางคณิตศาสตร์กว่า 180 ล้านบรรทัดในเวลาไม่กี่สัปดาห์ ผ่านการวิเคราะห์โปรแกรมทดสอบจาก 123 ไลบรารีโอเพนซอร์สในโปรเจกต์ OSS-Fuzz ของ Google

แทนที่จะเริ่มเขียนโค้ดใหม่ทั้งหมด Claude ได้เข้าไปตรวจสอบซอฟต์แวร์เดิมด้วยการแปลงการทดสอบการล่ม (crash tests) ให้เป็นโจทย์ทางคณิตศาสตร์ วิเคราะห์ machine code และสร้างข้อพิสูจน์ที่ครอบคลุม โดยมี Rocq ซึ่งเป็นโปรแกรมตรวจสอบอิสระทำหน้าที่ยืนยันความถูกต้องของข้อพิสูจน์เหล่านั้นอีกชั้นหนึ่ง กระบวนการนี้แทบไม่ต้องใช้มนุษย์รีวิวเลย ทำให้นักวิจัยเรียกมันว่าเป็นระบบ "อัตโนมัติเต็มรูปแบบ" (fully autonomous)

Claude ตรวจพบจุดบกพร่องที่การทดสอบนานหลายปีมองข้ามไป

ระหว่างการสร้างข้อพิสูจน์ Claude ได้ตรวจเจอจุดบกพร่องหลายร้อยแห่งและได้รับอนุญาตให้ทำการแก้ไขเอง ซึ่งจุดบกพร่องเหล่านี้มักเล็ดลอดการทดสอบทั่วไปเพราะจะแสดงอาการภายใต้เงื่อนไขที่เฉพาะเจาะจงมาก เช่น การจัดการไฟล์อินพุตที่มีขนาดใหญ่ผิดปกติ

ยกตัวอย่างเช่น ในการตรวจสอบโปรแกรมอ่าน PDF ทีมงานพบจุดบกพร่องด้านความปลอดภัยภายในสัปดาห์เดียวมากเท่ากับที่เคยได้รับรายงานมาทั้งปี หรือในอีกกรณีหนึ่ง Claude สามารถตรวจพบข้อผิดพลาดทางตรรกะที่ซ่อนอยู่มานานกว่า 10 ปี ซึ่ง Anthropic ระบุว่าแม้บางครั้งการพิสูจน์จะไม่สมบูรณ์ แต่ความพยายามของ AI ก็มักจะเผยให้เห็นบั๊กที่มีอยู่จริงเสมอ

สิ่งที่การตรวจสอบอย่างเป็นทางการทำได้และทำไม่ได้

อย่างไรก็ตาม Anthropic ยอมรับว่าคำว่า "การตรวจสอบอย่างเป็นทางการ" (formally verified) ไม่ได้การันตีว่าซอฟต์แวร์จะปราศจากข้อผิดพลาด 100% เนื่องจากข้อพิสูจน์จะมีผลภายใต้ขอบเขตที่กำหนดไว้เท่านั้น เช่น ต้องรันบนสถาปัตยกรรมโปรเซสเซอร์เฉพาะ หรืออินพุตต้องไม่เกิน 64 MB ซึ่งในโลกความเป็นจริง ซอฟต์แวร์เหล่านี้ต้องรันบนฮาร์ดแวร์ที่หลากหลายกว่านั้นมาก

นอกจากนี้ ค่าใช้จ่ายในการประมวลผลยังสูงมาก โดยการพิสูจน์แต่ละครั้งต้องใช้โทเค็นหลายร้อยล้านโทเค็น แม้จะไม่มีการเปิดเผยตัวเลขรวม แต่หาก AI พัฒนาจนสามารถตรวจสอบโค้ดตัวเองได้ นักพัฒนาจะเชื่อมั่นในซอฟต์แวร์ที่สร้างโดย AI ได้มากขึ้น ช่วยลดเวลาและงบประมาณในการรีวิวโค้ดในระยะยาว ซึ่งผลทดสอบเบื้องต้นพบว่าโมเดลรุ่นใหม่อย่าง Opus 5.5 เริ่มแก้โจทย์ได้ดีขึ้นโดยใช้โทเค็นน้อยลงถึง 40%

โปรเจกต์นี้ช่วยย้ำภาพชัดเจนว่า หาก AI สามารถพิสูจน์ได้ว่าโค้ดที่มันเขียนนั้นปลอดภัย คำถามสำคัญจะเปลี่ยนไปสู่การนำไปใช้จริงในวงกว้าง โดย Anthropic คาดหวังว่าการตรวจสอบแบบนี้จะกลายเป็นมาตรฐานใหม่ และ แผนงานของ Theorem ได้เริ่มขยายขอบเขตไปยังโครงสร้างพื้นฐานสำคัญอย่าง glibc, OpenSSL และ cURL แล้ว