สำนักข่าวต่างประเทศรายงานว่า บริษัทแอนโทรปิก เจ้าของโมเดลปัญญาประประดิษฐ์ “คล็อด” เพิ่งเปิดเผยเมื่อสัปดาห์ที่แล้วว่า เอไอคล็อด สามารถแปลง “บทพิสูจน์สุดท้ายของแฟร์มา” (Fermat’s Last Theorem) ซึ่งเป็นหนึ่งในโจทย์คณิตศาสตร์ที่ท้าทายที่สุดในประวัติศาสตร์ ให้กลายเป็นโค้ดภาษา Lean (ภาษาโปรแกรมที่ออกแบบมาเพื่อตรวจสอบความถูกต้องทางคณิตศาสตร์ โดยเปลี่ยนบทพิสูจน์หรือตรรกะที่มนุษย์เขียนให้กลายเป็นโค้ด เพื่อให้คอมพิวเตอร์สามารถเช็กทีละบรรทัดได้ 100% ว่าถูกต้อง โดยปราศจากข้อผิดพลาดหรืออคติของมนุษย์) ความยาวกว่า 13 ล้านบรรทัด ได้สำเร็จภายในเวลาเพียง 11 วัน โดยคอมพิวเตอร์สามารถตรวจสอบความถูกต้องทางตรรกะได้ด้วยตนเองทั้งหมดโดยไม่ต้องอาศัยการตรวจทานจากมนุษย์อีกต่อไป

ปิแอร์ เดอ แฟร์มา เป็นผู้เสนอบทพิสูจน์นี้โดยเขียนไว้ว่า “ไม่มีจำนวนเต็มบวกสามจำนวนที่เมื่อนำแต่ละจำนวนมายกกำลังด้วยตัวเลขที่มากกว่า 2 แล้ว จะทำให้สองจำนวนแรกบวกกันแล้วได้เท่ากับจำนวนที่สาม ($a^n + b^n = c^n$ เมื่อ $n > 2$)

แฟร์มาเขียนข้อความนี้ไว้ตรงขอบหน้าหนังสือคณิตศาสตร์เล่มหนึ่งเมื่อปี ค.ศ. 1637 พร้อมทิ้งท้ายไว้ว่า เขามี “บทพิสูจน์ที่อัศจรรย์ยิ่ง” แต่พื้นที่ตรงขอบหน้านั้นเล็กเกินกว่าจะเขียนได้ ต่อมา เขาก็เสียชีวิต ทำให้นักคณิตศาสตร์ต้องใช้เวลานานถึง 358 ปี เพื่อพิสูจน์โจทย์ข้อนี้ เมื่อ แอนดรูว์ ไวลส์ สามารถตีพิมพ์บทพิสูจน์ความยาว 129 หน้าได้สำเร็จในปี ค.ศ. 1995  

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

เดิมที เควิน บัซซาร์ด จากวิทยาลัยอิมพีเรียลแห่งลอนดอน ได้ตั้งโครงการอาสาสมัครเพื่อทำสิ่งนี้ โดยวางแผนงานไว้ถึงปี ค.ศ. 2029 แต่เอไอคล็อดกลับทำสำเร็จในเวลาเพียง 11 วัน

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

ด้วยการบริหารจัดการรายการคำสั่งแบบเรียลไทม์เพื่อป้องกันการทำงานซ้ำซ้อนนี้เอง ส่งผลให้เอเจนต์ เอไอคล็อด สามารถพิสูจน์ทฤษฎีบทย่อยได้มากกว่า 30,000 ทฤษฎีบท ปรากฏออกมาเป็นโค้ด 13 ล้านบรรทัด ซึ่งเทียบเท่ากับความยาวของนวนิยายถึง 160 เล่ม 

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

เรียบเรียงโดย : ทีมข่าวต่างประเทศ

ที่มา : decrypt.co

เครดิตภาพ : REUTERS