Toward Neural-Network-Guided Program Synthesis and Verification
summary
Proposes NeuGuS, a gray-box method that trains neural nets (four-layer; sometimes three-layer) then extracts inequalities from weights/biases to build Boolean combinations; implements a tool that synthesizes linear and quadratic formulas from positive/negative examples and implication constraints, recovering all qualifiers for conjunctive shapes and >90% for others. Integrates with ICE-based CHC solver HoIce as NeuHoIce, and the extended system solves benchmark instances that plain HoIce and Spacer previously time out on.
AI-written summary · about
chapters (9)
- 0:00Intro
- 0:46Outline
- 1:24Extracting Formulas from NNs: Example
- 3:15Neural Network Guided Synthesis (NeuGus)
- 5:57Synthesis Problems for Experiments
- 6:59Why 3-Layer NNs Showed Good Performance?
- 10:32Generalized Synthesis Problem
- 13:45Related Work
- 14:28Conclusion • NeuGus: a grey box approach to NN-guided synthesis of logical formulas
related talks
24mReward-Guided Synthesis of Intelligent Agents with Control Structures
01h 04mInvited Talk: Finding Good Programs by Avoiding Bad Ones
16mImproving Oracle-Guided Inductive Synthesis by Efficient Question Selection
16mModel-Guided Synthesis for LTL over Finite Traces
21mTowards Neural Synthesis for SMT-Assisted Proof-Oriented Programming
15mCurrent Practices for Building LLM-Powered Reasoning Tools Are Ad Hoc—and We Can Do Better
18mMaking Logic a First-Class Citizen in Generative ML for Networking
29mSynthesis of dependable and self-driving communication networks