Formal Synthesis of Neural Craig Interpolant via Counterexample Guided Deep Learning

Craig interpolation is a practical and powerful approach in formal verification and logic synthesis. However, Craig interpolant synthesis for nonlinear theory is still a challenge. This paper proposes a novel approach for synthesizing nonlinear Craig interpolants that are expressed as feed-forward neural networks for the general quantifier-free theory of nonlinear arithmetic. The approach employs a CounterExample-Guided Inductive Synthesis (CEGIS) procedure, where a learner and a verifier interact to synthesize neural interpolants. The learner trains a candidate interpolant that satisfies the interpolant conditions over a set of sampled data, and the verifier either ensures the validity of the candidate interpolant or yields counterexamples, which are passed back to further guide the learner. Our approach leverages efficient supervised learning algorithm, while guaranteeing formal soundness via symbolic solvers. We implement the tool SyntheNI and evaluate its performance over a set of benchmarks. The experimental results demonstrate the effectiveness and efficiency of our approach.