ทีมนักวิจัยเสนอ MAGS ระบบหลายเอเจนต์ช่วยตรวจสอบความปลอดภัยโค้ดจาก AI ด้วยคณิตศาสตร์
งานวิจัยใหม่เสนอระบบ MAGS ใช้หลายเอเจนต์แปลงโค้ดจากโมเดลภาษาขนาดใหญ่ให้อยู่ในรูปภาษา Dafny เพื่อตรวจสอบความปลอดภัยเชิงรูปนัย
ในยุคที่เอเจนต์ปัญญาประดิษฐ์ (LLM coding agents) สามารถเขียนโปรแกรมที่ซับซ้อนได้ในปริมาณมาก การตรวจสอบความปลอดภัยด้วยมนุษย์เริ่มทำได้ยากขึ้น วิธีการทั่วไป เช่น การทดสอบแบบฟัซซิ่ง (Fuzz testing) หรือการวิเคราะห์โค้ดแบบสถิต (Static analysis) อาจไม่สามารถครอบคลุมทุกกรณีขอบ (Edge cases) ได้ทั้งหมด ขณะที่การตรวจสอบความปลอดภัยเชิงรูปนัย (Formal verification) ต้องใช้แรงงานและความเชี่ยวชาญสูงในการเขียนข้อกำหนดและพิสูจน์ความถูกต้อง
ล่าสุด นักวิจัยได้เผยแพร่บทความบน arXiv หมายเลข 2609.19391 เมื่อวันที่ 16 กันยายน 2026 นำเสนอโครงร่างระบบหลายเอเจนต์ที่ชื่อว่า MAGS (Multi-agent Auto-formalization Guarantees Safety for Agentic Outputs) โดยทำหน้าที่สร้างโปรแกรมพร้อมการรับประกันความปลอดภัยตามหลักการทางคณิตศาสตร์ ระบบนี้ใช้ภาษา Dafny เป็นตัวแทนขั้นกลาง (Intermediate representation) เพื่อให้สามารถตรวจสอบข้อกำหนดความปลอดภัยทางกลไกได้ และจะวนแก้โค้ดอัตโนมัติหากพบข้อผิดพลาดตามผลการตรวจสอบ
จากการทดลองที่ทีมวิจัยรายงาน MAGS สามารถสร้างโปรแกรมที่ผ่านการรับประกันตามข้อกำหนดได้ครบ 220 กรณีจากทั้งหมด 220 กรณี ซึ่งประกอบด้วยชุดคำสั่งเคอร์เนลสำหรับ CUDA จำนวน 100 กรณี, สคริปต์เทอร์มินัล 100 กรณี และงานควบคุมแขนกล 20 กรณี อย่างไรก็ตาม คณะผู้วิจัยระบุข้อจำกัดสำคัญว่า ระบบยังคงเกิดความล้มเหลวได้หากโมเดลเชิงรูปนัยที่ใช้ยังไม่ครอบคลุมพฤติกรรมเป้าหมายที่แท้จริงทั้งหมด
เทคโนโลยีนี้อาจช่วยลดความเสี่ยงด้านความปลอดภัยของโค้ดที่สร้างโดยปัญญาประดิษฐ์ ซึ่งมีความสำคัญต่อการนำไปประยุกต์ใช้ในระบบที่มีความเสี่ยงสูงในอนาคต