2025-11-22T16:49:15.454007

Towards Autoformalization of LLM-generated Outputs for Requirement Verification

Gupte, S
Autoformalization, the process of translating informal statements into formal logic, has gained renewed interest with the emergence of powerful Large Language Models (LLMs). While LLMs show promise in generating structured outputs from natural language (NL), such as Gherkin Scenarios from NL feature requirements, there's currently no formal method to verify if these outputs are accurate. This paper takes a preliminary step toward addressing this gap by exploring the use of a simple LLM-based autoformalizer to verify LLM-generated outputs against a small set of natural language requirements. We conducted two distinct experiments. In the first one, the autoformalizer successfully identified that two differently-worded NL requirements were logically equivalent, demonstrating the pipeline's potential for consistency checks. In the second, the autoformalizer was used to identify a logical inconsistency between a given NL requirement and an LLM-generated output, highlighting its utility as a formal verification tool. Our findings, while limited, suggest that autoformalization holds significant potential for ensuring the fidelity and logical consistency of LLM-generated outputs, laying a crucial foundation for future, more extensive studies into this novel application.
academic

LLM-जनित आउटपुट के आवश्यकता सत्यापन के लिए स्वचालित औपचारिकीकरण की ओर

मूल जानकारी

  • पेपर ID: 2511.11829
  • शीर्षक: LLM-जनित आउटपुट के आवश्यकता सत्यापन के लिए स्वचालित औपचारिकीकरण की ओर
  • लेखक: मिहिर गुप्ते, रमेश एस. (जनरल मोटर्स)
  • वर्गीकरण: cs.CL, cs.AI, cs.FL, cs.LO
  • प्रकाशन समय: 18 नवंबर, 2025 (arXiv प्रीप्रिंट)
  • पेपर लिंक: https://arxiv.org/abs/2511.11829

सारांश

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

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

1. मूल समस्या

LLM अनुप्रयोगों के प्रसार के साथ, विशेषकर परीक्षण परिदृश्य स्वचालित रूप से उत्पन्न करने जैसे इंजीनियरिंग कार्यों में, एक महत्वपूर्ण चुनौती मौजूद है: LLM द्वारा जनित आउटपुट मूल प्राकृतिक भाषा आवश्यकता को सटीक रूप से प्रतिबिंबित करता है या नहीं, इसे सत्यापित करने के लिए औपचारिक विधियों की कमी। उदाहरण के लिए, "जब वाहन की गति ≥10 और सीटबेल्ट अनबद्ध हो, तो सीटबेल्ट अलर्ट शुरू करें" जैसी आवश्यकता से Gherkin परिदृश्य उत्पन्न करने के बाद, जनित सामग्री की तार्किक सही होने की गारंटी नहीं दी जा सकती।

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

ऑटोमोटिव इंजीनियरिंग जैसे सुरक्षा-महत्वपूर्ण क्षेत्रों में, आवश्यकता सत्यापन अत्यंत महत्वपूर्ण है। गलत आवश्यकता रूपांतरण निम्नलिखित का कारण बन सकता है:

  • अधूरे या गलत परीक्षण मामले
  • प्रणाली व्यवहार अपेक्षित से भिन्न
  • संभावित सुरक्षा जोखिम

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

  • पारंपरिक औपचारिक विधियां: मुख्य रूप से गणितीय प्रमेय प्रमाण में लागू होती हैं, इंजीनियरिंग आवश्यकता सत्यापन के लिए अनुप्रयोग की कमी
  • LLM मूल्यांकन विधियां: मानव जांच या अनुमानी विधियों पर निर्भर, कठोर तार्किक सत्यापन की कमी
  • स्वचालित औपचारिकीकरण अनुसंधान: मुख्य रूप से डेटासेट निर्माण और मॉडल प्रशिक्षण पर केंद्रित, वास्तविक इंजीनियरिंग अनुप्रयोगों पर कम ध्यान

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

यह पेपर LLM आउटपुट सत्यापन के इस नए परिदृश्य में स्वचालित औपचारिकीकरण तकनीक लागू करने का प्रस्ताव देता है, प्राकृतिक भाषा आवश्यकताओं और LLM-जनित आउटपुट दोनों को औपचारिक तर्क प्रतिनिधित्व (Lean 4) में परिवर्तित करके, तार्किक समतुल्यता सत्यापित करने के लिए प्रमेय प्रमाणक का उपयोग करके।

मूल योगदान

  1. LLM-जनित आउटपुट सत्यापन के लिए पहली स्वचालित औपचारिकीकरण पाइपलाइन प्रस्तावित की: प्राकृतिक भाषा आवश्यकताओं और LLM आउटपुट को Lean 4 औपचारिक प्रतिनिधित्व में परिवर्तित किया, और द्विशर्त समतुल्यता प्रमाण के माध्यम से तार्किक संगति सत्यापित की
  2. दो विशिष्ट अनुप्रयोग परिदृश्यों को सत्यापित किया:
    • विभिन्न शब्दों वाली प्राकृतिक भाषा आवश्यकताओं की तार्किक समतुल्यता की पहचान
    • LLM-जनित आउटपुट और मूल आवश्यकता के बीच तार्किक असंगति का पता लगाना
  3. मुख्य तकनीकी चुनौतियों की पहचान की:
    • चर आधारभूतकरण (variable grounding) की आवश्यकता और स्वचालन कठिनाई
    • औपचारिकीकरण पर LLM अनिश्चितता का प्रभाव
    • प्राकृतिक भाषा अस्पष्टता का प्रबंधन
  4. भविष्य की अनुसंधान दिशाएं प्रस्तावित कीं: विश्वसनीय LLM आउटपुट सत्यापन ढांचे के निर्माण के लिए आधार स्थापित किया

विधि विवरण

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

इनपुट:

  • सत्यापन के लिए तार्किक संबंध की आवश्यकता वाले कथनों की एक जोड़ी (S₁, S₂), जो हो सकते हैं:
    • दो प्राकृतिक भाषा आवश्यकताएं
    • एक प्राकृतिक भाषा आवश्यकता और एक LLM-जनित Gherkin परिदृश्य

आउटपुट:

  • तार्किक समतुल्यता निर्णय: समतुल्य (S₁ ↔ S₂ सिद्ध किया जा सकता है) या असमतुल्य (प्रमाण विफल)

बाधा शर्तें:

  • कथन को प्रस्तावनात्मक तर्क में औपचारिक बनाया जा सकता है
  • चर आधारभूतकरण के लिए प्रणाली संदर्भ जानकारी की आवश्यकता

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

संपूर्ण पाइपलाइन में चार मुख्य चरण शामिल हैं (चित्र 9 देखें):

चरण 1: स्वचालित औपचारिकीकरण

DeepSeek-Prover-v2 (7B मॉडल) का उपयोग करके प्राकृतिक भाषा कथनों को Lean 4 प्रस्तावों में परिवर्तित करें:

-- उदाहरण: आवश्यकता R1 का औपचारिकीकरण
variable (vehicle_speed_avg : ℝ)
variable (calibratable_speed : ℝ)
variable (seatbelt_active : Bool)
variable (initiate_chime : Bool)

def seatbelt_chime_condition : Prop :=
  (vehicle_speed_avg ≥ calibratable_speed ∨ ¬seatbelt_active) → initiate_chime

संकेत टेम्पलेट (परिशिष्ट A.1 देखें):

  • Lean 4 के def कथन उत्पन्न करने की स्पष्ट आवश्यकता
  • प्रस्तावनात्मक तर्क (Prop प्रकार) का उपयोग करने के लिए निर्दिष्ट करें
  • शर्तों को निहितार्थ संबंध (A ∧ B → C) के रूप में प्रतिनिधित्व करने की आवश्यकता

चरण 2: चर आधारभूतकरण (Variable Grounding)

वर्तमान कार्यान्वयन: विभिन्न औपचारिकीकरणों में समान अवधारणा की ओर इशारा करने वाले चर को मैन्युअल रूप से पहचानें और एकीकृत करें

समस्या उदाहरण:

  • R1 में vehicle_speed_avg और R2 में mean_vehicle_speed एक ही भौतिक मात्रा की ओर इशारा करते हैं
  • Lean संकलक को इस समतुल्यता संबंध को स्पष्ट रूप से बताने की आवश्यकता है
-- मैन्युअल आधारभूतकरण उदाहरण
(h_speed : vehicle_speed_avg = mean_vehicle_speed)
(h_belt : seatbelt_active = seatbelt_plugged_in)

चरण 3: द्विशर्त समतुल्यता प्रमेय निर्माण

तार्किक समतुल्यता सत्यापित करने के लिए औपचारिक प्रमेय का निर्माण करें:

theorem req1_eq_req2 
  (h_grounding : <चर आधारभूतकरण धारणाएं>) :
  (Proposition_A) ↔ (Proposition_B) := by
  <प्रमाण प्रक्रिया>

चरण 4: स्वचालित प्रमेय प्रमाण

Lean प्रमाण कोड उत्पन्न करने के लिए DeepSeek-Prover-v2 का फिर से उपयोग करें:

  • सफल प्रमाण → दोनों कथन तार्किक रूप से समतुल्य हैं
  • प्रमाण विफल → तार्किक असंगति मौजूद है

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

  1. अंतर-क्षेत्र अनुप्रयोग नवाचार: पहली बार गणितीय प्रमेय प्रमाण क्षेत्र की स्वचालित औपचारिकीकरण तकनीक को सॉफ्टवेयर इंजीनियरिंग आवश्यकता सत्यापन में लागू किया
  2. दोहरी-स्तरीय LLM उपयोग:
    • पहला स्तर: औपचारिकीकरण अनुवाद (NL → Lean)
    • दूसरा स्तर: प्रमेय प्रमाण (समतुल्यता सत्यापन)
  3. विफलता-आधारित सत्यापन तंत्र: प्रमेय प्रमाणक की विफलता को तार्किक असंगति के संकेतक के रूप में उपयोग करें, यह एक नवीन नकारात्मक सत्यापन विधि है
  4. चर आधारभूतकरण पहचान: स्पष्ट रूप से प्रस्तावित करें कि चर आधारभूतकरण स्वचालित औपचारिकीकरण पाइपलाइन में अपरिहार्य चरण है, जो पूर्व अनुसंधान में पर्याप्त रूप से जोर नहीं दिया गया था

प्रयोग सेटअप

डेटासेट

प्रयोग 1: आवश्यकता समतुल्यता सत्यापन

  • R1: "यदि वाहन की औसत गति ≥ अंशांकन योग्य सीटबेल्ट अनुस्मारक गति या सीटबेल्ट निष्क्रिय है तो सीटबेल्ट चाइम शुरू करें"
  • R2: "यदि औसत वाहन गति अंशांकन योग्य सीटबेल्ट अनुस्मारक गति से अधिक है या सीटबेल्ट प्लग नहीं है तो सीटबेल्ट के लिए चाइम शुरू करें"

प्रयोग 2: LLM आउटपुट सत्यापन

  • R3: "जब सामने यात्री सीटबेल्ट स्थिति 'बंधी हुई' में बदल जाती है तो सामने यात्री सीटबेल्ट अनुस्मारक संकेत चालू FALSE पर सेट किया जाएगा।"
  • G3: LLM द्वारा जनित Gherkin परिदृश्य (4 उदाहरण पंक्तियां शामिल हैं, seat_occupancy जैसे अतिरिक्त चर परिचय देते हैं)

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

गुणात्मक मेट्रिक्स:

  • Lean 4 संकलन सफलता/विफलता
  • प्रमेय प्रमाण सफलता/विफलता

सत्यापन मानदंड:

  • तार्किक समतुल्यता: प्रमेय PA ↔ PB सिद्ध किया जा सकता है
  • तार्किक असंगति: प्रमेय प्रमाण विफल या Lean कोड संकलित नहीं हो सकता

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

मॉडल चयन:

  • DeepSeek-Prover-v2 (7B)
  • चयन कारण:
    1. Lean 4 पर प्रशिक्षित
    2. प्राकृतिक भाषा समझ क्षमता रखता है
    3. उप-लक्ष्य अपघटन रणनीति अपनाता है

औपचारिकीकरण भाषा: Lean 4

  • शक्तिशाली प्रमेय प्रमाण क्षमता
  • सटीक तार्किक अभिव्यक्ति
  • DeepSeek-Prover-v2 के साथ संगत

मैन्युअल हस्तक्षेप:

  • चर आधारभूतकरण चरण पूरी तरह मैन्युअल
  • औपचारिकीकरण आउटपुट सत्यापन Lean संकलक पर निर्भर

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

मुख्य परिणाम

प्रयोग 1: आवश्यकता समतुल्यता सत्यापन (सफल मामला)

औपचारिकीकरण आउटपुट:

  • R1 और R2 को सफलतापूर्वक Lean प्रस्तावों में परिवर्तित किया गया (चित्र 3, चित्र 4)
  • चर मैपिंग मैन्युअल रूप से स्थापित की गई:
    • vehicle_speed_avg ≡ mean_vehicle_speed
    • seatbelt_active ≡ seatbelt_plugged_in

सत्यापन परिणाम (चित्र 5):

  • ✅ Lean संकलन सफल
  • ✅ प्रमेय req1_eq_req2 प्रमाण सफल
  • निष्कर्ष: R1 और R2 तार्किक रूप से समतुल्य हैं

महत्व: प्रमाणित करता है कि पाइपलाइन शब्दों में समान लेकिन अलग-अलग आवश्यकताओं को पहचान सकता है, आवश्यकता संगति जांच में सहायक है।

प्रयोग 2: LLM आउटपुट सत्यापन (विफल मामला)

औपचारिकीकरण आउटपुट:

  • R3: सरल प्रस्ताव, केवल सीटबेल्ट स्थिति परिवर्तन शर्त शामिल (चित्र 6)
  • G3: जटिल प्रस्ताव, अतिरिक्त चर शामिल (seat_occupancy, initial_seatbelt_status) (चित्र 7)

मुख्य खोज:

  • G3 ने R3 में अनुल्लिखित चर पेश किए
  • तार्किक संरचना अधिक जटिल है (4 परिदृश्य उदाहरण शामिल)

सत्यापन परिणाम (चित्र 8):

  • ❌ Lean कोड संकलन विफल या प्रमाण विफल
  • निष्कर्ष: G3 और R3 तार्किक रूप से असंगत हैं

महत्व: LLM-जनित आउटपुट की "अत्यधिक पीढ़ी" समस्या का सफलतापूर्वक पता लगाया - मूल आवश्यकता में अनुपस्थित शर्तें जोड़ी गई हैं।

केस विश्लेषण

केस: अस्पष्टता समस्या (R4)

आवश्यकता:

"जब सीटबेल्ट अनबद्ध हो और वाहन गति में हो तो सामने यात्री सीटबेल्ट अनुस्मारक संकेत चालू TRUE पर सेट किया जाएगा।"

समस्या: "वाहन गति में" का औपचारिकीकरण अस्पष्ट है

दो संभावित औपचारिकीकरण (चित्र 10):

  1. pass@1: बूलियन चर vehicle_in_motion : Bool
  2. pass@2: संख्यात्मक चर vehicle_speed > 0

विश्लेषण:

  • दोनों औपचारिकीकरण प्रणाली शब्दार्थ में संभवतः सही हैं
  • लेकिन वे औपचारिक तर्क में असमतुल्य हैं (विभिन्न प्रकार)
  • औपचारिकीकरण के लिए प्राकृतिक भाषा अस्पष्टता के प्रभाव को उजागर करता है

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

  1. औपचारिकीकरण व्याख्यात्मकता पर निर्भर है: LLM की अनिश्चितता के कारण एक ही आवश्यकता विभिन्न लेकिन दोनों "उचित" औपचारिकीकरण उत्पन्न कर सकती है
  2. चर आधारभूतकरण बाधा है:
    • सबसे समय लेने वाला चरण
    • प्रणाली डोमेन ज्ञान की आवश्यकता
    • वर्तमान में केवल मैन्युअल रूप से संभव
  3. प्रणाली संदर्भ अत्यंत महत्वपूर्ण है: स्पष्ट प्रणाली परिभाषा की कमी (जैसे डेटा शब्दकोश) औपचारिकीकरण असंगति का कारण बनती है
  4. नकारात्मक सत्यापन प्रभावी है: प्रमाण विफलता तार्किक असंगति को प्रभावी ढंग से संकेत कर सकती है

संबंधित कार्य

स्वचालित औपचारिकीकरण डेटासेट निर्माण

  • ProofNet: स्नातक स्तर की गणित स्वचालित औपचारिकीकरण
  • MiniF2F: ओलंपिक स्तर की गणित बेंचमार्क
  • बहुभाषी डेटासेट: Lean, Isabelle, Coq का संयुक्त प्रशिक्षण प्रदर्शन में सुधार

LLM प्रशिक्षण रणनीतियां

  • "ड्राफ्ट-स्केच-प्रमाण" विधि (Jiang et al.): प्रमाण रूपरेखा उत्पन्न करना औपचारिकीकरण को निर्देशित करता है
  • उप-लक्ष्य अपघटन: DeepSeek-Prover द्वारा अपनाई गई पुनरावर्ती खोज रणनीति
  • सुदृढ़ीकरण सीखना: प्रमेय प्रमाण सफलता दर में सुधार

अनिश्चितता का सामना करना

  • प्रतीकात्मक समतुल्यता ढांचा: pass@1 और pass@k के अंतर को संभालना
  • RAG विधि: सटीक औपचारिक परिभाषा पुनः प्राप्त करना संदर्भ प्रदान करता है

अनुप्रयोग क्षेत्र विस्तार

  • गणितीय समस्या समाधान: उच्च विद्यालय से विश्वविद्यालय गणित
  • कोड सत्यापन: प्रोग्राम सही होने का सत्यापन
  • जैव चिकित्सा: तथ्य सत्यापन

इस पेपर का योगदान: पहली बार स्वचालित औपचारिकीकरण को इंजीनियरिंग आवश्यकता सत्यापन और LLM आउटपुट सत्यापन में लागू किया, एक नई अनुप्रयोग दिशा खोली।

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

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

  1. व्यवहार्यता सत्यापन: स्वचालित औपचारिकीकरण पाइपलाइन LLM-जनित आउटपुट और मूल आवश्यकता के बीच तार्किक संगति को प्रभावी ढंग से सत्यापित कर सकता है
  2. दोहरा अनुप्रयोग मूल्य:
    • आवश्यकता संगति जांच (समतुल्य आवश्यकताओं की पहचान)
    • LLM आउटपुट गुणवत्ता नियंत्रण (तार्किक त्रुटियों का पता लगाना)
  3. अवधारणा प्रमाण: हालांकि नमूना सीमित है, लेकिन सॉफ्टवेयर इंजीनियरिंग में प्रमेय प्रमाण तकनीक लागू करने की संभावना को सफलतापूर्वक प्रदर्शित किया

सीमाएं

  1. पैमाने की सीमा:
    • केवल 3 आवश्यकता जोड़ी परीक्षण की गई
    • बड़े पैमाने पर मूल्यांकन की कमी
    • कोई सांख्यिकीय महत्व विश्लेषण नहीं
  2. मैन्युअल निर्भरता:
    • चर आधारभूतकरण पूरी तरह मैन्युअल
    • समय लेने वाला और त्रुटि-प्रवण
    • स्केलेबिलिटी को सीमित करता है
  3. मॉडल सीमाएं:
    • 7B मॉडल का उपयोग (संसाधन सीमित)
    • बड़े मॉडल (671B) बेहतर प्रदर्शन कर सकते हैं
    • औपचारिकीकरण गुणवत्ता मॉडल क्षमता पर निर्भर
  4. अस्पष्टता अनसुलझी:
    • प्राकृतिक भाषा की अंतर्निहित अस्पष्टता
    • प्रणाली ऑन्टोलॉजी समर्थन की कमी
    • कई "सही" लेकिन असमतुल्य औपचारिकीकरण उत्पन्न कर सकते हैं
  5. डोमेन विशिष्टता:
    • प्रयोग केवल ऑटोमोटिव सुरक्षा आवश्यकताओं तक सीमित
    • सामान्यीकरण क्षमता अज्ञात

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

पेपर तीन मुख्य अनुसंधान प्रश्न (RQ) प्रस्तावित करता है:

RQ1: सर्वोत्तम औपचारिकीकरण विधि

  • k-pass रणनीति की खोज (कई औपचारिकीकरण उत्पन्न करें, सबसे संभावित चुनें)
  • एकल रूपांतरण बनाम बहु-नमूना सटीकता की तुलना

RQ2: चर आधारभूतकरण स्वचालन

  • विधि 1: संदर्भ एकल औपचारिकीकरण (एकल कॉल में सभी कथनों को संभालें)
  • विधि 2: समानता-आधारित आधारभूतकरण (प्रणाली ऑन्टोलॉजी से मेल खाने के लिए एम्बेडिंग का उपयोग करें)
  • चुनौती: LLM के आधारभूतकरण धारणा की सही होने को कैसे सत्यापित करें

RQ3: सीमित प्रणाली में LLM सत्यापन

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

अन्य दिशाएं:

  • स्वचालित चर सामान्यीकरण तकनीक विकास
  • डोमेन-विशिष्ट ऑन्टोलॉजी एकीकरण (जैसे ऑटोमोटिव सिस्टम डेटा शब्दकोश)
  • अधिक जटिल तार्किक प्रतिनिधित्व समर्थन (जैसे समय तर्क)

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

शक्तियां

  1. समस्या परिभाषा नवीन:
    • पहली बार LLM आउटपुट सत्यापन में स्वचालित औपचारिकीकरण को व्यवस्थित रूप से लागू किया
    • इंजीनियरिंग अभ्यास में वास्तविक दर्द बिंदु का समाधान
    • एक नई अनुसंधान दिशा खोली
  2. पद्धति स्पष्ट:
    • पाइपलाइन डिजाइन सरल और स्पष्ट
    • परिपक्व उपकरण का उपयोग (Lean 4, DeepSeek-Prover)
    • पुनरुत्पादन क्षमता मजबूत
  3. समस्या पहचान गहन:
    • चर आधारभूतकरण की महत्ता स्पष्ट करता है
    • अस्पष्टता समस्या का गहन विश्लेषण
    • LLM अनिश्चितता के प्रभाव की ईमानदारी से चर्चा
  4. व्यावहारिक मूल्य उच्च:
    • सुरक्षा-महत्वपूर्ण क्षेत्र (ऑटोमोटिव इंजीनियरिंग) को लक्षित
    • आवश्यकता इंजीनियरिंग प्रवाह में सीधे अनुप्रयोग
    • LLM अनुप्रयोग विश्वसनीयता में सुधार में सहायता
  5. लेखन गुणवत्ता उत्कृष्ट:
    • संरचना स्पष्ट, तर्क कठोर
    • विस्तृत संकेत टेम्पलेट प्रदान (परिशिष्ट)
    • समृद्ध चित्र, समझने में आसान

कमियां

  1. प्रयोग पैमाना गंभीर रूप से अपर्याप्त:
    • केवल 3 नमूने: सांख्यिकीय निष्कर्ष निकालना असंभव
    • विभिन्न क्षेत्रों, विभिन्न जटिलता की आवश्यकताओं की परीक्षा की कमी
    • बड़े डेटासेट पर प्रदर्शन मूल्यांकन नहीं
    • सुझाव: पर्याप्त मूल्यांकन के लिए कम से कम 50-100 आवश्यकता जोड़ी की आवश्यकता
  2. मात्रात्मक मूल्यांकन की कमी:
    • सटीकता, पुनः प्राप्ति दर आदि मेट्रिक्स नहीं
    • औपचारिकीकरण सफलता दर की रिपोर्ट नहीं
    • मानव सत्यापन के साथ तुलना की कमी
    • सुझाव: मानक डेटासेट स्थापित करें, सटीकता मेट्रिक्स की गणना करें
  3. मैन्युअल हस्तक्षेप अत्यधिक:
    • चर आधारभूतकरण पूरी तरह मैन्युअल, स्वचालन दावे को कमजोर करता है
    • स्वचालन समाधान का विशिष्ट कार्यान्वयन नहीं
    • स्केलेबिलिटी संदिग्ध
    • सुझाव: कम से कम एक प्रोटोटाइप स्वचालित आधारभूतकरण प्रणाली लागू करें
  4. मॉडल चयन सीमित:
    • संसाधन सीमा के कारण केवल 7B मॉडल का उपयोग
    • 671B मॉडल या अन्य विकल्पों की खोज नहीं
    • परिणामों पर मॉडल आकार के प्रभाव का विश्लेषण नहीं
    • सुझाव: कम से कम कुछ नमूनों पर विभिन्न मॉडलों की तुलना करें
  5. विफलता केस विश्लेषण की कमी:
    • प्रमेय प्रमाण विफलता के कारणों का विस्तृत विश्लेषण नहीं
    • औपचारिकीकरण त्रुटि बनाम वास्तविक तार्किक असंगति के बीच अंतर नहीं
    • झूठी सकारात्मक/झूठी नकारात्मक विश्लेषण की कमी
    • सुझाव: त्रुटि वर्गीकरण प्रणाली स्थापित करें
  6. मूल्यांकन मानदंड एकल:
    • केवल Lean संकलन सफलता/विफलता पर निर्भर
    • आंशिक सही मामलों पर विचार नहीं
    • सूक्ष्म त्रुटि प्रकार विश्लेषण की कमी
  7. सामान्यीकरण क्षमता अज्ञात:
    • केवल ऑटोमोटिव सुरक्षा आवश्यकताओं परीक्षण
    • अन्य क्षेत्रों (चिकित्सा, वित्त आदि) में प्रयोज्यता सत्यापित नहीं
    • Gherkin परिदृश्य की विशिष्टता विधि की सामान्यता को सीमित कर सकती है

प्रभाव

क्षेत्र पर योगदान:

  • ⭐⭐⭐⭐ अवधारणा योगदान उच्च: नई अनुसंधान दिशा और अनुप्रयोग परिदृश्य प्रस्तावित
  • ⭐⭐ तकनीकी योगदान मध्यम: मुख्य रूप से मौजूदा तकनीकों का संयोजन अनुप्रयोग
  • ⭐⭐⭐ व्यावहारिक मूल्य अधिक: इंजीनियरिंग अभ्यास में वास्तविक समस्या का समाधान

व्यावहारिक मूल्य:

  • अल्पकालीन: आवश्यकता इंजीनियरों को सत्यापन विचार प्रदान
  • मध्यकालीन: विशेष आवश्यकता सत्यापन उपकरण का जन्म हो सकता है
  • दीर्घकालीन: LLM अनुप्रयोग गुणवत्ता आश्वासन की मानक प्रक्रिया बन सकता है

पुनरुत्पादन क्षमता:

  • ✅ खुले स्रोत उपकरण का उपयोग (Lean 4, DeepSeek-Prover)
  • ✅ विस्तृत संकेत टेम्पलेट प्रदान
  • ❌ कोड या डेटा प्रकाशित नहीं
  • ❌ मैन्युअल चरण पुनरुत्पादन में कठिन
  • मूल्यांकन: ⭐⭐⭐ (मध्यम)

अपेक्षित प्रभाव:

  • LLM आउटपुट औपचारिक सत्यापन पर अधिक अनुसंधान को प्रेरित कर सकता है
  • आवश्यकता इंजीनियरिंग और औपचारिक विधियों के संयोजन को बढ़ावा दे सकता है
  • चर आधारभूतकरण समस्या नया अनुसंधान केंद्र बन सकता है

प्रयोज्य परिदृश्य

उच्च प्रयोज्यता:

  • ✅ सुरक्षा-महत्वपूर्ण प्रणाली आवश्यकता सत्यापन (ऑटोमोटिव, विमान, चिकित्सा)
  • ✅ आवश्यकता संगति जांच और डुप्लिकेट हटाना
  • ✅ LLM-जनित परीक्षण मामलों की गुणवत्ता नियंत्रण

मध्यम प्रयोज्यता:

  • ⚠️ जटिल व्यावसायिक तर्क सत्यापन (औपचारिकीकरण क्षमता विस्तार की आवश्यकता)
  • ⚠️ बहु-मोडल आवश्यकताएं (जैसे चित्र युक्त आवश्यकताएं)
  • ⚠️ वास्तविक समय प्रणाली (समय तर्क विस्तार की आवश्यकता)

अप्रयोज्य:

  • ❌ अत्यधिक अस्पष्ट प्राकृतिक भाषा पाठ
  • ❌ स्पष्ट प्रणाली परिभाषा की कमी वाले परिदृश्य
  • ❌ वास्तविक समय प्रतिक्रिया की आवश्यकता वाले परिदृश्य (वर्तमान मैन्युअल चरण बहुत धीमे)

सुधार सुझाव

  1. तुरंत संभव:
    • कम से कम 50 आवश्यकता जोड़ी तक विस्तार
    • मूल स्वचालित चर आधारभूतकरण प्रोटोटाइप कार्यान्वयन
    • त्रुटि वर्गीकरण प्रणाली स्थापना
  2. अल्पकालीन सुधार:
    • विभिन्न आकार के मॉडलों की तुलना
    • मात्रात्मक मूल्यांकन मेट्रिक्स परिचय
    • बहु-क्षेत्र परीक्षण
  3. दीर्घकालीन लक्ष्य:
    • पूर्ण स्वचालन पाइपलाइन
    • डोमेन ज्ञान ग्राफ एकीकरण
    • समय तर्क और जटिल बाधा समर्थन

संदर्भ साहित्य (मुख्य संदर्भ)

  1. Weng et al. (2025): बड़े भाषा मॉडलों के युग में स्वचालित औपचारिकीकरण: एक सर्वेक्षण - सर्वेक्षण साहित्य
  2. Wu et al. (2022): बड़े भाषा मॉडलों के साथ स्वचालित औपचारिकीकरण - स्वचालित औपचारिकीकरण मूल कार्य
  3. Ren et al. (2025): DeepSeek-Prover-v2 - इस पेपर द्वारा उपयोग किया गया मूल मॉडल
  4. Jiang et al. (2022): ड्राफ्ट, स्केच, और प्रमाण - उप-लक्ष्य अपघटन विधि
  5. de Moura & Ullrich (2021): Lean 4 प्रमेय प्रमाणक - औपचारिकीकरण भाषा

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