DafnyBench

Dafnybench: Ein Benchmark für die formelle Softwareüberprüfung

Datensatz und Code für unser Papier Dafnybench: Ein Benchmark für die formelle Softwareverifizierung

Der Datensatz steht auch zum Download zur Verfügung? Umarmtes Gesicht.

Überblick

Dafnybench ist der größte Maß dieser Art für das Training und die Bewertung von maschinellen Lernsystemen für die formelle Softwareverifizierung mit über 750 DAFNY -Programmen.

Verwendung

• Datensatz : Der Datensatz für DafnyBench (mit 782 Programmen) ist im DafnyBench -Verzeichnis zu finden, das den Set ground_truth und das Set hints_removed enthält (mit Compiler -Hinweisen dh annoataions, entfernt).
• Bewertung : Bewerten Sie LLMs auf Dafnybench, indem Sie Modelle bitten, fehlende Hinweise in einer Testdatei aus dem Set hints_removed auszufüllen und zu überprüfen, ob das rekonstruierte Programm von DAFNY überprüft werden könnte. Bitte beachten Sie das eval -Verzeichnis.

Zur Bewertung einrichten?

1. Installieren Sie Dafny auf Ihrem Computer, indem Sie diesem Tutorial folgen
2. Klon & cd in dieses Repository
3. Richten Sie die Umgebung ein, indem Sie die folgenden Zeilen ausführen:

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

4. Richten Sie die Umgebungsvariable für das Stammverzeichnis ein:

 export DAFNYBENCH_ROOT=

5. Richten Sie die Umgebungsvariable für den Pfad zur ausführbaren Datei auf Ihrem Computer ein (z. /opt/homebrew/bin/Dafny ):

 export DAFNY_PATH=

6. Wenn Sie einen LLM über den API -Zugriff bewerten, richten Sie die API -Schlüssel ein. Zum Beispiel:

 export OPENAI_API_KEY=

7. Sie können eine LLM für ein einzelnes Testprogramm bewerten, z. B.:

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

oder im gesamten Datensatz bewerten:

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

Inhalt?

• DafnyBench
  • Eine Sammlung von 782 DAFNY -Programmen. ground_truth Programm hints_removed
• eval
  • Enthält Skripte zur Bewertung von LLMs auf Dafnybench
• results
  • results_summary - Datenrahmen, die den Erfolg von LLMS in jedem Testprogramm zusammenfassen
  • reconstructed_files - LLM Ausgänge mit Hinweisen, die wieder eingefüllt sind
  • analysis - enthält ein Notizbuch zur Analyse der Ergebnisse

Zitat?

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