{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:44:22Z","timestamp":1780994662221,"version":"3.54.1"},"reference-count":35,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2025,2,24]],"date-time":"2025-02-24T00:00:00Z","timestamp":1740355200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,2,24]],"date-time":"2025-02-24T00:00:00Z","timestamp":1740355200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100001691","name":"Japan Society for the Promotion of Science","doi-asserted-by":"publisher","award":["JP20H05703"],"award-info":[{"award-number":["JP20H05703"]}],"id":[{"id":"10.13039\/501100001691","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001691","name":"Japan Society for the Promotion of Science","doi-asserted-by":"publisher","award":["JP20H04162"],"award-info":[{"award-number":["JP20H04162"]}],"id":[{"id":"10.13039\/501100001691","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001691","name":"Japan Society for the Promotion of Science","doi-asserted-by":"publisher","award":["JP19K22842"],"award-info":[{"award-number":["JP19K22842"]}],"id":[{"id":"10.13039\/501100001691","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002241","name":"Japan Science and Technology Agency","doi-asserted-by":"publisher","award":["JPMJER1603"],"award-info":[{"award-number":["JPMJER1603"]}],"id":[{"id":"10.13039\/501100002241","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004721","name":"The University of Tokyo","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100004721","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2025,11]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    We propose a novel framework of program and invariant synthesis called neural network-guided synthesis (\n                    <jats:sc>NeuGuS<\/jats:sc>\n                    ). We first show that, by suitably designing and training neural networks, we can extract logical formulas over integers from the weights and biases of the trained neural networks. Based on the idea, we have implemented a tool to synthesize formulas from positive\/negative examples and implication constraints, and obtained promising experimental results. We also discuss two applications of our synthesis method. One is the use of our tool for qualifier discovery in the framework of ICE-learning-based CHC solving, which can in turn be applied to program verification and inductive invariant synthesis. Another application is to a new program development framework called oracle-based programming, which is a neural-network-guided variation of Solar-Lezama\u2019s program synthesis by sketching.\n                  <\/jats:p>","DOI":"10.1007\/s10703-024-00468-9","type":"journal-article","created":{"date-parts":[[2025,2,24]],"date-time":"2025-02-24T03:16:00Z","timestamp":1740366960000},"page":"222-254","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Towards neural-network-guided program synthesis and verification"],"prefix":"10.1007","volume":"67","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0537-0604","authenticated-orcid":false,"given":"Naoki","family":"Kobayashi","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Taro","family":"Sekiyama","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Issei","family":"Sato","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Hiroshi","family":"Unno","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,2,24]]},"reference":[{"key":"468_CR1","doi-asserted-by":"crossref","unstructured":"Garg P, L\u00f6ding C, Madhusudan P, Neider D (2014) ICE: a robust framework for learning invariants. In: Proceedings of CAV 2014. LNCS, vol 8559. Springer, pp 69\u201387","DOI":"10.1007\/978-3-319-08867-9_5"},{"key":"468_CR2","doi-asserted-by":"publisher","unstructured":"Zhu H, Xiong Z, Magill S, Jagannathan S (2019) An inductive synthesis framework for verifiable reinforcement learning. In: Proceedings of the 40th ACM SIGPLAN conference on programming language design and implementation, PLDI 2019. ACM, pp 686\u2013701. https:\/\/doi.org\/10.1145\/3314221.3314638","DOI":"10.1145\/3314221.3314638"},{"key":"468_CR3","doi-asserted-by":"publisher","unstructured":"Gehr T, Mirman M, Drachsler-Cohen D, Tsankov P, Chaudhuri S, Vechev MT (2018) AI2: safety and robustness certification of neural networks with abstract interpretation. In: 2018 IEEE symposium on security and privacy, SP 2018, proceedings. IEEE Computer Society, pp 3\u201318. https:\/\/doi.org\/10.1109\/SP.2018.00058","DOI":"10.1109\/SP.2018.00058"},{"key":"468_CR4","doi-asserted-by":"crossref","unstructured":"Zhao H, Zeng X, Chen T, Liu Z, Woodcock J (2020) Learning safe neural network controllers with barrier certificates","DOI":"10.1007\/978-3-030-62822-2_11"},{"key":"468_CR5","unstructured":"Anderson G, Verma A, Dillig I, Chaudhuri S (2020) Neurosymbolic reinforcement learning with formally verified exploration. In: Advances in neural information processing systems 33: annual conference on neural information processing systems 2020, NeurIPS 2020"},{"key":"468_CR6","doi-asserted-by":"publisher","unstructured":"Pulina L, Tacchella A (2010) An abstraction-refinement approach to verification of artificial neural networks. In: Computer aided verification, 22nd international conference, CAV 2010, proceedings. LNCS, vol 6174. Springer, pp 243\u2013257. https:\/\/doi.org\/10.1007\/978-3-642-14295-6_24","DOI":"10.1007\/978-3-642-14295-6_24"},{"key":"468_CR7","doi-asserted-by":"crossref","unstructured":"Narodytska N, Kasiviswanathan SP, Ryzhyk L, Sagiv M, Walsh T (2018) Verifying properties of binarized deep neural networks. In: Proceedings of the thirty-second AAAI conference on artificial intelligence, (AAAI-18), the 30th innovative applications of artificial intelligence (IAAI-18), and the 8th AAAI symposium on educational advances in artificial intelligence (EAAI-18). AAAI Press, pp 6615\u20136624","DOI":"10.1609\/aaai.v32i1.12206"},{"key":"468_CR8","unstructured":"Verma A, Murali V, Singh R, Kohli P, Chaudhuri S (2018) Programmatically interpretable reinforcement learning. In: Proceedings of the 35th international conference on machine learning, ICML 2018. Proceedings of machine learning research, vol 80. PMLR, pp 5052\u20135061"},{"key":"468_CR9","doi-asserted-by":"publisher","unstructured":"Katz G, Barrett CW, Dill DL, Julian K, Kochenderfer MJ (2017) Reluplex: an efficient SMT solver for verifying deep neural networks. In: Computer aided verification-29th international conference, CAV 2017, proceedings, Part I. LNCS, vol 10426. Springer, pp 97\u2013117. https:\/\/doi.org\/10.1007\/978-3-319-63387-9_5","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"468_CR10","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1016\/j.inffus.2019.12.012","volume":"58","author":"AB Arrieta","year":"2020","unstructured":"Arrieta AB, Rodr\u00edguez ND, Ser JD, Bennetot A, Tabik S, Barbado A, Garc\u00eda S, Gil-Lopez S, Molina D, Benjamins R, Chatila R, Herrera F (2020) Explainable artificial intelligence (XAI): concepts, taxonomies, opportunities and challenges toward responsible AI. Inf Fusion 58:82\u2013115. https:\/\/doi.org\/10.1016\/j.inffus.2019.12.012","journal-title":"Inf Fusion"},{"issue":"7","key":"468_CR11","doi-asserted-by":"publisher","first-page":"1393","DOI":"10.1007\/s10817-020-09571-y","volume":"64","author":"A Champion","year":"2020","unstructured":"Champion A, Chiba T, Kobayashi N, Sato R (2020) ICE-based refinement type discovery for higher-order functional programs. J Autom Reason 64(7):1393\u20131418","journal-title":"J Autom Reason"},{"key":"468_CR12","unstructured":"Solar-Lezama A (2008) Program synthesis by sketching. Ph.d thesis, University of California, Berkeley"},{"key":"468_CR13","unstructured":"Martius G, Lampert CH (2017) Extrapolation and learning equations. In: 5th International conference on learning representations, ICLR 2017, Toulon, France, April 24\u201326, 2017, workshop track proceedings. OpenReview.net. https:\/\/openreview.net\/forum?id=BkgRp0FYe"},{"key":"468_CR14","unstructured":"Petersen BK, Landajuela M, Mundhenk TN, Santiago CP, Kim SK, Kim JT (2021) Deep symbolic regression: recovering mathematical expressions from data via risk-seeking policy gradients. In: Proceedings of the international conference on learning representations"},{"key":"468_CR15","unstructured":"Sahoo S, Lampert C, Martius G (2018) Learning equations for extrapolation and control. In: Dy J, Krause A (eds) Proceedings of the 35th international conference on machine learning. Proceedings of machine learning research, vol 80. PMLR, Stockholmsm\u00e4ssan, Stockholm, Sweden, pp 4442\u20134450. http:\/\/proceedings.mlr.press\/v80\/sahoo18a.html"},{"key":"468_CR16","unstructured":"Ryan G, Wong J, Yao J, Gu R, Jana S (2020) CLN2INV: learning loop invariants with continuous logic networks. In: 8th International conference on learning representations, ICLR 2020. OpenReview.net"},{"key":"468_CR17","doi-asserted-by":"publisher","unstructured":"Yao J, Ryan G, Wong J, Jana S, Gu R (2020) Learning nonlinear loop invariants with gated continuous logic networks. In: Proceedings of the 41st ACM SIGPLAN international conference on programming language design and implementation, PLDI 2020. ACM, pp 106\u2013120. https:\/\/doi.org\/10.1145\/3385412.3385986","DOI":"10.1145\/3385412.3385986"},{"key":"468_CR18","doi-asserted-by":"publisher","unstructured":"Kobayashi N, Sekiyama T, Sato I, Unno H (2021) Toward neural-network-guided program synthesis and verification. In: Dragoi C, Mukherjee S, Namjoshi KS (eds) Static analysis - 28th international symposium, SAS 2021, Chicago, IL, USA, October 17\u201319, 2021, proceedings. Lecture notes in computer science, vol 12913. Springer, pp 236\u2013260. https:\/\/doi.org\/10.1007\/978-3-030-88806-0_12","DOI":"10.1007\/978-3-030-88806-0_12"},{"key":"468_CR19","unstructured":"Kingma DP, Ba J (2015) Adam: A method for stochastic optimization. In: 3rd International conference on learning representations, ICLR 2015, conference track proceedings. arXiv: 1412.6980"},{"key":"468_CR20","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner N, Gurfinkel A, McMillan KL, Rybalchenko A (2015) Horn clause solvers for program verification. In: Fields of logic and computation II\u2014essays dedicated to Yuri Gurevich on the occasion of his 75th birthday. LNCS, vol 9300. Springer, pp 24\u201351","DOI":"10.1007\/978-3-319-23534-9_2"},{"issue":"3","key":"468_CR21","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/s10703-016-0249-4","volume":"48","author":"A Komuravelli","year":"2016","unstructured":"Komuravelli A, Gurfinkel A, Chaki S (2016) Smt-based model checking for recursive programs. Formal Methods Syst Des 48(3):175\u2013205","journal-title":"Formal Methods Syst Des"},{"key":"468_CR22","doi-asserted-by":"crossref","unstructured":"Hojjat H, R\u00fcmmer P (2018) The eldarica horn solver. In: 2018 Formal methods in computer aided design (FMCAD), pp 1\u20137","DOI":"10.23919\/FMCAD.2018.8603013"},{"key":"468_CR23","doi-asserted-by":"crossref","unstructured":"Satake Y, Unno H, Yanagi H (2020) Probabilistic inference for predicate constraint satisfaction. In: The thirty-fourth AAAI conference on artificial intelligence, AAAI 2020, the thirty-second innovative applications of artificial intelligence conference, IAAI 2020, the tenth AAAI symposium on educational advances in artificial intelligence, EAAI 2020. AAAI Press, pp 1644\u20131651","DOI":"10.1609\/aaai.v34i02.5526"},{"key":"468_CR24","doi-asserted-by":"publisher","unstructured":"Garg P, Neider D, Madhusudan P, Roth D (2016) Learning invariants using decision trees and implication counterexamples. In: Proceedings of the 43rd annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL 2016. ACM, pp 499\u2013512. https:\/\/doi.org\/10.1145\/2837614.2837664","DOI":"10.1145\/2837614.2837664"},{"key":"468_CR25","unstructured":"Alur R, Fisman D, Padhi S, Singh R, Udupa A (2019) SyGuS-Comp 2018: results and analysis"},{"key":"468_CR26","doi-asserted-by":"publisher","unstructured":"Pavlinovic Z, Su Y, Wies T (2021) Data flow refinement type inference. Proc ACM Program Lang 5(POPL):1\u201331. https:\/\/doi.org\/10.1145\/3434300","DOI":"10.1145\/3434300"},{"key":"468_CR27","doi-asserted-by":"publisher","unstructured":"Zhu H, Magill S, Jagannathan S (2018) A data-driven CHC solver. In: Proceedings of the 39th ACM SIGPLAN conference on programming language design and implementation, PLDI 2018. ACM, pp 707\u2013721. https:\/\/doi.org\/10.1145\/3192366.3192416","DOI":"10.1145\/3192366.3192416"},{"key":"468_CR28","doi-asserted-by":"crossref","unstructured":"Kobayashi N, Sato R, Unno H (2011) Predicate abstraction and CEGAR for higher-order model checking. In: PLDI 2011. ACM Press, pp 222\u2013233","DOI":"10.1145\/1993498.1993525"},{"key":"468_CR29","doi-asserted-by":"publisher","unstructured":"Huang X, Kwiatkowska M, Wang S, Wu M (2017) Safety verification of deep neural networks. In: Computer aided verification\u201429th international conference, CAV 2017, proceedings, part I. LNCS, vol 10426. Springer, pp 3\u201329. https:\/\/doi.org\/10.1007\/978-3-319-63387-9_1","DOI":"10.1007\/978-3-319-63387-9_1"},{"key":"468_CR30","doi-asserted-by":"publisher","unstructured":"Kobayashi N, Wu M (2023) Neural network-guided synthesis of recursive list functions. In: Sankaranarayanan S, Sharygina N (eds) Tools and algorithms for the construction and analysis of systems\u201429th international conference, TACAS 2023, held as part of the european joint conferences on theory and practice of software, ETAPS 2023, Paris, France, April 22\u201327, 2023, proceedings, Part I. Lecture notes in computer science, vol 13993. Springer, pp 227\u2013245. https:\/\/doi.org\/10.1007\/978-3-031-30823-9_12","DOI":"10.1007\/978-3-031-30823-9_12"},{"key":"468_CR31","doi-asserted-by":"publisher","unstructured":"Padhi S, Sharma R, Millstein TD (2016) Data-driven precondition inference with learned features. In: Krintz C, Berger E (eds) Proceedings of the 37th ACM SIGPLAN conference on programming language design and implementation, PLDI 2016, Santa Barbara, CA, USA, June 13\u201317, 2016. ACM, pp 42\u201356. https:\/\/doi.org\/10.1145\/2908080.2908099","DOI":"10.1145\/2908080.2908099"},{"key":"468_CR32","doi-asserted-by":"crossref","unstructured":"Ezudheen P, Neider D, D\u2019Souza D, Garg P, Madhusudan P (2018) Horn-ICE learning for synthesizing invariants and contracts. Proc ACM Program Lang 2(OOPSLA):131\u2013113125","DOI":"10.1145\/3276501"},{"key":"468_CR33","doi-asserted-by":"publisher","unstructured":"Sharma R, Nori AV, Aiken A (2012) Interpolants as classifiers. In: Madhusudan P, Seshia SA (eds) Computer aided verification\u201424th international conference, CAV 2012, proceedings. LNCS, vol 7358. Springer, pp 71\u201387. https:\/\/doi.org\/10.1007\/978-3-642-31424-7_11","DOI":"10.1007\/978-3-642-31424-7_11"},{"key":"468_CR34","doi-asserted-by":"publisher","unstructured":"Padhi S, Millstein TD, Nori AV, Sharma R (2019) Overfitting in synthesis: theory and practice. In: Computer aided verification\u201431st international conference, CAV 2019, proceedings, part I. Lecture notes in computer science, vol 11561, pp 315\u2013334. Springer. https:\/\/doi.org\/10.1007\/978-3-030-25540-4_17","DOI":"10.1007\/978-3-030-25540-4_17"},{"key":"468_CR35","unstructured":"Si X, Dai H, Raghothaman M, Naik M, Song L (2018) Learning loop invariants for program verification. In: Advances in neural information processing systems 31: annual conference on neural information processing systems 2018, NeurIPS 2018, pp 7762\u20137773"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-024-00468-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-024-00468-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-024-00468-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T16:54:09Z","timestamp":1762448049000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-024-00468-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,2,24]]},"references-count":35,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2025,11]]}},"alternative-id":["468"],"URL":"https:\/\/doi.org\/10.1007\/s10703-024-00468-9","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,2,24]]},"assertion":[{"value":"2 August 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"25 December 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 February 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"This work was supported by JSPS KAKENHI Grant Numbers JP20H05703, JP20H04162, and JP19K22842, and ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST. The authors have no other Conflict of interest to declare that are relevant to the content of this article.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}]}}