อดีตนักวิจัยจาก Axiom Math และ Kimi ร่วมกันก่อตั้งสตาร์ทอัพ ใช้ AI พิชิตความท้าทายในการตรวจสอบชิป

动察 Beating ข่าวด่วน AI หนึ่งในสิ่งที่วงการออกแบบชิปกลัวที่สุดคือการค้นพบข้อผิดพลาดทางตรรกะหลังจากผลิตออกมาแล้ว เมื่อเกิดปัญหา อาจต้องออกแบบใหม่ ผลิตเวเฟอร์ใหม่ ซ้ำด้วยต้นทุนที่สูง การตรวจสอบชิปจึงมีเป้าหมายเพื่อค้นหาข้อผิดพลาดที่ซ่อนอยู่เหล่านี้ให้ได้มากที่สุดก่อนการผลิต

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

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

ตามรายงานของ雷峰网 จางจวี้เจี้ยน อดีตหัวหน้าฝ่ายตรวจสอบเชิงรูปแบบของ Axiom Math และหลิวจวิ้นฉี ซึ่งเคยวิจัยคณิตศาสตร์ AI ที่月之暗面 ได้ก่อตั้งบริษัท 北京有理数科技 โดยใช้ AI เพื่อทำงานพิสูจน์เชิงรูปแบบของชิปโดยอัตโนมัติมากขึ้น บริษัทได้ระดมทุนรอบ seed สำเร็จแล้ว

ทั้งสองคนมีพื้นฐานที่แข็งแกร่งด้านการพิสูจน์ทางคณิตศาสตร์ จางจวี้เจี้ยนเคยมีส่วนร่วมในการพัฒนา Mathlib และ AxiomProver หลิวจวิ้นฉีเป็นผู้เขียนหลักของ Numina-Lean-Agent ซึ่งระบบนี้เคยพิสูจน์โจทย์ทั้ง 12 ข้อของการแข่งขันคณิตศาสตร์ Putnam ปี 2025 ได้สำเร็จ และตรวจสอบกระบวนการพิสูจน์ผ่านเครื่องมือ Lean

ปัจจุบัน 有理数ได้ผ่านต้นแบบทางเทคนิคแล้ว ในโครงการชิปที่เกี่ยวข้องกับโค้ด RTL หลายแสนบรรทัด สามารถตรวจสอบข้อความยืนยันบางส่วนที่เครื่องมือ EDA ที่มีอยู่ไม่สามารถตัดสินได้ ทีมกำลังร่วมมือกับลูกค้าชิปเพื่อพยายามพัฒนาความสามารถนี้ให้เป็นบริการตรวจสอบเชิงพาณิชย์