💬 NLP

APE-Bench: Evaluating Automated Proof Engineering for Formal Math Libraries

यह शोध पत्र APE-Bench प्रस्तुत करता है, जो वास्तविक दुनिया के रिपॉजिटरी-स्केल कार्यों को निकालने और विविध एजेंट कार्यान्वयनों में सिंटैक्टिक संकलन (syntactic compilation) और सिमेंटिक शुद्धता (semantic correctness) दोनों को मान्य करने के लिए एक एकीकृत हार्नेस प्रदान करके औपचारिक गणित पुस्तकालयों में स्वचालित प्रमाण इंजीनियरिंग (automated proof engineering) के मूल्यांकन के लिए पहला व्यवस्थित ढांचा और बेंचमार्क है।

मूल लेखक: Huajian Xin, Luming Li, Xiaoran Jin, Jacques Fleuriot, Wenda Li

प्रकाशित 2026-02-03

📖 6 मिनट में पढ़ें🧠 गहराई से पढ़ें

CC BY 4.0

मूल लेखक: Huajian Xin, Luming Li, Xiaoran Jin, Jacques Fleuriot, Wenda Li

मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। ✨ नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें

कल्पना कीजिए कि आप एक रोबोट को गणितीय प्रमाणों (mathematical proofs) के एक विशाल, जीवित पुस्तकालय, जिसे Mathlib कहा जाता है, का मास्टर लाइब्रेरियन बनने के लिए सिखाने की कोशिश कर रहे हैं। यह पुस्तकालय लाखों पृष्ठों का है। यह केवल एक स्थिर पुस्तक नहीं है; इसे मानव विशेषज्ञों द्वारा लगातार फिर से लिखा, विस्तारित और सुधारा जा रहा है।

लंबे समय तक, शोधकर्ताओं ने रोबोटों का परीक्षण एकल, अलग-थलग गणितीय पहेलियों (जैसे "सिद्ध करें कि 2+2=4") को हल करने की उनकी क्षमता पर किया। लेकिन वास्तविक दुनिया में, गणितज्ञ होना केवल एक पहेली को हल करने के बारे में नहीं है; यह प्रूफ इंजीनियरिंग (proof engineering) के बारे में है। इसका अर्थ है पूरे पुस्तकालय में नेविगेट करना, सही उपकरणों को खोजना, टूटे हुए पृष्ठों को ठीक करना, और यह सुनिश्चित करना कि आपके नए जुड़ाव पहले से मौजूद लाखों पृष्ठों के साथ पूरी तरह फिट बैठें और किसी भी चीज़ को खराब न करें।

यह पेपर इन वास्तविक दुनिया के कौशल पर रोबोटों का परीक्षण करने का एक नया तरीका पेश करता है। यहाँ सरल उपमाओं (analogies) का उपयोग करके इसका विवरण दिया गया है:

1. समस्या: "अलग-थलग पहेली" बनाम "जीवित पुस्तकालय"

पुराना तरीका (miniF2F): कल्पना कीजिए कि एक शेफ का परीक्षण करने के लिए उन्हें एक एकल रेसिपी कार्ड दिया जाता है और उनसे एक व्यंजन बनाने के लिए कहा जाता है। यदि व्यंजन स्वादिष्ट है, तो वे पास हो जाते हैं। यह आपको यह नहीं बताता कि क्या वे एक पूरे रेस्टोरेंट किचन को संभाल सकते हैं, सामग्री मंगवा सकते हैं, या खराब ओवन को ठीक कर सकते हैं।
वास्तविकता: वास्तविक गणित का काम उस रेस्टोरेंट को चलाने जैसा है। आपको अन्य शेफ के साथ समन्वय करना होता है, विशिष्ट उपकरणों का उपयोग करना होता है, और यह सुनिश्चित करना होता है कि आपका नया व्यंजन मेनू को खराब न कर दे।
अंतराल (Gap): मौजूदा परीक्षण केवल यह जाँचते थे कि क्या रोबोट उस एकल व्यंजन को बना सकता है। उन्होंने यह नहीं जाँचा कि क्या रोबोट वास्तविक रसोई के शोर-शराबे और अराजकता को संभाल सकता है।

2. समाधान: APE-Bench ("जीवित पुस्तकालय" परीक्षण)

लेखकों ने APE-Bench बनाया, जो वास्तविक जीवन के पुस्तकालय रखरखाव की नकल करता है।

यह कैसे काम करता है: रोबोट को एक नकली पहेली देने के बजाय, सिस्टम Mathlib लाइब्रेरी के वास्तविक इतिहास को देखता है। यह एक ऐसा क्षण ढूँढता है जहाँ एक मानव विशेषज्ञ ने एक बदलाव (एक "commit") किया था, उस बदलाव को छिपा देता है, और रोबोट से पूछता है: "बदलाव से पहले का पुस्तकालय यहाँ है। यहाँ एक नोट है कि मानव क्या करना चाहता था। क्या आप वह बदलाव कर सकते हैं?"
ट्विस्ट: रोबोट को केवल इस आधार पर ग्रेड नहीं दिया जाता कि कोड "रन" (syntax) होता है या नहीं। इसे दो चीजों पर ग्रेड दिया जाता है:
1. कंपाइलेशन (Compilation): क्या कोड बिना किसी त्रुटि के कंपाइल हुआ? (क्या व्यंजन जल गया?)
2. सिमेंटिक चेक (Semantic Check): क्या रोबोट ने वास्तव में वही किया जो पूछा गया था? (क्या उन्होंने सही समस्या को ठीक किया, या उन्होंने बस यादृच्छिक रूप से लाइनें बदल दीं?)

3. इंफ्रास्ट्रक्चर: APE-Harness ("यूनिवर्सल किचन")

इन परीक्षणों को निष्पक्ष रूप से चलाने के लिए, उन्होंने APE-Harness नामक एक प्रणाली बनाई है। इसे एक यूनिवर्सल किचन सिम्युलेटर समझें।

"अनुबंध" (The Contract): प्रत्येक परीक्षण के साथ एक सख्त अनुबंध आता है। यह कहता है: "आप लाइब्रेरी के इस विशिष्ट संस्करण में हैं। आप केवल इन फाइलों को छू सकते हैं। आपको सिद्ध करना होगा कि आपने काम किया है।"
"स्कैफोल्ड्स" (The Scaffolds): सिस्टम को इस तरह डिज़ाइन किया गया है कि आप अलग-अलग रोबोटों (जैसे Claude Code, Codex, या अपना स्वयं का APE-Agent) को एक ही किचन में प्लग कर सकें। क्योंकि किचन के नियम (अनुबंध) सभी के लिए समान हैं, इसलिए आप निष्पक्ष रूप से तुलना कर सकते हैं कि कौन वास्तव में बेहतर शेफ है, बजाय इसके कि केवल यह देखें कि किसे निर्देशों में भाग्य मिला।
"टाइम ट्रैवल" ट्रिक: लाइब्रेरी के 67 विभिन्न संस्करण हैं (जैसे एक पुस्तक के 67 विभिन्न संस्करण)। उन सभी को स्टोर करने के लिए बहुत अधिक स्थान की आवश्यकता होगी। लेखकों ने एक चतुर "डुप्लीकेशन हटाने" (deduplication) प्रणाली बनाई है। यदि संस्करण 1 और संस्करण 67 में एक पेज समान है, तो सिस्टम उसे केवल एक बार स्टोर करता है और बस उसकी ओर संकेत करता है। इसने डेटा को प्रोसेस करने के लिए आवश्यक स्टोरेज स्पेस को 85% और पैसे को 98% बचा लिया।

4. परिणाम: परीक्षण में कौन पास हुआ?

उन्होंने तीन शीर्ष-स्तरीय AI मॉडल (GPT-5.2, Gemini 3 Pro, और Gemini 3 Flash) का इस नए, कठिन परीक्षण पर परीक्षण किया।

कठिनाई: नया परीक्षण पुराने "एकल पहेली" परीक्षणों की तुलना में बहुत कठिन था।
- पुराने परीक्षणों पर, रोबोट 80-90% सही थे।
- नए "लाइब्रेरी मेंटेनेंस" परीक्षण पर, सर्वश्रेष्ठ रोबोट केवल 47% सही था।
विजेता: Gemini 3 Flash सबसे कुशल था। इसने सबसे कम लागत में सबसे अधिक समस्याओं को हल किया। अन्य मॉडलों ने अधिक प्रयास किए (अधिक कन्वर्सेशन टर्न) लेकिन काम पूरा करने से पहले ही अपना "बजट" समाप्त कर दिया।
सबक: रोबोट अलग-थलग गणितीय समस्याओं को हलने में माहिर हैं, लेकिन वे एक विशाल, विकसित होते कोडबेस को प्रबंधित करने के जटिल कार्य के साथ अभी भी संघर्ष कर रहे हैं।

5. यह क्यों महत्वपूर्ण है

पेपर का दावा है कि यह पहली बार है जब हमारे पास यह परीक्षण करने का एक व्यवस्थित, स्वचालित तरीका है कि क्या AI "प्रमाणों के लिए सॉफ्टवेयर इंजीनियरिंग" कर सकता है।

यह लक्ष्य को "क्या AI एक गणित की समस्या हल कर सकता है?" से बदलकर "क्या AI एक टीम वातावरण में एक पेशेवर गणितज्ञ के रूप में काम कर सकता है?" पर ले जाता है।
यह एक समान खेल का मैदान प्रदान करता है जहाँ विभिन्न AI सिस्टमों की तुलना बिल्कुल समान नियमों और उपकरणों का उपयोग करके की जा सकती है।

संक्षेप में: लेखकों ने एक विशाल, अव्यवस्थित गणित पुस्तकालय का एक यथार्थवादी सिमुलेशन और यह परीक्षण करने के लिए नियमों का एक सेट बनाया है कि क्या AI इसे ठीक कर सकता है। उन्होंने पाया कि जबकि AI बेहतर हो रहा है, लेकिन जटिल, वास्तविक दुनिया के गणितीय प्रोजेक्ट्स को स्वतंत्र रूप से प्रबंधित करने के लिए अभी भी उसे लंबा रास्ता तय करना है।

तकनीकी सारांश: APE-Bench: औपचारिक गणित पुस्तकालयों के लिए स्वचालित प्रमाण इंजीनियरिंग का मूल्यांकन

समस्या विवरण

Large Language Model (LLM) आधारित औपचारिक गणित के लिए वर्तमान मूल्यांकन बेंचमार्क, जैसे कि miniF2F और FATE, मुख्य रूप से पृथक प्रमेय सिद्ध करने (isolated theorem proving) पर ध्यान केंद्रित करते हैं। ये बेंचमार्क एजेंटों से एक दिए गए औपचारिक कथन के लिए एक प्रमाण पद (proof term) संश्लेषित करने की मांग करते हैं जो टाइप-चेक हो सके। हालांकि, उत्पादन वातावरण (जैसे, Mathlib) में वास्तविक औपचारिक गणित विकास का अभ्यास रिपॉजिटरी-स्केल प्रमाण इंजीनियरिंग (repository-scale proof engineering) में विकसित हो गया है। वास्तविक दुनिया का विकास मल्टी-फाइल समन्वय, लाइब्रेरी विकास, क्रॉस-फाइल निर्भरता प्रबंधन और परिवर्तन के तहत रखरखाव जैसी प्रक्रियाओं में शामिल है—ऐसे कार्य जिन्हें पृथक प्रमेय सिद्ध करने वाले बेंचमार्क पकड़ने में विफल रहते हैं। मौजूदा प्रमाण रखरखाव उपकरण (जैसे, iCoq, REPLICA) काफी हद तक ह्यूरिस्टिक (heuristic) बने हुए हैं और उनमें महत्वपूर्ण मैन्युअल प्रयास की आवश्यकता होती है। उन रिपॉजिटरी-स्केल इंजीनियरिंग गतिविधियों के मूल्यांकन के लिए एक व्यवस्थित ढांचे की कमी है जो वास्तविक औपचारिक गणित विकास को परिभाषित करती हैं।

कार्यप्रणाली

1. स्वचालित प्रमाण इंजीनियरिंग (APE) सूत्रीकरण

लेखक स्वचालित प्रमाण इंजीनियरिंग (Automated Proof Engineering - APE) को एक कार्य सूत्रीकरण के रूप में पेश करते हैं जो रिपॉजिटरी-स्केल प्रमाण इंजीनियरिंग को क्रियान्वित करता है। एक APE कार्य को तीन घटकों द्वारा परिभाषित किया जाता है:

पिन्ड एनवायरनमेंट (Pinned Environment): एक विशिष्ट रिपॉजिटरी कमिट और टूलचेन संस्करण।
प्राकृतिक भाषा निर्देश (Natural-Language Instruction): इंजीनियरिंग उद्देश्य का एक विवरण (जैसे, "रिफैक्टर करना," "स्वचालन जोड़ना")।
दोहरा सत्यापन (Dual Verification):
- सिंटैक्टिक शुद्धता (Syntactic Correctness): संशोधित कोड को पिन्ड एनवायरनमेंट के भीतर सफलतापूर्वक संकलित (compile) होना चाहिए।
- सिमेंटिक शुद्धता (Semantic Correctness): समाधान को प्राकृतिक भाषा की आवश्यकताओं को पूरा करना चाहिए और स्कोप नियंत्रण (अनावश्यक परिवर्तनों से बचना) बनाए रखना चाहिए, जिसे LLM-as-Judge के माध्यम से सत्यापित किया जाता है।

यह सूत्रीकरण SWE-bench के प्रतिमान को दर्शाता है लेकिन औपचारिक गणित के लिए इसे अनुकूलित करता है, जहाँ यूनिट टेस्ट के स्थान पर जजमेंट-आधारित सत्यापन का उपयोग किया जाता है, क्योंकि प्रमाण कार्यों में अक्सर पूर्व-मौजूद टेस्ट सुइट्स का अभाव होता है।

2. APE-Harness इंफ्रास्ट्रक्चर

व्यवस्थित मूल्यांकन के समर्थन के लिए, लेखकों ने Task Contract Abstraction पर आधारित एक निष्पादन इंफ्रास्ट्रक्चर, APE-Harness बनाया है।

टास्क कॉन्ट्रैक्ट्स (Task Contracts): घोषणात्मक विनिर्देश जो कार्य आवश्यकताओं (उद्देश्य, सीमाएं, एनवायरनमेंट बाइंडिंग, सत्यापन प्रोटोकॉल) को निष्पादन रणनीतियों से अलग करते हैं। यह विभिन्न एजेंट स्कैफोल्ड्स को समान बाधाओं के तहत एक ही कार्य निष्पादित करने की अनुमति देता है।
इंफ्रास्ट्रक्चर सेवाएं:
- एग्जीक्यूट सर्विसेज (Execute Services): एजेंट कोड को अपरिवर्तनीय लक्ष्य लाइब्रेरी इंस्टॉलेशन के विरुद्ध संकलित करना।
- रिट्रीव सर्विसेज (Retrieve Services): विशिष्ट लाइब्रेरी संस्करणों तक सीमित सिमेंटिक सर्च सक्षम करना।
- वर्कस्पेस आइसोलेशन (Workspace Isolation): लक्ष्य लाइब्रेरीओं के लिए केवल 'रीड-ओनली' एक्सेस और स्क्रैच वर्कस्पेस के लिए 'राइट' एक्सेस लागू करना।
मल्टी-वर्जन दक्षता: सिस्टम 67 विभिन्न लाइब्रेरी संस्करणों में समान फाइलों को डुप्लिकेट करने के लिए कंटेंट-एड्रेस करने योग्य स्टोरेज (क्रिप्टोग्राफिक हैशिंग) का उपयोग करता है, जिससे स्टोरेज और एम्बेडिंग लागतों में क्रम-दर-ऑर्डर बचत होती है।

3. APE-Bench निर्माण

APE-Bench एक स्वचालित पाइपलाइन है जो वास्तविक Mathlib कमिट इतिहास से प्रमाण इंजीनियरिंग कार्यों को निकालती है।

प्रक्रिया: यह महत्वपूर्ण फाइल-स्तरीय संशोधनों (5-100 लाइनें) के लिए कमिट्स को फ़िल्टर करता है, और फिर अंतर (diffs) से प्राकृतिक-भाषा निर्देशों को संश्लेषित करने के लिए एक एजेंट का उपयोग करता है।
सत्यापन: पाइपलाइन यह सुनिश्चित करती है कि कार्य हल करने योग्य हैं और मूल पैच उत्पन्न निर्देश को दोहरे सत्यापन के तहत संतुष्ट करता है।
डेटासेट: प्रारंभिक रिलीज़ में 67 कमिट्स (2026-01-01 के बाद के) से निकाले गए 100 कार्य शामिल हैं ताकि फ्रंटियर मॉडल्स के लिए जीरो ट्रेनिंग डेटा कंटैमिनेशन सुनिश्चित किया जा सके।

4. मूल्यांकन स्कैफोल्ड्स

यह ढांचा स्कैफोल्ड इंटरचेंजेबिलिटी (interchangeability) का समर्थन करता है। लेखक APE-Agent (एक एकीकृत सत्यापन के साथ ReAct-शैली का स्कैफोल्ड) प्रदान करते हैं और इसकी तुलना Claude Code और Codex CLI के साथ करते हैं ताकि यह प्रदर्शित किया जा सके कि इंफ्रास्ट्रक्चर विभिन्न एजेंट कार्यान्वयन की निष्पक्ष तुलना कर सकता है।

प्रमुख योगदान

APE सूत्रीकरण और बेंचमार्क: रिपॉजिटरी-स्केल प्रमाण इंजीनियरिंग मूल्यांकन के लिए पहला पूर्ण इंफ्रास्ट्रक्चर, जिसमें एक स्वचालित पाइपलाइन (APE-Bench) है जो वास्तविक लाइब्रेरी विकास से कार्यों को निकालता है।
LLM Judge वैलिडेशन बेंचमार्क: विशेषज्ञ-एनोटेटेड एजेंट समाधानों का एक डेटासेट, जिसमें तीन-आयामी गुणवत्ता रेटिंग (सिमेंटिक शुद्धता, आवश्यकता संरेखण, स्कोप नियंत्रण) है, जो LLM जजों की विश्वसनीयता को प्रमाणित करता है।
APE-Harness: एक टास्क-कॉन्ट्रैक्ट-आधारित निष्पादन इंफ्रास्ट्रक्चर जो विविध कार्यों के बीच एकीकृत मूल्यांकन को सक्षम बनाता है, कार्यात्मक वर्कफ़्लो (जैसे निर्देश संश्लेषण) का समर्थन करता है, और स्कैफोल्ड इंटरचेंजेबिलिटी की अनुमति देता है।
APE-Agent: एक व्हाइट-बॉक्स, ReAct-शैली का स्कैफोल्ड जिसमें फाइल सिस्टम और सत्यापन उपकरण एकीकृत हैं, ताकि अनुसंधान और तुलना को सुगम बनाया जा सके।
मल्टी-वर्जन निष्पादन सेवाएं: कंटेंट डीडुप्लिकेशन का उपयोग करके कई लाइब्रेरी संस्करणों में कुशल संकलन और रिट्रीवल सेवाओं का कार्यान्वयन।

परिणाम

मॉडल प्रदर्शन

लेखकों ने $3 प्रति कार्य के निश्चित बजट के साथ APE-Bench, miniF2F और miniCTX पर फ्रंटियर मॉडल्स (GPT-5.2, Gemini 3 Pro, Gemini 3 Flash) का मूल्यांकन किया।

APE-Bench की कठिनाई: रिपॉजिटरी-स्केल इंजीनियरिंग, पृथक प्रमाण सिद्ध करने की तुलना में काफी कठिन साबित हुई। APE-Bench पर, Gemini 3 Flash ने 47.0% पास रेट प्राप्त किया, जो GPT-5.2 (27.0%) और Gemini 3 Pro (24.0%) से बेहतर प्रदर्शन करता है।
पृथक प्रमाण बनाम तुलना: miniF2F और miniCTX पर, मॉडल्स ने बहुत अधिक पास रेट (73–94%) प्राप्त किया, जो यह दर्शाता है कि APE-Bench में कठिनाई शुद्ध प्रमेय सिद्ध करने की क्षमता के बजाय इंजीनियरिंग जटिलता (समन्वय, स्कोप नियंत्रण) से उपजी है।
दक्षता: प्रदर्शन अंतराल लागत-दक्षता द्वारा संचालित थे। Gemini 3 Flash ने बेहतर प्रदर्शन इसलिए नहीं किया क्योंकि उसका प्रति-टर्न तर्क श्रेष्ठ था, बल्कि इसलिए क्योंकि उसने महंगे टूल कॉल्स या विस्तृत प्रॉम्प्टिंग के कारण होने वाली समयपूर्व बजट समाप्ति से बचने में सफलता प्राप्त की।

स्कैफोल्ड और टूल विश्लेषण

स्कैफोल्ड इंटरचेंजेबिलिटी: समान कार्यों पर APE-Agent ने Claude Code और Codex CLI की तुलना में काफी बेहतर प्रदर्शन किया (15–23 प्रतिशत अंक)।
- कारण: APE-Agent के एकीकृत सत्यापन (एटॉमिक एडिट + कंपाइल) ने अनावश्यक कॉल्स को कम किया। इसके विपरीत, Claude Code और Codex ने विस्तृत प्रॉम्प्ट्स, अलग निष्पादन कॉल्स और रूढ़िवादी रिट्रीवल पैटर्न के कारण उच्च लागत उठाई।
टूल एब्लेशन (Tool Ablation): रिट्रीवल, शेल, या फाइल ऑपरेशन्स को हटाने से केवल मामूली गिरावट (44–47% रेंज) देखी गई। यह सुझाव देता है कि प्राथमिक बाधा विशिष्ट उपकरणों की उपलब्धता नहीं, बल्कि रिपॉजिटरी-स्केल कार्यों के लिए मॉडल्स की तर्क क्षमता है।

जज की विश्वसनीयता

LLM-as-Judge पाइपलाइन ने सिमेंटिक शुद्धता, आवश्यकता संरेखण और स्कोप नियंत्रण आयामों में मानव विशेषज्ञ एनोटेशन के विरुद्ध उच्च सटीकता (90.6% समग्र) प्रदर्शित की, जो स्वचालित मूल्यांकन के लिए इसके उपयोग को प्रमाणित करती है।

इंफ्रास्ट्रक्चर दक्षता

कंटेंट डीडुप्लिकेशन ने 67 लाइब्रेरी संस्करणों के लिए स्टोरेज आवश्यकताओं को 480GB से घटाकर 71GB (85% की कमी) कर दिया और रिट्रीवल सेवाओं के लिए एम्बेडिंग लागत को 98.5% ( $12.9K से$ 197) कम कर दिया।

महत्व

यह पेपर दावा करता है कि यह रिपॉजिटरी-स्केल औपचारिक गणित विकास पर AI एजेंटों के व्यवस्थित मूल्यांकन के लिए एक आधार स्थापित करता है। पृथक प्रमेय सिद्ध करने से प्रमाण इंजीनियरिंग की ओर मूल्यांकन प्रतिमान को बदलकर, APE-Bench वर्तमान AI क्षमताओं और वास्तविक उत्पादन-स्केल औपचारिक पुस्तकालयों के रखरखाव की मांगों के बीच के अंतर को संबोधित करता है। यह कार्य प्रदर्शित करता है कि:

रिपॉजिटरी-स्केल प्रमाण इंजीनियरिंग, पृथक प्रमेय सिद्ध करने की तुलना में एक अलग और काफी अधिक चुनौतीपूर्ण कार्य है।
टास्क कॉन्ट्रैक्ट एब्स्ट्रैक्शन विविध एजेंट आर्किटेक्चर की निष्पक्ष, मानकीकृत तुलना को सक्षम बनाता है।
वर्तमान फ्रंटियर मॉडल्स में संभावना तो है, लेकिन वास्तविक दुनिया के लाइब्रेरी रखरखाव में लागू होने पर उन्हें इंजीनियरिंग अनुशासन, स्कोप नियंत्रण और लागत-दक्षता के मामले में बड़ी बाधाओं का सामना करना पड़ता है।

लेखक इस क्षेत्र में आगे के अनुसंधान को सुगम बनाने के लिए सारा कोड और बेंचमार्क डेटासेट ओपन-सोर्स के रूप में जारी करते हैं।