cs.LGMar 8, 2026

Using GPUs And LLMs Can Be Satisfying for Nonlinear Real Arithmetic Problems

Authors: Christopher Brix, Julia Walczak, Nils Lommen, Thomas Noll

Organizations: RWTH Aachen University

Read PDF
Ask AI
Cite

Copy citation

DOINot available for this paper

Abstract

Solving quantifier-free non-linear real arithmetic (NRA) problems is a computationally hard task. To tackle this problem, prior work proposed a promising approach based on gradient descent. In this work, we extend their ideas and combine LLMs and GPU acceleration to obtain an efficient technique. We have implemented our findings in the novel SMT solver GANRA (GPU Accelerated solving of Nonlinear Real Arithmetic problems). We evaluate GANRA on two different NRA benchmarks and demonstrate significant improvements over the previous state of the art. In particular, on the Sturm-MBO benchmark, we can prove satisfiability for more than five times as many instances in less than 1/20th of the previous state-of-the-art runtime.

Figures & tables

  Z3CVC5ugotNLNRAgoGANRA (ours)
      seq.manualLLM
     ϵ={\epsilon}=10−410^{-4}0010−410^{-4}10−410^{-4}
Kis.SAT [ ↑\uparrow ]3416273939184040
avg. runtime [s] [ ↓\downarrow ]38.01--24.7230.45-9.139.61
MBOSAT [ ↑\uparrow ]1010610575738
avg. runtime [s] [ ↓\downarrow ]--139.08-333.626.3914.8635.92
Table 1: Toolkit evaluation on the Kissing and Sturm-MBO benchmarks. We report the average runtime of those instances that could be verified by all tools that can prove satisfiability for at least 30 (Kissing) and 10 (Sturm-MBO) instances. ↑\uparrow ( ↓\downarrow ): Higher (lower) values are better.
Figure 1: Comparison of Z3 and GANRA on Sturm-MBO-like problems with varying number of summands and NN . White indicates 0% success at finding a satisfying input, black 100%.
 KissingSturm-MBO
L2O versionGANRANRAgougotNLGANRANRAgougotNL
SAT [ ↑\uparrow ]403839575756
avg. runtime [s] [ ↓\downarrow ]9.626.7912.6938.4242.92113.01
Table 2: Comparison of the different L2O definitions proposed in our work vs. ( Cimatti et al., 2022 ) and ( Liu et al., 2023 ) . We integrated their L2O definitions into GANRA, so all results benefit from GPU acceleration. ↑\uparrow ( ↓\downarrow ): Higher (lower) values are better.
Appendix figures & tables1 asset

Supplementary material from the paper’s appendix.

Appendix

 Z3CVC5ugotNLNRAgo
 OrigIntervalOrigIntervalOrigIntervalOrigInterval
SAT [ ↑\uparrow ]100010962
Appendix
Table 3: Performance of baseline tools on the original vs. a modified version of the Sturm-MBO benchmark.
More in this topic

Satisfiability Modulo Theories

Satisfiability modulo theories (SMT) checks whether logical formulas are satisfiable under theories such as arithmetic, strings, and bit-vectors.

See all 19 papers

Explore similar work

CardsList

  1. SOVER: Formal Certification of Optimization Reformulations via LLM-Assisted SMT Verification

    Sep 1, 2026Swapnil Bhattacharyya, Mayank BaranwalLarge Language Model-Guided Optimization

    TCS Research, Mumbai · Indian Institute of Technology Bombay

  2. Accelerating the Mitigation of LLM Inference Nondeterminism Across GPU Architectures

    Sep 22, 2026Liam Cooper, Shinnung Jeong, Hyeran Jeon +2GPU Kernel OptimizationLLM Inference Acceleration

    Georgia Institute of Technology · University of California, Merced

  3. Scaling Nonlinear Optimization: Many Problems One GPU

    Jun 24, 2026John Viljoen, Johanna Haffner, Masayoshi Tomizuka +1Trajectory OptimizationGPU Acceleration

    Department of Mechanical Engineering, University of California, Berkeley, CA, USA · Department of Biosystems Science and Engineering, ETH Zürich, Switzerland