Learning Simple Interpolants for Linear Integer Arithmetic

Craig interpolation plays a central role in formal verification tasks such as model checking, invariant generation, and abstraction refinement. In the domain of linear integer arithmetic (LIA), interpolants are crucial for deriving inductive invariants that characterize unreachable or safe program states, enabling scalable and precise reasoning about software and hardware correctness. Despite progress in interpolation algorithms, generating concise and interpretable interpolants remains a key challenge. We propose a lightweight learning-based approach to generating simple interpolants for LIA. Our model learns to lazily sample input problems directly and is complementary to existing logical methods. We show that when Z3 is guided by our learned model, the complexity of the interpolants it produces can be reduced by up to 47.3%. For older solvers, the reduction rate can reach up to 69.1%.

Recent advancements in machine learning have shown promise in complementing formal methods by providing heuristics that guide complex decision-making processes. Despite this progress, the integration of learning-based techniques into the domain of LIA interpolation remains relatively unexplored. Existing interpolation procedures primarily rely on symbolic reasoning and decision procedures, which, while sound and complete, may not always yield the most concise interpolants [1].

In this work, we introduce a novel learning-based framework aimed at simplifying interpolants in LIA. Our approach leverages a lightweight neural architecture that combines a message-passing graph neural network (GNN) [40] with a self-attention-based [34] selector mechanism. The GNN encodes the structural and semantic information of disjunction-free LIA formulas, while the selector network tries to identify minimal subsets of the input formulas that are sufficient for generating valid interpolants. This design enables a single invocation of the satisfiability modulo theories (SMT) solver during the computation, enhancing efficiency and scalability.

To facilitate this learning process, we require a dataset of challenging interpolation problems for both training and evaluation. As no such dataset exists in the literature to our knowledge, we construct one comprising approximately 66,000 interpolation problems in LIA. The dataset is generated through a 39th Conference on Neural Information Processing Systems (NeurIPS 2025). systematic process that ensures realistic and practical coverage of problem instances. We hope it will serve as a valuable resource for advancing learning-based interpolation methods.

Empirical evaluations demonstrate the effectiveness of our approach. When integrated with state-ofthe-art interpolation solvers such as Z3 [9], our model achieves a reduction in interpolant complexity of up to 47.3%. When applied to older solvers, the reduction rate increases to 69.1%, demonstrating the potential of our method to significantly enhance existing tools.

Our contributions can be summarized as follows:

• We propose a novel learning-based approach that guides the generation of simpler interpolants in linear integer arithmetic, complementing traditional logic-based methods. Motivated by the demands of downstream verification workloads, our model architecture emphasizes both fast evaluation and high-quality interpolant generation.

• We introduce a dataset containing approximately 66,000 challenging interpolation problems in linear integer arithmetic. We detail the generation process to ensure reproducibility and coverage.

• We demonstrate that our approach effectively reduces interpolant complexity, achieving significant improvements when integrated with both modern and legacy interpolation solvers.

Craig interpolation is a foundational concept in logic and program verification, widely used in constructing inductive invariants and enabling efficient model checking. Given two logical formulas A and B such that their conjunction A ∧ B is unsatisfiable, a Craig interpolant is a formula I satisfying the following properties: