Learning Simple Interpolants for Linear Integer Arithmetic
Authors: Minchao Wu
Naoki Kobayashi
Venue: NeurIPS 2025 poster ()
Keywords: Craig interpolation
Formal verification
Machine learning for logic
Linear integer arithmetic
Primary area: applications

Abstract: 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. 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%.

Learning Simple Interpolants for Linear Integer Arithmetic
Minchao Wu The University of Tokyo
Naoki Kobayashi The University of Tokyo koba@is s. u-tokyo..... ac. jp
minchaowag ecc. u-to.yo........... ac. jp
Abstract
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 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 lightweight learning-basse 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 produces can be reduced by up to 47.3%. For older solvers, the reduction rate can reach up 69.
Introduction
Craig interpolation is foundational technique in formal verification, instrumental in applications such as abstraction refinement, invariant generation, and compositional reasoning 20 14 21 22
[6
In the realm of linear integer arithmetic (LIA), interpolants serve as crucial intermediaries, connecting preconditions and postconditions within program verification frameworks. However, generating interpolants in LIA presents significant challenges due the discrete nature of integers and the complexity of associated arithmetic operations. Traditional methods often produce interpolants with large coefficients and intricate structures, which hinder the efficiency and scalability of verification tools.
15
23 33
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 [I].
In this work, we introduce novel learning-basse based framework aimed simplifying interpolants in LIA. Our approach leverages a lightweight neural architecture that combines message-passinn graph neural network (GNN) 40 with a self-attention-baas based [34 selector mechanism. The GNN encodes the structural and semantic information of disjunction-
LIA formulas, while the selector network tries to identify minimal subsets the input formulas that are sufficient for generating valid interpolants. This design enables 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 the literature 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 (NcurIPS 2025).

---

systematic process that ensures realistic and practical coverage of problem instances. We hope it will serve as a valuable resource for advancing learning-basee based interpolation methods.
Empirical evaluations demonstrate the effectiveness of our approach. When integrated with state-of- the-art interpolation solvers such 733 [9] our model achieves reduction in interpolant complexity of to 47.3%. When applied to older solvers, the reduction rate increases to 69.1 %, demonstrating the potential of our method significantly enhance existing tools.
Our contributions can be summarized as follows:
We propose a novel learning-based approach that guides the generation of simpler in- terpolants 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 dataset containing approximately 66,000 challenging interpolation problems in linear integer arithmetic. We detail the generation process 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.
2 Preliminaries
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 and B such that their conjunction A B unsatisfiable, a Craig interpolant is a formula satisfying the following properties:
A=1
2. 1= -B
3. VIrs(I) S. Vars(A) n Vars(B), where Vars(-) denotes the set of variables in a formula.
The existence of an interpolant is guaranteed by Craig's interpolation theorem for any two unsatisfiable (or disjoint) formulas A and B in LIA. In what follows, we refer to the complexity of a formula as the number of logical connectives it contains. Since our domain is integer arithmetic, negation is unnecessary and count only A and V.
As an example, consider the following formulas A and
A = (a 0 A 0) v (a = 1 = 2)=
(- 100 - y = 200)
One can verify that all of
= 0 A ( 1<<==
7 = r = 100 + y
y = 2x.
are interpolants between A and B.
2.1 Applications to Program Verification and Why Simple Interpolants Matter
In program verification, Craig interpolants often used to find invariant, which certifies that error states are unreachable. Let be a formula describing an approximation of states reachable from initial states, and B be formula describing an approximation of states reachable to error states, Then, an interpolant / between A and B serves as a candidate invariant.
The example interpolation problem above may be extracted from the following program.
x = 0; y = 0; while (*) {x++; y+=2} assert (x-100 => -020)):

---

The formula A - reachable within two iterations of the loop, and the formula B -2 100 = y 200) describes an error state. To prove that an error state is unreachable, we need to find an (inductive) invariant T such that = / and = -B, i.e., I is an interpolant between and B (with an additional condition that 7 is closed under the transition relation).
4) describes the states
In practice, the complexity of the interpolant I plays a crucial role as simplicity often leads to generality. A formula / being an interpolant between reachable states and error states is merely a necessary condition for I to be an inductive invariant I must additionally be closed under the transition relation - and that multiple interpolants can exist between the same pair of formulas. A simpler interpolant more likely to constitute true invariant, as less prone to overfitting to specific approximations A and B of reachable and error states. In the example above, both / and I2 are valid interpolants, but is not difficult to see that only I, the simplest of the three, is an inductive invariant of the program.
This is analogous to machine learning, where a simple model that captures the core pattern will generalize better than an overly complex one that overfits to training data. In the verification context, complex interpolant can "overfit" particular approximations of reachable and error states, whereas a concise interpolant focuses on the essential relationship and is less prone to depend on such approximations.
The importance of simple interpolants in program verification has been widely recognized. Albargh- outhi and McMillan [I] emphasized this point and empirically demonstrated that simpler interpolants can indeed improve the efficiency of verification.
2.2 Lazy Sampling Method
The lazy sampling method described in Albarghouthi and McMillan's 's compositional approach aims to generate simpler interpolants through compositional reasoning. It proceeds as follows:
1. Given an interpolation problem (A, B), the goal is construct an interpolant / satisfying the above conditions. Two initially empty sets, known as sample sets, are maintained for feasible disjuncts of A and B.
2. The algorithm lazily samples disjuncts from A and B using an SMT solver, and iteratively attempts to find simple interpolant 7 separating these samples.
3. If the candidate interpolant fails, additional disjuncts contradicting this interpolant are sampled and incorporated. The method then restarts with these newly updated sample sets, iteratively refining the interpolant.
As illustrative example, consider the following interpolation problem from
A = (a I < 3) v < B = (x 2 A 2 3) V (= 3322 < 3)
These formulas represent distinct convex regions two-dimensional space, and their conjunction A A B is unsatisfiable, as these regions do not intersect.
Applying the lazy sampling method, one might initially sample the disjunct (1 S x S 2 2) from A and (ar 2 ^ 3) from B. A candidate interpolant between the sets
SA (1 S < 2 S 2} SB f 22 3}
might be y < 2. However, since (x < 1 A y S 3) from A is a counterexample (because this interpolant fails the first condition A + I), this disjunct is subsequently sampled well. Now, considering the updated
S = (15 2 < 2, x (1ASS3) Sn= ( 22
a new valid interpolant + y < 4 between them may be found. In this case, the interpolant also successfully separates the original formulas A and B.
In practice, this fact is checked by SMT solver.
3

---

Note that the counterexample guided selection of new disjuncts does not guarantee simplicity. It is possible to end up with unnecessary disjuncts in the final sets S and Sp. especially when multiple disjuncts can serve as counterexamples simultaneously. In such cases, additional heuristics may be required to rank and prioritize the formulas.
3 Models
We now describe our approach to generating simple interpolants, following the lines described in Section 2.2] Since every LIA formula can converted to its disjunctive normal form, below we always treat an input formula of an interpolation problem as set (or sequence) of conjunctive formulas. Each formula in this set is referred as disjunct.
3.1 Motivation
naive way to improve upon the logical methods in Section 2.2 is to replace the counterexample- guided selection of formulas with learned heuristics. There are however major drawbacks with this approach. The first is that it would require multiple invocations of both the model and the SMT solver throughout the computation. This is because we essentially constructing the subsets of the two input formulas from the bottom up. Each time the SMT solver provides feedback on the validity of a candidate interpolant, the model is called to make prediction. A candidate is then composed, and the process is repeated. This becomes increasingly expensive as the input formulas grow larger. The second drawback is the lack of clear definition of ground truth in this setting. Given any timestep / and the selected subsets (SA), and (SB),. .. it is possible that no disjunct from the two input formulas, if added A) or (SB), will immediately yield valid interpolant between A and B. In such cases, no definitive signal can be provided to properly train the model.
A better way to achieve similar improvement is lazily sample the disjuncts in top-down manner. That is, we want the model to directly construct subsets SA C and SB C such that the interpolant between them is also valid interpolant between A and B. Once these subsets are identified, we only need to run the interpolation solver once on them.
This is a challenging task. Mathematically, any interpolant between A and B is also valid interpolant between any S C and SB C B. However, it is not generally true that there exist S C and SB C B such that any interpolant between them is valid interpolant between A and B.
In practice, lazily sampling a small number of disjuncts from A and often suffices to find an interpolant for A and B [[]. However, this heavily depends on the underlying mechanics of the interpolation solver. Given the same S C A and SB B, different solvers may produce different interpolants, and not all of them are necessarily valid interpolants for A and B.
This implies that ideal model will inevitably need to internalize certain aspects of the target solver's behavior. Modern SMT solvers such as Z3 have complex codebases and decades of carefully tuned optimizations. It would be fascinating if even a portion of such solver could be approximated by relatively small model.
We emphasize the importance of lightweight approach and intentionally avoid relying large language models (LLMs). This choice is motivated by the fact that both the speed and accuracy of interpolation solving are critical for downstream verification tasks.
To achieve this, we develop a model with two components: an encoder that learns representations of disjunction-free LIA formulas using a message- message-passing graph neural network, followed by an attention- based selector network that selects appropriate disjuncts from the original input formulas. The high-level computation flow is illustrated in Figure]] I
3.2 Encoding LIA Formulas
Given LIA formula, we first obtain its graph representation by converting it into the corresponding abstract syntax tree (AST). Each node in the formula graph is represented by a feature vector x, E R. where d = 1 d, 1 + 1, comprising:
A discrete node type indicator I; E {0,, 1,2) representing operators, variables, and constants, respectively

---

node Teatures
h
GNN
AST
formula embedding
edge
A
embedder
dil,
Norks
dity
B
embedder
posibonal
crcoddng
Figure Computation flow. The upper part illustrates the embedding process for single LIA
formula, as described in Sections 3.2 to 3.5 The lower part shows the disjunct selection mechanism, described in Section (36
A learnable token embedding vector e, R capturing semantic information
A depth value h, E N indicating the node's position in the formula tree
A raw value 82 E Z for constant nodes (zero-padded for non-constants)
LIA formula is thus represented by a set of node features along with the corresponding edge information, which then processed by message-passing graph neural network to compute feature embeddings.
We message-passing neural network architecture specifically designed to learn representations of integer arithmetic formulas. The model employs a hierarchical feature embedding scheme followed by multiple rounds of message passing to capture both local arithmetic constraints and the global structure of the formula.
3.3 Feature Embedding
The raw node features are transformed into latent representation through a multi-component embedding network:
type
Emb tpe (f:) TBd../1
2 token
Lookeenn (e:) E 12da/2
2 MLP (hi) E I d2d//8
depth
z poluc
MLP value (v:) dd
where d, is the hidden dimension. These embeddings are concatenated and passed through a feature combination network:
LayerNorm (MLP PelPPoomll (lz (z,ure, ;z," token, depth galucl)
z
The resulting node embeddings are then refined through multiple rounds message passing: each round, message is computed for every edge based on the concatenation of the source and target node embeddings, passed through a multi-layer perceptron (MIP),, and then aggregated additively at the target node.

---

3.4 Message Passing
Our message passing scheme iteratively updates node representations over L layers. At each layer 4, the message function M and update function ( are defined as:
M (h.
.n = MLP
:h I)
m;
meg
E
(1)
a,
m.
(3)
(EN(()
h (+1) (h a (())))) LayerNorm(hh MLP
upd (apa(ll (ah"":a"")))
where (i) denotes the neighbors of node in the formula graph. Residual connections and layer normalization are applied at each layer to stabilize training.
3.5 Lereula-Level Representation
After the message-passe paassengggnnggggg phase, node embeddings are aggregated into single graph-level vector. Specifically, we compute the final latent representation for the formula using the node embeddings in its AST. The final graph representation obtained by combining global mean and sum pooling operations:
g = (eannpool ((b. (,) sumpool( ((h; (b))
(4)
followed by final transformation:
ML.Pourg)
(5)
This architecture explicitly captures both local arithmetic relationships through message passing and global formula structure through hierarchical embedding and pooling mechanisms. The resulting formula-level embedding is then ready for downstream tasks, including- sampling method for interpolation solving. The process of encoding a (disjunction-free) LIA formula and computing its latent representation illustrated in the upper part of Figure]
not limited to-our lazy
3.6 Selector Network
By the nature of interpolation solving, the two input formulas must be interdependent when deciding whether a particular disjunct necessary. Each disjunct A should aware every disjunct B, and vice versa, in order to compute valid interpolant. Moreover, since are particularly interested identifying redundancy within the input formulas, each formula A (respectively, in B) should also attend other formulas within A (or B). For this reason, employ self-attention rather than cross-attention the selector network.
Given the two sequences of embeddings for formulas in A and B computed by the GNN, we first concatenate them obtain a matrix of formula emheddings X E IR-xxd where N is the total number of formulas in A U B, and d is the embedding dimension.
To preserve set membership information, each embedding in X is augmented with learnable posi- tional encoding. Specifically, a trainable vector e E Rd is added to all embeddings corresponding formulas in set A, and a separate vector ep [Rd is added those from B. This produces set-aware input embeddings:
e
if set_ids,, = (indicating set A) e if set_ids;j = 1 (indicating set B)
X X +++E E,
where E.
This enriched input X is passed through a series of self-attention and feedforward blocks, enabling each disjunct to attend all others in the combined input. In particular, self-attention computes

---

attention weights d; that quantify the influence of formula j on formula i, allowing the model to reason about interdependencies and relative importance across A U B.This is especially valuable when certain formulas are redundant or contextually less informative. The combination of set-aware encoding and self-attention allows the selector to make globally informed decisions about which disjuncts are most relevant in context.
The resulting tensor is then passed through feedforward scoring head, which projects each formula embedding to scalar score used to rank disjuncts from the input formulas.
4 Experiments
4.1 Dataset
To demonstrate the effectiveness of our approach, we require a dataset of challenging interpolation problems for both training and evaluation. As no such dataset exists in the literature our knowledge. we construct one ourselves and describe the generation process in detail.
We begin by creating bank of disjunction-fres free LIA formulas that as the "atomic" components of our dataset. This done by running an existing software verification tool on real downstream tasks (e.g.. functional program verification), where interpolation solving is used subroutine We then extract the execution traces of the interpolation solver and collect all disjunction-free LIA formulas and subformulas that occur in these traces.
We then scan the entire formula bank and construct dictionary D, where each formula serves as key, and its value is list of formulas that are all disjoint from the key. Given sequence of disjunction-fiee formulas p1..... Pnn it is not difficult to verify that
n V+ 9: B #==N Pipi]
forms valid interpolation problem, provided that N D[p.] is nonempty.
To ensure variety in the dataset, we must randomly access different combinations of keys in D. How- ever, when D is large, enumerating all combinations and then sampling from them is computationally infeasible. Instead, we randomly sample an index e and compute the c-th combination directly. We omit the implementation details of this procedure here.
The generation of the dataset is controlled by two parameters, Ci and C2, denoting the maximum length of A and B, respectively. Problems where either A or B is a singleton are excluded to ensure sufficient complexity. We denote the resulting dataset Interp(ei, Cg). In the experiments that follow, we primarily use Interp (4, 4).
Although we use relatively small values of and c2 due to computational constraints, Interp (4 4) already contains challenging problems for state-of-the-ar interpolation solvers. This is partly because place restriction the internal complexity of the disjuncts in the input formulas- onlu their count. Table I summarizes statistics for Interp(4. (4 4). The full dataset is split into training and testing sets using 80%-20% ratio.
Table 1: Dataset Statistics
Statistic
Value
Description
Number of problems
65,981
Total number of data points Highest observed formula complexity Average over all input formulas Absolute value range of constants Variable names and operators only
Maximum complexity
31
Average complexity
9
Constant range
0-112
Vocabulary size
355
For this paper, use model checker called MoCHi 19 its test benchmarks.
7

---

4.2 Ground Truths and Hy Hyperparameters
To generate ground truths, we compute interpolants between all pairs (SA, SB) such that SA P(A) and SB E PBB). using target solver (e.g., Z3). A pair (SA, SB) B is considered candidate if the interpolant between SA and SB is also valid for the original formulas and B. Among all valid candidates, the shortest pair (in terms of set size) is selected as the ground truth.
In practice, observe that many problems admit multiple valid ground truths. Randomly selecting one can introduce noise and hinder model training. To provide more deterministic supervision, we apply two additional criteria to select among the candidates:
(SA. SB) has the fewest total tokens among all valid candidates.
TThe sum of the absolute values of constants occurring in (Sa, SB) is minimal.
In the experiments below, fix the token embedding dimension to 16 and the formula embedding dimension to 32. The hidden feature size of both the GNN encoder and the selector network is set to 128. We use 4 heads in the multi-head attention mechanism. The parameters of the graph encoder, selector network, and token embedding layer are jointly trained with a batch size of 256 using the Adam optimizer [18] for 300 epochs.
The learning rate initially set to 1e-3 and is reduced by a factor of 0.5 every 50 epochs. Training is performed using PyTorch's 's Metal backend 227 2 and takes approximately 1.5 days on a single MacBook Pro with the MI MAX chip.
4.3 Improving Interpolants Found by Z3
We begin by evaluating the improvements our model brings to Z3 in terms of interpolant complexity. Although Z3 is already highly optimized and capable of producing concise interpolants for many problems in our dataset, it does not always yield the simplest solution. To better illustrate the benefit of our approach, we focus on the subset of test problems that are challenging for Z3. We define a problem as challenging if there exists an interpolant whose complexity is at least two units lower than that of the one produced by 73 F This results subset of 532 such problems from the test set. Table 2 presents comparison between the original 73 and 73 guided by our model.
Table 2: Performance Gain. Numbers are averaged over valid solutions.
Methods
Valid
Complexity
Length
Z3 Time (s)
Original Z3 Z3 guided by model
100%
5.38
186.7
0.012 0.009
72.9%
2.83
108.6
As shown in Table 2 the complexity of the interpolants produced by Z3 is reduced by 47.3% when guided by our model, result further supported by the corresponding reduction in plain-text length. The execution time of Z3 is also reduced by 30% under model guidance.
The 72.9% success rate may appear suboptimal, but this is not significant limitation in practice- one can simply fall back to the original solver in cases of failure. While this fallback mechanism introduces small overhead due model invocation (averaging 20ms in our experiments), the overall impact on performance remains modest.
Importantly, the improvement in interpolant quality can have substantial downstream benefits: a better interpolant can often enable verification tasks to succeed that would otherwise time out completely.
4.4 Reviving an Older Solver
As discussed in Section 3.1 the effectiveness of lazy sampling is solver-dependent. Given an interpolation problem B), the sampled subsets (SA. SB) that work for Z3 may not generalize to other solvers. In this section, we evaluate how well the trained model transfers to different solver. Specifically, we experiment with an interpolation solver called CSIsat 44, an older tool whose interpolants on our test problems have an average complexity of 1 11.5. We assess the performance of
This definition is independent of the model's predictions.
8

---

both Z3 and CSIsat when guided by models trained using their respective ground truths, as well as when guided by "exotic" ground truths ie.. ground truths generated for the other solver.
Table 3: Performance of Solvers Guided by Different Models on All Test Problems
Model
trained with Z3 ground truths
trained with CSIsat ground truths
Valid
Complexity
Solver Time (s)
Valid
Complexity
Solver Time (s)
73
74.2%
2.84
0.009
52.7%
2.23
0.011 0.007
CSlsat
59.2%
5.13
0.007
73.7%
3.57
As shown in Table we observe roughly symmetric pattern in success rates. Both solvers manage to achieve around 55% % validity when guided by a model trained on exotic ground truths. This suggests that the model captures and transfers some of the underlying interpolation heuristics shared between Z3 and CSIsat.
However, each solver performs significantly better when guided by the model trained specifically for it. This indicates that the dedicated models have acquired solver-specific knowledge during training. Interestingly, when Z3 is guided by the model trained CSIsat ground truths, the resulting interpolants appear slightly simpler (in terms of complexity) than those generated using the dedicated Z3 model. We do not overinterpret this effect, as it is likely due to the complexity being averaged over a smaller subset of valid solutions.
Lastly, we note that the complexity of the interpolants produced by CSIsat is significantly reduced when guided by either model-by up to 69.1%. This demonstrates that we can elevate CSIsat's performance to modern standard without modifying its legacy codebase.
Such capability is particularly valuable in scenarios where alternative interpolants are sought for difficult problems in downstream verification tasks. In this role, the revived CSIsat can now serve as a practical and efficient tool.
Related Work
Craig Interpolation in Integer Arithmetic Craig interpolation has been extensively studied in the context of formal verification, particularly for generating intermediate assertions safety analysis and model checking. Cimatti et al. [6] provides comprehensive overview of efficient interpolation procedures for satisfiability modulo theories (SMT). Compositional methods [ have proven especially effective for producing high-qualit
interpolants. Although learning- based methods for LIA interpolation remains relatively unexplored, traditional statistical machine learning techniques, such Support Vector Machines (SVMs) [8] have been applied to the problem of finding half-space interpolants 311. However, such approaches are typically incomplete when the interpolation problem not linearly separable.
Learning-Basse Bassd Methods in Theorem Proving The integration of machine learning into automated theorem proving has gained significant traction in recent years. Deep learning has been widely explored in the context of traditional automated theorem proving (ATP), including SAT solving 30 29 36 5 [2]. In contrast to SAT solving, interpolation in LIA involves richer logical language
and requires more sophisticated encoding. While a SAT solution consists cither a satisfying truth assignment or proof of unsatisfiability, interpolant is an arbitrary formula within the underlying theory. This additional expressiveness presents unique challenges for applying learning- techniques.
In the field of interactive theorem proving (ITP) with proof assistants such as Lean [00 Isabelle (66
and Coq [7]. large language models (LLMs) have been extensively used for tasks such as autofor-
malization 37 25
28 proof sketching [7 [ 32, tactic generation [13 17 35 and premise
selection 24 38 While LLMs are powerful at suggesting formulas, they tend to be slow and
imprecise when comes to symbolic reasoning, making them less suitable for our task, which requires efficient and accurate interpolation.

---

Limitations
Characterization of Complexity. In this paper, we primarily characterize the complexity of a linear arithmetic formula by the number of its logical connectives. This metric captures one of the most intuitive and relevant aspects of interpolant simplicity. However, complexity is inherently multi-dimensional. For instance, the magnitude of constants appearing an interpolant also plays an important role, as large constants can introduce difficulties in downstream verification tasks. Similarly, the number of variables provides another useful perspective: fewer connectives suggest less redundant "regional" information, while fewer variables imply less redundant "dimensional" information. Depending on the downstream application, an interpolant with more connectives but fewer variables may in fact be preferable.
We have incorporated some of this intuition into the design of the deterministic selection criteria described in Section 4.2 Nonetheless, future work could explore dedicated learning-based heuristics better capture and optimize for these other dimensions of interpolant complexity.
Applications and Separated Learning. Although our model-guided interpolation solvers can produce significantly simpler interpolants, the benefits do not always translate directly to downstream applications. Many verification tools invoke interpolation as a subroutine and may pre-process or decompose complex problems into simpler ones, resulting in trivial interpolation queries. In such cases, our approach offers limited advantage over standard interpolation solvers.
Moreover, interpolants of the same syntactic complexity can yield vastly different outcomes in downstream tasks, depending on the nature of the application and the behavior of the overarching ("master") solver. If the objective is to produce interpolants that more effective for specific downstream task, then the training process must incorporate feedback from that task. This would allow the model to internalize the task-specific heuristics and interaction patterns of the broader verification pipeline.
Conclusion
In this work, we introduced a lightweight learning- based framework for simplifying Craig interpolants in linear integer arithmetic (LIA). Our approach combines message-passinne graph neural network selector network to directly identify minimal subsets of input
(GNN) with a self-attention-basee formulas sufficient to produce valid interpolants. This design complements existing logical techniques and enables improvements over both modern and legacy interpolation solvers solvers-withon modifying their underlying implementations.
Empirical evaluations demonstrate the effectiveness of our approach. When integrated with Z3, state-of-the-art SMT solver, our model reduces interpolant complexity by up to 47.3%. When applied to older solvers, the reduction increases to 69.1 1%, highlighting the method's potential substantially enhance existing tools.
Because our method does not rely on linearity, promising direction for future work its extension to richer domains such as non-linear integer arithmetic or array theories. Additionally, integrating our framework into downstream masks-such as invariant synthesis termination analysis- -assi further demonstrate its generality and practical value.
Acknowledgments
This work was supported by JSPS KAKENHI Grant Number JP20H05703. We thank the anonymous reviewers for their insightful comments and suggestions. We thank Ryosuke Sato for adapting MoCHi for this project.
References
[1] Aws Albarghouthi and Kenneth L. McMillan. Beautiful interpolants. In Natasha Sharygina and Helmut Veith, editors, Computer Aided Verification, pages 313-329, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg.
10

---

[2] Apple. Accelerated pytorch training on mac. https::/ddveloperr apple. com com/metal/ pytorch/ 2025. Accessed: 2025-05-15.
[3] Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt. Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar. cvc5; A versatile and industrial-strennth smt solver. In Dana Fisman and Grigore Rosu, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 415 442, Cham, 2022. Springer International Publishing.
[4] Dirk Beyer, Damien Zufferey, and Rupak Majumdar. Csisat: Interpolation for la+euf. In Aarti Gupta and Sharad Malik, editors, Computer Aided Verification, pages 304-308, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg.
[5] Chris Cameron, Rex Chen, Jason Hartford, and Kevin Leyton-Brown. Predicting proposi- tional satisfiability via end-to-end learning. Proceedings of the AAAI Conference on Artificial Intelligence, 34(04):3324 -3331, Apr. 2020.
[6] Alessandro Cimatti, Alberto Griggio, and Roberto Sebastiani. Efficient generation of craig interpolants in satisfiability modulo theories, 2009.
[7] Coq Development Team. The Coq proof assistant reference manual, 2004. Version 8.0.
[8] Corinna Cortes and Vladimir Vapnik. Support- networks. Machine learning, 20(3):273- 297, 1995.
[9] Leonardo de Moura and Nikolaj Bjømer. Z3: An efficient SMT solver. In C. R. Ramakrishnan and Jakob Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 337-340, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg.
[10] Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doomn and Jakob von Raumer. The Lean theorem prover (system description). In Amy P. Felty and Aart Middeldorp. edi- tors, Automated Deduction CADE-25, pages 378-388, Cham, 2015. Springer International Publishing.
[11] Emily First, Markus N Rabe, Talia Ringer, and Yuriy Brun. Baldur: Whole-proof generation and repair with large language models. In Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, pages 1229-1241, 2023.
[12] Mohamed Ghanem, Frederik Schmitt, Julian Siber, and Bernd Finkbeiner. Learning better representations from less data for propositional satisfiability. In The Thirty-eighth Annual Conference Neural Information Processing Systems, 2024.
[13] Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W Ayers, and Stanislas Polu. Proof artifact co-training for theorem proving with language models. arXiv preprint arXiv:2102.06203, 2021.
[14] Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Kenneth I.. McMillan. Abstractions from proofs. In Neil Jones and Xavier Leroy, editors, Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium Principles of Programming Languages, POPL 2004, Venice, Italy, January 14-16, 2004, pages 232-244. ACM, 2004.
[15] Ranjit Jhala, Rupak Majumdar, and Ru-Gang Xu. State of the union: Type inference via craig interpolation. In Orna Grumberg and Michael Huth, editors, Tools and Algorithms for the Construction and Analysis of Systems, 13th International Conference, TACAS 2007, Held as Part of the Joint European Conferencer on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24 April 1, 2007, Proceedings, volume 4424 of Lecture Notes in Computer Science pages 553-567. Springer, 2007.
[16) Ranjit Jhala and Kenneth L.. McMillan. Interpolant-based transition relation approximation. Log. Methods Comput. Sci., 3(4), 2007.

---

[17] Albert Q Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, and Guillaume Lample. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. arXiv preprint arXiv:2210. /2283,, 2022.
[18] Diederik P Kingma. Adam: A method for stochastic optimization. arXiv preprint arXiv:1412.6980, 2014.
[19] Naoki Kobayashi, Ryosuke Sato, and Hiroshi Unno. Predicate abstraction and cegar for higher- order model checking. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI 11, page 223-233, New York, NY, USA, 2011. Association for Computing Machinery.
[20] Kenneth L. McMillan. Interpolation and sat-based model checking. Warren A. Hunt Jr. and Fabio Somenzi, editors, Computer Aided Verification, 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings, volume 2725 of Lecture Notes in Computer Science, pages 1-13. Springer, 2003.
[21] Kenneth L. McMillan. An interpolating theorem prover. Theor. Comput. Sci., 345(1):101-121, 2005.
[22] Kenneth L. McMillan. Lazy abstraction with interpolants. In Thomas Ball and Robert B. Jones, editors, Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, volume 4144 of Lecture Notes in Computer Science, pages 123-136. Springer, 2006.
[23] Kenneth L.. McMillan. Quantified invariant generation using an interpolating saturation prover. In C. R. Ramakrishnan and Jakob Rehof, editors, Tools and Algorithmss for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, volume 4963 of Lecture Notes in Computer Science, pages 413-427. Springer, 2008
[24] Maciej Mikula, Szymon Tworkowski, Szymon Antoniak, Bartosz Piotrowski, Albert Q. Jiang, Jin Peng Zhou, Christian Szegedy, Lukasz Kucińisii, Piotr Milos, and Yuhuai Wu. Mag- nushammer:
transformer-based approach to premise selection. The Twelfth International Conference Learning Representations, 2024.
[25] Logan Murphy, Kaiyu Yang. Jialiang Sun, Zhaoyu Li, Anima Anandkumar, and Xujie Si. Autoformalizing euclidean geometry, 2024.
[26] Tobias Nipkow, Lawrence C Paulson, and Markus Wenzel. Isabelle/HOL: proof assistant for higher-order logic, volume 2283. Springer Science Business Media, 2002.
[27] Adam Paszke, Sam Gross, Francisco Massa, Adam Lerer, James Bradbury, Gregory Chanan, Trevor Killeen, Zeming Lin, Natalia Gimelshein, Luca Antiga, Alban Desmaison, Andreas Kopf, Edward Yang, Zachary Vitooo, Martin Raison, Alykhan Tejani, Sasank Chilamkurthy, Benoit Steiner, Lu Fang. Junjie Bai, and Soumith Chintala. Pytorch: An imperative style, high-performance deep learning library. In Advances in Neural Information Processing Systems 32, pages 8024-8035. Curran Associates, Inc., 2019.
[28] Auguste Poiroux, Gail Weiss, Viktor Kunčak, and Antoine Bosselut. Improving autoformaliza- tion using type checking, 2025.
[29] Daniel Selsam and Nikolaj Bjørner. Guiding perf-peerormance sat solvers with unsat-core predictions. In Mikoláš Janota and InOs Lynce, editors, Theory and Applications of Satisfiability Testing SAT 2019, pages 353, Cham, 2019. Springer International Publishing.
[30] Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo de Moura, and David L Dill. Learning sat solver from single-bit supervision. arXiv preprint arXiv:1802.088: 2018.
[31] Rahul Sharma, Aditya V. Nori, and Alex Aiken. Interpolants as classifiers. In P. Madhusudan and Sanjit A. Seshia, editors, Computer Aided Verification, pages 71-87, Berlin, Heidelberg, 2012. Springer Berlin Heidelberg.
12

---

[32] Trieu H Trinh, Yuhuai Wu, Quoe V Le, He He, and Thang Luong. Solving olympiad geometry without human demonstrations, Nature, 62577995):476-482, 2024.
[33] Hiroshi Unno and Naoki Kobayashi. Dependent type inference with interpolants. António Porto and Francisco Javier López-Frrauuas, editors, Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, September 7-9,
2009, Coimbra, Portugal, pages 277-288. ACM, 2009.
[34] Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, Lukasz Kaiser, and Illia Polosukhin. Attention is all you need. Advances in neural information processing systems, 30, 2017.
[35] Haiming Wang, Huajian Xin, Chuanyang Zheng, Lin Li, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, et al. Lego-pun prover: Neural theorem proving with growing libraries. arXiv preprint arXiv:3310000666, 2023.
[36] Wenxi Wang, Yang Hu, Mohit Tiwari, Sarfraz Khurshid, Kenneth McMillan, and Risto Miikku- lainen. Neuroback: Improving CDCL SAT solving using graph neural networks. In The Twelfth International Conference on Learning Representations, 2024.
[37] Yuhuai Wu, Albert Qiaochu Jiang. Wenda Li, Markus Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models. Advances in Neural Information Processing Systems, 35:32353-32368, 2022.
[38] Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J Prenger, and Animashree Anandkumar. Leandojo: Theorem proving with retrieval-augmented language models. Advances in Neural Information Processing Systems, 36:21573-21612, 2023.
[39] Lan Zhang, Xin Quan, and Andre Freitas. Consistent autoformalization for constructing mathematical libraries. In Yaser Al-Onaizan, Mohit Bansal, and Yun-Nung Chen, editors, Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing, pages 4020-4033, Miami, Florida, USA, November 2024. Association for Computational Linguistics.
[40] Jie Zhou, Ganqu Cui, Shengding Hu, Zhengyan Zhang, Cheng Yang, Zhiyuan Liu, Lifeng Wang, Changcheng Li, and Maosong Sun. Graph neural networks: A review of methods and applications. Al open, 1:57-81, 2020.
13

---

NeurIPS Paper Checklist
1. Claims
Question: Do the main claims made in the abstract and introduction accurately reflect the paper's contributions and scope?
Answer: [Yes]
Justification: We base our claims on the experimental results. As for the dataset, conducted an extensive search on the internet but were unable to find any that are suitable for training and evaluating learning-based approaches interpolation solving.
Guidelines:
The answer NA means that the abstract and introduction do not include the claims made the paper.
The abstract and/or introduction should clearly state the claims made, including the contributions made in the paper and important assumptions and limitations. A No NA answer to this question will not be perceived well by the reviewers.
The claims made should match theoretical and experimental results, and reflect how much the results can be expected to generalize to other settings.
is fine to include aspirational goals as motivation as long as is clear that these goals not attained by the paper.
2. Limitations
Question: Does the paper discuss the limitations of the work performed by the authors?
Answer: [Yes]
Justification: Please see Section Guidelines:
The answer NA means that the paper has limitation while the answer No means that the paper has limitations, but those are not discussed in the paper.
The authors are encouraged to create separate "Limitations" section in their paper.
The paper should point out any strong assumptions and how robust the results are to violations of these assumptions (c.g.. independence assumptions, noiseless settings, model cell-specification. asymptotic approximations only holding locally). The authors should reflect on how these assumptions might be violated in practice and what the implications would be.
The authors should reflect on the scope of the claims made, e.g. if the approach was only tested on few datasets or with few runs. In general, empirical results often depend on implicit assumptions, which should be articulated.
The authors should reflect on the factors that influence the performance of the approach. For example, facial recognition algorithm may perform poorly when image resolution low or images are taken in low lighting. Or speech-to-tex, system might not be used reliably to provide closed captions for online lectures because it fails handle technical jargon.
The authors should discuss the computational efficiency of the proposed algorithms and how they scale with dataset size.
If applicable, the authors should discuss possible limitations of their approach to address problems of privacy and faimesss.
While the authors might fear that complete honesty about limitations might be used by reviewers as grounds for rejection, a worse outcome might be that reviewers discover limitations that aren't 't acknowledged in the paper. The authors should use their best judgment and recognize that individual actions in favor of transparency play an impor- tant role in developing norms that preserve the integrity of the community, Reviewers will be specifically instructed to not penalize honesty concerning limitations.
3. Theory assumptions and proofs
Question: For each theoretical result, does the paper provide the full set of assumptions and complete (and correct) proof?
14

---

Answer: [NA]
Justification:
The paper does not include theoretical results.
Guidelines:
The answer NA means that the paper does not include theoretical results.
All the theorems, formulas, and proofs in the paper should be numbered and cross- referenced.
All assumptions should be clearly stated or referenced in the statement of any theorems.
The proofs can either appear in the main paper or the supplemental material, but if they appear in the supplemental material, the authors are encouraged to provide a short proof sketch provide intuition.
Inversely, any informal proof provided in the core of the paper should complemented by formal proofs provided in appendix or supplemental material.
Theorems and Lemmas that the proof relies upon should be properly referenced.
4. Experimental result reproducibility
Does the paper fully disclose all the information needed to reproduce the main ex- perimental results the paper to the extent that affects the main claims and/or conclusions of the paper (regardless of whether the code and data are provided not)?
Question:
Answer: [Yes]
Justification: We described the architecture of our models in Section We detailed all our experimental setups in the Section
Guidelines:
The answer NA means that the paper does not include experiments.
If the paper includes experiments, a No answer to this question will not be perceived well by the reviewers: Making the paper reproducible is important, regardless of whether the code and data are provided or not.
If the contribution is dataset and/or model, the authors should describe the steps taken to make their results reproducible or verifiable.
Depending on the contribution, reproducibility can be accomplished in various ways. For example, if the contribution is a novel architecture, descríbing the architecture fully might suffice, or if the contribution is specific model and empirical evaluation, it may be necessary to either make possible for others to replicate the model with the same dataset, provide access to the model. In general. releasing code and data is often one good way to accomplish this, but reproducibility can also be provided via detailed instructions for how to replicate the results, access to a hosted model (e.g.. g., in the case of a large language model), releasing of a model checkpoint, or other means that are appropriate to the research performed.
While NeurIPS does not require releasing code, the conference does require all submis- sions to provide some reasonable avenue for reproducibility, which may depend on the nature of the contribution. For example
(a) the contribution is primarily a new algorithm, the paper should make clear how reproduce that algorithm. (b) If the contribution is primarily new model architecture, the paper should describe the architecture clearly and fully.
(c) the contribution is new model (e-g., a large language model), then there should either be way to access this model for reproducing the results or way to reproduce the model (e.g., with an open-source dataset or instructions for how to construct the dataset).
(d) We recognize that reproducibility may be tricky in some cases, in which case authors are welcome describe the particular way they provide for reproducibility. In the case of closed-source models, it may be that access to the model is limited in some way (e.g., to registered users), but it should possible for other researchers to have some path to reproducing verifying the results.
5. Open access to data and code
15

---

Question: Does the paper provide open access to the data and code, with sufficient instruc- tions faithfully reproduce the main experimental results, as described in supplemental material?
Answer: [Yes]
Justification:
The code and datasets will be available at https://githut. cow/hopw/
scilia The dataset generation process is fully documented in Section 4. Others should also able to generate their own dataset if interested.
Guidelines:
The answer NA means that paper does not include experiments requiring code.
Please see the NeurlPS code and data submission guidelines (https://niis..c.
for more details.
While we encourage the release of code and data, we understand that this might not be possible, so "No" an acceptable answer. Papers cannot be rejected simply for not including code, unless this is central to the contribution (e.g., for new open-source benchmark).
The instructions should contain the exact command and environment needed to run to reproduce the results. See the NeurlPS code and data submission guidelines (https
Poiolliiccyyp for more details.
The authors should provide instructions on data access and preparation, including how to access the raw data, preprocessed data, intermediate data, and generated data, etc.
The authors should provide scripts to reproduce all experimental results for the new proposed method and baselines. If only subset of experiments are reproducible, they should state which ones are omitted from the script and why.
At submission time, to preserve anonymity, the authors should release anonymized versions (if applicable).
Providing much information possible in supplemental material (appended to the paper) recommended, but including URLs to data and code permitted.
6. Experimental setting/details
Question: Does the paper specify all the training and test details (e.g., data splits, hyper- parameters, how they were chosen, type of optimizer, etc.) necessary to understand the results?
Answer: [Yes]
Justification:
We detailed all our experimental setups in the Section $
Guidelines:
The answer NA means that the paper does not include experiments.
The experimental setting should be presented the core the paper to level of detail that is necessary to appreciate the results and make sense of them.
The full details can be provided either with the code, in appendix, as supplemental material.
7. Experiment statistical significance
Question: Does the paper report error bars suitably and correctly defined or other appropriate information about the statistical significance of the experiments?
Answer: [No]
Justification: Errors bars reported due computational budget.
Guidelines:
The answer NA means that the paper does not include experiments.
The authors should answer "Yes" if the results are accompanied by error bars, confi- dence intervals, or statistical significance tests, least for the experiments that support the main claims of the paper.
The factors of variability that the error bars are capturing should be clearly stated (for example, train/test split, initialization, random drawing of some parameter, or overall with given experimental conditions).
16

---

The method for calculating the error bars should be explained (closed form formula, call a library function, bootstrap, etc.)
The assumptions made should be given (e.g., Normally distributed errors).
It should be clear whether the error bar is the standard deviation or the standard error of the mean.
is OK to report 1-sigma error bars, but one should state it. The authors should preferably report a 2-sigma enror bar than state that they have 96% CI, if the hypothesis of Normality of errors is not verified.
For asymmetric distributions, the authors should be careful not to show in tables or figures symmetric error bars that would yield results that are range (e.g. negative enror rates).
If error bars reported in tables plots, The authors should explain in the text how they were calculated and reference the corresponding figures or tables the text.
8. Experiments compute resources
For each experiment, does the paper provide sufficient information on the com- puter resources (type of compute workers, memory, time of execution) needed reproduce the experiments?
Question:
Answer: [Yes]
Justification:
The resources needed are included in Section
Guidelines:
The answer NA means that the paper does not include experiments.
The paper should indicate the type of compute workers CPU or GPU, internal cluster, cloud provider, including relevant memory and storage.
The paper should provide the amount of compute required for each of the individual experimental runs well estimate the total compute.
The paper should disclose whether the full research project required more compute than the experiments reported in the paper (e.g., preliminary or failed experiments that didn't make into the paper).
9. Code of ethics
Question: Does the research conducted in the paper conform, in every respect, with the NeurIPS Code of Ethics htttps:/nneurips.com http://aaarr....c.oaaaa//cccccea
Answer: [Yes]
Justification: No harms were caused by the research process. We do not expect harmful consequences from the integer arithmetic problems considered in this work.
Guidelines:
The answer NA means that the authors have not reviewed the NeurIPS Code of Ethics.
If the authors answer No, they should explain the special cireumstances that require deviation from the Code of Ethics.
The authors should make sure to preserve anonymity (e.g.. if there is special consid- eration due to laws or regulations their jurisdiction).
10. Broader impacts
Question: Does the paper discuss both potential positive societal impacts and negative societal impacts of the work performed?
Answer: [NA]
Justification: As discussed throughout the paper, interpolation solving primarily supports downstream verification tasks and does have direct societal impact.
Guidelines:
The answer NA means that there no societal impact of the work performed.
If the authors answer NA or No, they should explain why their work has no societal impact why the paper does not address societal impact.
17

---

Examples of negative societal impacts include potential malicious unintended uses (e.g., disinformation, generating fake profiles, surveillance), faireess considerations (e.g., deployment of technologies that could make decisions that unfairly impact specific groups), privacy considerations, and security considerations.
The conference expects that many papers will be foundational research and not tied to particular applications, let alone deployments. However, if there is direct path to any negative applications, the authors should point it out. For example, it is legitimate to point out that an improvement in the quality of generative models could be used to generate deepfakes for disinformation. On the other hand, it is not needed to point out that a generic algorithm for optimizing neural networks could enable people to train models that generate Deepfakes faster.
The authors should consider possible harms that could arise when the technology is being used as intended and functioning correctly, harms that could arise when the technology is being used as intended but gives incorrect results, and harms following from (intentional unintentional) misuse of the technology.
If there are negative societal impacts, the authors could also discuss possible mitigation strategies (e.g., gated release of models, providing defenses in addition to attacks, mechanisms for monitoring misuse, mechanisms to monitor how a system learns from feedback over time, improving the efficiency and accessibility of ML).
11. Safeguards
Does the paper describe safeguards that have been put in place for responsible release of data models that have high risk for misuse (e.g., pretrained language models, image generators, or scraped datasets)?
Question:
Answer: [NA]
Justification: Our paper poses such risks.
Guidelines:
The answer NA means that the paper poses no such risks.
Released models that have high risk for misuse or dual-use should be released with necessary safeguards to allow for controlled use of the model, for example by requiring that users adhere usage guidelines restrictions to access the model or implementing safety filters.
Datasets that have been scraped from the Internet could pose safety risks. The authors should describe how they avoided releasing unsafe images.
We recognize that providing effective safeguards is challenging, and many papers do not require this, but we encourage authors to take this into account and make best faith effort.
12. Licenses for existing assets
Are the creators or original owners of assets (e.g.. code, data, models), used in the paper, properly credited and are the license and terms of use explicitly mentioned and properly respected?
Question:
Answer: [Yes]
Justification: For the interpolation solvers used in the experiments, they all credited and all the licenses are respected.
Guidelines:
The answer NA means that the paper does not use existing assets.
The authors should cite the original paper that produced the code package or dataset.
The authors should state which version of the asset is used and, if possible, include URL.
The name of the license (e.g., CC-BY 4.0) should be included for each asset.
For scraped data from a particular source (e.g., website), the copyright and terms of service of that source should be provided.
18

---

If assets are released, the license, copyright information, and terms of use in the thcode. has curated licenses for some datasets. Their licensing guide can help determine the license of dataset.
package should be provided. For popular datasets, paperswi
batasets.papersstt
For existing datasets that are re-packaged, both the original license and the license of the derived asset (if it has changed) should be provided.
If this information is not available online, the authors encouraged to reach out the asset's s creators.
13. New assets
Question: Are assets introduced in the paper well documented and is the documentation provided alongside the assets?
Answer: [NA]
We will make assets publically available after the Mouble-bling review ended.
Justification:
Guidelines:
The answer NA means that the paper does not release new assets.
Researchers should communicate the details of the dataset/code/moodl as part of their submissions via structured templates. This includes details about training, license, limitations, etc.
The paper should discuss whether and how consent was obtained from people whose asset is used.
At submission time, remember to anonymize your assets (if applicable). You can either create an anonymized URL or include an anonymized zip file.
14. Crowdsoureing and research with human subjects
Question: For crowdsourcing experiments and research with human subjects, does the paper include the full text of instructions given to participants and screenshots, if applicable, as well details about compensation (if any)?
Answer: [NA]
Justification:
The paper does not involve crowdsourcing nor research with human subjects.
Guidelines:
The answer NA means that the paper does not involve crowdsourcing nor research with human subjects.
Including this information in the supplemental material is fine, but if the main contribu- tion of the paper involves human subjects, then much detail as possible should be included the main paper.
According to the NeurlPS Code of Ethics, workers involved in data collection, curation, other labor should be paid at least the minimum wage in the country of the data collector.
15. Institutional review board (IRB) approvals or equivalent for research with human subjects
Question: Does the paper describe potential risks incurred by study participants, whether such risks were disclosed to the subjects, and whether Institutional Review Board (IRB) approvals (or an equivalent approval/review based on the requirements of your country or institution) were obtained?
Answer: [NA]
Justification:
The paper does not involve crowdsourcing nor research with human subjects.
Guidelines:
The answer NA means that the paper does involve crowdsourcing nor research with human subjects.
Depending the country in which research is conducted, IRB approval (or equivalent) may be required for any human subjects research. If you obtained IRB approval, you should clearly state this in the paper.
19

---

We recognize that the procedures for this may vary significantly between institutions and locations, and we expect authors adhere the NeurIPS Code of Ethics and the guidelines for their institution.
For initial submissions, do not include any information that would break anonymity (if applicable), such as the institution conducting the review.
16. Declaration of LLM usage
Does the paper describe the usage of LLMs if it is an important, original, or non-standard component of the core methods in this research? Note that if the LLM is used only for writing, editing, formatting purposes and does not impact the core methodology, scientific rigorousness, or originality of the research, declaration is not required.
Question:
Answer: [NA]
Justification: The core method development in this research does involve LLMs as any important, original, or non-standard components.
Guidelines:
The answer NA means that the core method development in this research does not involve LLMs as any important, original, non-standard components.
Please refer to our LLM for what should or should not be described.
20

---

A Variables and Constants in Interpolants
In addition the number of logical connectives in an interpolant, also report the number of distinct variables and the largest constant appearing in each interpolant.
Table 4: Variables and constants. Numbers are averaged over all valid solutions across all test problems.
Model
trained with Z3 GT
trained with CSIsat GT
Original
Variables
Constants
Variables
Constants
Variables
Constants
Z3
2.45
5.97 16386579
2.39
6.39
2.45
4.24
CSIsat
2.50
2.52
460537
2.60
7476237725
The number of variables in a solution does not change significantly when either solver is guided by the model. However, the largest constants in CSIsat-generated solutions drop by several orders of magnitude when the solver is guided by the model. This may be attributed to CSIsat lacking effective heuristics for optimizing over integer domains.
B Example Problems from Dataset
Below we include three example problems from Interp(4.4). The included "Z3-solutions" are solutions generated by the original Z3.
The "simp-solutions" are the solutions found by Z3 when guided by the model trained specifically for Z3. These not part of the original Interp 4, 4) dataset, but we include them here for reference.
'inputi': [
'1 + v_sep_x2 <= v_sep_x3',
(v_sep_x3 v_sep_xi and (6 v_sep_x0 and v_sep_x0 v_
(95 <= v_sep_xi and v_sep_xi <= 100) '(1 <= v_sep_z0 and 1 v_sep_x0 <= v_sep_x1)'
}.
'input2':
(1 == v_sep_xi and (0 <= v_sep_x3 and (v_sep_x1 <= v_sep_x2 and 1
+ v_sep_x3 <= v_se)_x2)))*,
'00 v_sep_x1 and (v_sep_x2 v_sep_x3 and v_sep_x3))
'(1 v_sep_x3
and
v_sep_xi and (v_sep_xi v_sep_x2
and <= v_sep_x2)))²
1.
'23 '23-solution'; not (v_sep_x1
not (v_sep_x3 -1+
v_sep_x2 <= -1)) & not (v_sep_x1 0) 11 not v_sep_x3 + -1tv_sep_x2 <= 0))²,
'simp-solution'; not (v_sep_xi 1) II (v_sep_xt -1# v_sep_x3 0)
>time:: 0.012347221374511779
}
{
'inputi': " + v_aep_x2 <= v_sep_x31,
(92 v_sep_x1 and v_sep_x1 97)
((2 + v_sep_x2 <= v_sep_var961 and (3 v_sep_x2 <- v_sep_var961
and (2 -= v_sep_var961 and ser-pp_vr9911 <= v_sep_var962 and
v_sep_var961 < v.sop_
21

---

1(2 + v_sep_x2 <= v_sep_var702 and (4 v_sep_x2 <= v_sep_var702
and (3 v_sep_var702 and (v_sep_var702 <= v_ and
v_sep_var702 v_sep_
1,
'input2';
'0 == v_sep_ x3 and (0 1 v_ and (1
v_ var3005 and (2 v_sep_x1 and v_sep_x2))))'
'(1 == v_sep_x1 and (0 <= v_sep_x3 and (v_sep_x1 <= v_sep_ _2 and 1
+ v_sep_x3 <= v_sep_x2)))',
(1 v_sep_x3 <= and (1 v_sep_x1 and (v_sep_x1 v_sep_x2 and v_sep_x2)))',
'0 v_sep_x1 and (v_sep_x2 v_ and
__sep_x3))'
1,
'23-solution;; )( (v_sep_x1 <= 1) I1 not (v_sep_x3 >= 0)
I1 not (v_sep_x2 + -ivv_sep_x0 >= 0)) & not (v_sep_x1
<= 1) II not (v_sep_x3 <= 1) Il not (v_sep_x2 >= 1))
& not (v_sep_xl <= 2)
11 not (v_sep_x3 <= 0) 11
not (v_sep_x2 >- 2))²,
'( not (v_sep_xt 0) 11 not (v_sep_x3 <= 0)) & not (v_sep_x1 x1 < 1) 11
2) || not (v_sep_Xx x2 >=
not (v_sep_x3 >= 0) II not (v_sep_xx x3 + -1ev_sep.22 < 0))
"time': 0.0149981195555441922
}
'inputi':
" vv_sep_X == 1 v_sep_x2',
(96 <= v_sep_xi and v_sep_x1 <= 100)
(92 v_sep_xi v_sep_var122 100)',
'(1 + v_sep_x2 <= and (1 + v_sep_x3 <= and v_sep_x3 <= 1))
1,
'input2':
(0 v_sep_x3 and (0
v_sep_ and (1
v_sep_var3005 and (2 == v_sep_xi and 2 <= v_sep_x2)))),
'(1 == v_sep_x1 and (0 <= v_sep_x3 and (v_sep_x1 <= v_sep_x2 and 1
+ v_sep_x3 <= v_sse_xx)))',
(( + v_sep_x3 <= and (1 v_sep_xi and (v_sep_x1 v_sep_x2
and <= v_sep_x2)))=
(0 = v_sep_xi and (v_sep_x2 a= v_sep_x3 and <= v_sep_x3))
1,
'2 77l-solution's ' not (v_sep_x1
2) II not (v_sep_x3
0)
11 not (v_sep_x2 x2 >= 2)) & not (v_sep_x1 <= 1) 11
not (v_sep_ x3 <= 1) Il not (v_sep_x2 >= 1)) &b ( not (
v_sep_x1 < 1) I1 not (v_sep_x3 S= 0) 11 not (v_sep_x3 -1v___ep_22
0))?,
solmpisolutinn '( not (v_sep_x1 <= 1) II not (v_sep_xx x3 >= 0)
not (v_sep_x2 + -isv_sep_xt >= 0)) & not (v_sep_xi
2) 1I not (v_sep_x3 0) || not (v_sep_x2 1))
'time 0. 9.0166450996398825778
22

---

C Experiments with CVC5
In addition Z3 and CSIsat, also report limited evaluation with CVC5 [3]. Technically, while CVC5 supports interpolation, it struggles with our benchmark suite. In our experiments, CVCS failed to solve 85% of the problems within the timeout of 5 seconds. For the remaining 15%, the problems were so simple that the original interpolants already had complexity 1 and could not be further simplified.
Nonetheless, we observe significant reduction (-28% with a conservative estimation) in solver time which is comparable the 30% reduction observed for 73 in Table 2 Table guiding CVC5 using the model trained on Z3's ground truths.
5 shows the statistics
Table 5: Solver performance (mean 95% CI) for solver time.
Method
Valid
Complexity
Solver time (s)
Original CVC5
15.3% Guided CVC5
0.301 + 0.116
7.3%
0.107 + 0.031
23


Reviews:
[{"review_id": "YeM7DLOtu0", "reviewer": "Reviewer_ZEyo", "summary": "This paper introduces a novel learning-based approach to improve interpolation solvers for Linear Integer Arithmetic (LIA) by generating simpler interpolants. The authors propose using Graph Neural Networks (GNNs) combined with a self-attention mechanism to learn embeddings of LIA formulas, which capture both local arithmetic constraints and the global structure of the formulas. These embeddings enable the model to identify the most relevant subsets of the formulas to create minimal, valid interpolants, thereby simplifying the interpolation process.\n\nThe method is integrated with existing SMT solvers like Z3, showing significant improvements in performance. Experimental results demonstrate that the approach achieves up to 47.3% reduction in interpolant complexity for modern solvers and up to 69.1% reduction for older solvers, offering a promising solution for software and hardware verification. The authors argue that this approach combines symbolic reasoning with machine learning, making it a practical and efficient enhancement for formal verification tasks.", "questions": "Due to my limited familiarity with this field, my judgment may not be entirely accurate.", "limitations": "N.A.", "rating": 4, "confidence": 1, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 2, "clarity": 2, "significance": 2, "originality": 2, "strengths_and_weaknesses": "Strengths\n1. Quality: The paper introduces a novel learning-based method using GNNs and self-attention to improve LIA interpolation solvers, demonstrating significant performance gains.\n\n2. Clarity: The paper is well-written, with clear explanations of the methodology and empirical results that are easy to follow.\n\n3. Significance: The approach addresses a practical problem in formal verification, offering improvements in software and hardware verification through simpler interpolants.\n\n4. Originality: The integration of machine learning with symbolic reasoning to simplify interpolation is innovative, adding a new dimension to existing methods.\n\nWeaknesses\n\n1. Limited Evaluation: The method is evaluated on a small set of benchmark problems, with no discussion of its scalability or performance on more complex, real-world data.\n\n2. Lack of Comparison: The paper does not adequately compare the proposed method with other state-of-the-art techniques for simplifying interpolants or optimizing LIA solvers.\n\n3. Interpretability: The GNN-based model's decision process is not clearly explained, which could limit its acceptance in practical, safety-critical applications.\n\n4. Theoretical Depth: The paper lacks a thorough theoretical analysis of the generalization and robustness of the model to different LIA problem structures.", "was_revised": true, "final_justification": "The rebuttal clarified several of my concerns:\n\n- The dataset size (66K problems) is reasonable for formal verification, and the authors explained its construction and scalability well.\n\n- The lack of direct comparisons is justified, as no prior work exists for ML-based LIA interpolation. The method complements symbolic solvers rather than replacing them.\n\n- Interpretability concerns are partly mitigated, as the learned components do not make correctness-critical decisions—soundness is guaranteed by the SMT solver.\n\nGiven the clarifications, I have raised my score, while remaining open to further discussion due to my limited familiarity with the area.", "rebuttal": "Thank you for the review. We understand that unfamiliarity with the field may have led to some confusion, and we would like to clarify each of the concerns raised.\n\n> “Limited Evaluation: The method is evaluated on a small set of benchmark problems, with no discussion of its scalability...”\n\nTo the best of our knowledge, no benchmark suite currently exists for learning-based LIA interpolation. We presented the first dataset, and did our best to ensure complexity and a rich coverage. We detailed the complete generation process in Section 4.1 and explained how the dataset **scales** with parameters c1 and c2 in **Interp**(c1, c2).\n\nWe also respectfully disagree that our dataset consisting of 66K problems is “small” in the context of formal verification. In this field, high-quality data are much more limited than other applications of machine learning. As a reference, previous works on learning SAT typically use 8K to 10K problems. See [2] [3] for example. \n\n[2] *Learning a SAT Solver from Single-Bit Supervision.* D. Selsam, M. Lamm, B. Bünz, P. Liang, L. de Moura, and D. L. Dill. ICLR 2019.\n\n[3] *Learning Better Representations From Less Data For Propositional Satisfiability.* Mohamed Ghanem and Frederik Schmitt and Julian Siber and Bernd Finkbeiner. NeurIPS 2024.\n\n> “Lack of Comparison: The paper does not adequately compare the proposed method with other state-of-the-art techniques for simplifying interpolants ...”\n\nAs Reviewer eKSy noted, Craig interpolation via ML has not been seriously attempted before. **Direct comparisons are thus not possible—no existing method learns to simplify interpolants in LIA using neural models.**\n\nAs for the techniques on the symbolic side, our proposed approach **improves upon them**. Our approach further augments, rather than replaces, traditional symbolic methods already built into mature solvers like Z3. It learns heuristics that exploit redundancies in the input to produce simpler interpolants—something traditional approaches are not designed to do. This is why our approach is a combination of machine learning and symbolic methods. The benefits are demonstrated empirically in Section 4.\n\n> “Interpretability: The GNN-based model's decision process is not clearly explained, which could limit its acceptance in practical, safety-critical applications.”\n\nThe GNN model does not make any decision on which disjuncts to choose. It only encodes the formulas into the latent space.\n\nThe selector model does not make any correctness-critical decisions, either. It only proposes subsets of formulas to guide interpolation. The SMT solver is ultimately responsible for computing the interpolant and guaranteeing soundness. Our approach is designed for safety-critical applications from the very beginning.\n\n> “Theoretical Depth: The paper lacks a thorough theoretical analysis of the generalization and robustness of the model to different LIA problem structures.”\n\nAs indicated in our submission, this is an application paper (see “Primary Area” and Checklist Item 3 on theoretical guarantees). That said, we did our best to provide an analysis of the generalization and robustness of the model to different underlying solvers in Section 4.4.\n\nHowever, we are unsure what is meant by “different LIA problem structures” in the question. Craig interpolation in LIA is concerned with unsatisfiable formula pairs; structural variation is implicitly captured in the disjunctive inputs we generate. If the reviewer can provide a more precise definition, we are happy to address it.\n\n---\n\nWe hope these clarify the confusion! We would greatly appreciate it if you could take our response into account when considering the final score."}, {"review_id": "PBVO8O7mny", "reviewer": "Reviewer_gZmf", "summary": "This work highlights a task from classical SMT solving/symbolic reasoning and uses GNNs to approximately solve it. In particular, the authors focus on Criag Interpolation. They are able to show 40% reduction in complexity testing on Z3.", "questions": "1. How do these results apply to CVC5? Are these gains specific to the algorithm behind Z3?\n2. What is the train and test split? In some sense the generalization is what's interesting as solving a single instance of craig interpolation isn't as interesting if the machine is leveraging parallel GPU computation.", "limitations": "It's not clear to me what the broader impacts are. What does this say about how we should design learning algorithms ?", "rating": 3, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 2, "clarity": 2, "significance": 2, "originality": 3, "strengths_and_weaknesses": "Strength: \n1. This work poses an interesting problem that presents a fundamental learning challenge. \n2. It's working on a problem that's unique. \n\nWeakness: \n1. It's not clear that the learnings from this work will translate to other relevant problems in the field.\n2. Would appreciate a concrete motivating example of a craig interpolant in the text to motivate why this is problem that matters and what makes it hard. The abstract problem instance is hard to appreciate.", "was_revised": true, "final_justification": "I am very concerned that the results do not generalize outside of the narrow settings tested in the paper. In particular, the ask was made to test on at least 10 problems in the standard LIA-Inv_Track from sygus. The loop invariant inference problems are exactly in the flavor that the authors motivate their paper and no more difficult than \n```x = 0; y = 0;\nwhile(*) {x++; y+=2}\nassert(x=100=> y=200);```\n\nproblem they highlighted in the rebuttal.\n\nI think the authors should consider either supporting array theories or be applied to LIA problems in a downstream application to strengthen the paper.", "rebuttal": "Thank you for the supportive review. We first address your specific questions, followed by a paragraph regarding your major concern about the broader impact of finding simple interpolants.\n\n> “... apply to CVC5?... gains specific to the algorithm behind Z3?”\n\nThere are two ways to apply our method to other solvers. One approach is to retrain the model using ground truths generated by the target solver. The other is to directly apply a model trained on ground truths from a different solver (e.g., Z3). The former is ideal, as it allows the model to learn the specific behaviors of the target solver. However, as shown in Section 4.4, even a pre-trained model can transfer effectively across solvers to some extent. In either case, **the gains are not tied to Z3's internal algorithms.** The learning framework we propose can be applied to other solvers without modification—particularly when retraining is possible.\n\nTechnically, while CVC5 supports interpolation, it struggles with our benchmark suite. In our experiments, CVC5 failed to solve 85% of the problems within the timeout of 5 seconds. For the remaining 15%, the problems were so simple that the original interpolants already had complexity 1 and could not be further simplified.\n\nNonetheless, we still observe significant reduction (-66%) in solver time. Below we report the statistics on guiding CVC5 using the model trained on Z3’s ground truths.\n\n| Method | Valid | Complexity | Solver time (s)|\n|:------|:-----:|:------:|:------:|\n| Original CVC5 | 15.3% | 1 | 0.301 |\n| Guided CVC5 | 7.3% | 1 | 0.107 |\n\n> “What is the train and test split? ...  parallel GPU computation.”\n\nThe train-test split is 80:20, as stated on lines 220-221.  We would also like to clarify that parallel GPU computation does not introduce any form of “cheating” here. The interpolants are always computed and verified by the SMT solver which runs on CPU. The model’s role is limited to analyzing the original input formulas and providing suggestions to avoid redundancy. It does not compute the interpolants by itself using GPU power.\n\n> “... what the broader impacts are... how we should design learning algorithms ?” & “... translate to other relevant problems in the field.”\n\n**The main purpose of this work is to break the ice on a largely unexplored topic** — the application of learning to interpolation solving with simplification. (Please see below for its significance in verification.)  \n\nAs Reviewer eKSy noted in the review, Craig interpolation via ML has not been seriously attempted before. Consequently, there is currently no established understanding or baseline about how learning algorithms should be designed for this problem, nor what properties are desirable or generalizable.\n\nRather than claiming to answer the higher-level design questions, our goal is to create the first stepping stone: to show that learning-based methods can in fact produce useful results for finding simple interpolants, a symbolic reasoning task previously considered difficult to learn. The fact that our lightweight model is able to improve solvers like Z3 demonstrates that meaningful learning signals exist and can be extracted.\n\nWe believe the broader impact lies precisely here. We provide concrete empirical evidence that this new direction is feasible and promising. Future work will be better positioned to address the deeper question of how learning algorithms should be designed for interpolation and similar tasks — but such exploration must start somewhere, and we believe this paper provides a well-motivated and technically grounded beginning.\n\n---\n\n# Addressing the Concern on Potential Impact\nWe noticed that the only substantive concern raised by reviewers eKSy and gZmf centers on the potential impact of our work. Reviewer DWpJ echoed this by asking “Why is producing simpler interpolants important?”\n\nThis is an oversight on our part. While we briefly mentioned the reasons on lines 19–21, we did not elaborate further, as this fact is often taken for granted in the literature on interpolation-based verification.\n\nWe now provide a clarification on the significant impact of simpler interpolants, addressing both conceptual and practical aspects. \n\nWe would like to emphasize that this is not an artificial problem chosen merely to showcase machine learning techniques. Rather, it addresses a longstanding and practical challenge in formal verification—one that directly impacts the effectiveness and scalability of verification tools.\n\n## Conceptually\n\nIn program verification, Craig interpolants are often used to extract candidate invariants from proofs of bounded cases. Intuitively, an interpolant is a formula that captures a property implied by one part of the system and inconsistent with another, using only the common variables.\n\n**The key insight is that simplicity leads to generality.** A simpler interpolant tends to omit the incidental details of a particular execution, making it more likely to hold in general (i.e. be inductive for all executions).\n\nThis is analogous to machine learning, where a simple model that captures the core pattern will generalize better than an overly complex one that overfits to training data. In the verification context, a complex interpolant can “overfit” a bounded proof (including many specific corner-case conditions), whereas a concise interpolant focuses on the essential relationship and is less prone to depend on particular aspects of that bounded run.\n\nThe result is an interpolant that is more likely to be a true invariant for the unbounded system, rather than a brittle formula that breaks with minor changes. A concise interpolant (e.g. a single linear inequality or equality) is less tied to a specific execution, so it generalizes to new executions. Invariant generation becomes easier because the formula isn’t cluttered with special-case conditions that might fail as soon as we go beyond the originally analyzed trace.\n\nIn short, simpler interpolants serve as more general and robust invariants, which is exactly what we need for scalable verification.\n\n### **Example**:\n\nConsider the following example of finding a loop invariant. Suppose we have a C program:\n```\nx = 0; y = 0;\nwhile(*) {x++; y+=2}\nassert(x=100=> y=200);\n```\nThe key to proving the assertion lies in discovering the loop invariant y = 2x. A common strategy for finding such invariants is interpolation. \n\nLet $I(x,y)$ be an (unknown) invariant.\n\nThen by unfolding the loop a few times, we would get the constraints:\n\n$(x=0\\wedge y=0)\\vee (x=1\\wedge y=2)\\vee (x=2 \\wedge y=4) \\Rightarrow I(x,y)$\n\n$I(x,y) \\Rightarrow (x=100 \\Rightarrow y=200)$\n\nThis induces the interpolation problem:\n\n$A = (x=0\\wedge y=0)\\vee (x=1\\wedge y=2)\\vee (x=2 \\wedge y=4)$\n\n$B = \\neg (x=100 \\Rightarrow y=200)$\n\nAll of\n\n$I_1 = (x=0\\wedge y=0)\\vee (x=1\\wedge y=2)\\vee (x=2 \\wedge y=4)$\n\n$I_2 = (x=100 \\Rightarrow y=200)$\n\n$I = y = 2x$\n\nare interpolants between A and B, but only $y=2x$, the simplest among these, is a valid loop invariant of the original C program.\n\n### **Where is the difficulty?**\nIn practice, interpolation solvers can (and often) generate interpolants like $I_1$ or $I_2$. In the simple two dimensional case as in this example, a human expert might be able to simplify the solutions by hand. But it quickly becomes infeasible in higher dimensions (i.e., more variables) with more regions (i.e., more logic connectives). \n\nWhether machine learning can guide interpolation solvers to find simpler interpolants has been an open question. Our work makes the first attempt to guide interpolation solvers toward producing simpler interpolants, and shows that this is both possible and effective.\n\n## Practically\nFrom an engineering perspective, using simpler interpolants pays off in the following ways.\n\n- **Verification Convergence**: Interpolants are used iteratively to search for an inductive invariant. Simpler interpolants are more likely to generalize across all program executions, increasing the probability that one of them will be inductive. This, in turn, improves the chance that the verification process will eventually succeed. In contrast, overly complex interpolants tend to overfit bounded traces and often fail to generalize, which can cause the verification loop to stagnate or diverge entirely. As a result, the system may perform many unproductive solver calls or even time out.\n\n- **Solver efficiency**: Less complex formulas are cheaper for solvers to handle. Every additional literal or clause in an interpolant is something the downstream SMT query has to reason about. A 447-clause interpolant might trigger many more internal computations (Boolean case splits, calls to arithmetic subsolvers, etc.) than a 2-clause interpolant. By keeping interpolants minimal, we cut down the search space and the overhead in the subsequent SAT/SMT procedures. This often translates to more solvable downstream problems and/or faster verification times, as seen in Figure 4 of [1].\n\n- **Proof reuse**: Simpler interpolants often enable a more compositional verification approach, where one can reuse the same inductive argument across different components or unrolling lengths. If the invariant is a small conjunction of facts, it can be plugged in modularly; if it’s a huge disjunction of special cases, it’s much harder to reuse or even comprehend. Thus simplicity can improve the scalability of the verification process itself, not just the single SMT query.\n\nFor further theoretical justification and more empirical evidence, we refer to the classical literature by Aws Albarghouthi and Kenneth L. McMillan such as [1].\n\n[1] *Beautiful Interpolants.* Aws Albarghouthi and Kenneth L. McMillan. CAV 2013: Proceedings of the 25th International Conference on Computer Aided Verification - Volume 8044 Pages 313 - 329\n\n--- \n\nWe thank the reviewer for the feedback. If the clarifications above have addressed your concerns, we would greatly appreciate it if you could consider increasing your score."}, {"review_id": "QfvqoicgV8", "reviewer": "Reviewer_eKSy", "summary": "At a high level, this paper proposes a novel graph-neural-network-based approach for learning how to allocate attention when focusing on relationships between formulas when doing Craig interpolation for Linear Integer Arithmetic (LIA). When solving verification problems, verifiers are often producing Craig interpolants in a tight loop alongside enumeration. Thus, these Craig interpolants can be thought of as \"intermediate formulas\" which the solver (verifier, etc.) is exploring on its way to a solution (counterexample, proof, etc.). In the case of LIA, these look like polynomial (in)equalities. Traditional approaches to Craig interpolation produce unwieldy, large interpolants, with possibly-large coefficients--incurring unnecessarily-large state-space enumeration in the subsequent saturation part of the engine / verifier. The goal is to get small (but correct) interpolants.\n\nThe authors approach is to deeply integrate a GNN and a self-attention-based selector mechanism. The GNN encodes semantic relationships between clauses in the knowledge base, and a selector network then selects subsets of formulas from which to attempt to generate interpolants. This requires a new dataset of interpolation problems--the authors build a new dataset of 66k LIA interpolation problems, which seems like a seriously hefty dataset to me.\n\nThe authors emphasize the needs to focus on traditional ML and a GNN-based approach, and that it would be especially irrelevant to use an LLM. I agree, it would be irrelevant to use an LLM here. The authors also stress the importance of calling the solver *once*, rather than in a loop, in a bottom-up fashion. This necessitates that the authors decompose their exploration in a top-down manner. \n\n# Overall score and justification\n\nOverall, I am very impressed by this work. However, I am very surprised that this is not a very hot area, and it seems surprising to me that Craig interpolation via ML has not been seriously attempted before. My main concern rests on the significance of the work. The authors show reduced interpolant complexity, but I have an outstanding question: how can I put this work into perspective in terms of its impact on the field? Even though small interpolants are nice, are they really a critical component in verification pipelines?\n\nI cannot tell if this paper is a cool, incremental contribution to a challenging field or a truly revolutionary step forward. However, in either case it is well written, intuitive, and easy to read, even as an outsider. I argue that it should be accepted.\n\nSome caveats about my review: I am knowledgable about Craig interpolation and its use in verification, but I do not deeply understand the mechanisms for constructing Craig interpolants and am not sure I am fully prepared to give a nuanced review versus the state of the art.", "questions": "- There is a depth into the tree, but not any structural information. How is this depth used? I guess the hierarchical information is captured by the MPNN?\n\n- How do I put your approach into context for how this might impact the future of SMT solvers and verification? I understand in the abstract that small interpolants are good--but no experiments in the paper can convince me of the promise of the approach to, say, accelerate SMT. Do you have any thoughts on this?", "limitations": "yes", "rating": 5, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 4, "clarity": 3, "significance": 3, "originality": 3, "strengths_and_weaknesses": "# Strengths \n\n- Craig interpolation is an important, long-standing, challenging problem that sits at the tight loop of verification, SMT solving, and many important problems in logic and automated reasoning. This paper attacks a particularly pertinent instance of Craig interpolation: for LIA, an important first-order theory that is one of the most popular in SMTLIB.\n\n- The authors got real interpolation problems from downstream tasks, though it is a bit unclear exactly what these are. The authors build a huge knowledge database of LIA facts and then compute self-attention between all of them, which would appear to be a very compelling approach, to me. It is really using the self-attention idea in a manner that can credibly inform the construction of interpolants in an on-demand way.\n\n- The encodings of formulas (Sec 3.2) is brief but makes a lot of sense. You want to be able to learn the hierarchical structure of formulas. Naturally, you need to run as many rounds of iteration as the tallest AST you have (one would assume).\n\n- Writing is overall of high caliber and makes sense. \n\n# Weaknesses\n\n- The major weakness is limited potential impact. It seems that there is limited downstream application for making small Craig interpolants. At least, the authors have included no compelling evaluation which demonstrates why we should believe this will be the case. This is a potentially major concern, although I do believe the approach is still relevant and interesting nonetheless.\n\n- The idea of pooling together all interpolants seen dynamically throughout tons of sample instances seems reasonable, but importantly seems to throw away the context inherent to the problem. I am not sure if this is a weakness or if this is explicitly something you want to do.", "was_revised": true, "final_justification": "I argue the paper should be accepted. The authors have offered convincing, thoughtful, and reflective commentary and feedback, both in the original paper and in the subsequent rebuttal.\n\nThe paper is on a complex, challenging, and important area--complaints that the paper needs to be changed to accommodate non-experts are unfounded, as the paper tackles a well-known, important, and long-standing problem. The authors provide further detail in their rebuttal here--I would encourage them to incorporate some of this feedback into the paper, anticipating that it might help the paper's context with respect to work appearing at NeurIPS.\n\nThe authors offer convincing evidence that their approach is promising, at least good enough over the existing state of the art that it is worthy of publication at NeurIPS '25.\n\nThe scoping of paper, size of contribution, and evaluation of results is reasonable, even for a top conference.\n\nHere is my only negative feedback to the authors: what you wrote above, and to a degree in the paper, is a thoughtful argument that makes a lot of intuitive sense--as someone who is somewhat-versed in the usage of Craig interpolation, the reasoning above makes total sense to me. Ideally, work appearing at NeurIPS (or any other top conference) would also take the reasoning above and truly demonstrate the impact on downstream tasks--that is a bit lacking in this paper. However, I do not see that alone as a reason for rejecting this paper--I do not want to see that happen, in this case, and feel it is unfair to impose that standard given all of the work the authors have done here.\n\nI argue the paper should be accepted, and maintain my score. I encourage the AC to consider the importance, relevance, generality, and long-standing nature of the problem being attacked in this work.\n\nMy score is 5--I recognize the paper has some flaws, but (with no intended offense to other reviewers) I think it is important to argue for strong, technically-focused work with rich technical foundations. The paper harmonizes machine learning with a challenging and relevant task that lies at the core of automated reasoning.\n\nI do not argue 6 because I recognize that the paper does have some attack surface, but I think given the totality of the situation, it would be best for NeurIPS '25 to accept the paper.", "rebuttal": "We would like to express our heartfelt thanks to the reviewer for their detailed and supportive review. Among the reviews we received, this one stood out for its depth of engagement, clarity of reasoning and evident familiarity with the topic. We are especially grateful for the reviewer's recognition of the novelty and relevance of our approach, and we truly value your support and insightful comments throughout.\n\nWe first address your specific questions, followed by a paragraph regarding your major concern about the potential impact of finding simple interpolants.\n\n> “There is a depth into the tree, but not any structural information. How is this depth used?”\n\nDepth is included as part of the GNN’s node features and is used in conjunction with the “edge information” (see the upper part of Figure 1) to encode structure. The edge information is a list of node pairs that explicitly capture the formula’s tree structure. For example, if nodes 2 and 3 are children of node 1 in the AST, the edge list will include the pairs (1, 2) and (1, 3). We apologize for not making this clearer in the main text and will revise the description accordingly in the next version. Thank you for pointing this out!\n\n> “.. but importantly seems to throw away the context inherent to the problem. I am not sure if this is a weakness … ”\n\nIt is true that the GNN encoder processes each disjunct independently and does not see the full formula. However, this limitation is mitigated by the subsequent selector model, which has access to the entire context, including all original disjuncts from both input formulas. Therefore, while the encoding is local, the overall model still retains and reasons over the global structure of the problem.\n\n> “How do I put your approach into context for how this might impact the future of SMT solvers and verification?”\n\nWe address this point with a common response to reviewers gZmf, eKSy, and DWpJ as follows.\n\n---\n\n# Addressing the Concern on Potential Impact\nWe noticed that the only substantive concern raised by reviewers eKSy and gZmf centers on the potential impact of our work. Reviewer DWpJ echoed this by asking “Why is producing simpler interpolants important?”\n\nThis is an oversight on our part. While we briefly mentioned the reasons on lines 19–21, we did not elaborate further, as this fact is often taken for granted in the literature on interpolation-based verification.\n\nWe now provide a clarification on the significant impact of simpler interpolants, addressing both conceptual and practical aspects. \n\nWe would like to emphasize that this is not an artificial problem chosen merely to showcase machine learning techniques. Rather, it addresses a longstanding and practical challenge in formal verification—one that directly impacts the effectiveness and scalability of verification tools.\n\n## Conceptually\n\nIn program verification, Craig interpolants are often used to extract candidate invariants from proofs of bounded cases. Intuitively, an interpolant is a formula that captures a property implied by one part of the system and inconsistent with another, using only the common variables.\n\n**The key insight is that simplicity leads to generality.** A simpler interpolant tends to omit the incidental details of a particular execution, making it more likely to hold in general (i.e. be inductive for all executions).\n\nThis is analogous to machine learning, where a simple model that captures the core pattern will generalize better than an overly complex one that overfits to training data. In the verification context, a complex interpolant can “overfit” a bounded proof (including many specific corner-case conditions), whereas a concise interpolant focuses on the essential relationship and is less prone to depend on particular aspects of that bounded run.\n\nThe result is an interpolant that is more likely to be a true invariant for the unbounded system, rather than a brittle formula that breaks with minor changes. A concise interpolant (e.g. a single linear inequality or equality) is less tied to a specific execution, so it generalizes to new executions. Invariant generation becomes easier because the formula isn’t cluttered with special-case conditions that might fail as soon as we go beyond the originally analyzed trace.\n\nIn short, simpler interpolants serve as more general and robust invariants, which is exactly what we need for scalable verification.\n\n### **Example**:\n\nConsider the following example of finding a loop invariant. Suppose we have a C program:\n```\nx = 0; y = 0;\nwhile(*) {x++; y+=2}\nassert(x=100=> y=200);\n```\nThe key to proving the assertion lies in discovering the loop invariant y = 2x. A common strategy for finding such invariants is interpolation. \n\nLet $I(x,y)$ be an (unknown) invariant.\n\nThen by unfolding the loop a few times, we would get the constraints:\n\n$(x=0\\wedge y=0)\\vee (x=1\\wedge y=2)\\vee (x=2 \\wedge y=4) \\Rightarrow I(x,y)$\n\n$I(x,y) \\Rightarrow (x=100 \\Rightarrow y=200)$\n\nThis induces the interpolation problem:\n\n$A = (x=0\\wedge y=0)\\vee (x=1\\wedge y=2)\\vee (x=2 \\wedge y=4)$\n\n$B = \\neg (x=100 \\Rightarrow y=200)$\n\nAll of\n\n$I_1 = (x=0\\wedge y=0)\\vee (x=1\\wedge y=2)\\vee (x=2 \\wedge y=4)$\n\n$I_2 = (x=100 \\Rightarrow y=200)$\n\n$I = y = 2x$\n\nare interpolants between A and B, but only $y=2x$, the simplest among these, is a valid loop invariant of the original C program.\n\n### **Where is the difficulty?**\nIn practice, interpolation solvers can (and often) generate interpolants like $I_1$ or $I_2$. In the simple two dimensional case as in this example, a human expert might be able to simplify the solutions by hand. But it quickly becomes infeasible in higher dimensions (i.e., more variables) with more regions (i.e., more logic connectives). \n\nWhether machine learning can guide interpolation solvers to find simpler interpolants automatically has been an open question. Our work makes the first attempt to guide interpolation solvers toward producing simpler interpolants, and shows that this is both possible and effective.\n\n## Practically\nFrom an engineering perspective, using simpler interpolants pays off in the following ways.\n\n- **Verification Convergence**: Interpolants are used iteratively to search for an inductive invariant. Simpler interpolants are more likely to generalize across all program executions, increasing the probability that one of them will be inductive. This, in turn, improves the chance that the verification process will eventually succeed. In contrast, overly complex interpolants tend to overfit bounded traces and often fail to generalize, which can cause the verification loop to stagnate or diverge entirely. As a result, the system may perform many unproductive solver calls or even time out.\n\n- **Solver efficiency**: Less complex formulas are cheaper for solvers to handle. Every additional literal or clause in an interpolant is something the downstream SMT query has to reason about. A 447-clause interpolant might trigger many more internal computations (Boolean case splits, calls to arithmetic subsolvers, etc.) than a 2-clause interpolant. By keeping interpolants minimal, we cut down the search space and the overhead in the subsequent SAT/SMT procedures. This often translates to more solvable downstream problems and/or faster verification times, as seen in Figure 4 of [1].\n\n- **Proof reuse**: Simpler interpolants often enable a more compositional verification approach, where one can reuse the same inductive argument across different components or unrolling lengths. If the invariant is a small conjunction of facts, it can be plugged in modularly; if it’s a huge disjunction of special cases, it’s much harder to reuse or even comprehend. Thus simplicity can improve the scalability of the verification process itself, not just the single SMT query.\n\nFor further theoretical justification and more empirical evidence, we refer to the classical literature by Aws Albarghouthi and Kenneth L. McMillan such as [1].\n\n[1] *Beautiful Interpolants.* Aws Albarghouthi and Kenneth L. McMillan. CAV 2013: Proceedings of the 25th International Conference on Computer Aided Verification - Volume 8044 Pages 313 - 329\n\n---\n\nWe are grateful for your careful reading and generous feedback, and we hope these clarifications reinforce your positive assessment of the paper."}, {"review_id": "zIGBdhCQxj", "reviewer": "Reviewer_DWpJ", "summary": "Linear integer arithmetic (LIA), is a logic that allows one to express linear\nconstraints on integers: equalities, inequalities, and divisibility by non-zero integers. \nThis paper proposes a learning-based approach toward computing simpler (than previous logic based\nmethods) interpolants in LIA, complementing. In addition, they provide a new large dataset of interpolation problems\non which they demonstrate the  ability of their learning approach to simplify interpolants compared to previous approaches.", "questions": "I am not an expert in the field.\nIt would help me to understand exactly where and how interpolants are used and why the \nproblem of producing \"simpler\" interpolants is important as well as a better explanation of the \n\"simplicity\" definition.", "limitations": "I think so.", "rating": 3, "confidence": 1, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 2, "clarity": 2, "significance": 3, "originality": 2, "strengths_and_weaknesses": "Strengths\n1. The problem of computing interpolants for ILA is useful for program verification.\n2. The paper uses light weight learning rather than LLMs\n3. The Dataset provided could be certainly  useful for testing solutions for this problem in the future.\n\nWeaknesses\n1. Its unclear to what extent one can verify the claim of \"simplicity\" compared to previous solutions, the definition\nof simplicity was not made clear.\n2. Quoting \"We show that when Z3 is guided by our learned model, the complexity of the interpolants it produces can\nbe reduced by up to 47.3%\". Not sure how this figure was reached. Also, does this mean that the simpler interpolants were more useful?", "was_revised": false, "final_justification": "", "rebuttal": "Thank you for the review. We understand that unfamiliarity with the field may have led to some confusion, and we would like to clarify each of the concerns raised.\n\n> “It's unclear to what extent one can verify the claim of \"simplicity\" compared to previous solutions, the definition of simplicity was not made clear.” & “... the complexity of the interpolants it produces can be reduced by up to 47.3%. Not sure how this figure was reached”\n\nWe respectfully clarify the reviewer’s concern regarding the notion of “simplicity” and how the reported 47.3% reduction was measured.\n\nWe define the complexity of a formula as the number of logical connectives it contains—specifically, the number of $\\wedge$ and $\\vee$ operators. This **definition is formally stated on lines 62–63 in Section 2** and aligns with the standard interpretation of formula complexity in the verification literature.\n\nThe term “simplicity” is thus used in a precise and quantitative sense. All comparisons in Table 2 and Table 3 follow this definition. Specifically, the 47.3% reduction figure is derived from Table 2:\n\n- Average complexity of Z3’s original interpolants: 5.38\n\n- Average complexity of model-guided interpolants: 2.83\n\n- Percentage reduction: (5.38−2.83)/5.38×100%=47.3%\n\n> “It would help me to understand exactly where and how interpolants are used and why the problem of producing \"simpler\" interpolants is important as well as a better explanation of the \"simplicity\" definition.”\n\nWe explain this as a common response to reviewers gZmf, eKSy and DWpJ as follows.\n\n---\n\n# Addressing the Concern on Potential Impact\nWe noticed that the only substantive concern raised by reviewers eKSy and gZmf centers on the potential impact of our work. Reviewer DWpJ echoed this by asking “Why is producing simpler interpolants important?”\n\nThis is an oversight on our part. While we briefly mentioned the reasons on lines 19–21, we did not elaborate further, as this fact is often taken for granted in the literature on interpolation-based verification.\n\nWe now provide a clarification on the significant impact of simpler interpolants, addressing both conceptual and practical aspects. \n\nWe would like to emphasize that this is not an artificial problem chosen merely to showcase machine learning techniques. Rather, it addresses a longstanding and practical challenge in formal verification—one that directly impacts the effectiveness and scalability of verification tools.\n\n## Conceptually\n\nIn program verification, Craig interpolants are often used to extract candidate invariants from proofs of bounded cases. Intuitively, an interpolant is a formula that captures a property implied by one part of the system and inconsistent with another, using only the common variables.\n\n**The key insight is that simplicity leads to generality.** A simpler interpolant tends to omit the incidental details of a particular execution, making it more likely to hold in general (i.e. be inductive for all executions).\n\nThis is analogous to machine learning, where a simple model that captures the core pattern will generalize better than an overly complex one that overfits to training data. In the verification context, a complex interpolant can “overfit” a bounded proof (including many specific corner-case conditions), whereas a concise interpolant focuses on the essential relationship and is less prone to depend on particular aspects of that bounded run.\n\nThe result is an interpolant that is more likely to be a true invariant for the unbounded system, rather than a brittle formula that breaks with minor changes. A concise interpolant (e.g. a single linear inequality or equality) is less tied to a specific execution, so it generalizes to new executions. Invariant generation becomes easier because the formula isn’t cluttered with special-case conditions that might fail as soon as we go beyond the originally analyzed trace.\n\nIn short, simpler interpolants serve as more general and robust invariants, which is exactly what we need for scalable verification.\n\n### **Example**:\n\nConsider the following example of finding a loop invariant. Suppose we have a C program:\n```\nx = 0; y = 0;\nwhile(*) {x++; y+=2}\nassert(x=100=> y=200);\n```\nThe key to proving the assertion lies in discovering the loop invariant y = 2x. A common strategy for finding such invariants is interpolation. \n\nLet $I(x,y)$ be an (unknown) invariant.\n\nThen by unfolding the loop a few times, we would get the constraints:\n\n$(x=0\\wedge y=0)\\vee (x=1\\wedge y=2)\\vee (x=2 \\wedge y=4) \\Rightarrow I(x,y)$\n\n$I(x,y) \\Rightarrow (x=100 \\Rightarrow y=200)$\n\nThis induces the interpolation problem:\n\n$A = (x=0\\wedge y=0)\\vee (x=1\\wedge y=2)\\vee (x=2 \\wedge y=4)$\n\n$B = \\neg (x=100 \\Rightarrow y=200)$\n\nAll of\n\n$I_1 = (x=0\\wedge y=0)\\vee (x=1\\wedge y=2)\\vee (x=2 \\wedge y=4)$\n\n$I_2 = (x=100 \\Rightarrow y=200)$\n\n$I = y = 2x$\n\nare interpolants between A and B, but only $y=2x$, the simplest among these, is a valid loop invariant of the original C program.\n\n### **Where is the difficulty?**\nIn practice, interpolation solvers can (and often) generate interpolants like $I_1$ or $I_2$. In the simple two dimensional case as in this example, a human expert might be able to simplify the solutions by hand. But it quickly becomes infeasible in higher dimensions (i.e., more variables) with more regions (i.e., more logic connectives). \n\nWhether machine learning can guide interpolation solvers to find simpler interpolants automatically has been an open question. Our work makes the first attempt to guide interpolation solvers toward producing simpler interpolants, and shows that this is both possible and effective.\n\n## Practically\nFrom an engineering perspective, using simpler interpolants pays off in the following ways.\n\n- **Verification Convergence**: Interpolants are used iteratively to search for an inductive invariant. Simpler interpolants are more likely to generalize across all program executions, increasing the probability that one of them will be inductive. This, in turn, improves the chance that the verification process will eventually succeed. In contrast, overly complex interpolants tend to overfit bounded traces and often fail to generalize, which can cause the verification loop to stagnate or diverge entirely. As a result, the system may perform many unproductive solver calls or even time out.\n\n- **Solver efficiency**: Less complex formulas are cheaper for solvers to handle. Every additional literal or clause in an interpolant is something the downstream SMT query has to reason about. A 447-clause interpolant might trigger many more internal computations (Boolean case splits, calls to arithmetic subsolvers, etc.) than a 2-clause interpolant. By keeping interpolants minimal, we cut down the search space and the overhead in the subsequent SAT/SMT procedures. This often translates to more solvable downstream problems and/or faster verification times, as seen in Figure 4 of [1].\n\n- **Proof reuse**: Simpler interpolants often enable a more compositional verification approach, where one can reuse the same inductive argument across different components or unrolling lengths. If the invariant is a small conjunction of facts, it can be plugged in modularly; if it’s a huge disjunction of special cases, it’s much harder to reuse or even comprehend. Thus simplicity can improve the scalability of the verification process itself, not just the single SMT query.\n\nFor further theoretical justification and more empirical evidence, we refer to the classical literature by Aws Albarghouthi and Kenneth L. McMillan such as [1].\n\n[1] *Beautiful Interpolants.* Aws Albarghouthi and Kenneth L. McMillan. CAV 2013: Proceedings of the 25th International Conference on Computer Aided Verification - Volume 8044 Pages 313 - 329\n\n---\n\nWe hope these clarify the confusion! We would greatly appreciate it if you could take our response into account when considering the final score."}]

Author rebuttal:

Meta-review: This paper introduces a novel, learning-based approach to generating simpler Craig interpolants for Linear Integer Arithmetic (LIA), a crucial component in formal verification. The proposed method uses a Graph Neural Network (GNN) to guide SMT solvers like Z3, and demonstrates a significant reduction in the complexity of the generated interpolants on a new, large-scale dataset created by the authors.

The reviewers are split. There is consensus on the novelty and originality of the work. However, there are significant disagreements, importantly along the axis of future significance and generalization. 

I am leaning to accept the paper on the basis of starting a new, hopefully fruitfull, interaction between ML and symblic methods.
Decision: Accept (poster)