View in EDS

Towards neural-network-guided program synthesis and verification.

Saved in:
Bibliographic Details
Title: Towards neural-network-guided program synthesis and verification.
Authors: Kobayashi, Naoki1 (AUTHOR) koba@is.s.u-tokyo.ac.jp, Sekiyama, Taro2 (AUTHOR), Sato, Issei1 (AUTHOR), Unno, Hiroshi3 (AUTHOR)
Source: Formal Methods in System Design. Nov2025, Vol. 67 Issue 2, p222-254. 33p.
Subjects: Artificial neural networks, Computer software correctness, Model validation, Code generators, Predicate calculus, Constraint satisfaction
Abstract: We propose a novel framework of program and invariant synthesis called neural network-guided synthesis (NeuGuS). 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's program synthesis by sketching. [ABSTRACT FROM AUTHOR]
Copyright of Formal Methods in System Design is the property of Springer Nature and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
Database: Engineering Source
FullText Text:
  Availability: 0
Header DbId: egs
DbLabel: Engineering Source
An: 189134714
AccessLevel: 6
PubType: Academic Journal
PubTypeId: academicJournal
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: Towards neural-network-guided program synthesis and verification.
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22Kobayashi%2C+Naoki%22">Kobayashi, Naoki</searchLink><relatesTo>1</relatesTo> (AUTHOR)<i> koba@is.s.u-tokyo.ac.jp</i><br /><searchLink fieldCode="AR" term="%22Sekiyama%2C+Taro%22">Sekiyama, Taro</searchLink><relatesTo>2</relatesTo> (AUTHOR)<br /><searchLink fieldCode="AR" term="%22Sato%2C+Issei%22">Sato, Issei</searchLink><relatesTo>1</relatesTo> (AUTHOR)<br /><searchLink fieldCode="AR" term="%22Unno%2C+Hiroshi%22">Unno, Hiroshi</searchLink><relatesTo>3</relatesTo> (AUTHOR)
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22Formal+Methods+in+System+Design%22">Formal Methods in System Design</searchLink>. Nov2025, Vol. 67 Issue 2, p222-254. 33p.
– Name: Subject
  Label: Subjects
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22Artificial+neural+networks%22">Artificial neural networks</searchLink><br /><searchLink fieldCode="DE" term="%22Computer+software+correctness%22">Computer software correctness</searchLink><br /><searchLink fieldCode="DE" term="%22Model+validation%22">Model validation</searchLink><br /><searchLink fieldCode="DE" term="%22Code+generators%22">Code generators</searchLink><br /><searchLink fieldCode="DE" term="%22Predicate+calculus%22">Predicate calculus</searchLink><br /><searchLink fieldCode="DE" term="%22Constraint+satisfaction%22">Constraint satisfaction</searchLink>
– Name: Abstract
  Label: Abstract
  Group: Ab
  Data: We propose a novel framework of program and invariant synthesis called neural network-guided synthesis (NeuGuS). 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's program synthesis by sketching. [ABSTRACT FROM AUTHOR]
– Name: AbstractSuppliedCopyright
  Label:
  Group: Ab
  Data: <i>Copyright of Formal Methods in System Design is the property of Springer Nature and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract.</i> (Copyright applies to all Abstracts.)
PLink https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=189134714
RecordInfo BibRecord:
  BibEntity:
    Identifiers:
      – Type: doi
        Value: 10.1007/s10703-024-00468-9
    Languages:
      – Code: eng
        Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 33
        StartPage: 222
    Subjects:
      – SubjectFull: Artificial neural networks
        Type: general
      – SubjectFull: Computer software correctness
        Type: general
      – SubjectFull: Model validation
        Type: general
      – SubjectFull: Code generators
        Type: general
      – SubjectFull: Predicate calculus
        Type: general
      – SubjectFull: Constraint satisfaction
        Type: general
    Titles:
      – TitleFull: Towards neural-network-guided program synthesis and verification.
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: Kobayashi, Naoki
      – PersonEntity:
          Name:
            NameFull: Sekiyama, Taro
      – PersonEntity:
          Name:
            NameFull: Sato, Issei
      – PersonEntity:
          Name:
            NameFull: Unno, Hiroshi
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 01
              M: 11
              Text: Nov2025
              Type: published
              Y: 2025
          Identifiers:
            – Type: issn-print
              Value: 09259856
          Numbering:
            – Type: volume
              Value: 67
            – Type: issue
              Value: 2
          Titles:
            – TitleFull: Formal Methods in System Design
              Type: main
ResultId 1