{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T21:30:32Z","timestamp":1784237432580,"version":"3.55.0"},"publisher-location":"New York, NY, USA","reference-count":19,"publisher":"ACM","funder":[{"name":"SRC grant","award":["SRC 2023-CT-3175"],"award-info":[{"award-number":["SRC 2023-CT-3175"]}]},{"name":"AMD Center of Excellence grant"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,6,30]]},"DOI":"10.1145\/3716368.3735300","type":"proceedings-article","created":{"date-parts":[[2025,6,27]],"date-time":"2025-06-27T13:58:23Z","timestamp":1751032703000},"page":"547-553","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["PREFACE - A Reinforcement Learning Framework for Code Verification via LLM Prompt Repair"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5613-7039","authenticated-orcid":false,"given":"Manvi","family":"Jha","sequence":"first","affiliation":[{"name":"University of Illinois Urbana-Champaign, Urbana, Illinois, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8006-0019","authenticated-orcid":false,"given":"Jiaxin","family":"Wan","sequence":"additional","affiliation":[{"name":"University of Illinois Urbana-Champaign, Urbana, Illinois, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4426-9736","authenticated-orcid":false,"given":"Huan","family":"Zhang","sequence":"additional","affiliation":[{"name":"University of Illinois Urbana-Champaign, Urbana, Illinois, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3016-0270","authenticated-orcid":false,"given":"Deming","family":"Chen","sequence":"additional","affiliation":[{"name":"University of Illinois Urbana-Champaign, Urbana, Illinois, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,6,29]]},"reference":[{"key":"e_1_3_3_1_2_2","unstructured":"Yuqing Du Olivia Watkins Zihan Wang C\u00e9dric Colas Trevor Darrell Pieter Abbeel Abhishek Gupta and Jacob Andreas. 2023. Guiding Pretraining in Reinforcement Learning with Large Language Models. arxiv:https:\/\/arXiv.org\/abs\/2302.06692\u00a0[cs.LG] https:\/\/arxiv.org\/abs\/2302.06692"},{"key":"e_1_3_3_1_3_2","unstructured":"Binyuan Hui and Others. 2024. Qwen2.5-Coder Technical Report. arxiv:https:\/\/arXiv.org\/abs\/2409.12186\u00a0[cs.CL] https:\/\/arxiv.org\/abs\/2409.12186"},{"key":"e_1_3_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/3643795.3648384"},{"key":"e_1_3_3_1_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_3_3_1_6_2","unstructured":"Yue\u00a0Chen Li Stefan Zetzsche and Siva Somayyajula. 2025. Dafny as Verification-Aware Intermediate Language for Code Generation. arxiv:https:\/\/arXiv.org\/abs\/2501.06283\u00a0[cs.SE] https:\/\/arxiv.org\/abs\/2501.06283"},{"key":"e_1_3_3_1_7_2","first-page":"21558","volume-title":"Advances in Neural Information Processing Systems","volume":"36","author":"Liu Jiawei","year":"2023","unstructured":"Jiawei Liu, Chunqiu\u00a0Steven Xia, Yuyao Wang, and LINGMING ZHANG. 2023. Is Your Code Generated by ChatGPT Really Correct? Rigorous Evaluation of Large Language Models for Code Generation. In Advances in Neural Information Processing Systems, A.\u00a0Oh, T.\u00a0Naumann, A.\u00a0Globerson, K.\u00a0Saenko, M.\u00a0Hardt, and S.\u00a0Levine (Eds.), Vol.\u00a036. Curran Associates, Inc., 21558\u201321572. https:\/\/proceedings.neurips.cc\/paper_files\/paper\/2023\/file\/43e9d647ccd3e4b7b5baab53f0368686-Paper-Conference.pdf"},{"key":"e_1_3_3_1_8_2","unstructured":"Chloe Loughridge Qinyi Sun Seth Ahrenbach Federico Cassano Chuyue Sun Ying Sheng Anish Mudide Md\u00a0Rakib\u00a0Hossain Misu Nada Amin and Max Tegmark. 2024. DafnyBench: A Benchmark for Formal Software Verification. arxiv:https:\/\/arXiv.org\/abs\/2406.08467\u00a0[cs.SE] https:\/\/arxiv.org\/abs\/2406.08467"},{"key":"e_1_3_3_1_9_2","unstructured":"Lezhi Ma Shangqing Liu Yi Li Xiaofei Xie and Lei Bu. 2025. SpecGen: Automated Generation of Formal Program Specifications via Large Language Models. arxiv:https:\/\/arXiv.org\/abs\/2401.08807\u00a0[cs.SE] https:\/\/arxiv.org\/abs\/2401.08807"},{"key":"e_1_3_3_1_10_2","doi-asserted-by":"publisher","unstructured":"Md\u00a0Rakib\u00a0Hossain Misu Cristina\u00a0V. Lopes Iris Ma and James Noble. 2024. Towards AI-Assisted Synthesis of Verified Dafny Methods. Proc. ACM Softw. Eng. 1 FSE Article 37 (July 2024) 24\u00a0pages. 10.1145\/3643763","DOI":"10.1145\/3643763"},{"key":"e_1_3_3_1_11_2","unstructured":"William Murphy Nikolaus Holzer Feitong Qiao Leyi Cui Raven Rothkopf Nathan Koenig and Mark Santolucito. 2024. Combining LLM Code Generation with Formal Specifications and Reactive Program Synthesis. arxiv:https:\/\/arXiv.org\/abs\/2410.19736\u00a0[cs.SE] https:\/\/arxiv.org\/abs\/2410.19736"},{"key":"e_1_3_3_1_12_2","unstructured":"OpenAI et\u00a0al. 2024. GPT-4 Technical Report. arxiv:https:\/\/arXiv.org\/abs\/2303.08774\u00a0[cs.CL] https:\/\/arxiv.org\/abs\/2303.08774"},{"key":"e_1_3_3_1_13_2","unstructured":"Gabriel Poesia Chloe Loughridge and Nada Amin. 2024. dafny-annotator: AI-Assisted Verification of Dafny Programs. arxiv:https:\/\/arXiv.org\/abs\/2411.15143\u00a0[cs.SE] https:\/\/arxiv.org\/abs\/2411.15143"},{"key":"e_1_3_3_1_14_2","unstructured":"Qwen and Others. 2025. Qwen2.5 Technical Report. arxiv:https:\/\/arXiv.org\/abs\/2412.15115\u00a0[cs.CL] https:\/\/arxiv.org\/abs\/2412.15115"},{"key":"e_1_3_3_1_15_2","unstructured":"Yi Ren and Danica\u00a0J. Sutherland. 2025. Learning Dynamics of LLM Finetuning. arxiv:https:\/\/arXiv.org\/abs\/2407.10490\u00a0[cs.LG] https:\/\/arxiv.org\/abs\/2407.10490"},{"key":"e_1_3_3_1_16_2","first-page":"80","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"Reynolds Andrew","year":"2015","unstructured":"Andrew Reynolds and Viktor Kuncak. 2015. Induction for SMT Solvers. In Verification, Model Checking, and Abstract Interpretation, Deepak D\u2019Souza, Akash Lal, and Kim\u00a0Guldstrand Larsen (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 80\u201398."},{"key":"e_1_3_3_1_17_2","unstructured":"Yuan Wei Xiaohan Shan and Jianmin Li. 2025. LERO: LLM-driven Evolutionary framework with Hybrid Rewards and Enhanced Observation for Multi-Agent Reinforcement Learning. arxiv:https:\/\/arXiv.org\/abs\/2503.21807\u00a0[cs.LG] https:\/\/arxiv.org\/abs\/2503.21807"},{"key":"e_1_3_3_1_18_2","doi-asserted-by":"publisher","DOI":"10.1109\/ISEDA62518.2024.10617643"},{"key":"e_1_3_3_1_19_2","unstructured":"Tianyang Zhong and Others. 2024. Evaluation of OpenAI o1: Opportunities and Challenges of AGI. arxiv:https:\/\/arXiv.org\/abs\/2409.18486\u00a0[cs.CL] https:\/\/arxiv.org\/abs\/2409.18486"},{"key":"e_1_3_3_1_20_2","unstructured":"Yuan Zhuang Yi Shen Zhili Zhang Yuxiao Chen and Fei Miao. 2024. YOLO-MARL: You Only LLM Once for Multi-agent Reinforcement Learning. arxiv:https:\/\/arXiv.org\/abs\/2410.03997\u00a0[cs.MA] https:\/\/arxiv.org\/abs\/2410.03997"}],"event":{"name":"GLSVLSI '25: Great Lakes Symposium on VLSI 2025","location":"New Orleans LA USA","acronym":"GLSVLSI '25","sponsor":["SIGDA ACM Special Interest Group on Design Automation"]},"container-title":["Proceedings of the Great Lakes Symposium on VLSI 2025"],"original-title":[],"deposited":{"date-parts":[[2025,6,27]],"date-time":"2025-06-27T14:36:07Z","timestamp":1751034967000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3716368.3735300"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,29]]},"references-count":19,"alternative-id":["10.1145\/3716368.3735300","10.1145\/3716368"],"URL":"https:\/\/doi.org\/10.1145\/3716368.3735300","relation":{},"subject":[],"published":{"date-parts":[[2025,6,29]]},"assertion":[{"value":"2025-06-29","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}