This dataset Live-FM-bench is continuously updated and contamination-free evaluation benchmark of LLMs for program verification (a.k.a., formal specification generation). Currently, it contains 360 C programs under verification together with the properties to be verified.
This dataset can be used for:
Specification generation task (Code2Proof): given program and properties to be verified as input, output program with specification that can pass the prover.… See the full description on the dataset page:
https://huggingface.co/datasets/fm-universe/Live-FM-Bench.
