Toward neural-network-guided program synthesis and verification

DOI10.1007/978-3-030-88806-0_12zbMATH Open1497.68114arXiv2103.09414OpenAlexW3210636085MaRDI QIDQ2145332FDOQ2145332

Naoki Kobayashi, Taro Sekiyama, Issei Sato, Hiroshi Unno

Publication date: 17 June 2022

Abstract: We propose a novel framework of program and invariant synthesis called neural network-guided synthesis. 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.

Full work available at URL: https://arxiv.org/abs/2103.09414

Recommendations

• Code2Inv: a deep learning framework for program verification
• Example Guided Synthesis of Linear Approximations for Neural Network Verification
• From program verification to program synthesis
• Learning abstractions for program synthesis
• Programmable program synthesis

Mathematics Subject Classification ID

Learning and adaptive systems in artificial intelligence (68T05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Cites Work

• Learning safe neural network controllers with barrier certificates
• SMT-based model checking for recursive programs
• Safety verification of deep neural networks
• Reluplex: an efficient SMT solver for verifying deep neural networks
• Horn Clause Solvers for Program Verification
• Overfitting in synthesis: theory and practice
• ICE-based refinement type discovery for higher-order functional programs

Cited In (6)

• Guiding an automated theorem prover with neural rewriting
• Code2Inv: a deep learning framework for program verification
• Title not available (Why is that?)
• Example Guided Synthesis of Linear Approximations for Neural Network Verification
• Challenging SMT solvers to verify neural networks
• Neural network-guided synthesis of recursive list functions

Uses Software

• Spacer
• Adam
• Reluplex
• nncontroller
• AI2
• CLN2INV

This page was built for publication: Toward neural-network-guided program synthesis and verification

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2145332)