Notice: The reproducibility variables underlying each score are classified using an automated LLM-based pipeline, validated against a manually labeled dataset. LLM-based classification introduces uncertainty and potential bias; scores should be interpreted as estimates. Full accuracy metrics and methodology are described in Coakley et alK. L. Coakley, T. Snelleman, H. Hoos, and O. E. Gundersen, "The embrace of open science: An analysis of a decade of AI research and 56 800 conference papers," Under Review, 2026..
Learning Simple Interpolants for Linear Integer Arithmetic
Authors: Minchao Wu, Naoki Kobayashi
NeurIPS 2025 | Venue PDF | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Empirical evaluations demonstrate the effectiveness of our approach. When integrated with state-of-the-art interpolation solvers such as Z3 [9], our model achieves a reduction in interpolant complexity of up to 47.3%. When applied to older solvers, the reduction rate increases to 69.1%. |
| Researcher Affiliation | Academia | Minchao Wu The University of Tokyo EMAIL Naoki Kobayashi The University of Tokyo EMAIL |
| Pseudocode | No | The paper describes the model architecture and computation flow in sections 3.2-3.6 using text, mathematical formulas, and diagrams (Figure 1), but does not contain a dedicated pseudocode or algorithm block. |
| Open Source Code | Yes | The code and datasets will be available at https://github.com/hopv/scilia. |
| Open Datasets | Yes | As no such dataset exists in the literature to our knowledge, we construct one ourselves and describe the generation process in detail. ... The code and datasets will be available at https://github.com/hopv/scilia. |
| Dataset Splits | Yes | The full dataset is split into training and testing sets using an 80% 20% ratio. |
| Hardware Specification | Yes | Training is performed using Py Torch s Metal backend [27, 2] and takes approximately 1.5 days on a single Mac Book Pro with the M1 MAX chip. |
| Software Dependencies | No | While the paper mentions 'Py Torch s Metal backend' and 'Z3', it does not provide specific version numbers for PyTorch or Z3 used in the experiments. The references for PyTorch [27] (2019) and Z3 [9] (2008) are general citations and do not specify the exact versions used for current experiments. |
| Experiment Setup | Yes | In the experiments below, we 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 is initially set to 1e-3 and is reduced by a factor of 0.5 every 50 epochs. |