Vitalik Buterin ผู้ร่วมก่อตั้ง Ethereum ได้เสนอแนวคิดเกี่ยวกับภาษาโปรแกรมใหม่ ซึ่งจะถูกแปลรหัสโดยตรงไปยัง Lean หรือ HOL ซึ่งเป็นโปรแกรมช่วยตรวจสอบข้อพิสูจน์ทางคณิตศาสตร์อีกตัวหนึ่ง
แนวคิดนี้มุ่งเป้าไปที่ช่องว่างเฉพาะในการที่ผู้คนอ่านผลลัพธ์ของ AI เนื่องจากปัญญาประดิษฐ์สามารถสร้างบล็อกข้อพิสูจน์โดยอัตโนมัติขนาดใหญ่ได้มากขึ้นเรื่อยๆ และรวดเร็วยิ่งกว่าทีมนักพัฒนามนุษย์ใดๆ จะสามารถเขียนด้วยมือได้ ผู้อ่านเพียงไม่กี่คนเท่านั้นที่สามารถยืนยันอย่างรวดเร็วได้ว่าข้อพิสูจน์เหล่านั้นพิสูจน์เรื่องใดจริงๆ
ภาษาที่สร้างขึ้นเพื่อผู้อ่านข้อพิสูจน์ของ AI เท่านั้น
Lean เป็นโปรแกรมช่วยตรวจสอบข้อพิสูจน์ซึ่งเป็นซอฟต์แวร์ที่นักคณิตศาสตร์และวิศวกรใช้ในการเขียนข้อพิสูจน์ที่คอมพิวเตอร์สามารถตรวจสอบทีละบรรทัดได้ นักวิจัย Ethereum ก็ใช้โปรแกรมนี้ในการตรวจสอบโค้ดการเข้ารหัสและตรรกะของฉันทามติ โปรแกรมช่วยตรวจสอบข้อพิสูจน์มีมาหลายสิบปีแล้ว แต่ก็ยังคงเป็นกลุ่มความสนใจเฉพาะทาง
ใน โพสต์ของเขา Buterin อธิบายว่าขั้นตอนภายในของข้อพิสูจน์มีข้อกำหนดเพียงอย่าเดียวคือความถูกต้องทางคณิตศาสตร์และไม่มีสิ่งอื่นใด ผู้อ่านจะไม่ตรวจสอบกลไกภายในเหล่านั้นโดยตรง เพราะคำจำกัดความและทฤษฎีบทนั้นแตกต่างกัน เนื่องจากมนุษย์อ่านส่วนเหล่านั้นเพื่อเรียนรู้ว่าซอฟต์แวร์รับประกันอะไรเป็นหลัก
Buterin ยังได้สำรวจความแตกต่างที่เกี่ยวข้องใน บล็อกของเขาในเดือนพฤษภาคมว่า ข้อพิสูจน์ทางคณิตศาสตร์ช่วยแสดงให้เห็นว่าโค้ดระดับต่ำที่มีประสิทธิภาพนั้นตรงตามข้อกำหนดแยกที่อ่านเข้าใจได้ ดังนั้นการตรวจสอบครั้งเดียวจะครอบคลุมทั้งสองเวอร์ชันพร้อมกัน
นอกจากนี้ ระยะเวลานี้ยังสอดคล้องกับความพยายามสร้างระบบใหม่ของ Ethereum ซึ่งมีฉายาว่า Lean Ethereum roadmap และนักวิจัยก็กำลังพัฒนา ZK-EVM ที่ตรวจสอบได้อย่างเป็นทางการ ซึ่งเป็นเวอร์ชันโปร่งใสด้วย zero-knowledge ของ EVM ของ Ethereum โดยใช้วิธีการที่คล้ายกัน
AI เขียนข้อพิสูจน์ มนุษย์ตรวจสอบข้ออ้าง
โมเดลภาษาแบบใหญ่สามารถเขียนข้อพิสูจน์ Lean ที่ใช้งานได้แล้ว โดย Buterin ได้ระบุชื่อ Claude และ Deepseek 4 Pro ว่าเป็นเครื่องมือที่มีความสามารถ ควบคู่กับ Leanstral ซึ่งเป็นโมเดลขนาดเล็กที่ปรับแต่งมาโดยเฉพาะสำหรับ Lean ตัวอย่างหนึ่งคือโปรเจกต์ evm-asm ซึ่งเป็นการนำ EVM ไปใช้งานจริงและได้รับการตรวจสอบกับแหล่งอ้างอิงที่อ่านเข้าใจได้ ความสามารถนี้สะท้อนถึงทักษะการให้เหตุผลที่นักพัฒนาแสดงให้เห็นใน ชาเลนจ์ AI ล่าสุดของ Buterin โดยผู้ทดสอบสามารถแก้ปัญหาได้ภายในไม่กี่ชั่วโมง
อย่างไรก็ตาม ประเด็นนี้มีความสำคัญมากกว่าแค่เรื่องความสะดวกสบาย เพราะนักวิจัยด้านความปลอดภัยได้ติดตามพบการพยายามนำ AI เข้ามาช่วยในการ โจมตีช่องโหว่ มากขึ้นในปีนี้ โค้ดที่ตรวจสอบตามหลักการจะเป็นแนวป้องกันแนวหนึ่งต่อแนวโน้มดังกล่าว และถ้ามีภาษาสเปกที่เป็นมิตรมากขึ้น นักพัฒนาก็จะตรวจสอบข้อเรียกร้องได้ โดยไม่ต้องอ่านข้อพิสูจน์ที่อยู่รอบข้างทั้งหมด
ไกลกว่ากลุ่มนักวิจัยของ Ethereum
Buterin ยังคงทดสอบแนวคิดเหล่านี้ต่อสาธารณะ เพราะไม่นานมานี้เขาได้สาธิต billboard แบบไม่ระบุตัวตน ที่สร้างด้วย zero-knowledge proofs ซึ่งการสาธิตนี้ได้แสดงให้เห็นว่าการอ้างสิทธิ์ที่ตรวจสอบได้สามารถเปลี่ยนจากคลังวิจัยไปสู่ผลิตภัณฑ์ที่ใช้งานจริงได้อย่างไร นอกจากนี้ นักวิจัยยังได้เริ่มต้นทำการตรวจสอบ client ของ consensus บน Lean เพื่อจับข้อบกพร่องตั้งแต่เนิ่นๆ อีกด้วย
อย่างไรก็ตาม ทิศทางนี้ยังคงสะท้อนรูปแบบที่คุ้นเคย ซึ่งก็คือการแยกรหัสที่ทำงานได้รวดเร็วออกจากการอ้างสิทธิ์ที่อ่านเข้าใจง่าย จากนั้นจึงพิสูจน์ว่าทั้งสองส่วนสอดคล้องกัน
ในขณะนี้ ยังไม่มีต้นแบบของภาษานี้ใหม่ และ Buterin ก็ยังไม่กำหนดโครงสร้างภาษาที่ชัดเจน นักพัฒนาอาจรวมตัวกันเลือกใช้มาตรฐานเดียว หรืออาจจะมีหลายสำเนียงที่เข้ากันไม่ได้ก็เป็นได้ ซึ่งตัวเลือกนี้อาจกลายเป็นปัจจัยตัดสินว่าระบบผลิตจะนำเอาโค้ดที่ได้รับการตรวจสอบจาก AI ไปใช้ได้เร็วเพียงใด
