DafnyBench

Dafnybench: มาตรฐานสำหรับการตรวจสอบซอฟต์แวร์อย่างเป็นทางการ

ชุดข้อมูลและรหัสสำหรับกระดาษ Dafnybench ของเรา: มาตรฐานสำหรับการตรวจสอบซอฟต์แวร์อย่างเป็นทางการ

ชุดข้อมูลยังมีให้ดาวน์โหลดหรือไม่? กอดใบหน้า

ภาพรวม

Dafnybench เป็นเกณฑ์มาตรฐานที่ใหญ่ที่สุดสำหรับการฝึกอบรมและประเมินระบบการเรียนรู้ของเครื่องสำหรับการตรวจสอบซอฟต์แวร์อย่างเป็นทางการโดยมีโปรแกรม DAFNY มากกว่า 750 โปรแกรม

การใช้งาน

• ชุดข้อมูล : ชุดข้อมูลสำหรับ DAFNYBENCH (พร้อมโปรแกรม 782) สามารถพบได้ในไดเรกทอรี DafnyBench ซึ่งมีชุด ground_truth & The hints_removed Set (พร้อมคำแนะนำคอมไพเลอร์เช่น Annoataions ลบออก)
• การประเมินผล : ประเมิน LLMs บน Dafnybench โดยขอให้โมเดลกรอกคำแนะนำที่ขาดหายไปในไฟล์ทดสอบจากชุด hints_removed และตรวจสอบว่าโปรแกรมที่สร้างขึ้นใหม่สามารถตรวจสอบได้โดย DAFNY โปรดดูไดเรกทอรี eval

ตั้งค่าสำหรับการประเมินผล?

1. ติดตั้ง dafny บนเครื่องของคุณโดยทำตามบทช่วยสอนนี้
2. Clone & 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
  • คอลเลกชันของโปรแกรม DAFNY 782 แต่ละโปรแกรมมีเวอร์ชัน ground_truth ที่ได้รับการตรวจสอบอย่างเต็มที่ด้วย Dafny & A hints_removed เวอร์ชันที่มีคำแนะนำ (เช่นคำอธิบายประกอบ) ลบ
• eval
  • มีสคริปต์เพื่อประเมิน LLMs บน dafnybench
• results
  • results_summary - DataFrames ที่สรุปความสำเร็จของ 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 }
}