PSI รายงานการพิสูจน์ข้อคาดเดา Aaronson-Ambainis ที่ผ่านการตรวจสอบด้วยเครื่อง

Physical Superintelligence ประกาศเมื่อวันที่ 6 พฤศจิกายน 2026 ว่าระบบวิจัยภายในซึ่งทำงานโดยใช้โมเดล Anthropic ที่ยังไม่เปิดเผยต่อสาธารณะหลายชุด ค้นพบข้อพิสูจน์ของข้อคาดเดา Aaronson-Ambainis ซึ่งเป็นปัญหาด้านคอมพิวเตอร์ควอนตัมที่ยังไม่มีคำตอบมาตั้งแต่ปี 2008

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

ข้อคาดเดานี้บอกอะไรเกี่ยวกับการเร่งความเร็วด้วยควอนตัม

คำถามนี้เกี่ยวข้องกับกรณีที่คอมพิวเตอร์ควอนตัมทำงานได้เร็วกว่าคอมพิวเตอร์แบบคลาสสิกในระดับเอ็กซ์โพเนนเชียล อัลกอริทึมแยกตัวประกอบของ Shor ในปี 1994 อาศัยโครงสร้างบางอย่าง กล่าวคือ อินพุตมีรูปแบบซ้ำที่อัลกอริทึมสามารถใช้ประโยชน์ได้ ผลลัพธ์ของ PSI กล่าวถึงกรณีตรงกันข้าม ซึ่งอินพุตเป็นแบบสุ่มหรือไม่มีโครงสร้าง และโดยทั่วไปไม่มีรูปแบบดังกล่าว

ในแบบจำลองการเรียกถาม อัลกอริทึมแบบคลาสสิกอ่านข้อมูลครั้งละหนึ่งบิตต่อการเรียกถามหนึ่งครั้ง ขณะที่การเรียกถามแบบควอนตัมสามารถกระจายอยู่ในสถานะซ้อนทับครอบคลุมตำแหน่งอินพุตหลายตำแหน่งได้ คำอธิบายของ PSI เชื่อมโยงแบบจำลองนี้กับพหุนาม กล่าวคือ หลังจากเรียกถามแบบควอนตัม T ครั้ง ความน่าจะเป็นที่อัลกอริทึมจะตอบว่าใช่จะเป็นพหุนามมีขอบเขตของบิตอินพุต ซึ่งมีดีกรีไม่เกิน 2T ดังนั้น การจำลองอัลกอริทึมควอนตัมจึงกลายเป็นปัญหาการประมาณค่าพหุนามนั้น โดยไม่ต้องอ่านบิตอินพุตจำนวนมหาศาลในระดับเอ็กซ์โพเนนเชียล

ในบทความต้นฉบับของพวกเขา Scott Aaronson และ Andris Ambainis ตั้งข้อคาดเดาว่าพหุนามดีกรีต่ำที่มีขอบเขตทุกตัวจะมีตัวแปรที่มีอิทธิพลสูง พวกเขาพิสูจน์ว่า หากข้อคาดเดานี้เป็นจริง อัลกอริทึมควอนตัมที่เรียกถาม T ครั้งทุกตัวจะจำลองได้สำหรับอินพุตส่วนใหญ่ด้วยอัลกอริทึมแบบคลาสสิกที่เรียกถามจำนวนพหุนามตาม T ผลที่ตามมาคือ จำนวนการเรียกถามแบบคลาสสิกเพิ่มขึ้นในอัตราพหุนาม แทนที่จะเป็นเอ็กซ์โพเนนเชียล สำหรับค่าความคลาดเคลื่อนในการประมาณและสัดส่วนของอินพุตที่ตัดออกใด ๆ ที่กำหนดไว้คงที่ อย่างไรก็ตาม ผลนี้ไม่ได้ตัดความเป็นไปได้ที่ควอนตัมจะได้เปรียบแบบเอ็กซ์โพเนนเชียลสำหรับปัญหาที่มีโครงสร้างเหมาะสม

ในรูปแบบทางการ คลังเก็บงานพิจารณาพหุนามจำนวนจริง p ซึ่งมีดีกรีไม่เกิน d และมีค่าอยู่ระหว่าง 0 ถึง 1 บนลูกบาศก์ไม่ต่อเนื่อง หากความแปรปรวนของพหุนามเมื่อพิจารณาอินพุตสุ่มแบบสม่ำเสมอมีค่าอย่างน้อย ε จะมีพิกัดหนึ่งที่มีอิทธิพลอย่างน้อย (8√15 / (125π⁴)) · ε^(5/2) / d⁶ และด้วยเหตุนี้จึงมีค่าอย่างน้อย (ε/d)⁷ อิทธิพลคือค่าคาดหมายของกำลังสองของการเปลี่ยนแปลงใน p เมื่อพลิกบิตของพิกัดนั้น

การสร้างและตรวจสอบข้อพิสูจน์

ข้อพิสูจน์นี้ทำตามแนวทางที่ Shachar Lovett และ Jiapeng Zhang วางไว้ โดยอาศัยใบรับรองเศษส่วนและเซตระดับ แต่แทนที่อสมการหนึ่งซึ่งแนวทางดังกล่าวยังตั้งไว้เป็นข้อคาดเดา ด้วยอสมการใหม่ที่ครอบคลุมทุกคู่ ดีเทอร์มิแนนต์ทำให้เกิดการจับคู่แบบหนึ่งต่อหนึ่งระหว่างการกำหนดค่าอินพุต PSI ระบุว่าการจับคู่นี้มีคุณสมบัติเหนือกว่าการจับคู่ใน Butterfly Lemma ของ David Reimer ซึ่งมีข้อกำหนดอ่อนกว่า เพราะยังจำกัดความถี่ที่ค่าซึ่งจับคู่กันจะตรงกันในแต่ละพิกัดด้วย ซึ่งเป็นขอบเขตที่จำเป็นต่ออสมการใหม่

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

ตามบันทึกการตรวจสอบที่คลังเก็บงานเผยแพร่ การพัฒนารูปแบบทางการไม่มีช่องว่างที่เว้นไว้สำหรับข้อพิสูจน์หรือสัจพจน์ที่เพิ่มเข้ามา มีการตรวจสอบประกาศต่าง ๆ ซ้ำผ่านเคอร์เนลของ Lean และ lean4lean ซึ่งเป็นการนำตัวตรวจสอบชนิดข้อมูลของ Lean มาใช้อย่างเป็นอิสระ ในการทำงานแบบแซนด์บ็อกซ์ เครื่องมือเปรียบเทียบที่ใช้เคอร์เนลของ nanoda และ Lean ยอมรับทฤษฎีบทสุดท้ายทั้งสี่ข้อ ส่วนในการทดสอบบนเครื่องอีกเครื่องหนึ่ง เครื่องมือนี้ยอมรับคำตอบขนาดเล็กที่ถูกต้องหนึ่งคำตอบ และปฏิเสธคำตอบที่จงใจทำให้ผิดสี่คำตอบ

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

บทบาทของมนุษย์และการตรวจทานโดยผู้เชี่ยวชาญ

David Turturean ซึ่งเป็นสมาชิกทีมเทคนิคของ PSI พัฒนาและเรียกใช้ระบบวิจัย กำหนดขอบเขตของปัญหา กระตุ้นให้โมเดลจัดทำร่างแรก ตรวจทานร่างดังกล่าว และรับผิดชอบต่อความถูกต้องของบทความ คลังเก็บงานระบุว่าโมเดล AI เป็นผู้สร้างข้อความทางคณิตศาสตร์ ร่างแรก และการทำให้เป็นรูปแบบทางการด้วย Lean Jim Halverson ตรวจสอบข้อพิสูจน์ ส่วน Phiala Shanahan ให้ความเห็นเกี่ยวกับการทำให้เป็นรูปแบบทางการ

ประกาศนี้เกิดขึ้นหลังจากมีบทความที่ส่งเมื่อวันที่ 19 สิงหาคม 2026 โดย Guy Blanc, Jordan Docter, Carmen Strassle และ Li-Yang Tan ผู้เขียนเหล่านั้นได้พิสูจน์ผลสืบเนื่องเกี่ยวกับการจำลองแบบคลาสสิกสำหรับอัลกอริทึมควอนตัมแบบขนาน โดยแสดงให้เห็นว่าอัลกอริทึมที่เรียกถาม t ครั้งและทำงาน d รอบ สามารถจำลองได้สำหรับอินพุตส่วนใหญ่ด้วยการเรียกถามแบบคลาสสิก t^(O(d²)) ครั้ง PSI ระบุว่าทั้งสี่คนกำลังอ่านข้อพิสูจน์ฉบับเต็ม ได้ให้ความเห็นแล้ว และกำลังเตรียมคำอธิบายฉบับย่อสำหรับผู้เชี่ยวชาญ

ในการประเมินที่เผยแพร่โดย PSI นักวิจัยเขียนไว้ว่า “นี่เป็นผลลัพธ์ครั้งสำคัญ ซึ่งช่วยคลี่คลายข้อคาดการณ์ที่ค้างคามานานหลายทศวรรษ และมีนัยสำคัญต่อธรรมชาติของปัญหาที่ทำให้เกิดการเร่งความเร็วด้วยควอนตัม พิสูจน์นี้ต่อยอดและขยายแนวทางการศึกษาหลายสาย ทั้งในด้านการวิเคราะห์ฟังก์ชันบูลีนและคณิตศาสตร์เชิงการจัดแบบความน่าจะเป็น ทุกอย่างถูกรวบรวมเข้าไว้ด้วยกันอย่างน่าอัศจรรย์”

บททดสอบในทันทีมีรูปธรรมอย่างยิ่ง กล่าวคือ เคอร์เนลอิสระสามารถนำข้อโต้แย้งที่เข้ารหัสไว้มาเล่นซ้ำได้ ขณะที่ผู้เชี่ยวชาญยังต้องยืนยันว่าข้อความที่เข้ารหัสตรงกับข้อคาดการณ์ของ Aaronson และ Ambainis หรือไม่ และประเมินส่วนต่าง ๆ ของบทความที่อยู่นอก Lean การแบ่งหน้าที่เช่นนี้เป็นตัวกำหนดว่าการตรวจสอบด้วยเครื่องยืนยันอะไรได้บ้าง และส่วนใดยังต้องอาศัยการทบทวนทางคณิตศาสตร์โดยมนุษย์