Skip to content

Latest commit

 

History

History
63 lines (45 loc) · 1.59 KB

README.md

File metadata and controls

63 lines (45 loc) · 1.59 KB
Raw

Automation tool for verifying code using LLMs

Example usage:

export GRAZIE_JWT_TOKEN=insert grazie token
poetry run verified-cogen --insert-conditions-mode=llm --llm-profile=gpt-4-1106-preview --prompts-directory=prompts/rust_invariants -i RustBench/ground_truth/binary_search.rs

or

export GRAZIE_JWT_TOKEN=insert grazie token
poetry run verified-cogen --insert-conditions-mode=llm --llm-profile=gpt-4-1106-preview --prompts-directory=prompts/dafny_invariants -i DafnyBench/hints_removed/630-dafny_tmp_tmpz2kokaiq_Solution_no_hints.dfy

To run the gui, run it directly from the verified-cogen directory or install the cli using poetry:

poetry install

Add .venv/bin to your PATH and use verified-cogen freely.

cargo run --manifest-path=gui/Cargo.toml

Screenshot of GUI

Available insertion modes:

  • regex - insert invariants manually after the loop, only works if the program has exactly one while loop, works only for dafny
  • llm - use LLM to insert invariants into the correct place, as a separate step from producing them
  • llm-single-step - use LLM to add invariants to rewrite the program to include invariants, as a singlestep

Profiles are from grazie, useful ones:

  • gpt-4-1106-preview - GPT4-Turbo
  • gpt-4o - GPT-4o
  • anthropic-claude-3-opus - Claude 3 Opus

Current status

Verified with modification for Rust:

  • Cubes
  • Reverse
  • Replace Chars
  • Max Array
  • String Xor
  • Binary Search
  • Two Sum
  • Is Sorted
  • Integer Square Root
  • Intersperse
  • Unique With Hint
  • Unique No Hints

Failed:

  • Smallest Missing Number
  • Has Close Elements