ConcoLLMic: एजेंटिक कंकोलिक निष्पादन

पेपर: IEEE S&P 2026

ConcoLLMic पहला भाषा- और सिद्धांत-अज्ञेय कंकोलिक निष्पादक है जो LLM एजेंटों द्वारा संचालित है। पारंपरिक प्रतीकात्मक निष्पादन उपकरणों के विपरीत जिन्हें भाषा-विशिष्ट कार्यान्वयन की आवश्यकता होती है और बाधा समाधान में संघर्ष करते हैं, ConcoLLMic:

किसी भी प्रोग्रामिंग भाषा और पर्यावरण अंतःक्रियाओं के साथ काम करता है — C, C++, Python, Java, ..., और बहु-भाषा प्रणालियों का भी समर्थन करता है; किसी अतिरिक्त पर्यावरण मॉडलिंग की आवश्यकता नहीं है और उन्हें कुशलतापूर्वक संभालता है।
विविध बाधा सिद्धांतों को संभालता है — जिसमें फ्लोटिंग-पॉइंट अंकगणित, स्ट्रिंग्स, संरचित डेटा और बिट-स्तरीय संचालन शामिल हैं।
बेहतर कवरेज प्राप्त करता है — लगभग 4 घंटों में, ConcoLLMic अत्याधुनिक उपकरणों KLEE की तुलना में 115%-233% अधिक शाखाओं को कवर करता है और 48 घंटों तक चलने वाले AFL++ से 81% अधिक।
वास्तविक बग ढूंढता है — वास्तविक दुनिया के सॉफ़्टवेयर में 10+ पहले से अज्ञात कमजोरियाँ पहले ही खोज चुका है।

यह कैसे काम करता है: ConcoLLMic LLM एजेंटों का उपयोग करके

स्रोत स्तर पर कोड में fprintf(stderr, ...) जैसे लॉगिंग कथनों के साथ इंस्ट्रूमेंटेशन करता है;
पथ बाधाओं को प्राकृतिक भाषा, कोड या SMT सूत्रों में लचीले ढंग से संक्षेपित करता है;
बाधाओं को बुद्धिमानी से हल करता है — बाधाओं को शब्दार्थ पर सीधे तर्क करके और आवश्यकता पड़ने पर ग्राउंडेड सॉल्वरों को सौंपता है।

इससे हाथ से बनाए गए भाषा-विशिष्ट प्रतीकात्मक इंटरप्रेटर और पर्यावरण मॉडलिंग के साथ-साथ महँगे बाधा समाधान की आवश्यकता समाप्त हो जाती है।

कार्यप्रवाह उदाहरण

चरण 1: इंस्ट्रूमेंटेशन

ConcoLLMic का इंस्ट्रूमेंटेशन

FP-Bench से src/count.c का उदाहरण इंस्ट्रूमेंटेशन, निष्पादन में प्रमुख बिंदुओं पर fprintf डालकर। stderr में आउटपुट हमें गतिशील निष्पादन पथ का पुनर्निर्माण करने की अनुमति देता है।

चरण 2: कंकोलिक परीक्षण

ConcoLLMic का परीक्षण चरण

यह ConcoLLMic के साथ कंकोलिक निष्पादन का एक दौर दिखाता है। विस्तृत, कार्यान्वयन-स्तरीय सूत्रों वाले पारंपरिक उपकरणों की तुलना में:

start = atof(I[0]) ∧ end = atof(I[1]) ∧ start < end ∧ cur[0] = start ∧ 
(∀ 0 ≤ i < cnt, cur[i] ≠ end) ∧ cur[cnt] = end ∧ cnt ≤ 20

ConcoLLMic पथ बाधाओं को उच्च-स्तरीय प्राकृतिक भाषा का उपयोग करके संक्षेप में प्रस्तुत करता है:

सीमा में प्रतिनिधित्व योग्य FP मानों की संख्या ≤ 20 होनी चाहिए।

शुरुआत करना

आवश्यक शर्तें

Python 3.10 या उच्चतर
Claude Sonnet के लिए API कुंजी (Anthropic से)

स्थापना

रिपॉजिटरी क्लोन करें

git clone https://github.com/ConcoLLMic/ConcoLLMic.git
cd ConcoLLMic

Python निर्भरताएँ स्थापित करें

pip install -r requirements.txt
pip install -r requirements-dev.txt # वैकल्पिक

अपनी API कुंजी सेट करें

export ANTHROPIC_API_KEY="your_api_key_here"

डिफ़ॉल्ट रूप से, ConcoLLMic Claude 4.5 Sonnet का उपयोग करता है। आप ACE.py में अन्य मॉडल कॉन्फ़िगर कर सकते हैं (setup_model() देखें)।

अपना पहला उदाहरण चलाना

ConcoLLMic के कार्यप्रवाह में दो मुख्य चरण होते हैं: इंस्ट्रूमेंटेशन और संकलन तथा कंकोलिक निष्पादन। नीचे आरंभ करने के लिए दो उदाहरण दिए गए हैं:

उदाहरण 1: ब्रैकेट मिलान सत्यापन

एक सरल ब्रैकेट मिलान सत्यापन प्रोग्राम जो जाँचता है कि ब्रैकेट संतुलित हैं या नहीं।

चरण 1: इंस्ट्रूमेंटेशन और संकलन

इंस्ट्रूमेंटेड कोड पहले से ही code_example/instr/validate_brackets.cpp में उपलब्ध है।

शुरुआत से इंस्ट्रूमेंट करने के लिए:

rm ./code_example/instr/validate_brackets.cpp

python3 ACE.py instrument \
    --src_dir ./code_example/src/ \
    --out_dir ./code_example/instr/ \
    --instr_languages c,cpp,python,java

नोट: --instr_languages फ़्लैग केवल फ़ाइलों को एक्सटेंशन द्वारा फ़िल्टर करने के लिए उपयोग किया जाता है। किसी अतिरिक्त भाषा-विशिष्ट समर्थन की आवश्यकता नहीं है।

इंस्ट्रूमेंटेड कोड को सामान्य रूप से संकलित करें:

g++ -o ./code_example/instr/validate_brackets ./code_example/instr/validate_brackets.cpp

चरण 2: कंकोलिक निष्पादन

प्रदान किए गए टेस्ट हार्नेस code_example/harness/validate_brackets.py के साथ कंकोलिक निष्पादन एजेंट चलाएँ, जो एक Python फ़ंक्शन है जो प्रोग्राम इनपुट तैयार करता है और प्रोग्राम निष्पादित करता है:

python3 ACE.py run \
    --project_dir ./code_example/instr/ \
    --execution ./code_example/harness/validate_brackets.py \
    --out ./out/ \
    --rounds 2 \
    --parallel_num 3

कमांड पैरामीटर समझाया गया:

--project_dir: इंस्ट्रूमेंटेड कोड और संकलित प्रोग्राम वाली निर्देशिका
--execution: टेस्ट हार्नेस (एक Python स्क्रिप्ट जो लक्ष्य प्रोग्राम को निष्पादित करती है और stderr + एग्ज़िट कोड लौटाती है)
--out: जनरेट किए गए परीक्षण मामलों और लॉग के लिए आउटपुट निर्देशिका
--rounds: कंकोलिक निष्पादन दौरों की संख्या (डिफ़ॉल्ट: कवरेज पठार तक असीमित)
--parallel_num: प्रति दौर अधिकतम समवर्ती परीक्षण मामला निर्माण

सुझाव: एजेंट के चरण-दर-चरण कार्यप्रवाह को अधिक स्पष्ट रूप से देखने के लिए (जैसे, डेमो या डिबगिंग के लिए), --parallel_num 1 सेट करें ताकि प्रत्येक चरण क्रमिक रूप से चले।

आउटपुट:

./out/ConcoLLMic_*.log — विस्तृत निष्पादन लॉग
./out/queue/id:*.yaml — मेटाडेटा के साथ जनरेट किए गए परीक्षण मामले

चरण 3: आँकड़े देखें (वैकल्पिक)

परीक्षण आँकड़ों का विश्लेषण करें (टोकन उपयोग, लागत):

python3 ACE.py run_data --out_dir ./out/

चरण 4: पुनः चलाएँ और कवरेज मापें (वैकल्पिक)

# कवरेज के साथ संकलन
cd ./code_example/src/
g++ --coverage -o validate_brackets validate_brackets.cpp
lcov -z -d .
cd ../../

# परीक्षण मामलों को पुनः चलाएँ
python3 ACE.py replay \
    ./out/ \
    ./code_example/src/ \
    ./coverage.csv \
    --cov_script ./code_example/src/coverage.sh

आउटपुट:

./coverage.csv — प्रत्येक परीक्षण मामले के लिए समय-श्रृंखला कवरेज डेटा
./code_example/src/validate_brackets.cpp.gcov — पंक्ति-दर-पंक्ति कवरेज रिपोर्ट

उदाहरण 2: फ्लोटिंग-पॉइंट गणना

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