เกิดอะไรขึ้น
- วันที่ 22 ต.ค. 2026 ทีมฟรอนเทียร์ เรดทีมของแอนโทรปิก ลงผลวิจัยว่า AI ทำให้การพิสูจน์ซอฟต์แวร์แบบเป็นทางการ (ฟอร์มอลเวริฟิเคชัน) ทำได้ในสเกลใหญ่ขึ้นมาก
- ใช้ Claude ร่วมกับ Theorem พิสูจน์ไลบรารีโอเพนซอร์ส 123 ตัวจากโครงการ OSS-Fuzz รวม 239 จุดเรียกใช้งาน
- ระหว่างทาง Claude ยังแก้บั๊กที่ตัวเองเจอให้ด้วย
พิสูจน์อะไรกันแน่
- พิสูจน์ว่าโปรแกรมไม่มีวันพัง ไม่มีบั๊กหน่วยความจำหรือเงื่อนไขตรวจสอบที่ล้มเหลว ไม่ว่าป้อนข้อมูลอะไรเข้าไป ขอแค่ไม่เกิน 64 เมกะไบต์
- พิสูจน์กันถึงระดับภาษาเครื่อง RISC-V เลย ไม่ใช่แค่ดูโค้ดต้นฉบับ
- มีเงื่อนไขกำกับ คือโปรแกรมทำงานเธรดเดียว ลิงก์แบบสแตติก หน่วยความจำคงที่ รันบนซีพียู RISC-V กับลินุกซ์
- บทพิสูจน์รวมกันราว 180 ล้านบรรทัดในภาษา Rocq ตัวหนึ่งยาวราว 6 แสนบรรทัด
- ไม่ต้องมีคนนั่งอ่าน เพราะตัวตรวจบทพิสูจน์ของ Rocq เช็กให้เอง สิ่งที่ต้องเชื่อมีแค่แบบจำลอง RISC-V กับลินุกซ์ ตัวโจทย์ที่ตั้ง และตัวตรวจ
เจอบั๊กแบบไหนบ้าง
- เจอบั๊กหลายร้อยจุด หลายตัวเป็นแบบที่การสุ่มป้อนข้อมูลทดสอบ (ฟัซซิง) แทบไม่มีทางเจอ
- ตัวคลายไฟล์บีบอัดมีตัวนับติดลบ จนเขียนข้อมูลเกินขอบเขต แต่จะเกิดเฉพาะไฟล์ขนาดราว 20 เมกะไบต์
- ตัวถอดรหัสรูปภาพอ่านข้อมูลเกินขอบเขต ต้องป้อนไฟล์ 64 เมกะไบต์และใช้หน่วยความจำเกิน 2 กิกะไบต์ถึงจะโผล่
- เจอช่องโหว่ CVE-2026-56132 ใน libexpat ซ้ำอีกรอบ
- เจอบั๊กเชิงตรรกะที่ฟีเจอร์จำกัดการเข้าถึงไฟล์ไม่ได้ทำงานทุกครั้ง
ทดลองอะไรอีก
- ให้ Claude เขียนข้อกำหนดของรูปแบบบีบอัด zlib ตามมาตรฐาน RFC 1950 ให้เป็นภาษาคณิตศาสตร์
- จากนั้นพิสูจน์ว่าโค้ดบีบอัดในเคอร์เนลลินุกซ์ทำงานตรงตามข้อกำหนดนั้นจริง โดยดูถึงไฟล์ภาษาเครื่อง x86
- แบบจำลองซีพียู x86 ที่ใช้ Claude ก็สร้างเอง และละเอียดพอจะบูตระบบ Ubuntu ได้
- สร้างตัวรันภาษาไพทอนด้วยภาษา Rust แล้วพิสูจน์ด้วยเครื่องมือ Verus ว่าทำงานเหมือน CPython ลองสุ่มโปรแกรม 1.7 ล้านตัว ได้ผลตรงกัน 99.95%
- เจอบั๊กเชิงตรรกะที่ซ่อนอยู่เกินสิบปีในแอปที่คนใช้กันเยอะ
- ในโปรแกรมอ่านไฟล์ PDF ตัวหนึ่ง เจอบั๊กความปลอดภัยในสัปดาห์เดียวพอ ๆ กับที่ปกติมีคนแจ้งกันทั้งปี
- โมเดล Opus 5.5 พิสูจน์โจทย์เล็ก 36 ข้อได้ครึ่งหนึ่ง โดยใช้โทเคนน้อยกว่า Opus 5 ราว 40% และถ้าให้เอเจนต์แชร์บทพิสูจน์กัน ใช้โทเคนลดลงอีก 17%
ทำไมเรื่องนี้สำคัญ
- เคอร์เนลลินุกซ์เพิ่งมีช่องโหว่ถูกเปิดเผยกว่า 1,000 รายการ การหาบั๊กทีละตัวไม่ทันแล้ว
- ระบบปฏิบัติการ seL4 ที่ขึ้นชื่อเรื่องพิสูจน์แล้ว ใช้คนสร้าง 2 คน-ปี แต่ใช้พิสูจน์ถึง 20 คน-ปี
- ถ้า AI ช่วยทำส่วนที่แพงที่สุดนี้ได้ โค้ดพื้นฐานที่ทั้งโลกใช้ก็มีโอกาสถูกพิสูจน์มากขึ้น
ต่อจากนี้
- แอนโทรปิกจะปล่อยบทพิสูจน์บางส่วน พร้อมแบบจำลอง RISC-V และระบบปฏิบัติการให้คนนอกใช้
- Theorem รับรันระบบนี้ให้โครงการโอเพนซอร์สอื่น และเผยแพร่สกิลสำหรับ Claude ให้ใช้เอง
- Theorem วางแผนจะพิสูจน์ซอฟต์แวร์ในระบบนิเวศ Nix ต่อ
- เป้าหมายมีทั้ง glibc และ OpenSSL รวมถึงเครื่องมือดึงข้อมูลเว็บอย่าง cURL
ข้อจำกัดที่ต้องรู้
- พิสูจน์แล้วไม่ได้แปลว่าไม่มีบั๊กเลย
- บทพิสูจน์ครอบคลุมเฉพาะโปรแกรมบนซีพียู RISC-V แบบลิงก์สแตติกที่ใช้ไลบรารี musl
- แต่ของจริงส่วนใหญ่รันบนซีพียู x86 หรือ ARM และใช้ glibc
- เครื่องมือ ASan ที่ใช้จับบั๊กก็ไม่ได้จับบั๊กหน่วยความจำได้ทุกแบบ
- ยังพิสูจน์ไม่ครบทุกจุดเรียกใช้งาน และแต่ละรอบใช้โทเคนหลายร้อยล้าน
สรุป
การพิสูจน์ว่าโค้ดปลอดภัยแบบคณิตศาสตร์เคยเป็นงานแพงที่ทำได้แค่กับระบบเล็ก ๆ ถ้า AI ทำได้ถูกลงเรื่อย ๆ แบบนี้ ไลบรารีที่ทั้งโลกพึ่งอยู่ก็อาจได้การรับประกันที่หนักแน่นกว่าการสุ่มทดสอบ
แหล่ง: Anthropic, Theorem · 22 ต.ค. 2026