DafnyBench

Dafnebench: معيار للتحقق من البرامج الرسمية

مجموعة البيانات والرمز لورقة Dafnebench: معيار للتحقق من البرامج الرسمية

مجموعة البيانات متاحة أيضا للتنزيل على؟ الوجه المعانقة.

ملخص

تعد Dafnebench أكبر معيار من نوعها لتدريب وتقييم أنظمة التعلم الآلي للتحقق الرسمي من البرامج ، مع أكثر من 750 برنامج DAFNY.

الاستخدام

• مجموعة البيانات : يمكن العثور على مجموعة البيانات الخاصة بـ Dafnebench (مع 782 برنامجًا) في دليل DafnyBench ، والذي يحتوي على مجموعة ground_truth ومجموعة hints_removed (مع تلميحات البرمجيات ، أي innoataions ، تمت إزالتها).
• التقييم : قم بتقييم LLMS على Dafnebench من خلال مطالبة النماذج بملء تلميحات مفقودة في ملف اختبار من مجموعة hints_removed والتحقق مما إذا كان يمكن التحقق من البرنامج المعاد بناؤه بواسطة DAFNY. يرجى الرجوع إلى دليل eval .

إعداد للتقييم؟

1. قم بتثبيت dafny على جهازك باتباع هذا البرنامج التعليمي
2. استنساخ cd في هذا المستودع
3. إعداد البيئة عن طريق تشغيل الأسطر التالية:

 python -m venv stats
source stats/bin/activate
pip install -r requirements.txt
cd eval

4. إنشاء متغير البيئة لدليل الجذر:

 export DAFNYBENCH_ROOT=

5. إعداد البيئة المتغير للمسار إلى dafny قابلة للتنفيذ على جهازك (على سبيل المثال ، /opt/homebrew/bin/Dafny ):

 export DAFNY_PATH=

6. إذا كنت تقوم بتقييم LLM من خلال وصول API ، قم بإعداد مفتاح API. على سبيل المثال:

 export OPENAI_API_KEY=

7. يمكنك اختيار تقييم LLM على برنامج اختبار واحد ، مثل:

 python fill_hints.py --model "gpt-4o" --test_file "Clover_abs_no_hints.dfy" --feedback_turn 3 --dafny_path "$DAFNY_PATH"

أو تقييم على مجموعة البيانات بأكملها:

 export model_to_eval='gpt-4o'
./run_eval.sh

محتويات ؟

• DafnyBench
  • مجموعة من 782 برنامج دافني. يحتوي كل برنامج على إصدار ground_truth يتم التحقق منه بالكامل مع إصدار Dafny & A hints_removed الذي يحتوي على تلميحات (IE) التي تمت إزالتها
• eval
  • يحتوي على البرامج النصية لتقييم LLMs على Dafnebench
• results
  • results_summary - إطارات البيانات التي تلخص نجاح LLMS في كل برنامج اختبار
  • reconstructed_files - مخرجات LLM مع تلميحات مملوءة مرة أخرى
  • analysis - يحتوي على دفتر ملاحظات لتحليل النتائج

الاقتباس؟

 @article { loughridge2024dafnybench ,
         title = { DafnyBench: A Benchmark for Formal Software Verification } , 
         author = { Chloe Loughridge and Qinyi Sun and Seth Ahrenbach and Federico Cassano and Chuyue Sun and Ying Sheng and Anish Mudide and Md Rakib Hossain Misu and Nada Amin and Max Tegmark } ,
         year = { 2024 } ,
         journal = { arXiv preprint arXiv:2406.08467 }
}