คำตอบเร็ว: Anthropic รายงานว่า Claude ช่วยสร้างบทพิสูจน์สำหรับ 239 จุดเริ่ม fuzz test ใน 123 ไลบรารี และ Theorem เผยแพร่ชุดย่อย 60 จุดใน 25 ไลบรารีซึ่ง repo ระบุว่าตรวจด้วย Rocq 9.2.0 งานนี้ไม่ได้พิสูจน์ว่าไลบรารีทั้ง 123 ปลอดบั๊กหรือถูกต้องทุกกรณี เราอ่านรายงานและ repo โดยไม่รันหรือทำซ้ำ proof
ข่าวนี้น่าสนใจเพราะนำการพิสูจน์แบบ machine-checked มาใช้กับโค้ด C/C++ จาก OSS-Fuzz ในหลายสิบไลบรารี แต่คำว่า “พิสูจน์แล้ว” ต้องอ่านพร้อมขอบเขต: พิสูจน์คุณสมบัติที่ระบุไว้ของเส้นทางโปรแกรมที่เลือก ไม่ใช่ใบรับรองความปลอดภัยครอบจักรวาลให้ทั้งโครงการ
เกิดอะไรขึ้น และตัวเลขนับอะไร
Anthropic เผยแพร่รายงานเมื่อ 22 ตุลาคม 2026 ว่าร่วมกับ Theorem ใช้ Claude สร้างบทพิสูจน์ให้ fuzz test entry point 239 จุด ซึ่งครอบคลุม 123 ไลบรารีใน OSS-Fuzz รายงานระบุว่าบทพิสูจน์ที่ผ่านมีรวมราว 180 ล้านบรรทัด Rocq ตัวเลข 239 คือจำนวน entry point ที่เริ่มการทดสอบ ไม่ใช่จำนวนบั๊กที่แก้ ไม่ใช่จำนวนฟังก์ชันทั้งหมด และไม่ใช่หลักฐานว่าทุกไฟล์หรือทุก API ใน 123 ไลบรารีผ่านการตรวจ
คำว่า “180 ล้านบรรทัด” เป็นปริมาณข้อความบทพิสูจน์ที่ระบบตรวจยอมรับตามรายงาน ไม่ใช่ตัววัดความปลอดภัยโดยตรง ภาคผนวกระบุว่ามีการสร้างข้อความบทพิสูจน์จำนวนมากที่ไม่ผ่านด้วย และต้นทุนสร้างรวมสูง การตรวจโดย Rocq kernel แยกจากการให้โมเดลตัดสินเองว่าคำตอบถูก จึงเป็นคุณสมบัติสำคัญของแนวทางนี้
กลไกการตรวจทำงานอย่างไร
ทีมเริ่มจาก fuzz test ที่มีอยู่ แปลงพฤติกรรมของ test เป็นสเปก แล้วสร้างไบนารี RISC-V ใช้ formal semantics ของ RISC-V/Linux ที่ Theorem พัฒนาขึ้นเพื่อกำหนดความหมายของ execution จากนั้น Claude สร้าง proof term และ Rocq kernel ตรวจ proof นั้น รายงานกำหนดอินพุตที่มีขนาดต่ำกว่า 64 MB และ target เป็น static, single-threaded binary บน RISC-V/Linux ภายใต้งบประมาณหน่วยความจำคงที่ การพิสูจน์เป็นข้อความทางคณิตศาสตร์ภายใต้ semantics เหล่านี้ ไม่ใช่การสุ่มจำลองโปรแกรมบนทุกระบบปฏิบัติการหรือทุกสถาปัตยกรรม
สเปกมุ่งตรวจว่าอินพุตตามเงื่อนไขที่กำหนดไม่ทำให้โปรแกรมจบด้วย crash ที่ formalization ตรวจจับได้ เช่น การเข้าถึงหน่วยความจำผิดขอบเขตหรือการหารด้วยศูนย์ ภายใต้เงื่อนไขและงบทรัพยากรที่ระบุ ผู้เขียนงานระบุ trusted components หลักเป็น formal semantics, theorem statements ที่ตรงกับเป้าหมาย และ Rocq checker สำหรับข้อสรุปของไบนารีที่เลือก การนำผลไปอ้างกับซอร์สหรือระบบ deploy จริงยังต้องจับคู่ build/compiler และสภาพแวดล้อมให้ตรง
สิ่งที่ผลนี้ยืนยัน และสิ่งที่ยังไม่ยืนยัน
ยืนยันได้: สำหรับ entry point และไบนารีที่เผยแพร่พร้อม proof แล้ว Rocq ตรวจบทพิสูจน์ได้ภายใต้สเปกและสมมติฐานของงานนั้น Repo สาธารณะของ Theorem เปิด proof สำหรับ 60 entry point ใน 25 ไลบรารี และระบุการตรวจด้วย Rocq 9.2.0 นี่เป็นชุดเผยแพร่สาธารณะซึ่งมีขนาดเล็กกว่าตัวเลขทั้งหมดในรายงาน Anthropic
ยังยืนยันไม่ได้: ผลนี้ไม่พิสูจน์ว่าค่าที่โปรแกรมคืนถูกต้องตามเจตนาผู้ใช้ ไม่ครอบคลุมทุก API, caller, configuration หรือ runtime environment และไม่รับรองว่าไม่มีข้อมูลรั่วหรือผลข้างเคียงผิดพลาด ภาคผนวกยังระบุว่าไม่มีทฤษฎีบททั่วไปที่รับรองการสิ้นสุดของโปรแกรม หากมีบั๊กที่สเปกไม่ได้กล่าวถึง proof ก็อาจไม่ตรวจพบความผิดนั้น
การคอมไพล์ static binary สำหรับ RISC-V ช่วยให้แบบจำลองมีขอบเขตชัด แต่ไลบรารีจริงมักทำงานบน x86 หรือ ARM และอาจพึ่งพา glibc หรือสภาพแวดล้อมแบบ dynamic พฤติกรรมที่ต่างจากแบบจำลองจึงยังต้องตรวจด้วยการทดสอบและการวิเคราะห์อื่น ไม่มีการทดสอบซ้ำอิสระครบทั้ง 239 จุดในแหล่งที่ตรวจรอบนี้; repo ที่เปิดเผยเป็นส่วนหนึ่งของโครงการเดียวกัน ไม่ใช่การทำซ้ำจากทีมอิสระ
ทดลองอ่านขอบเขตผลลัพธ์
เลือกองค์ประกอบด้านล่างเพื่อดูว่าข้อสรุปเปลี่ยนอย่างไรเมื่อถามคนละคำถาม ตัวเลข 60/25 มาจาก repo สาธารณะ ส่วน 239/123 มาจากรายงานโครงการโดย Anthropic; สองชุดนี้มีขอบเขตการเผยแพร่ต่างกัน
หลักฐานรองรับเฉพาะไบนารีและ entry point ตามสเปกที่ระบุ
มุม fact-check: สรุปว่า “AI พิสูจน์ซอฟต์แวร์ปลอดบั๊ก” ได้หรือไม่
คำตัดสิน: เกินจริงถ้าหมายถึงทั้งไลบรารีหรือซอฟต์แวร์ใช้งานจริงทุกสภาพแวดล้อม หลักฐานที่ตรวจรองรับคำกล่าวที่แคบกว่า: Claude ช่วยสร้างบทพิสูจน์จำนวนมากซึ่ง Rocq ตรวจผ่าน สำหรับ fuzz test entry point และไบนารีที่เลือก ภายใต้สเปกกับ semantics ที่ประกาศไว้ ความสำเร็จเชิงขนาดมีนัยสำคัญ แต่ไม่เท่ากับพิสูจน์ความถูกต้องเชิงหน้าที่หรือไม่มีช่องโหว่ทั้งหมด
สิ่งที่ทีมพัฒนาควรทำต่อ
ใช้ proof เป็นหลักฐานเพิ่มสำหรับเส้นทางที่กำหนด แล้วอ่านสเปกและสมมติฐานก่อนนำไปอ้างในเอกสารความปลอดภัย ตรวจเวอร์ชัน compiler, binary, dependencies และ target architecture ให้ตรงกับ deployment จริง รวมทั้งคง fuzzing, static/dynamic analysis, code review และการทดสอบผลลัพธ์เชิงหน้าที่ไว้ ผู้ใช้ควรตรวจ repo ว่า proof ครอบคลุม entry point ใดและมีเงื่อนไขอะไร แทนการอาศัยตัวเลขรวมของโครงการ
แนวทางตรวจข้อกล่าวอ้างและแหล่งอ้างอิงสำหรับผู้อ่านทั่วไปมีเพิ่มเติมในบทความ ตรวจสอบคำตอบ AI: เช็กข้อเท็จจริง ตัวเลข และอ้างอิงปลอม
คำถามที่พบบ่อย
Rocq คืออะไร
Rocq เป็น proof assistant ซึ่ง kernel ตรวจ proof term ตามกฎตรรกะที่ระบบกำหนด การตรวจผ่านยืนยันว่าข้อพิสูจน์ตาม formalization นั้นถูกต้องภายในระบบ แต่ไม่ได้ทำให้สเปกหรือแบบจำลองตรงกับความต้องการจริงโดยอัตโนมัติ
60 จุดใน repo ขัดกับ 239 จุดในรายงานหรือไม่
ไม่จำเป็นต้องขัดกัน รายงานสรุปขนาดงานทั้งหมด ส่วน repo แสดง proof ที่เผยแพร่สาธารณะ ณ release ที่ตรวจได้ การเผยแพร่สาธารณะเป็น subset; ห้ามนำ 60 ไปแทนจำนวนงานทั้งหมด หรือกล่าวว่า repo มี proof ครบ 239 จุด
Proof นี้รับรองว่าไม่มีช่องโหว่หรือไม่
ไม่รับรองทั้งหมด รับรองเฉพาะคุณสมบัติที่ระบุไว้สำหรับ target ที่เลือกภายใต้สมมติฐานและแบบจำลองที่ใช้ ข้อผิดพลาดด้านตรรกะ ผลลัพธ์ผิด การรั่วไหล หรือพฤติกรรมที่อยู่นอกสเปกยังอาจมีได้
แหล่งข้อมูลและข้อจำกัด
- Anthropic: Formal verification for AI-generated code (22 ต.ค. 2026)
- Theorem Labs: OSS Verify proofs repository — README ระบุชุดสาธารณะ 60 entry point ใน 25 ไลบรารี
- release.yaml — release 2026.10.0 วันที่ 22 ต.ค. 2026 และเวอร์ชัน Rocq
- ภาคผนวกเทคนิค (PDF) — รายละเอียดสเปก ขอบเขต และข้อจำกัด
- Theorem OSS Verify — คำอธิบายจากผู้พัฒนา
การตรวจนี้อ่านแหล่งปฐมภูมิและ repo โดยไม่ติดตั้งหรือรันซอฟต์แวร์ ยังไม่พบการทำซ้ำอิสระที่ครอบคลุมงานทั้ง 239 จุด และไม่ได้ตรวจสอบทุก proof แบบอิสระทีละรายการ สัญญาอนุญาตระดับ repo แสดง MIT แต่ไฟล์หรือไลบรารีที่รวมไว้อาจมีสัญญาอนุญาตต้นทางต่างกัน จึงควรตรวจ license รายส่วนก่อนนำไปใช้
ใส่ความเห็น