{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,22]],"date-time":"2025-05-22T05:50:47Z","timestamp":1747893047329,"version":"3.28.0"},"reference-count":41,"publisher":"IEEE","license":[{"start":{"date-parts":[[2023,10,28]],"date-time":"2023-10-28T00:00:00Z","timestamp":1698451200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2023,10,28]],"date-time":"2023-10-28T00:00:00Z","timestamp":1698451200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023,10,28]]},"DOI":"10.1109\/iccad57390.2023.10323681","type":"proceedings-article","created":{"date-parts":[[2023,11,30]],"date-time":"2023-11-30T18:58:45Z","timestamp":1701370725000},"page":"1-9","source":"Crossref","is-referenced-by-count":1,"title":["LFPS: Learned Formal Proof Strengthening for Efficient Hardware Verification"],"prefix":"10.1109","author":[{"given":"Minwoo","family":"Kang","sequence":"first","affiliation":[{"name":"UC Berkeley"}]},{"given":"Azade","family":"Nova","sequence":"additional","affiliation":[{"name":"Google DeepMind"}]},{"given":"Eshan","family":"Singh","sequence":"additional","affiliation":[{"name":"Google"}]},{"given":"Geetheeka Sharron","family":"Bathini","sequence":"additional","affiliation":[{"name":"Google"}]},{"given":"Yuriy","family":"Viktorov","sequence":"additional","affiliation":[{"name":"Google"}]}],"member":"263","reference":[{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.5555\/3026877.3026899"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1145\/996566.996629"},{"key":"ref3","article-title":"Program synthesis with large language models","author":"Austin","year":"2021","journal-title":"arXiv preprint"},{"key":"ref4","article-title":"Deepcoder: Learning to write programs","author":"Balog","year":"2016","journal-title":"arXiv preprint"},{"key":"ref5","article-title":"Learning to reason in large theories without imitation","author":"Bansal","year":"2019","journal-title":"arXiv preprint"},{"key":"ref6","first-page":"1877","article-title":"Language models are few-shot learners","volume":"33","author":"Brown","year":"2020","journal-title":"Advances in neural information processing systems"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-011-0134-0"},{"key":"ref8","article-title":"Evaluating large language models trained on code","author":"Chen","year":"2021","journal-title":"arXiv preprint"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011276507260"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876643"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35746-6_1"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_13"},{"key":"ref13","article-title":"BERT: Pre-training of deep bidirectional transformers for language understanding","author":"Devlin","year":"2018","journal-title":"arXiv preprint"},{"key":"ref14","article-title":"The 2022 wilson research group ic\/asic functional verification treads","author":"Foster","year":"2022","journal-title":"White Paper. Wilson Research Group and Mentor, A Siemens Business"},{"key":"ref15","article-title":"Automated assume-guarantee reasoning by abstraction refinement","volume":"5123","author":"P\u0103s\u0103reanu","year":"2008","journal-title":"Computer Aided Verification. CAV 2008. Lecture Notes in Computer Science"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028765"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2013.2241176"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1162\/neco.1997.9.8.1735"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1561\/2200000081"},{"key":"ref20","first-page":"5110","article-title":"Learning and evaluating contextual embedding of source code","volume-title":"International conference on machine learning","author":"Kanade","year":"2020"},{"key":"ref21","article-title":"Semi-supervised classification with graph convolutional networks","author":"Kipf","year":"2016","journal-title":"arXiv preprint"},{"key":"ref22","first-page":"3499","article-title":"Stochastic beams and where to find them: The gumbel-top-k trick for sampling sequences without replacement","volume-title":"International Conference on Machine Learning","author":"Kool","year":"2019"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-03809-3"},{"key":"ref24","first-page":"9608","article-title":"Can q-learning with graph networks learn a generalizable branching heuristic for a sat solver?","volume":"33","author":"Kurin","year":"2020","journal-title":"Advances in Neural Information Processing Systems"},{"key":"ref25","article-title":"Learning heuristics for quantified boolean formulas through deep reinforcement learning","author":"Lederman","year":"2018","journal-title":"arXiv preprint"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2015.71"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1109\/ICCV.2017.324"},{"key":"ref28","article-title":"Decoupled weight decay regularization","author":"Loshchilov","year":"2017","journal-title":"arXiv preprint"},{"key":"ref29","article-title":"On the complexity of the model checking problem","volume":"abs\/1210.6893","author":"Madelaine","year":"2012","journal-title":"CoRR"},{"key":"ref30","article-title":"Text and code embeddings by contrastive pre-training","author":"Neelakantan","year":"2022","journal-title":"arXiv preprint"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2019.2921374"},{"issue":"1","key":"ref32","first-page":"5485","article-title":"Exploring the limits of transfer learning with a unified text-to-text transformer","volume":"21","author":"Raffel","year":"2020","journal-title":"The Journal of Machine Learning Research"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1109\/ICASSP.2012.6289079"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/p16-1162"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-40922-X_8"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v35i14.17474"},{"key":"ref37","first-page":"23491","article-title":"Learning semantic representations to verify hardware designs","volume":"34","author":"Vasudevan","year":"2021","journal-title":"Advances in Neural Information Processing Systems"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2010.5457129"},{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.1706.03762"},{"key":"ref40","first-page":"9330","article-title":"Tacticzero: Learning to prove theorems from scratch with deep reinforcement learning","volume":"34","author":"Wu","year":"2021","journal-title":"Advances in Neural Information Processing Systems"},{"key":"ref41","article-title":"Neural guided constraint logic programming for program synthesis","volume":"31","author":"Zhang","year":"2018","journal-title":"Advances in Neural Information Processing Systems"}],"event":{"name":"2023 IEEE\/ACM International Conference on Computer Aided Design (ICCAD)","start":{"date-parts":[[2023,10,28]]},"location":"San Francisco, CA, USA","end":{"date-parts":[[2023,11,2]]}},"container-title":["2023 IEEE\/ACM International Conference on Computer Aided Design (ICCAD)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/10323590\/10323543\/10323681.pdf?arnumber=10323681","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,2]],"date-time":"2024-03-02T22:03:38Z","timestamp":1709417018000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/10323681\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,28]]},"references-count":41,"URL":"https:\/\/doi.org\/10.1109\/iccad57390.2023.10323681","relation":{},"subject":[],"published":{"date-parts":[[2023,10,28]]}}}