DafnyBench

Dafnybench: une référence pour la vérification des logiciels formels

Ensemble de données et code pour notre papier dafnybench: une référence pour la vérification des logiciels formels

L'ensemble de données est également disponible en téléchargement? Visage étreint.

Aperçu

Dafnybench est la plus grande référence du genre pour la formation et l'évaluation des systèmes d'apprentissage automatique pour la vérification formelle des logiciels, avec plus de 750 programmes DAFNY.

Usage

• Ensemble de données : L'ensemble de données de Dafnybench (avec 782 programmes) peut être trouvé dans le répertoire DafnyBench , qui contient l'ensemble ground_truth et l'ensemble hints_removed (avec des conseils de compilateur, c'est-à-dire des anoataions, supprimés).
• Évaluation : Évaluez les LLM sur Dafnybench en demandant aux modèles de remplir des conseils manquants dans un fichier de test à partir de l'ensemble hints_removed et de la vérification si le programme reconstruit pouvait être vérifié par DAFNY. Veuillez vous référer au répertoire eval .

Configuré pour l'évaluation?

1. Installez Dafny sur votre machine en suivant ce tutoriel
2. Clone & cd dans ce référentiel
3. Configurez l'environnement en exécutant les lignes suivantes:

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

4. Configurer la variable d'environnement pour le répertoire racine:

 export DAFNYBENCH_ROOT=

5. Configurez la variable d'environnement pour le chemin d'accès à Dafny sur votre machine (par exemple, /opt/homebrew/bin/Dafny ):

 export DAFNY_PATH=

6. Si vous évaluez un LLM via l'accès à l'API, configurez la clé de l'API. Par exemple:

 export OPENAI_API_KEY=

7. Vous pouvez choisir d'évaluer un LLM sur un seul programme de test, tel que:

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

ou évaluer sur l'ensemble de données:

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

Contenu?

• DafnyBench
  • Une collection de 782 programmes DAFNY. Chaque programme a une version ground_truth qui est entièrement vérifiée avec Dafny et une version hints_removed qui a des indices (c'est-à-dire des annotations)
• eval
  • Contient des scripts pour évaluer les LLM sur Dafnybench
• results
  • results_summary - DataFrames qui résument le succès de LLMS sur chaque programme de test
  • reconstructed_files - Sorties LLM avec des indices remplis
  • analysis - contient un cahier pour analyser les résultats

Citation?

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