DafnyBench

Dafnybench: Benchmark untuk verifikasi perangkat lunak formal

Dataset & Kode untuk makalah kami Dafnybench: Benchmark untuk Verifikasi Perangkat Lunak Formal

Dataset juga tersedia untuk diunduh? Wajah memeluk.

Ringkasan

Dafnybench adalah tolok ukur terbesar dari jenisnya untuk pelatihan dan mengevaluasi sistem pembelajaran mesin untuk verifikasi perangkat lunak formal, dengan lebih dari 750 program DAFNY.

Penggunaan

• Dataset : Dataset untuk DafnyBench (dengan 782 program) dapat ditemukan di direktori DafnyBench , yang berisi set ground_truth & set hints_removed (dengan petunjuk kompiler, yaitu annoataions, dihapus).
• Evaluasi : Mengevaluasi LLMS di Dafnybench dengan meminta model untuk mengisi petunjuk yang hilang dalam file uji dari set hints_removed dan memeriksa apakah program yang direkonstruksi dapat diverifikasi oleh DAFNY. Silakan merujuk ke Direktori eval .

Didirikan untuk evaluasi?

1. Instal Dafny di mesin Anda dengan mengikuti tutorial ini
2. Klon & cd ke dalam repositori ini
3. Mengatur lingkungan dengan menjalankan baris berikut:

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

4. Mengatur variabel lingkungan untuk direktori root:

 export DAFNYBENCH_ROOT=

5. Mengatur Variabel Lingkungan untuk Path to Dafny dapat dieksekusi di mesin Anda (misalnya, /opt/homebrew/bin/Dafny ):

 export DAFNY_PATH=

6. Jika Anda mengevaluasi LLM melalui akses API, atur kunci API. Misalnya:

 export OPENAI_API_KEY=

7. Anda dapat memilih untuk mengevaluasi LLM pada program pengujian tunggal, seperti:

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

atau evaluasi di seluruh dataset:

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

Isi?

• DafnyBench
  • Koleksi 782 program DAFNY. Setiap program memiliki versi ground_truth yang sepenuhnya diverifikasi dengan versi Dafny & a hints_removed yang memiliki petunjuk (yaitu anotasi) dihapus
• eval
  • Berisi skrip untuk mengevaluasi LLM di Dafnybench
• results
  • results_summary - DataFrames yang merangkum keberhasilan LLMS di setiap program pengujian
  • reconstructed_files - output llm dengan petunjuk diisi kembali
  • analysis - berisi buku catatan untuk menganalisis hasilnya

Kutipan?

 @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 }
}