โครงการที่ประกาศเมื่อเร็วๆ นี้ซึ่งอ้างว่าสามารถตรวจสอบความถูกต้องอย่างเป็นทางการสำหรับโมเดลการเรียนรู้ของเครื่อง (ML) ได้รับความกังขาอย่างมากจากชุมชนเทคนิค โครงการ Formal Verification of Machine Learning Models in Lean อ้างว่าเสนอกรอบการทำงานสำหรับการพิสูจน์คุณสมบัติต่างๆ เช่น ความทนทาน ความเป็นธรรม และความสามารถในการตีความของโมเดล ML โดยใช้โปรแกรมพิสูจน์ทฤษฎี Lean 4
โครงการนี้นำเสนอตัวเองว่าเป็นโซลูชันที่ครอบคลุมพร้อมคุณสมบัติต่างๆ รวมถึงไลบรารี Lean ที่มีคำจำกัดความอย่างเป็นทางการสำหรับสถาปัตยกรรมเครือข่ายประสาทเทียมแบบต่างๆ, ตัวแปลงโมเดลสำหรับการแปลงโมเดลที่ผ่านการฝึกฝนแล้วเป็นโค้ด Lean และอินเทอร์เฟซเว็บสำหรับการแสดงผลและการจัดการการพิสูจน์ อย่างไรก็ตาม ผู้เชี่ยวชาญในสาขานี้ได้แสดงความกังวลอย่างมากเกี่ยวกับความเป็นไปได้และความน่าเชื่อถือของข้อกล่าวอ้างเหล่านี้
ข้อจำกัดทางเทคนิคและการสัญญาที่เกินจริง
สมาชิกในชุมชนที่มีความเชี่ยวชาญด้านการตรวจสอบความถูกต้องอย่างเป็นทางการได้ชี้ให้เห็นถึงข้อจำกัดพื้นฐานในแนวทางนี้ การตรวจสอบความถูกต้องอย่างเป็นทางการของโมเดล ML ที่ซับซ้อนเผชิญกับความท้าทายที่มีอยู่ในตัวซึ่งโครงการดูเหมือนจะมองข้ามไป การพิสูจน์คุณสมบัติที่มีความหมายเกี่ยวกับเครือข่ายประสาทเทียมเป็นเรื่องที่ยากอย่างเห็นได้ชัด โดยเฉพาะอย่างยิ่งสำหรับการใช้งานในโลกแห่งความเป็นจริง
ดูเหมือนไร้ประโยชน์... ส่วนที่ยากจริงๆ คือการพิสูจน์เอง ซึ่งพวกเขาดูเหมือนจะไม่ได้แก้ไขปัญหานี้ ทฤษฎีบทประเภทที่ว่าโมเดล X ทำสิ่งที่พึงประสงค์นี้เสมอเกือบจะเป็นเท็จเสมอ (เพราะเป็นโมเดลที่ไม่แม่นยำ) และทฤษฎีบทประเภทที่ว่าโมเดล X ทำสิ่งที่พึงประสงค์นี้ Y% ของเวลาดูเหมือนจะยากมากที่จะพิสูจน์
ตัวอย่างในพื้นที่เก็บข้อมูลของโครงการถูกวิจารณ์ว่าเป็นเรื่องง่ายและไม่เป็นตัวแทนของความท้าทายในการตรวจสอบความถูกต้องในโลกแห่งความเป็นจริง ผู้แสดงความคิดเห็นคนหนึ่งสังเกตว่าตัวอย่างความเป็นธรรมเพียงแค่พิสูจน์ว่าตัวจำแนกที่ตอบว่าใช่เสมอจะมีเปอร์เซ็นต์การจำแนกเดียวกันในทุกกลุ่มประชากร—ซึ่งเป็นผลลัพธ์ทางคณิตศาสตร์ที่ง่ายและไม่มีความสำคัญในทางปฏิบัติ
คำถามเกี่ยวกับความน่าเชื่อถือ
ผู้แสดงความคิดเห็นหลายคนได้แสดงความกังวลเกี่ยวกับความน่าเชื่อถือของโครงการเอง โค้ด Lean ในพื้นที่เก็บข้อมูลถูกอธิบายว่าเป็นการผสมผสานระหว่าง Lean 3 และ 4 ที่สร้างโดย AI ซึ่งอาจไม่สามารถคอมไพล์ได้อย่างถูกต้อง การขาดการอ้างอิงผลงานทางวิทยาศาสตร์หรือบทความวิจัยที่เกี่ยวข้องยิ่งทำให้ความน่าเชื่อถือของโครงการลดลง
สมาชิกชุมชนคนหนึ่งแสดงความประหลาดใจที่โครงการนี้ขึ้นไปถึงหน้าแรกของ Hacker News ทั้งๆ ที่ดูเหมือนจะเต็มไปด้วยโครงร่างและคำสัญญาที่สร้างโดย AI มากกว่าเนื้อหาที่มีสาระ การขาดพื้นฐานทางวิทยาศาสตร์เป็นเรื่องที่น่ากังวลอย่างยิ่งเมื่อพิจารณาถึงความซับซ้อนของขอบเขตปัญหา
ประเด็นสำคัญที่ชุมชนยกขึ้นมา:
- ข้อกังวลเกี่ยวกับคุณภาพโค้ด: ถูกอธิบายว่าเป็น "โค้ดที่ผสมระหว่าง Lean 3 และ 4 ที่สร้างโดย AI" ซึ่งอาจไม่สามารถคอมไพล์ได้
- การพิสูจน์ที่จำกัด: ตัวอย่างพิสูจน์เฉพาะคุณสมบัติที่ไม่ซับซ้อน (เช่น ตัวจำแนกที่ตอบ "ใช่" เสมอจะมีอัตราการจำแนกถูกต้อง 100% สำหรับทุกกลุ่ม)
- ขาดพื้นฐานทางวิทยาศาสตร์: ไม่มีการอ้างอิงงานวิจัยหรือกรอบทฤษฎี
- ความท้าทายที่ยังไม่ได้รับการแก้ไข:
- การจัดการกับองค์ประกอบที่ไม่แน่นอนใน AI แบบสร้างสรรค์
- การกำหนดเกณฑ์วัดที่เป็นรูปธรรมสำหรับแนวคิดเช่น "ความเป็นธรรม"
- การพิสูจน์คุณสมบัติที่มีความหมายเกี่ยวกับเครือข่ายประสาทเทียมที่ซับซ้อน
แนวทางทางเลือกที่ได้กล่าวถึง:
- DARPA's ANSR (Assured Neuro-Symbolic Reasoning)
- DARPA's TIAMAT (Transfer from Imprecise Models for Assured Tactical Autonomy)
ความท้าทายพื้นฐานในการตรวจสอบ ML
การอภิปรายเน้นย้ำถึงความท้าทายพื้นฐานหลายประการในการตรวจสอบโมเดล ML อย่างเป็นทางการซึ่งโครงการไม่ได้จัดการอย่างเพียงพอ สำหรับโมเดลแบบสโตแคสติก—ซึ่งรวมถึงระบบ AI เชิงสร้างส่วนใหญ่—การตรวจสอบยิ่งซับซ้อนมากขึ้น ดังที่ผู้แสดงความคิดเห็นคนหนึ่งถามว่า พวกเขาจัดการกับโมเดลที่มีองค์ประกอบแบบสุ่มอย่างไร? ไม่แน่ใจว่าคุณตั้งใจจะพิสูจน์การสุ่มตัวอย่างอย่างไร
แม้แต่การกำหนดว่าควรตรวจสอบคุณสมบัติใดก็ยังเป็นความท้าทายที่สำคัญ แนวคิดเช่นความเป็นธรรมโดยธรรมชาติแล้วมีความคลุมเครือและยากที่จะกำหนดอย่างเป็นวัตถุวิสัยในเชิงคณิตศาสตร์ ในขณะเดียวกัน การพิสูจน์ว่าโมเดลภาษาไม่ส่งออกข้อความเท็จดูเหมือนจะเป็นปัญหาที่แก้ไขไม่ได้
แม้จะมีความกังขาเกี่ยวกับโครงการนี้โดยเฉพาะ แต่ชุมชนก็ตระหนักถึงความสำคัญของงานในทิศทางนี้ แนวทางทางเลือกที่กล่าวถึงรวมถึงโปรแกรม ANSR (Assured Neuro-Symbolic Reasoning) และ TIAMAT (Transfer from Imprecise Models for Assured Tactical Autonomy) ของ DARPA ซึ่งกำลังแก้ไขความท้าทายที่เกี่ยวข้องในการตรวจสอบ AI ด้วยหลักฐานทางวิทยาศาสตร์ที่เข้มงวดมากขึ้น
การอภิปรายนี้เป็นการเตือนให้ระลึกถึงช่องว่างระหว่างข้อกล่าวอ้างที่ทะเยอทะยานในความปลอดภัยของ AI และความเป็นจริงทางเทคนิคในปัจจุบัน ในขณะที่การตรวจสอบความถูกต้องอย่างเป็นทางการของคุณสมบัติง่ายๆ สำหรับโมเดล ML เฉพาะเป็นไปได้ กรอบการตรวจสอบที่ครอบคลุมซึ่งสามารถจัดการกับระบบการเรียนรู้เชิงลึกสมัยใหม่ยังคงเป็นความท้าทายในการวิจัยที่เปิดกว้างมากกว่าปัญหาที่แก้ไขแล้ว
อ้างอิง: Formal Verification of Machine Learning Models in Lean