ทีมวิจัยของ Google DeepMind ได้เสร็จสิ้นการตรวจสอบรูปแบบความปลอดภัยของข้อความใน Signal และระบุว่านี่เป็นครั้งแรกที่มีการใช้ปัญญาประดิษฐ์ในการช่วยสร้างหลักฐาน ซึ่งเชื่อมโยงการรับประกันความปลอดภัยในระดับโปรโตคอลกับการใช้งานจริงในทางคณิตศาสตร์ที่ได้รับความนิยมอย่างแพร่หลาย
งานนี้ได้ใช้ AlphaProof Code ซึ่งเป็นกรอบการทำงานสำหรับการกำหนดและตรวจสอบรูปแบบซอฟต์แวร์ที่มีหลายตัวแทน ในกระบวนการนี้ ตัวแทนที่ได้รับการแนะนำโดยมนุษย์จะเขียนข้อกำหนด Lean ประเมินความหมายของรหัสเครื่อง จากนั้นตัวแทนจะสร้างหลักฐานและส่งให้กับแกนหลักของ Lean เพื่อตรวจสอบตามข้อกำหนดทีละข้อ
วัตถุที่ได้รับการตรวจสอบคือการจับมือ PQXDH หลังควอนตัมของ Signal และ Triple Ratchet ซึ่งยืนยันการออกแบบของ libsignal ในด้านความลับข้างหน้า การรับรองตัวตน ความสามารถในการฟื้นฟูหลังจากการรั่วไหลของกุญแจ และความลับในการจับมือ ซึ่งเป็นอีกก้าวที่ใกล้เคียงกับแนวคิดที่เสนอโดยมูลนิธิปัญญาประดิษฐ์ที่เป็นประโยชน์ในเดือนเมษายนปีนี้: มูลนิธินี้หวังที่จะใช้การตรวจสอบรูปแบบ Lean เพื่อยืนยันโปรโตคอลและแอปพลิเคชัน Signal
วิธีการเฉพาะคือการทำงานร่วมกับหลายโมเดลเพื่อเปลี่ยนเป้าหมายด้านความปลอดภัยของ Signal ให้เป็นข้อกำหนดทางคณิตศาสตร์ที่ได้รับการตรวจสอบโดยมนุษย์ จากนั้นให้ Gemini Carbon สร้างรหัส Lean ตามนั้นเพื่อพิสูจน์ความถูกต้องของการดำเนินการของ libsignal ตัวแทนได้สร้างรหัสรวมทั้งหมด 6.5 ล้านบรรทัด ทีมงานได้ดำเนินการตรวจสอบรอบหนึ่งและระบุส่วนที่ต้องการการตรวจสอบโดยมนุษย์
Google DeepMind ประสบความสำเร็จในการตรวจสอบความปลอดภัยของข้อความใน Signal
“นี่คือระบบที่ถูกสร้างขึ้นจากพื้นฐานเพื่อให้มนุษย์และปัญญาประดิษฐ์ทำงานร่วมกัน” Swarat Chaudhuri นักวิจัยของ Google DeepMind และศาสตราจารย์ที่มหาวิทยาลัยเท็กซัสที่ออสตินกล่าว เขาอธิบายว่า วิธีการแบบดั้งเดิมคือ นักคณิตศาสตร์จะส่งปัญหาที่ชัดเจนให้กับปัญญาประดิษฐ์เพื่อพิสูจน์ แต่ครั้งนี้ต้องเริ่มจากการทำความเข้าใจว่าต้องพิสูจน์อะไร