Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Christopher Brix, Julia Walczak, Nils Lommen, Thomas Noll

TL;DR

This work combines LLMs and GPU acceleration to obtain an efficient technique for solving quantifier-free non-linear real arithmetic problems and implements its findings in the novel SMT solver GANRA (GPU Accelerated solving of Nonlinear Real Arithmetic problems).

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.

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

TL;DR

This work combines LLMs and GPU acceleration to obtain an efficient technique for solving quantifier-free non-linear real arithmetic problems and implements its findings in the novel SMT solver GANRA (GPU Accelerated solving of Nonlinear Real Arithmetic problems).

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.
Paper Structure (34 sections, 5 equations, 1 figure, 3 tables)

This paper contains 34 sections, 5 equations, 1 figure, 3 tables.

Table of Contents

  1. Introduction
  2. Contributions:
  3. Structure:
  4. Related Work
  5. Gradient Descent as a GPU-accelerated Heuristic
  6. Logic-to-Optimization Technique
  7. Example
  8. Ensuring Soundness
  9. Manual Optimization for GPU Acceleration
  10. Kissing
  11. Sturm-MBO
  12. LLM-Based Optimization for GPU Acceleration
  13. Case Studies
  14. Kissing
  15. Sturm-MBO
  16. ...and 19 more sections

Figures (1)

  • Figure 1: Comparison of Z3 and GANRA on Sturm-MBO-like problems with varying number of summands and $N$. White indicates 0% success at finding a satisfying input, black 100%.