ผู้ร่วมก่อตั้ง Ethereum Vitalik Buterin เสนอภาษาโปรแกรมใหม่ ซึ่งจะคอมไพล์โดยตรงเป็น Lean หรือ HOL ซึ่งเป็นเครื่องมือช่วยพิสูจน์ทางรูปแบบอีกชนิดหนึ่ง
แนวคิดนี้มุ่งเน้นไปที่ช่องว่างเฉพาะในการอ่านผลลัพธ์จากปัญญาประดิษฐ์ ปัญญาประดิษฐ์ผลิตหลักฐานอัตโนมัติจำนวนมากขึ้นเรื่อยๆ มักเร็วกว่าทีมมนุษย์ใดๆ จะเขียนด้วยมือ ผู้อ่านน้อยรายสามารถยืนยันได้อย่างรวดเร็วว่าหลักฐานเหล่านั้นพิสูจน์อะไร
ภาษาที่สร้างขึ้นเฉพาะสำหรับผู้ตรวจสอบของ AI
Lean เป็นเครื่องมือช่วยพิสูจน์ ซึ่งเป็นซอฟต์แวร์ที่นักคณิตศาสตร์และวิศวกรใช้เขียนการพิสูจน์ที่คอมพิวเตอร์สามารถตรวจสอบทีละบรรทัด นักวิจัยของ Ethereum ได้ใช้มันแล้วเพื่อยืนยันรหัสเข้ารหัสและตรรกะการบรรลุข้อตกลง เครื่องมือช่วยพิสูจน์มีอยู่มานานเกือบ 60 ปี แต่สาขา này ยังคงเป็นการศึกษาที่มีผู้สนใจน้อย
ใน โพสต์ ของเขา บูเทอรินโต้แย้งว่าขั้นตอนภายในของหลักฐานมีเพียงข้อกำหนดเดียว นั่นคือความถูกต้องทางคณิตศาสตร์ ไม่มีอะไรเพิ่มเติม ผู้อ่านไม่เคยตรวจสอบกลไกนั้นโดยตรง นิยามและทฤษฎีบททำงานต่างกัน เพราะมนุษย์อ่านส่วนเหล่านั้นเพื่อเรียนรู้ว่าซอฟต์แวร์ชิ้นหนึ่งรับประกันอะไรจริงๆ
บูเทอรินได้สำรวจการแบ่งแยกที่เกี่ยวข้องในโพสต์บล็อกเดือน blog ที่ผ่านมา ซึ่งมีการพิสูจน์ทางคณิตศาสตร์แสดงว่าโค้ดระดับต่ำที่มีประสิทธิภาพสอดคล้องกับข้อกำหนดที่อ่านเข้าใจได้แยกต่างหาก ดังนั้นการตรวจสอบเพียงครั้งเดียวจึงครอบคลุมทั้งสองเวอร์ชันพร้อมกัน
เวลาของเขาสอดคล้องกับความพยายามในการปรับปรุงใหม่ของ Ethereum ซึ่งมีชื่อเล่นอีกชื่อหนึ่งว่า Lean Ethereum roadmap ในขณะเดียวกัน นักวิจัยกำลังพัฒนา formally verified ZK-EVM ซึ่งเป็นเวอร์ชันของเครื่องเสมือนของ Ethereum (EVM) ที่สามารถพิสูจน์ด้วย zero-knowledge โดยใช้วิธีการที่คล้ายกัน
AI เขียนหลักฐาน มนุษย์ตรวจสอบข้ออ้าง
โมเดลภาษาขนาดใหญ่สามารถเขียนหลักฐาน Lean ที่ใช้งานได้แล้ว บูเทอรินได้ระบุ Claude และ Deepseek 4 Pro เป็นเครื่องมือที่มีความสามารถ ร่วมกับ Leanstral ซึ่งเป็นโมเดลขนาดเล็กที่ถูกปรับแต่งโดยเฉพาะสำหรับ Lean ตัวอย่างโครงการหนึ่งคือ evm-asm ซึ่งเป็นการนำเอวีเอ็มมาตรวจสอบเทียบกับเอกสารอ้างอิงที่อ่านเข้าใจได้ ความสามารถนี้สะท้อนทักษะการให้เหตุผลของนักพัฒนาที่แสดงออกมาในความท้าทาย AI ของบูเทอรินเมื่อเร็วๆ นี้ ผู้ทดสอบสามารถแก้ความท้าทายนี้ภายในไม่กี่ชั่วโมง
การ Stake ไม่ได้จำกัดอยู่แค่ความสะดวกสบายเท่านั้น นักวิจัยด้านความปลอดภัยได้ติดตามการเพิ่มขึ้นของความพยายามในการโจมตีที่ได้รับการช่วยเหลือจาก AI exploit attempts ในปีนี้ โค้ดที่ได้รับการยืนยันอย่างเป็นทางการเป็นหนึ่งในวิธีป้องกันแนวโน้มนี้ ภาษาคำอธิบายที่ใช้งานง่ายกว่าจะช่วยให้นักพัฒนาสามารถตรวจสอบข้ออ้างโดยไม่ต้องเจาะลึกผ่านหลักฐานที่อยู่รอบข้าง
เกินกว่าวงการวิจัยของ Ethereum
บูเทอรินยังคงทดสอบแนวคิดเหล่านี้ในที่สาธารณะ โดยล่าสุดเขาได้สาธิต ป้ายโฆษณาแบบไม่เปิดเผยตัวตน ที่สร้างขึ้นด้วย zero-knowledge proof การสาธิตนี้แสดงให้เห็นว่าการอ้างสิทธิ์ที่สามารถตรวจสอบได้สามารถย้ายจากคลังการวิจัยไปสู่ผลิตภัณฑ์ที่ใช้งานได้จริง นักวิจัยยังเริ่มตรวจสอบ consensus clients อย่างเป็นทางการใน Lean เพื่อจับบั๊กตั้งแต่เนิ่นๆ
อย่างไรก็ตาม ทิศทางนี้สะท้อนรูปแบบที่คุ้นเคย: แยกโค้ดที่เร็วออกจากข้ออ้างที่อ่านเข้าใจได้ แล้วพิสูจน์ว่าทั้งสองสิ่งนี้ตรงกัน
ยังไม่มีต้นแบบของภาษาใหม่นี้ และบูเทอรินได้ปล่อยให้ไวยากรณ์ที่แน่นอนเปิดอยู่ นักพัฒนาอาจรวมตัวกันไปสู่มาตรฐานร่วมเดียว หรืออาจยอมรับหลายสำเนียงที่ไม่สามารถใช้งานร่วมกันได้ การตัดสินใจนี้อาจกำหนดความเร็วที่โค้ดที่ได้รับการยืนยันโดย AI จะเข้าสู่ระบบผลิต