# AlphaProof Code and Signal: การตรวจสอบหลักฐานความปลอดภัยของโค้ดเครื่องและการสันนิษฐานที่เชื่อถือได้

Published: 2026-11-11

Google DeepMind รายงานการพิสูจน์ที่ผ่านการตรวจสอบด้วยเครื่องสำหรับคุณสมบัติความปลอดภัยที่เลือกไว้สำหรับชุดคำสั่ง command-line ของ libsignal ที่คอมไพล์แล้ว Lean ตรวจสอบการพิสูจน์ ในขณะที่มนุษย์อนุมัติข้อกำหนดและการสันนิษฐานของมัน ตัวเปรียบเทียบแยกต่างหากจะตรวจสอบทฤษฎีและคำจำกัดความที่เกี่ยวข้องทั้งหมดเทียบกับเป้าหมายที่ได้รับอนุมัติ

Canonical: https://thedailydiff.dev/th/video/2026-11-10-signal-machine-proof/

## วิดีโอนี้ครอบคลุมอะไรบ้าง

- AI agents สร้างหลักฐานที่เป็นไปได้; เคอร์เนลของ Lean ตรวจสอบว่าหลักฐานเหล่านั้นยืนยันข้อเรียกร้องอย่างเป็นทางการที่มนุษย์อนุมัติหรือไม่
- เป้าหมายที่ได้รับการยืนยันคือชุดคำสั่ง CLI ของ libsignal ที่คอมไพล์แล้วโดยเฉพาะ โดยมีความหมายที่เชื่อถือได้และสัญญาการเข้ารหัสลับ
- การพิสูจน์ไบนารีที่คอมไพล์แล้วจะลบ Rust compiler ออกจากฐานที่เชื่อถือได้สำหรับคุณสมบัติที่ระบุของไบนารีนั้น
- นักวิจัยรายงานการนำข้อผิดพลาดที่เคยแก้ไขแล้วกลับมาใช้ใหม่สองครั้ง ซึ่งละเมิดทฤษฎีความปลอดภัยเชิงสัญลักษณ์ของพวกเขา
- ตัวเปรียบเทียบจะตรวจสอบทฤษฎีและคำจำกัดความที่เกี่ยวข้องทั้งหมดเทียบกับข้อกำหนดที่ได้รับการอนุมัติซึ่งได้รับการป้องกัน; การแก้ไขจะผ่านกระบวนการตรวจสอบแยกต่างหาก

## คำถามและคำตอบ

### AlphaProof Code พิสูจน์อะไรเกี่ยวกับการใช้งาน Signal?

Google DeepMind รายงานการพิสูจน์ที่ผ่านการตรวจสอบสำหรับคุณสมบัติความปลอดภัยที่เลือกไว้สำหรับชุดคำสั่ง command-line ของ libsignal ที่คอมไพล์แล้ว เอกสารทางเทคนิคครอบคลุมการรักษาความลับและการรับรองความถูกต้องของข้อความ พร้อมด้วยความลับไปข้างหน้าและความปลอดภัยหลังการละเมิดภายใต้โมเดลที่ระบุ ผลลัพธ์ยังคงมีเงื่อนไขเกี่ยวกับผู้โจมตี เซสชัน และสมมติฐานการเข้ารหัสลับ ขอบเขตของมันไม่รวมการรับประกันแบบครอบคลุมสำหรับทุกแอปพลิเคชันหรือการติดตั้ง Signal

### ใครเป็นผู้ตัดสินว่าหลักฐานความปลอดภัยที่สร้างโดย AI ต้องยืนยันอะไร?

ผู้ตรวจสอบที่เป็นมนุษย์อนุมัติข้อกำหนดและสมมติฐานของมัน เอกสารทางเทคนิคของ Google DeepMind อธิบายถึง agents ที่ร่างข้อกำหนดด้วยคำแนะนำจากมนุษย์ และผู้ตรวจสอบที่ทดสอบว่าข้อความเหล่านั้นครอบคลุมคุณสมบัติความปลอดภัยที่มีความหมายหรือไม่ Lean ตรวจสอบตรรกะของการพิสูจน์ที่เกิดขึ้น มนุษย์ยังคงรับผิดชอบในการเลือกเป้าหมายที่แข็งแกร่ง ตรวจสอบสมมติฐาน และตัดสินการเปลี่ยนแปลงที่เสนอต่อข้อกำหนดที่ได้รับการอนุมัติ

### ทำไมต้องตรวจสอบโค้ดเครื่องที่คอมไพล์แล้ว แทนที่จะเชื่อใจ Rust compiler?

การพิสูจน์เกี่ยวกับไบนารีที่คอมไพล์แล้วจะยืนยันคุณสมบัติที่ระบุสำหรับสิ่งประดิษฐ์นั้นโดยตรง เอกสารของ Google DeepMind อธิบายว่าข้อผิดพลาดของคอมไพเลอร์ที่ละเมิดคุณสมบัติเหล่านั้นจะทำให้ทฤษฎีเป็นเท็จ ดังนั้น Rust compiler จึงออกจากฐานที่เชื่อถือได้สำหรับข้อเรียกร้องนี้ การพิสูจน์ยังคงเชื่อมั่นในโมเดลคำสั่ง เคอร์เนลของ Lean และสัญญาการเข้ารหัสลับที่ระบุไว้

### ตัวเปรียบเทียบหยุด agent ที่พิสูจน์จากการลดความแข็งแกร่งของเป้าหมายได้อย่างไร?

ตัวเปรียบเทียบจะตรวจสอบทฤษฎีและทุกคำจำกัดความที่ทฤษฎีนั้นขึ้นอยู่กับเทียบกับข้อกำหนดที่ได้รับการอนุมัติซึ่งได้รับการป้องกัน เอกสารของ Google DeepMind ระบุว่า agents ที่พิสูจน์ไม่สามารถเขียนไปยังสำเนาที่เก็บไว้ได้ ตัวตรวจสอบยังตรวจสอบสัจพจน์ที่ได้รับอนุญาตและเล่นซ้ำการพิสูจน์ในเคอร์เนลใหม่ การแก้ไขข้อกำหนดที่เสนอจะตามกระบวนการตรวจสอบแยกต่างหาก ในขณะที่มนุษย์ยังคงรับผิดชอบต่อความแข็งแกร่งของเป้าหมาย

### คำตัดสินของ The Daily Diff เกี่ยวกับเวิร์กโฟลว์การพิสูจน์ที่ตรวจสอบแล้วคืออะไร?

คำตัดสินของ The Daily Diff คือ SHIP IT Niko จะจัดส่งเวิร์กโฟลว์การพิสูจน์ที่ตรวจสอบแล้วเพราะข้อเรียกร้องที่ได้รับการอนุมัติยังคงแยกต่างหากจาก agent ที่สร้างคำตอบ เขาจะเก็บขอบเขตและสมมติฐานไว้กับทุกผลลัพธ์ รายงานนำเสนอสิ่งประดิษฐ์การพิสูจน์ที่เผยแพร่ของ Google โดยไม่สร้างใหม่ด้วยตัวเอง และอนุมัติเวิร์กโฟลว์ภายในขอบเขตของหลักฐานเหล่านั้น

## บท

- 0:00 ใครเป็นผู้ตรวจสอบหลักฐานความปลอดภัยของ AI?
- 0:57 ข้อเรียกร้องจะกลายเป็นเป้าหมายการพิสูจน์ได้อย่างไร?
- 1:39 ทำไมต้องพิสูจน์ไบนารีที่คอมไพล์แล้ว?
- 2:16 คุณสมบัติความปลอดภัยใดบ้างที่รอดพ้นจากช่องว่างของการใช้งาน?
- 2:59 ข้อกำหนดสามารถปฏิเสธโค้ดที่เสียหายได้หรือไม่?
- 3:36 การพิสูจน์ที่ถูกต้องสามารถตอบคำถามที่ผิดได้หรือไม่?
- 4:13 อะไรเป็นตัวจับเป้าหมายที่เคลื่อนไหว?
- 4:53 ฉันจะใช้เวิร์กโฟลว์การพิสูจน์นี้หรือไม่?

## บทถอดเสียงที่แปลแล้ว

แปลจากการบรรยายภาษาอังกฤษต้นฉบับ เสียงและคำบรรยายที่มีให้จะควบคุมโดย YouTube

### ใครเป็นผู้ตรวจสอบหลักฐานความปลอดภัยของ AI?

0:00 การตรวจสอบความปลอดภัยของ AI ยังคงฟังดูเหมือนการเชื่อใจแชทบอท ผลลัพธ์ Signal ใหม่ของ Google มาพร้อมกับการพิสูจน์ทางคณิตศาสตร์แยกต่างหาก ตรวจสอบ ในวิดีโอนี้ Google พิสูจน์อะไร? และพวกเขาจะหยุดเอเจนต์จากการเปลี่ยนเป้าหมายได้อย่างไร? นี่คือคำตอบที่เป็นประโยชน์ โมเดลเขียนหลักฐานที่เป็นไปได้ และ Lean ตรวจสอบหลักฐานเทียบกับ ข้อเรียกร้องที่มนุษย์อนุมัติเกี่ยวกับโค้ดที่คอมไพล์แล้วที่เลือกไว้ มนุษย์ยังคงเป็นเจ้าของข้อเรียกร้องและสมมติฐาน

0:21 คุณสามารถตรวจสอบผลลัพธ์ได้โดยไม่ต้องเชื่อคำกล่าวอ้างชัยชนะของโมเดล การตรวจสอบแยกต่างหากจะจับการเปลี่ยนแปลงคำถามอย่างเงียบๆ เราจะติดตามลงไปถึงคำจำกัดความ วันนี้วันอังคารที่สิบพฤศจิกายน และนี่คือ The Daily Diff AlphaProof Code คือกรอบงานของ Google สำหรับการเขียนข้อกำหนดซอฟต์แวร์ด้วย คำแนะนำจากมนุษย์และการสร้างหลักฐานที่ตรวจสอบแล้วด้วย AI agents การศึกษานี้กำหนดเป้าหมาย libsignal ซึ่งเป็นไลบรารี Rust ที่ใช้โปรโตคอลการส่งข้อความของ Signal ภายในโปรแกรม command-line เฉพาะ

0:45 Google ได้ประกาศงานนี้ในวันนี้ เอกสารระบุว่านักวิจัยห้าคนทำงานกว่าสี่สัปดาห์ Agents เขียนหลักฐาน ในขณะที่มนุษย์ใช้ความพยายามส่วนใหญ่ไปกับ ข้อกำหนด ความต้องการได้พบวิธีที่จะกลายเป็น การประชุมที่แพงขึ้น ข้อกำหนดระบุว่าโปรแกรมต้องทำอะไร

### ข้อเรียกร้องจะกลายเป็นเป้าหมายการพิสูจน์ได้อย่างไร?

0:59 สิ่งที่ผู้โจมตีควบคุม และสมมติฐานใดที่การโต้แย้งต้องการ ผู้ตรวจสอบถามว่ามันครอบคลุมความปลอดภัยที่ผู้คนให้ความสำคัญหรือไม่ คำตอบที่ตรวจสอบอย่างสวยงามสำหรับคำถามที่อ่อนแอทำให้คำถามนั้นยังคงอยู่ ทีมงานสร้างจากงานวิจัยก่อนหน้าเกี่ยวกับการจับมือของ Signal และกุญแจข้อความ ratchet การวิเคราะห์อย่างเป็นทางการได้ศึกษาการออกแบบเหล่านั้นแล้ว ข้อเรียกร้องของ Google เชื่อมโยงข้อโต้แย้งด้านความปลอดภัยของพวกเขากับการผลิตที่ไม่ถูกแก้ไข การใช้งานไลบรารีที่คอมไพล์แล้ว ซึ่งการออกแบบต้องรอดพ้นจากการสัมผัสกับ โค้ดจริง Ehren Kret ประธานเจ้าหน้าที่ฝ่ายเทคโนโลยีของ Signal

1:27 อธิบายการขยายตัวนอกเหนือจากขอบเขตที่เล็กกว่าของการตรวจสอบก่อนหน้า รายละเอียดการใช้งานรวมถึงข้อความที่ไม่เรียงลำดับ และเซสชันที่เก็บถาวรสำหรับ ข้อความที่ล่าช้า ซอฟต์แวร์จริงเก็บใบเสร็จที่คุณทิ้งไปในแผนภาพที่สวยงาม นักวิจัยคอมไพล์ไลบรารี Rust ที่ไม่ถูกแก้ไขด้วยคอมไพเลอร์มาตรฐาน

### ทำไมต้องพิสูจน์ไบนารีที่คอมไพล์แล้ว?

1:41 เป็นไฟล์ปฏิบัติการ Arm 64 Linux ทฤษฎีของพวกเขาอธิบายไบนารีนั้นโดยใช้โมเดลคำสั่งที่เป็นทางการ ครอบคลุมช่องว่างระหว่างโค้ดต้นฉบับและโค้ดเครื่องที่ได้รับการปรับแต่ง ข้อผิดพลาดของคอมไพเลอร์ที่ทำให้คุณสมบัติที่ระบุเสียไปจะทำให้ทฤษฎีของมันเป็นเท็จ ดังนั้นคอมไพเลอร์จึงออกจากฐานที่เชื่อถือได้สำหรับไบนารีนี้ คุณยังคงเชื่อมั่นในโมเดลคำสั่งและตัวตรวจสอบของ Lean ขอบเขตความเชื่อมั่นเปลี่ยนไปแล้ว และมันมีที่อยู่ หลักฐานที่ตรวจสอบแล้วประมาณหกและครึ่งล้านบรรทัดอยู่บนพื้นฐานของประมาณยี่สิบหก

2:06 พันบรรทัดของข้อกำหนดที่เชื่อถือได้และบรรทัดความหมายของคำสั่ง นี่คือจำนวนสิ่งประดิษฐ์ การถือว่ามันเป็นคะแนนความฉลาดก็เหมือนกับการจัดอันดับนักพัฒนาตามขนาดของ โฟลเดอร์โมดูลโหนดของพวกเขา

### คุณสมบัติความปลอดภัยใดบ้างที่รอดพ้นจากช่องว่างของการใช้งาน?

2:16 ข้อโต้แย้งครอบคลุมการรักษาความลับและการรับรองความถูกต้องของข้อความ พร้อมด้วยความลับไปข้างหน้าและความปลอดภัยหลังการละเมิดภายใต้โมเดลที่ระบุ สองรายการสุดท้ายอธิบายขีดจำกัดความเสียหายของกุญแจที่ถูกขโมยและการกู้คืนหลังจากการแลกเปลี่ยนใหม่ การรับประกันแต่ละอย่างมีเงื่อนไขเกี่ยวกับผู้โจมตีและเซสชัน Cryptographic primitives อยู่เบื้องหลังสัญญาที่เชื่อถือได้ การพิสูจน์สมมติว่ารูทีนเหล่านั้นทำงานตามที่ระบุและขึ้นอยู่กับข้อสมมติฐานด้านความปลอดภัยของการเข้ารหัสลับ การพิสูจน์หนึ่งอุดมคติการเข้ารหัสลับ; อีกหนึ่งใช้เหตุผลเกี่ยวกับ ความน่าจะเป็นความสำเร็จของผู้โจมตี

2:42 ทั้งสองมีข้อจำกัดเกี่ยวกับสถานการณ์ที่ครอบคลุม ถามว่าสร้างแบบไหน คุณสมบัติแบบไหน และข้อสมมติฐานแบบไหน ผลลัพธ์นี้เกี่ยวข้องกับชุดคำสั่ง command-line ของนักวิจัย การส่งข้อความแบบกลุ่มคืองานในอนาคต และโมเดลการคำนวณไม่รวม สถานะหลายอุปกรณ์ การเรียกทุกการติดตั้ง Signal ว่าปราศจากข้อผิดพลาดนั้นอยู่นอกขอบเขต ของทฤษฎี นักวิจัยได้นำข้อผิดพลาด Signal ที่เคยแก้ไขแล้วสองรายการกลับมาใช้ใหม่ใน

### ข้อกำหนดสามารถปฏิเสธโค้ดที่เสียหายได้หรือไม่?

3:02 สำเนาที่แยกออกและคอมไพล์มัน หลักฐานที่ตรวจสอบแล้วแสดงให้เห็นว่าไบนารีเหล่านั้นละเมิดทฤษฎีความปลอดภัยเชิงสัญลักษณ์ นั่นเป็นการทดสอบว่าข้อกำหนดสามารถปฏิเสธการใช้งานที่เสียหายจริงได้หรือไม่ เครื่องหมายถูกสีเขียวของคุณต้องการการทดสอบสีแดง Google เผยแพร่ข้อกำหนดและหลักฐานพร้อมคำแนะนำในการตรวจสอบ ที่เก็บข้อมูลระบุว่าการสร้างใหม่ที่สะอาดใช้เวลาหลายชั่วโมงและหน่วยความจำจำนวนมาก การอ่านประกาศบนแล็ปท็อปนั้นง่ายกว่ามาก โมเดลฮาร์ดแวร์และสัญญาที่เชื่อถือได้ยังคงต้องได้รับการตรวจสอบ

3:26 ฉันยังไม่ได้สร้างสิ่งประดิษฐ์ขนาดใหญ่สำหรับตอนนี้ เรากำลังรายงานผลลัพธ์ที่เผยแพร่และขอบเขตของมัน คนภายนอกมีเส้นทางในการตรวจสอบ ซึ่งสำคัญกว่าชัยชนะของ AI ครั้งอื่นสำหรับฉัน เอาละกับดัก

### การพิสูจน์ที่ถูกต้องสามารถตอบคำถามที่ผิดได้หรือไม่?

3:36 Lean สามารถยอมรับการพิสูจน์ที่ถูกต้องของข้อความที่เกือบไม่มีอะไรเลย สมมติฐานที่เป็นไปไม่ได้สามารถทำให้ทฤษฎีว่างเปล่าได้ การเปลี่ยนแปลงคำจำกัดความที่ซ่อนอยู่ใต้ทฤษฎีหลักสามารถทำให้ เป้าหมายอ่อนแอลง เอกสารออกแบบการตรวจสอบเพื่อป้องกันสิ่งนี้ ผู้เฝ้าประตูเก็บข้อกำหนดที่ได้รับการอนุมัติซึ่งไม่ได้ถูกเขียนโดย agents ที่พิสูจน์ พวกเขาสามารถเสนอการแก้ไขผ่านกระบวนการแก้ไขแยกต่างหาก การลดความปลอดภัยจะถูกยกระดับเป็นข้อบกพร่องที่อาจเกิดขึ้น การประกาศความสำเร็จของผู้พิสูจน์ไม่มีอำนาจที่นี่

4:00 มนุษย์ตัดสินการเปลี่ยนแปลงสมมติฐานที่เชื่อถือได้ โดยตรงหรือผ่านนโยบายของพวกเขา และตรวจสอบการแก้ไขหลังแต่ละแคมเปญ ผู้เชี่ยวชาญยังคงรับผิดชอบ เอเจนต์สามารถขอการมอบหมายที่แตกต่างกันได้ มันไม่สามารถให้คะแนนผ่านแก่ตัวเองได้

### อะไรเป็นตัวจับเป้าหมายที่เคลื่อนไหว?

4:13 นี่คือการตรวจสอบตามสัญญา ตัวเปรียบเทียบของ Lean เปรียบเทียบทฤษฎีและทุกคำจำกัดความที่ทฤษฎีนั้นขึ้นอยู่กับ กับสำเนาที่ได้รับการอนุมัติที่ได้รับการป้องกันนั้น นอกจากนี้ยังตรวจสอบสัจพจน์ที่ได้รับอนุญาตและเล่นซ้ำการพิสูจน์ในเคอร์เนลใหม่ ดังนั้นการลดความแข็งแกร่งของคำจำกัดความผู้ช่วยอย่างเงียบๆ จึงเปลี่ยนสิ่งที่กำลัง เปรียบเทียบ การพิสูจน์ที่ได้รับการยอมรับจะต้องสร้างเป้าหมายที่ได้รับการอนุมัติ นั่นยังคงทำให้มนุษย์รับผิดชอบในการเลือกเป้าหมายที่แข็งแกร่งและสมมติฐานที่ซื่อสัตย์ สำหรับเวิร์กโฟลว์ AI ของคุณเอง ให้เก็บเกณฑ์การยอมรับไว้นอก

4:37 สิทธิ์การแก้ไขของพนักงาน และตรวจสอบการเปลี่ยนแปลงที่เสนอแยกต่างหาก ผลลัพธ์ของ Google ทำให้การแยกส่วนนี้เป็นรูปธรรม ผู้เขียนหลักฐานทำงาน; ขอบเขตการตรวจสอบจะตัดสินว่ามันนับหรือไม่ ถ้าคุณอยากอ่านสิ่งนี้มากกว่าที่จะได้ยินฉันพูด The Daily Diff จะส่งถึงกล่องจดหมายของคุณ ทุกเช้า ฟรีที่ thedailydiff.dev ลิงก์ด้านล่าง ดังนั้นคำตัดสินของวันนี้คือ SHIP IT

### ฉันจะใช้เวิร์กโฟลว์การพิสูจน์นี้หรือไม่?

4:54 ฉันจะจัดส่งเวิร์กโฟลว์การพิสูจน์ที่ตรวจสอบแล้วนี้ เพราะข้อเรียกร้องที่ได้รับการอนุมัติยังคงแยกต่างหาก จากเอเจนต์ที่สร้างคำตอบ ฉันจะเก็บขอบเขตและสมมติฐานไว้กับทุกผลลัพธ์ สมัครสมาชิก กดกระดิ่ง และบอกฉันในความคิดเห็นว่าคุณจะประทับมัน แตกต่างกันหรือไม่ และนั่นคือความแตกต่างสำหรับวันนี้ ฉันชื่อ Niko จาก Axrisi รวมอย่างรับผิดชอบ

## แหล่งที่มา

- [AlphaProof Code: Verifying Signal's Security at the Machine-Code Level — technical scope, trusted base and gatekeeping](https://google-deepmind.github.io/code-verification/) — Swarat Chaudhuri and colleagues / Google DeepMind and Google
- [Introducing AlphaProof Code — November 10 announcement and attributed Signal CTO response](https://deepmind.google/blog/introducing-alphaproof-code/) — Pushmeet Kohli and Swarat Chaudhuri / Google DeepMind
- [Code-verification repository — initial commit, public artifacts and checking instructions](https://github.com/google-deepmind/code-verification) — Google DeepMind / GitHub
- [The PQXDH Key Agreement Protocol — older official specification and prior-analysis context](https://signal.org/docs/specifications/pqxdh/) — Ehren Kret and Rolfe Schmidt / Signal
- [The Double Ratchet Algorithm — Triple Ratchet section](https://signal.org/docs/specifications/doubleratchet/) — Trevor Perrin, Moxie Marlinspike and Rolfe Schmidt / Signal
- [Google DeepMind leadership — Demis Hassabis's relevant lab identity](https://deepmind.google/about/) — Google DeepMind
- [Demis Hassabis in 2025 — authentic portrait, cropped/resized/compressed and unflipped; no background removal or generated expression/detail; lab identity only, no authorship, proof writing, current reaction or endorsement](https://commons.wikimedia.org/wiki/File:Demis_Hassabis_in_2025_by_Christopher_Michel.jpg) — Christopher P. Michel / Cmichel67 / Wikimedia Commons
- [Portrait licence — CC BY-SA 4.0; attribution, adaptation disclosure and ShareAlike](https://creativecommons.org/licenses/by-sa/4.0/) — Creative Commons
- [Expanding Brain template — cropped/captioned artifact-count satire, brief transformed <=2s commentary; no benchmark, hosting licence, legal-clearance or blanket reuse claim](https://imgflip.com/memetemplate/Expanding-Brain) — Imgflip / user-uploaded meme template
- [Tom and Jerry — Boomerang Official actual animated reaction, silent resized/captioned 1.875s excerpt; brief transformed process commentary, no actual researcher or executive reaction, hosting licence, legal-clearance or blanket reuse claim](https://giphy.com/gifs/boomerangtoons-mad-upset-1gdkNV0hroZjOXSHOU) — Boomerang Official / GIPHY / Tom and Jerry
- [Boomerang GIF source link — uploader-provided provenance](https://boomtn.co/GIPHY) — Boomerang
- [AlphaProof Code discussion — attention context, anonymous opinions excluded from factual proof claims](https://news.ycombinator.com/item?id=50439193) — Hacker News
- [Code-verification licence — Apache 2.0 for Google code, third-party licences retained](https://github.com/google-deepmind/code-verification/blob/808b4b7ffef198e6a91f71ed776d641a1c236882/LICENSE) — Google / GitHub