AlphaProof Code กับ MathForm-8B: สองขั้นตอนของ Lean Pipeline เดียวกัน ไม่ใช่คู่แข่งกันสองราย

อ่านบทความ AlphaProof Code อย่างละเอียดแล้วจะมีตัวเลขหนึ่งผุดขึ้นมาซึ่งประกาศไม่ได้เน้น: จากสี่สัปดาห์ที่นักวิจัยห้าคนของ DeepMind ใช้ตรวจสอบ Signal ส่วนที่ไม่สามารถทำให้เป็นอัตโนมัติได้คือช่วงหน้า ผู้เชี่ยวชาญที่เป็นมนุษย์ทำงานร่วมกับโมเดลหลายแบบผสมกันเพื่อแปลเป้าหมายด้านความปลอดภัยของ Signal ให้เป็นข้อกำหนด Lean เชิงรูปแบบ และผู้เชี่ยวชาญตรวจทานทุกข้อก่อนที่งานพิสูจน์ใด ๆ จะเริ่มต้น นั่นคือคอขวด MathForm-8B โมเดล autoformalization ขนาด 8 พันล้านพารามิเตอร์ของ OpenBMB ที่เปิดตัวบน Hugging Face เมื่อวันที่ 14 สิงหาคม 2026 คือความพยายามโดยตรงที่จะทำให้ขั้นตอนนั้นเป็นอัตโนมัติ — รับข้อความทางคณิตศาสตร์ในภาษาธรรมชาติและส่งออกข้อความทฤษฎีบท Lean 4 ที่พร้อมให้คนอื่นนำไปพิสูจน์ เมื่อวางเทียบกัน คุณไม่ได้กำลังเปรียบเทียบผลิตภัณฑ์สองตัว คุณกำลังมองสองขั้นตอนที่ต่อเนื่องกันของไปป์ไลน์เดียว โดยคั่นด้วยความแตกต่างระหว่างคณิตศาสตร์กับความปลอดภัยของโปรโตคอล

ไปป์ไลน์ ตามลำดับขั้นตอนการทำงาน

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

MathForm-8B ทำงานที่หนึ่งสำหรับกลุ่มอินพุตที่แคบ นั่นคือข้อความทางคณิตศาสตร์แบบตำราเรียน ถ้าให้ข้อความว่า “สำหรับจำนวนจริง x ทุกจำนวน x² ไม่เป็นลบ” มันจะคืนคำสั่ง import ชนิด และส่วนหัวทฤษฎีบทใน Lean 4 สิ่งที่มันไม่คืนมาคือบทพิสูจน์ และผู้เขียนระบุอย่างชัดเจนว่าการค้นหาบทพิสูจน์เป็นเรื่องของคนอื่น ตัวเลขที่รายงาน ซึ่งเป็นข้อมูลจากผู้ขายทั้งหมดและยังไม่มีการทำซ้ำ คือ 88.06% เฉลี่ย Pass@8 ภายใต้การตรวจสอบไวยากรณ์ และ 72.37% ภายใต้การตรวจสอบความสอดคล้องที่เข้มงวดกว่า ในหกเกณฑ์มาตรฐาน ช่องว่างระหว่างตัวเลขสองตัวนั้นคือมาตรวัดที่ตรงไปตรงมาว่าข้อความที่ถูกต้องตามไวยากรณ์มีความหมายต่างจากสิ่งที่ขอไว้บ่อยเพียงใด

AlphaProof Code ทำงานที่สองและสาม รวมถึงขั้นตอนการกำหนดข้อกำหนดเฉพาะที่ MathForm-8B ไม่สามารถแตะต้องได้ เป้าหมายด้านความปลอดภัยของ Signal ไม่ใช่ข้อกล่าวอ้างทางคณิตศาสตร์ในความหมายแบบที่ MathForm ถูกฝึกมา แต่เป็นข้อความเกี่ยวกับโปรโตคอล — ว่าข้อความยังคงได้รับการปกป้องก่อนและหลังอุปกรณ์ถูกบุกรุกชั่วคราว และว่าผู้เริ่มต้นกับผู้ตอบกลับเป็นผู้ที่ตนอ้างว่าเป็น การแปลงสิ่งเหล่านี้ให้เป็น Lean ต้องใช้ความเชี่ยวชาญด้านโปรโตคอลที่ระบบออโตฟอร์มาลไลเซอร์ขนาด 8B ไม่มี เมื่อข้อกำหนดเฉพาะมีอยู่แล้ว งานพิสูจน์ก็ถูกมอบให้เอเจนต์ทั้งหมด และการตรวจสอบก็ถูกมอบให้เคอร์เนลของ Lean พร้อมกับเอเจนต์ผู้เฝ้าประตูที่ใช้ comparatorกับสำเนาข้อกำหนดที่เก็บแยกไว้

ค่าใช้จ่ายที่แท้จริงของแต่ละอย่างเมื่อคุณใช้งาน

• {{1}}เวต{{/1}} — MathForm-8B: ดาวน์โหลดได้, Apache 2.0, safetensors สี่ชาร์ดใน BF16, ไฟน์ทูนจาก Qwen3-8B. {{2}}AlphaProof Code{{/2}}: ไม่มี. รีลีสนี้ประกอบด้วยงานพัฒนาด้วย Lean, semantics ของ AArch64 และ libsignal binding ที่ github.com/google-deepmind/code-verification.

• การรันมัน — MathForm-8B: Transformers, vLLM หรือ SGLang ซึ่งทั้งหมดเปิดเอนด์พอยต์ที่เข้ากันได้กับ OpenAI บนฮาร์ดแวร์ที่คุณเป็นเจ้าของ AlphaProof Code: ไม่มีเอนด์พอยต์ ไม่มี API ไม่มีรายการรอ ไม่มีราคา; มันเป็นกรอบการวิจัยที่ DeepMind กล่าวว่าต้องมี "การวิจัยอย่างต่อเนื่อง" ก่อนที่จะขยายขนาดได้

• อินพุต — MathForm-8B: ข้อความคณิตศาสตร์ในภาษาธรรมชาติ AlphaProof Code: ข้อกำหนดเชิงรูปแบบพร้อมไบนารีที่คุณต้องการให้พิสูจน์เทียบกับข้อกำหนดนั้น

• ผลลัพธ์ — MathForm-8B: ข้อความทฤษฎีบท Lean 4 ที่ยังไม่ได้พิสูจน์ AlphaProof Code: การพิสูจน์ที่ตรวจสอบโดยเครื่อง หรือการหักล้างเมื่อโค้ดมีข้อผิดพลาด

• การตรวจทานโดยมนุษย์ — MathForm-8B: คุณจะตรวจทานข้อความที่ส่งออกมา และด้วยความสอดคล้อง 72.37% คุณจะต้องตรวจทานข้อความเหล่านี้เป็นจำนวนมาก AlphaProof Code: ผู้เชี่ยวชาญตรวจทานทุกข้อกำหนดก่อนที่งานพิสูจน์จะเริ่มต้น จากนั้นเอเจนต์จะแจ้งให้ตรวจสอบโค้ดเบสประมาณ 1% อีกครั้ง

• ข้อจำกัดที่ทราบ — MathForm-8B: รองรับเฉพาะข้อความทางคณิตศาสตร์เท่านั้น ไม่มีการสร้างข้อพิสูจน์ และที่เก็บโค้ดที่ลิงก์ใน README ยังเป็นตัวยึดตำแหน่ง ณ เวลาที่เผยแพร่ AlphaProof Code: ไม่มีการรับประกันหลังควอนตัมสำหรับการฟื้นฟู SPQR ไม่มีความเป็นส่วนตัวของเพย์โหลด หนึ่งเซสชันต่อการโปรโมต และขอบเขตการปลอมแปลง MAC ที่กลายเป็นโมฆะเมื่อใกล้ 25,000 ข้อความในเซสชันเดียว

ช่องว่างที่ MathForm-8B จะต้องปิด

มันชวนให้พูดว่า autoformalizer น่าจะเขียนข้อกำหนดของ Signal ได้และช่วยนักวิจัยประหยัดเวลาหลายสัปดาห์ที่ต้องทุ่มเทตั้งแต่ต้น แต่บทความเองบอกไว้เป็นอย่างอื่น และเหตุผลก็เฉพาะเจาะจง ข้อกำหนดของโปรโตคอลไม่ใช่การทวนข้อกล่าวอ้างซ้ำ แต่เป็นการเลือกเกี่ยวกับแบบจำลองฝ่ายตรงข้าม งานของ Signal มีเส้นทางเชิงสัญลักษณ์ในแบบ Dolev–Yao ด้วยผู้โจมตีเชิงควอนตัมที่ทำลาย Diffie–Hellman หลังแฮนด์เชก และมีเส้นทางเชิงคำนวณด้วยฝ่ายตรงข้ามแบบคลาสสิกและขอบเขตที่เป็นรูปธรรม สองเส้นทางนี้กล่าวถึงทฤษฎีบทที่ต่างกันเกี่ยวกับโค้ดเดียวกัน และการเลือกระหว่างสองสิ่งนี้เป็นการตัดสินใจทางวิศวกรรมที่ส่งผลต่อความปลอดภัย ไม่มีแบบจำลองใดที่ถูกฝึกมาให้เปลี่ยน "show that x² ≥ 0" เป็น Lean ที่จะตัดสินใจเรื่องนั้นได้

สิ่งที่ออโตฟอร์มาลไลเซอร์น่าจะทำได้คือส่วนที่เป็นกลไกของงานนั้น เมื่อได้รับเป้าหมายความปลอดภัยที่เขียนเป็นร้อยแก้วและไลบรารีของนิยาม Lean ที่มีอยู่ ก็สร้างร่างแรกของข้อความในสำนวนเฉพาะของโครงการ เพื่อให้ผู้เชี่ยวชาญแก้ไข นั่นเป็นการประหยัดจริง และน้อยกว่าที่พาดหัวข่าวชี้ให้เห็นมาก บทความรายงานแคตตาล็อกความเบี่ยงเบนจากสเปกซึ่งมีรายการเชิงคำนวณกว่า 200 รายการและรายการเชิงสัญลักษณ์ประมาณ 35 รายการ โดยสิบห้ารายการเป็นช่องว่างหรือบั๊กในการวิเคราะห์ Double Ratchet ซึ่งเป็นสิ่งที่ขั้นตอนการตรวจทานโดยมนุษย์พบ โมเดลที่ร่างข้อความจะต้องถูกวัดเทียบกับแคตตาล็อกนั้น ไม่ใช่เทียบกับคะแนน Pass@8 บนแบบทดสอบมาตรฐานด้านคณิตศาสตร์

ในกรณีที่ตัวเลขทั้งสองไม่สามารถเปรียบเทียบกันได้เลย

MathForm-8B ที่ 88.06% และ AlphaProof Code ที่ 6.5 ล้านบรรทัดวัดคนละสิ่งและไม่ควรนำมาใส่ในคอลัมน์เดียวกันเด็ดขาด ตัวหนึ่งคืออัตราการตอบถูกบนชุดแบบทดสอบที่ผู้เขียนสร้างขึ้น ส่วนอีกตัวคือปริมาณการพิสูจน์ที่ผลิตขึ้นสำหรับเป้าหมายเดียว ผู้ขายยอมรับตรงๆ ว่า 88.06% ใช้การตรวจสอบไวยากรณ์ ซึ่งเป็นเกณฑ์ที่อ่อน — ข้อความหนึ่งสามารถคอมไพล์ผ่านได้แต่ยังจัดรูปนัยข้อกล่าวอ้างที่ผิด ซึ่งเป็นเหตุให้ตัวเลขความสอดคล้องต่ำกว่า 16 จุด

ตัวอย่าง AlphaProof Code ที่มีลักษณะเทียบเคียงได้คืองานตรวจสอบความถูกต้อง: บั๊ก Signal สองรายการที่เคยได้รับการแก้ไขแล้ว ซึ่งได้แก่บั๊กสถานะอ่อน (weak-state bug) และบั๊กกลุ่มย่อยเล็ก (small-subgroup bug) ถูกนำกลับเข้าสู่สำเนาที่แยกออกมา และในทั้งสองกรณี ระบบได้สร้างข้อพิสูจน์ที่ตรวจสอบด้วยเครื่องได้ว่าเวอร์ชันที่มีบั๊กล้มเหลวต่อทฤษฎีบทความปลอดภัย นั่นคือการทดสอบเชิงลบ และการทดสอบเชิงลบคือสิ่งที่เกณฑ์มาตรฐานสำหรับ autoformalizer ขาดไปโดยสิ้นเชิง MathForm-8B ไม่ได้รายงานผลลัพธ์ในรูปแบบที่ว่า “เมื่อกำหนดข้อความที่ผิดโดยเจตนา โมเดลกลับบอกว่าเป็นเช่นนั้น”

คุณจะนำพวกมันไปใช้ร่วมกันจริง ๆ ได้อย่างไร

ในทางปฏิบัติ และนี่เป็นส่วนเดียวของการเปรียบเทียบที่มีเส้นทางระยะใกล้: ใช้ autoformalizer เพื่อร่าง ใช้โมเดลทั่วไปที่แข็งแกร่งเพื่อวิจารณ์ร่าง และใช้เอเจนต์พิสูจน์เพื่อพยายามพิสูจน์ แต่ละขั้นตอนมีโหมดความล้มเหลวที่แตกต่างกัน และการกำหนดเส้นทางทั้งสามผ่านคีย์เดียวคือความสะดวกเชิงปฏิบัติ บน OrcaRouter, โมเดลมากกว่า 200 โมเดลอยู่เบื้องหลัง API เดียวในราคาตามรายการของผู้ให้บริการโดยบวกเพิ่ม 0% ดังนั้นลูปการร่างสเปกที่ส่งข้อความเดียวกันไปยังสองโมเดลและหาความแตกต่างระหว่าง Lean ของทั้งสองจึงเป็นการเรียก routing-DSL มากกว่าจะเป็นสัญญาสามฉบับและ SDK สามตัว การ failover อัตโนมัติครอบคลุมกรณีที่โมเดลที่คุณเลือกกำลังเจอช่วงบ่ายที่แย่.

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

เหตุผลที่ต้องอ่านทั้งสองบทความแทนที่จะเลือกว่าฝ่ายไหนชนะ

MathForm-8B เป็นอาร์ติแฟกต์ที่มีประโยชน์ ทำงานเฉพาะทางแคบ ๆ และมีเพดานความแม่นยำจริงที่วัดได้ AlphaProof Code คือการสาธิตเวิร์กโฟลว์ ซึ่งข้อค้นพบที่ถ่ายทอดไปใช้ได้มากที่สุดไม่ใช่ปริมาณการพิสูจน์ แต่คือการแบ่งแยก: งานด้านข้อกำหนดต้องการมนุษย์และโมเดลทั่วไปที่แข็งแกร่ง งานพิสูจน์ต้องการทีมเอเจนต์และเคอร์เนล และเส้นแบ่งระหว่างสองสิ่งนี้คือที่ที่ความยากทั้งหมดอยู่ ใครก็ตามที่สร้างไปป์ไลน์การตรวจสอบยืนยันควรให้ความสำคัญกับการแบ่งแยกนี้อย่างจริงจัง และมองว่าการทำให้เป็นทางการอัตโนมัติเป็นส่วนที่ลดต้นทุนของระยะแรก — ไม่ใช่ส่วนที่เข้ามาแทนที่มัน

สรุปตรงไปตรงมาสำหรับทีมที่กำลังตัดสินใจว่าจะดาวน์โหลดอะไรในเดือนนี้: MathForm-8B ใช่ ถ้าคุณทำงานกับ Lean และต้องการเครื่องมือช่วยร่าง สำหรับ AlphaProof Code ให้อ่านที่เก็บอาร์ติแฟกต์และแค็ตตาล็อกความเบี่ยงเบนจากข้อกำหนด เพราะแค็ตตาล็อกให้ข้อมูลเกี่ยวกับสิ่งที่การทวนสอบเชิงรูปนัยของโค้ดที่ใช้งานจริงยังไม่สามารถเข้าถึงได้ มากกว่าที่ประกาศใด ๆ จะบอกได้