🧩 AI กำลังทำให้ Formal Verification กลายเป็นกระแสหลักในซอฟต์แวร์ Formal Verification หรือการพิสูจน์ความถูกต้องของซอฟต์แวร์ด้วยหลักคณิตศาสตร์ เคยเป็นเรื่องที่ใช้เฉพาะในงานวิจัยหรือระบบที่มีความเสี่ยงสูง เช่น ระบบการบินหรือการเข้ารหัสข้อมูล เนื่องจากต้องใช้เวลาและความเชี่ยวชาญสูงมาก เช่น กรณี seL4 microkernel ที่ใช้เวลาถึง 20 ปีคนในการพิสูจน์ความถูกต้องของโค้ดเพียงไม่กี่พันบรรทัด. แต่ปัจจุบัน AI โดยเฉพาะ LLM-based coding assistants กำลังเข้ามาช่วยลดภาระนี้อย่างมหาศาล. AI ไม่เพียงแต่ช่วยเขียนโค้ด แต่ยังสามารถสร้าง proof scripts เพื่อยืนยันว่าโค้ดนั้นสอดคล้องกับสเปกที่กำหนดไว้ Proof checkers อย่าง Isabelle หรือ Lean จะทำหน้าที่ตรวจสอบความถูกต้อง ทำให้แม้ AI จะ “หลอน” หรือสร้างโค้ดผิดพลาด ก็ไม่สามารถผ่านการตรวจสอบได้ สิ่งนี้เปลี่ยนสมการทางเศรษฐศาสตร์ของการพัฒนา เพราะต้นทุนการพิสูจน์ลดลงอย่างมากเมื่อเทียบกับต้นทุนของบั๊กที่อาจสร้างความเสียหาย. นอกจากการลดต้นทุนแล้ว AI ยังสร้าง “ความจำเป็นใหม่” ในการใช้ Formal Verification เนื่องจากโค้ดที่สร้างโดย AI มีความเร็วสูงแต่เสี่ยงต่อข้อผิดพลาดที่มนุษย์อาจตรวจไม่พบ การให้ AI พิสูจน์ความถูกต้องของโค้ดที่มันสร้างเอง จึงเป็นวิธีที่น่าเชื่อถือกว่าการตรวจสอบด้วยสายตามนุษย์ และอาจกลายเป็นมาตรฐานใหม่ในอุตสาหกรรม. อย่างไรก็ตาม ความท้าทายยังอยู่ที่การเขียน formal specification หรือการกำหนดคุณสมบัติที่ต้องการให้โค้ดมี ซึ่งยังต้องใช้ความเชี่ยวชาญและการตีความที่ถูกต้อง หากสเปกไม่ชัดเจน การพิสูจน์ก็ไม่มีความหมาย นักวิจัยบางส่วนจึงมองว่า AI อาจช่วยแปลสเปกจากภาษาธรรมชาติเป็นภาษาทางการได้ แต่ก็ยังมีความเสี่ยงเรื่องการตีความผิดพลาดที่ต้องระวัง. 📌 สรุปเป็นหัวข้อ ✅ AI กำลังทำให้ Formal Verification เข้าสู่กระแสหลัก ➡️ Proof assistants เช่น Lean, Isabelle, Agda ถูกใช้ร่วมกับ AI เพื่อลดภาระการเขียน proof scripts ➡️ ต้นทุนการพิสูจน์ลดลง ทำให้การตรวจสอบโค้ดมีความคุ้มค่ามากขึ้น ✅ AI สร้างความจำเป็นใหม่ในการตรวจสอบโค้ด ➡️ โค้ดที่สร้างโดย LLMs มีความเร็วสูงแต่เสี่ยงต่อบั๊ก ➡️ Proof checkers สามารถป้องกันข้อผิดพลาดที่มนุษย์อาจมองไม่เห็น ✅ การเปลี่ยนแปลงเชิงเศรษฐศาสตร์และมาตรฐานอุตสาหกรรม ➡️ ต้นทุนบั๊กสูงกว่าต้นทุนการพิสูจน์ ทำให้ Formal Verification มีความคุ้มค่า ➡️ อาจกลายเป็นมาตรฐานใหม่ในซอฟต์แวร์ที่ต้องการความน่าเชื่อถือสูง ‼️ ความท้าทายและข้อควรระวัง ⛔ การเขียน formal specification ยังต้องใช้ความเชี่ยวชาญสูง หากผิดพลาดจะทำให้การพิสูจน์ไร้ค่า ⛔ การใช้ AI แปลสเปกจากภาษาธรรมชาติอาจเสี่ยงต่อการตีความผิดพลาด https://martin.kleppmann.com/2025/12/08/ai-formal-verification.html