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

TL;DR

This paper introduces GANRA, a GPU-accelerated SMT solver combining LLMs and gradient descent to efficiently solve nonlinear real arithmetic problems, significantly outperforming previous methods on benchmark tests.

Contribution

The paper presents a novel SMT solver that integrates LLMs and GPU acceleration, achieving substantial improvements in solving nonlinear real arithmetic problems.

Findings

Proves satisfiability for over five times more instances on the Sturm-MBO benchmark.

Reduces runtime to less than 1/20th of previous state-of-the-art.

Demonstrates the effectiveness of combining LLMs with GPU acceleration.

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.