Reproduce “Verified but Vacuous: Three Failure Surfaces of LLM-Driven Verified Code Generation” on OpenResearch
Turn your favorite coding agents into research agents that review literature, develop hypotheses, and run experiments.
Universal app for Apple silicon and Intel. Requires macOS 11 or later.
About this paper
Aditya Vempaty, Himaneesh Sompalle, Manan Tayal, Mowafak Allaham, Prasenjit Dey, Ashish Jagmohan, Ravi Kokku
The authors audit code-generation verification across three questions: whether a verifier accepts a proof, whether it binds to a specification, and whether that specification captures the requirement. On HumanEval, Li@Opus has 99.1% verifier acceptance but only 1.9% binding among accepted samples; VCG has 14.82% hidden-test failure among structurally verified samples. Hidden-test failure is a proxy under trusted-toolchain and correct-oracle assumptions.
Summary by alphaXiv.
Tip: change arxiv.org to autoarxiv.org in any arXiv abstract link to open the paper here.