2025-11-13T01:07:10.778375

MASA: LLM-Driven Multi-Agent Systems for Autoformalization

Zhang, Valentino, Freitas

Autoformalization serves a crucial role in connecting natural language and formal reasoning. This paper presents MASA, a novel framework for building multi-agent systems for autoformalization driven by Large Language Models (LLMs). MASA leverages collaborative agents to convert natural language statements into their formal representations. The architecture of MASA is designed with a strong emphasis on modularity, flexibility, and extensibility, allowing seamless integration of new agents and tools to adapt to a fast-evolving field. We showcase the effectiveness of MASA through use cases on real-world mathematical definitions and experiments on formal mathematics datasets. This work highlights the potential of multi-agent systems powered by the interaction of LLMs and theorem provers in enhancing the efficiency and reliability of autoformalization, providing valuable insights and support for researchers and practitioners in the field.

academic

MASA: स्वचालित औपचारिकीकरण के लिए LLM-संचालित बहु-एजेंट प्रणालियाँ

मूल जानकारी

पेपर ID: 2510.08988
शीर्षक: MASA: LLM-Driven Multi-Agent Systems for Autoformalization
लेखक: Lan Zhang (मैनचेस्टर विश्वविद्यालय), Marco Valentino (शेफील्ड विश्वविद्यालय), André Freitas (मैनचेस्टर विश्वविद्यालय, Idiap अनुसंधान संस्थान, राष्ट्रीय बायोमार्कर केंद्र)
वर्गीकरण: cs.CL (कम्प्यूटेशनल भाषाविज्ञान), cs.FL (औपचारिक भाषाएँ)
प्रकाशन समय: 10 अक्टूबर 2025 (arXiv प्रीप्रिंट)
पेपर लिंक: https://arxiv.org/abs/2510.08988

सारांश

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

अनुसंधान पृष्ठभूमि और प्रेरणा

समस्या परिभाषा

स्वचालित औपचारिकीकरण (Autoformalization) प्राकृतिक भाषा गणितीय कथनों को मशीन-सत्यापन योग्य औपचारिक तर्क सूत्रों में स्वचालित रूप से परिवर्तित करने का कार्य है। इस समस्या की मूल चुनौतियाँ हैं:

अर्थ संबंधी अंतराल: प्राकृतिक भाषा की अस्पष्टता और औपचारिक भाषा की कठोरता के बीच विशाल अंतर
जटिलता: वास्तविक दुनिया के गणितीय कथन अक्सर जटिल अवधारणाओं और तर्क श्रृंखलाओं को शामिल करते हैं
सटीकता की आवश्यकता: औपचारिकीकरण परिणाम वाक्य रचना और अर्थ दोनों में सही होने चाहिए

समस्या की महत्ता

स्वचालित औपचारिकीकरण महत्वपूर्ण है:

गणितीय सत्यापन: प्रमेय प्रमाण और गणितीय सत्यापन के लिए आधार प्रदान करना
तर्क पारदर्शिता: प्राकृतिक भाषा तर्क की तुलना में औपचारिक तर्क अधिक व्यवस्थित, पारदर्शी और कठोर है
स्वचालन की आवश्यकता: मैनुअल औपचारिकीकरण को बड़े विशेषज्ञ ज्ञान और समय की आवश्यकता होती है

मौजूदा विधियों की सीमाएँ

LLM-आधारित मौजूदा स्वचालित औपचारिकीकरण प्रणालियों में निम्नलिखित समस्याएँ हैं:

एकल-इकाई वास्तुकला सीमाएँ: एकल LLM जटिल वास्तविक दुनिया की स्वचालित औपचारिकीकरण समस्याओं को संभालने में कठिनाई करता है
मॉड्यूलरिटी की कमी: मौजूदा कार्यान्वयन में मॉड्यूलरिटी, लचीलापन और स्केलेबिलिटी की कमी है
घटक इंटरैक्शन अपर्याप्त: कई इंटरैक्टिव घटकों को प्रभावी ढंग से एकीकृत नहीं कर सकते

अनुसंधान प्रेरणा

लेखकों ने MASA ढांचा प्रस्तावित करने की प्रेरणा है:

स्वचालित औपचारिकीकरण की जटिलता को हल करने के लिए मॉड्यूलर बहु-एजेंट प्रणाली बनाना
शोधकर्ताओं को सिस्टम को तेजी से विकसित और विस्तारित करने के लिए लचीला और स्केलेबल ढांचा प्रदान करना
एजेंट सहयोग के माध्यम से स्वचालित औपचारिकीकरण की दक्षता और विश्वसनीयता में सुधार करना

मुख्य योगदान

मॉड्यूलर बहु-एजेंट ढांचा प्रस्तावित किया: MASA स्वचालित औपचारिकीकरण बहु-एजेंट प्रणालियों के निर्माण के लिए एक मॉड्यूलर ढांचा प्रदान करता है, जिसमें अच्छी लचीलापन और स्केलेबिलिटी है
वास्तविक दुनिया के अनुप्रयोग प्रदर्शित किए: एजेंटों के माध्यम से वास्तविक दुनिया की गणितीय परिभाषाओं को औपचारिक बनाकर, ढांचे की व्यावहारिक क्षमता को उजागर किया
व्यवस्थित मूल्यांकन: तीन बहु-एजेंट सेटिंग्स के तहत ढांचे का मूल्यांकन किया, इसकी प्रभावशीलता साबित की और मूल्यवान अंतर्दृष्टि प्रदान की। अंतिम पुनरावृत्तिमूलक स्व-सुधार प्रणाली Qwen2.5-7B और GPT-4.1-mini पर क्रमशः 35.25% और 61.89% वाक्य रचना सही और अर्थ संरेखित औपचारिकीकरण दर प्राप्त करती है
ओपन-सोर्स कार्यान्वयन: पूर्ण कोड और डेटा प्रदान करके, अनुसंधान की बाधा को कम किया

विधि विवरण

कार्य परिभाषा

स्वचालित औपचारिकीकरण को एक रूपांतरण फ़ंक्शन A के रूप में परिभाषित किया जा सकता है, जो प्राकृतिक भाषा कथन s को इसके औपचारिक प्रतिनिधित्व φ = A(s) में मैप करता है। पारंपरिक विधियाँ LLM प्रॉम्प्टिंग के माध्यम से कार्यान्वित होती हैं: A = LLM(prompt)। MASA इस परिभाषा को विस्तारित करता है, बहु-एजेंट प्रणाली के माध्यम से अधिक जटिल रूपांतरण प्रक्रिया को लागू करता है।

मॉडल आर्किटेक्चर

MASA ढांचे में पाँच मुख्य घटक हैं:

1. एजेंट (Agent)

एजेंट विशिष्ट कार्यों को निष्पादित करने वाले मूल तत्व हैं, जिनमें शामिल हैं:

AutoformalizationAgent: कम-नमूना स्वचालित औपचारिकीकरण निष्पादित करता है
HardCritiqueAgent: प्रमेय प्रोवर के आधार पर वाक्य रचना स्तर की आलोचना प्रदान करता है
SoftCritiqueAgent: LLM के आधार पर अर्थ स्तर की आलोचना प्रदान करता है
FormalRefinementAgent: कठोर आलोचना के आधार पर औपचारिक कोड में सुधार करता है
InformalRefinementAgent: नरम आलोचना के आधार पर औपचारिक कोड में सुधार करता है
DenoisingAgent: शोर हटाने वाला उपकरण एजेंट
ImportRetrievalAgent: आयात पुनर्प्राप्ति उपकरण एजेंट

2. बड़ा भाषा मॉडल (Large Language Model)

LLM एजेंटों को तर्क और भाषा क्षमता प्रदान करता है, समर्थन करता है:

OpenAI मॉडल (जैसे GPT-4.1-mini)
HuggingFace स्थानीय मॉडल (जैसे Qwen2.5-7B, DeepSeek-Math)

3. ज्ञान आधार (Knowledge Base)

औपचारिक भाषा पुस्तकालय की जानकारी संग्रहीत करता है, संबंधित ज्ञान पुनर्प्राप्ति का समर्थन करता है। वर्तमान कार्यान्वयन Isabelle/HOL औपचारिक कथन और प्रमाणों के ज्ञान आधार को शामिल करता है।

4. पुनर्प्राप्तिकर्ता (Retriever)

गणितीय पुस्तकालय में डेटा बिंदुओं की प्रासंगिकता को रैंक करता है, वर्तमान कार्यान्वयन BM25 विधि पर आधारित है।

5. प्रमेय प्रोवर (Theorem Prover)

औपचारिक कोड की वाक्य रचना सही और तार्किक सही होने को सत्यापित करता है, त्रुटि संदेश प्रदान करता है। समर्थन करता है:

Isabelle (समर्पित सर्वर के माध्यम से)
Lean4 (REPL के माध्यम से)

तकनीकी नवाचार बिंदु

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

प्रयोग सेटअप

डेटासेट

miniF2F: Isabelle/HOL और Lean4 के वास्तविक औपचारिकीकरण प्रदान करता है, बेंचमार्किंग के लिए
ProofNet: Lean4 कोड के वास्तविक औपचारिकीकरण प्रदान करता है

मूल्यांकन मेट्रिक्स

वाक्य रचना सही होना

Pass Rate: वाक्य रचना सही औपचारिकीकरण का प्रतिशत

अर्थ मूल्यांकन

BLEU-4: वास्तविक औपचारिकीकरण के साथ n-gram ओवरलैप
ChrF: वर्ण-स्तरीय F-score
RUBY: कोड माइग्रेशन मूल्यांकन मेट्रिक

एजेंट मूल्यांकन

Alignment Faithfulness (AF): क्या औपचारिक कोड प्राकृतिक भाषा अर्थ को सटीक रूप से संरेखित करता है
Formalization Correctness (FC): क्या औपचारिक कोड स्वयं वैध, प्राकृतिक और अच्छी तरह से स्वरूपित है

तुलनात्मक विधियाँ

शून्य-नमूना प्रॉम्प्टिंग (ZS): LLM का सीधे औपचारिकीकरण के लिए उपयोग
कम-नमूना प्रॉम्प्टिंग (FS): 3 उदाहरणों का उपयोग करके औपचारिकीकरण
विभिन्न LLM संयोजन: GPT-4.1-mini, DeepSeek-Math-7B, Qwen2.5-7B

कार्यान्वयन विवरण

नरम आलोचना एजेंट के बैकएंड LLM के रूप में GPT-4.1-mini का उपयोग
Isabelle/HOL और Lean4 दोनों औपचारिक भाषाओं का समर्थन
पूर्ण Python कार्यान्वयन और Jupyter Notebook उदाहरण प्रदान करता है

प्रयोग परिणाम

मुख्य परिणाम

कठोर आलोचना औपचारिक सुधार प्रणाली (तालिका 1)

miniF2F-Test (Isabelle/HOL):

GPT-4.1-mini शून्य-नमूना: Pass Rate 65.57% → 77.05% (+11.48%)
GPT-4.1-mini कम-नमूना: Pass Rate 76.23% → 86.48% (+10.25%)
DeepSeek-Math कम-नमूना: Pass Rate 29.10% → 36.48% (+7.38%)

ProofNet-Test (Lean4):

GPT-4.1-mini शून्य-नमूना: Pass Rate 3.30% → 3.85% (+0.55%)
GPT-4.1-mini कम-नमूना: Pass Rate 12.09% → 14.84% (+2.75%)

नरम आलोचना अनौपचारिक सुधार प्रणाली (तालिका 2)

miniF2F (Lean4):

DeepSeek-Math + GPT-4.1-mini सुधार: AF 38.52% → 90.57%, FC 47.54% → 79.92%
Qwen2.5-7B + GPT-4.1-mini सुधार: AF 54.51% → 93.44%, FC 62.70% → 85.25%

पुनरावृत्तिमूलक स्व-सुधार प्रयोग

चित्र 2 परिणाम दिखाते हैं:

Qwen2.5-7B: 4 दौरों के बाद, वाक्य रचना सही और अर्थ संरेखित का अनुपात 35.25% तक पहुँचता है
GPT-4.1-mini: 4 दौरों के बाद, वाक्य रचना सही और अर्थ संरेखित का अनुपात 61.89% तक पहुँचता है

प्रयोग निष्कर्ष

कम-नमूना शून्य-नमूना से बेहतर है: सभी सेटिंग्स में, कम-नमूना सीखना प्रदर्शन में महत्वपूर्ण सुधार करता है
मॉडल क्षमता प्रभाव: मजबूत मॉडल (GPT-4.1-mini) औपचारिक सुधार में बेहतर प्रदर्शन करते हैं
पुनरावृत्तिमूलक सुधार प्रभावी: बहु-दौर पुनरावृत्ति औपचारिकीकरण गुणवत्ता में निरंतर सुधार कर सकती है
क्रॉस-मॉडल सुधार: मजबूत मॉडल कमजोर मॉडल के आउटपुट में सुधार कर सकते हैं

निष्कर्ष और चर्चा

मुख्य निष्कर्ष

ढांचे की प्रभावशीलता: MASA ने सफलतापूर्वक एक मॉड्यूलर बहु-एजेंट स्वचालित औपचारिकीकरण प्रणाली का निर्माण किया
प्रदर्शन सुधार: बहु-एजेंट सहयोग स्वचालित औपचारिकीकरण की सटीकता में महत्वपूर्ण सुधार करता है
व्यावहारिक मूल्य: ढांचा शोधकर्ताओं को एक लचीला विकास मंच प्रदान करता है

सीमाएँ

केंद्रीय नियंत्रण की कमी: प्रणाली में विभिन्न एजेंटों को आवंटित और नियंत्रित करने के लिए केंद्रीय एजेंट नहीं है
अर्थ मूल्यांकन सीमाएँ: अर्थ मूल्यांकन केवल उच्च-स्तरीय निर्णय तक सीमित है, अधिक सूक्ष्म मूल्यांकन मानदंड की आवश्यकता है
मॉडल निर्भरता: प्रणाली का प्रदर्शन बहुत हद तक अंतर्निहित LLM की क्षमता पर निर्भर करता है

भविष्य की दिशाएँ

केंद्रीय नियंत्रण में सुधार: अधिक उन्नत बहु-एजेंट प्रणाली नियंत्रण तंत्र विकसित करना
मूल्यांकन को परिष्कृत करना: अधिक सूक्ष्म अर्थ मूल्यांकन मानदंड स्थापित करना
अनुप्रयोग विस्तार: ढांचे को अधिक व्यापक औपचारिकीकरण कार्यों में लागू करना

गहन मूल्यांकन

शक्तियाँ

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

कमियाँ

अपर्याप्त सैद्धांतिक विश्लेषण: बहु-एजेंट सहयोग तंत्र के सैद्धांतिक विश्लेषण की कमी
कम्प्यूटेशनल लागत: बहु-एजेंट प्रणाली की कम्प्यूटेशनल ओवरहेड विश्लेषण अपर्याप्त है
त्रुटि प्रसार: एजेंटों के बीच त्रुटि प्रसार समस्या का गहन विश्लेषण नहीं
मूल्यांकन सीमाएँ: अर्थ मूल्यांकन अभी भी LLM निर्णय पर निर्भर है, पूर्वाग्रह हो सकता है

प्रभाव

शैक्षणिक योगदान: स्वचालित औपचारिकीकरण अनुसंधान के लिए नया प्रतिमान प्रदान करता है
व्यावहारिक मूल्य: ढांचा सीधे व्यावहारिक अनुप्रयोग विकास में उपयोग किया जा सकता है
पुनरुत्पादनशीलता: पूर्ण ओपन-सोर्स कार्यान्वयन पुनरुत्पादनशीलता सुनिश्चित करता है
विकास को बढ़ावा देना: औपचारिकीकरण क्षेत्र में बहु-एजेंट के अनुप्रयोग को बढ़ावा देने की संभावना है

लागू परिदृश्य

गणितीय औपचारिकीकरण: जटिल गणितीय प्रमेय और परिभाषाओं के स्वचालित औपचारिकीकरण के लिए उपयुक्त
शैक्षणिक अनुप्रयोग: गणित शिक्षण में औपचारिकीकरण प्रशिक्षण के लिए उपयोग किया जा सकता है
अनुसंधान उपकरण: स्वचालित औपचारिकीकरण अनुसंधान के लिए आधार मंच प्रदान करता है
औद्योगिक अनुप्रयोग: औपचारिक सत्यापन की आवश्यकता वाली सॉफ्टवेयर प्रणालियों में एकीकृत किया जा सकता है

संदर्भ

मुख्य संदर्भ साहित्य में शामिल हैं:

Wu et al. (2022): Autoformalization with large language models
Zheng et al. (2022): miniF2F: a cross-system benchmark for formal olympiad-level mathematics
Azerbayev et al. (2023): ProofNet: Autoformalizing and formally proving undergraduate-level mathematics
Jiang et al. (2023): Draft, sketch, and prove: Guiding formal theorem provers with informal proofs

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