Reproduce “Path2Spec: Path-Aware Specification Generation via Large Language Models” 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
Dan Huang, Zhensu Sun, Huihui Huang, Jinfeng Jiang, Xiaofei Xie, Yintong Huo, David Lo
Path2Spec generates formal Java/JML specifications by having an LLM describe individual execution paths, checking them with OpenJML, and merging verified cases; it recursively splits programs at branches when needed. On SV-COMP with GPT-5, it verified 220 of 265 programs (83.0%), versus SpecGen’s 117 of 265 (44.2%). Verification success does not establish completeness, and the study covers Java/JML with OpenJML.
Summary by alphaXiv.
Tip: change arxiv.org to autoarxiv.org in any arXiv abstract link to open the paper here.