DafnyBench

Dafnybench: un punto de referencia para la verificación formal de software

Conjunto de datos y código para nuestro documento Dafnybench: un punto de referencia para la verificación formal de software

¿El conjunto de datos también está disponible para descargar? Cara abrazada.

Descripción general

DafnyBench es el punto de referencia más grande de su tipo para capacitar y evaluar sistemas de aprendizaje automático para la verificación formal de software, con más de 750 programas DAFNY.

Uso

• DataSet : el conjunto de datos para DafnyBench (con 782 programas) se puede encontrar en el directorio DafnyBench , que contiene el conjunto ground_truth y el conjunto de hints_removed (con sugerencias del compilador, es decir, annataions, eliminado).
• Evaluación : Evalúe las LLM en DafnyBench pidiéndole a los modelos que llenen sugerencias faltantes en un archivo de prueba del conjunto de hints_removed y verificación si DAFNY podría verificar el programa reconstruido. Consulte el directorio eval .

Configurar para la evaluación?

1. Instale Dafny en su máquina siguiendo este tutorial
2. Clon & cd en este repositorio
3. Configurar el entorno ejecutando las siguientes líneas:

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

4. Configurar la variable de entorno para el directorio raíz:

 export DAFNYBENCH_ROOT=

5. Configurar la variable de entorno para el ejecutable de ruta a DAFNY en su máquina (por ejemplo, /opt/homebrew/bin/Dafny ):

 export DAFNY_PATH=

6. Si está evaluando un LLM a través del acceso de API, configure la tecla API. Por ejemplo:

 export OPENAI_API_KEY=

7. Puede optar por evaluar un LLM en un solo programa de prueba, como:

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

o evaluar en todo el conjunto de datos:

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

¿Contenido?

• DafnyBench
  • Una colección de 782 programas DAFNY. Cada programa tiene una versión ground_truth que se verifica completamente con DAFNY & A hints_removed Versión que tiene sugerencias (es decir, anotaciones) eliminadas
• eval
  • Contiene scripts para evaluar LLM en DafnyBench
• results
  • results_summary : marcos de datos que resumen el éxito de LLMS en cada programa de prueba
  • reconstructed_files - salidas LLM con pistas llenas de nuevo en
  • analysis : contiene un cuaderno para analizar los resultados

Cita?

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