用大模型和显卡加速，让非线性实数问题求解快五倍以上。
Using GPUs And LLMs Can Be Satisfying for Nonlinear Real Arithmetic Problems
- 结合大模型与显卡并行计算，提升非线性实数逻辑求解效率。
- 在Sturm-MBO基准上，求解成功率超前代5倍，耗时不足1/20。
- 适合需要快速验证复杂数学约束的系统验证与形式化方法研究者。
求解无量词非线性实数算术（NRA）问题是计算上极具挑战的任务。此前工作提出基于梯度下降的有前景方法。本文扩展该思路，将大语言模型（LLM）与GPU加速结合，实现高效求解技术。我们将其集成于新型SMT求解器GANRA（GPU加速的非线性实数算术求解）。在两个不同的NRA基准上评估，结果显著优于现有最先进水平。尤其在Sturm-MBO基准上，可证明超过五倍于以往的实例满足性，且耗时不足先前最优方案的1/20。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。