DafnyBench

Dafnybench: uma referência para verificação formal de software

DataSet & Code para nosso papel Dafnybench: uma referência para verificação formal de software

O conjunto de dados também está disponível para download? Abraçando o rosto.

Visão geral

A Dafnybench é a maior referência do gênero para treinamento e avaliação de sistemas de aprendizado de máquina para verificação formal de software, com mais de 750 programas dafny.

Uso

• DataSet : o conjunto de dados para Dafnybench (com 782 programas) pode ser encontrado no diretório DafnyBench , que contém o conjunto ground_truth & the hints_removed Set (com dicas do compilador, ou seja, Anotaions, removido).
• Avaliação : Avalie o LLMS no Dafnybench, solicitando aos modelos que preencham dicas ausentes em um arquivo de teste do conjunto hints_removed e verificando se o programa reconstruído puder ser verificado por Dafny. Consulte o diretório eval .

Configurado para avaliação?

1. Instale Dafny em sua máquina seguindo este tutorial
2. Clone & cd neste repositório
3. Configure o ambiente executando as seguintes linhas:

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

4. Configurar variável de ambiente para o diretório raiz:

 export DAFNYBENCH_ROOT=

5. Configure a variável de ambiente para o caminho para o executável dafny em sua máquina (por exemplo, /opt/homebrew/bin/Dafny ):

 export DAFNY_PATH=

6. Se você estiver avaliando um LLM através do acesso da API, configure a tecla API. Por exemplo:

 export OPENAI_API_KEY=

7. Você pode optar por avaliar um LLM em um único programa de teste, como:

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

ou avaliar em todo o conjunto de dados:

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

Conteúdo?

• DafnyBench
  • Uma coleção de 782 programas dafny. Cada programa possui uma versão ground_truth que é totalmente verificada com a versão Dafny & a hints_removed que tem dicas (por exemplo, anotações) removidas
• eval
  • Contém scripts para avaliar LLMs no Dafnybench
• results
  • results_summary - DataFrames que resumem o sucesso da LLMS em todos os programas de teste
  • reconstructed_files - saídas LLM com dicas preenchidas de volta
  • analysis - Contém um notebook para analisar os resultados

Citação?

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