DafnyBench

Dafnybench: эталон для формальной проверки программного обеспечения

Набор данных и код для нашей статьи Dafnybench: эталон для формальной проверки программного обеспечения

Набор данных также доступен для загрузки? Обнимающееся лицо.

Обзор

Dafnybench является крупнейшим ориентиром в своем роде для обучения и оценки систем машинного обучения для формальной проверки программного обеспечения с более чем 750 Dafny программами.

Использование

• Набор данных : набор данных для Dafnybench (с 782 программами) можно найти в каталоге DafnyBench , который содержит набор ground_truth и набор hints_removed (с подсказками компилятора, то есть annoataions, удален).
• Оценка : Оцените LLMS на Dafnybench, попросив модели заполнить отсутствующие намеки в тестовом файле из набора hints_removed и проверить, может ли реконструированная программа быть подтверждена Dafny. Пожалуйста, обратитесь к каталогу eval .

Настройка для оценки?

1. Установите Dafny на вашу машину, следуя этому руководству
2. Клон и cd в этот репозиторий
3. Установите среду, выполнив следующие строки:

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

4. Настройка переменной среды для корневого каталога:

 export DAFNYBENCH_ROOT=

5. Установите переменную среды для Path to Dafny исполняемого на вашей машине (например, /opt/homebrew/bin/Dafny ):

 export DAFNY_PATH=

6. Если вы оцениваете LLM через доступ к API, настройте ключ API. Например:

 export OPENAI_API_KEY=

7. Вы можете оценить LLM в одной программе тестирования, такой как:

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

или оценить весь набор данных:

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

Содержимое?

• DafnyBench
  • Коллекция из 782 программ DAFNY. Каждая программа имеет версию ground_truth , которая полностью проверена с помощью версии Dafny & A hints_removed , которая имеет подсказки (т.е. аннотации)
• eval
  • Содержит сценарии для оценки LLM на Dafnybench
• results
  • results_summary - DataFrames, которые суммируют успех LLMS в каждой программе тестирования
  • reconstructed_files - Выходы LLM с подсказками, заполненными обратно
  • analysis - содержит ноутбук для анализа результатов

Цитата?

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