เมื่อเร็ว ๆ นี้ ChatGPT ได้รับความนิยมและมีผู้ใช้งานเกิน 100 ล้านคนในเวลาเพียงสองเดือนนับตั้งแต่เปิดตัว การใช้มันเพื่อเขียนบทความ เขียนโค้ด ตกหลุมรัก หางาน และตอบอีเมลกลายเป็นงานประจำ มีหลายวิธี ที่จะสอนให้คุณใช้ซอฟต์แวร์นี้เพื่อ "สร้างรายได้" บนอินเทอร์เน็ต แม้แต่ศาสตราจารย์จาก Wharton School of Business แห่งมหาวิทยาลัยเพนซิลเวเนียอ้างว่า "นักเรียน" ChatGPT ผ่านการสอบการจัดการธุรกิจ

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

ปัญญาประดิษฐ์หรือ "ผลิตภัณฑ์คอมพิวเตอร์" เช่นการตรวจสอบอย่างเป็นทางการสามารถแทนที่มนุษย์ได้หรือไม่? ในโลกของ Web3.0 การตรวจสอบอย่างเป็นทางการสามารถแทนที่การตรวจสอบด้วยตนเองได้หรือไม่

การตรวจสอบอย่างเป็นทางการ

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

การประยุกต์ใช้การตรวจสอบอย่างเป็นทางการ

การตรวจสอบอย่างเป็นทางการเป็นเครื่องมือที่สามารถใช้กันอย่างแพร่หลายในระบบต่างๆ รวมถึง:

• การออกแบบฮาร์ดแวร์คอมพิวเตอร์: ตรวจสอบให้แน่ใจว่าวงจรรวมและระบบดิจิทัลเป็นไปตามข้อกำหนดที่จำเป็นและทำงานได้อย่างถูกต้อง

• วิศวกรรมซอฟต์แวร์: การตรวจสอบความถูกต้องและความน่าเชื่อถือของระบบซอฟต์แวร์ โดยเฉพาะอย่างยิ่งในแอปพลิเคชัน/โดเมนที่มีความสำคัญต่อภารกิจ เช่น การบิน อุปกรณ์ทางการแพทย์ และระบบการเงิน

• ความปลอดภัยเครือข่าย: ประเมินความปลอดภัยของอัลกอริธึมการเข้ารหัสและโปรโตคอล และระบุช่องว่างด้านความปลอดภัยในระบบที่ไวต่อความปลอดภัย

• AI และการเรียนรู้ของเครื่อง: ตรวจสอบคุณสมบัติและพฤติกรรมของโมเดล AI และ ML เพื่อให้มั่นใจว่าทำงานได้ตามที่คาดหวังและคาดการณ์ได้อย่างแม่นยำ

• การพิสูจน์ทฤษฎีบทอัตโนมัติ: การตรวจสอบทฤษฎีบททางคณิตศาสตร์และการพิสูจน์การคาดคะเนทางคณิตศาสตร์ นำไปใช้ในสาขาคณิตศาสตร์ ฟิสิกส์ และวิทยาการคอมพิวเตอร์

• บล็อกเชนและสัญญาอัจฉริยะ: ตรวจสอบความถูกต้อง ความปลอดภัย และความน่าเชื่อถือของระบบบล็อกเชนและสัญญาอัจฉริยะ

การตรวจสอบอย่างเป็นทางการของสัญญาอัจฉริยะ

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

กระบวนการนี้รวมถึง:

• ข้อกำหนดและคุณสมบัติของสัญญาถูกกำหนดเป็นภาษาที่เป็นทางการ

• แปลรหัสของสัญญา"” ในการแสดงที่เป็นทางการ เช่น ตรรกะทางคณิตศาสตร์หรือแบบจำลอง

• ใช้ตัวพิสูจน์ทฤษฎีบทอัตโนมัติหรือตัวตรวจสอบแบบจำลองเพื่อตรวจสอบว่าข้อกำหนดและคุณสมบัติของสัญญามีอยู่จริง

• ทำขั้นตอนการตรวจสอบซ้ำเพื่อค้นหาและแก้ไขข้อผิดพลาดหรือการเบี่ยงเบนจากความคาดหวัง

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

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

การตรวจสอบอย่างเป็นทางการสามารถใช้กับสัญญาเดียวหรือหลายสัญญาในเวลาเดียวกัน โครงการ Web3.0 มักใช้สัญญาหลายฉบับ และสิ่งสำคัญคือต้องแน่ใจว่าสัญญาเหล่านี้ทำงานร่วมกันและใช้ฟังก์ชันโครงการที่ต้องการอย่างถูกต้อง

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

ทำให้รหัสเป็นทางการ

ข้อมูลโค้ดตัวอย่างที่หนึ่ง

รหัสต่อไปนี้แสดงโปรแกรมฟังก์ชันการถ่ายโอนโทเค็นอย่างง่าย: มีผู้ใช้สองคน แต่ละคนมีโทเค็นบางส่วน (บาลานซ์และบาลานซ์ 2) ฟังก์ชัน TransferFromUser 1 จะถ่ายโอนโทเค็นจากผู้ใช้ 1 ไปยังผู้ใช้ 2 โปรแกรมมีค่าไม่แปรผันที่การจัดหาโทเค็นทั้งหมดจะเท่ากับผลรวมของยอดคงเหลือเสมอ

ข้อมูลโค้ด 1: โปรแกรมโอนโทเค็น

เราแสดงค่าคงที่ด้วยสูตรทางคณิตศาสตร์และกำหนดหมายเลขสูตร ในสูตรทางคณิตศาสตร์ "=" หมายถึง "เท่ากับ" ไม่ใช่การมอบหมาย

ตัวอย่างโค้ด 2

รหัสต่อไปนี้แสดงวิธีการเพิ่มสูตรตรรกะ (จำนวนเต็มล้นจะถูกละเว้นเพื่อความง่ายและความชัดเจนของตัวอย่าง)

ข้อมูลโค้ด 2: ฟังก์ชันสูตรตรรกะที่แสดงความหมายของโค้ด

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

การทำงานร่วมกันของการตรวจสอบอย่างเป็นทางการและการตรวจสอบด้วยตนเอง

ในแง่ของการรับประกันความปลอดภัยของสัญญาอัจฉริยะ การตรวจสอบอย่างเป็นทางการและการตรวจสอบด้วยตนเองอาจกล่าวได้ว่าเสริมซึ่งกันและกัน

การตรวจสอบอย่างเป็นทางการ:

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

เมื่อต้องรับมือกับสัญญาที่ซับซ้อนหรือหลายฉบับ เป็นเรื่องยากสำหรับมนุษย์ที่จะให้เหตุผลเกี่ยวกับชุดค่าผสมและความเป็นไปได้ทั้งหมดที่ต้องตรวจสอบ ในขณะที่เครื่องจักรนั้น "ไม่มีแรงกดดัน"

การตรวจสอบด้วยตนเอง:

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

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

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

ผู้เชี่ยวชาญด้านความปลอดภัยออนไลน์ AMA

ไม่สามารถประเมินพลังของการตรวจสอบอย่างเป็นทางการได้ต่ำเกินไป แต่ไม่ควรเพิกเฉยต่อความสำคัญของการตรวจสอบด้วยตนเอง บนเว็บไซต์อย่างเป็นทางการของ ChatGPT ได้ยอมรับข้อบกพร่องของตัวเอง และการอภิปรายทั่วไปที่ว่าปัญญาประดิษฐ์ไม่สามารถแทนที่ความคิดและการสร้างสรรค์ของมนุษย์สามารถละเว้น 10,000 คำที่นี่... ไม่ Bard ทำผิดพลาด และราคาหุ้นของ Google ดิ่งลง

ในทำนองเดียวกัน การตรวจสอบอย่างเป็นทางการไม่สามารถแทนที่การตรวจสอบด้วยตนเองได้ และทั้งสองส่วนเสริมซึ่งกันและกันในการตรวจสอบสัญญาอัจฉริยะอย่างสมบูรณ์

มีคำถามใด ๆ หลังจากอ่านบทความ? ทำไมไม่มาเป็นแขกรับเชิญที่ [CertiK Twitter AMA] ใน [วันศุกร์ที่ 10 กุมภาพันธ์ ประเทศญี่ปุ่น] และถามตอบออนไลน์แบบตัวต่อตัวกับผู้เชี่ยวชาญ! เพื่อน ๆ ที่ไม่สามารถเข้าร่วมได้เนื่องจากอาการเจ็ตแล็กสามารถฝากข้อความไว้เบื้องหลัง และเราจะแจ้งให้คุณทราบและเผยแพร่เนื้อหาของการเล่นซ้ำของ AMA!