論文の概要: Using GPUs And LLMs Can Be Satisfying for Nonlinear Real Arithmetic Problems
- arxiv url: http://arxiv.org/abs/2603.07764v1
- Date: Sun, 08 Mar 2026 18:59:06 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-03-10 15:13:15.201933
- Title: Using GPUs And LLMs Can Be Satisfying for Nonlinear Real Arithmetic Problems
- Title(参考訳): 非線形実算数問題に対するGPUとLLMの満足度
- Authors: Christopher Brix, Julia Walczak, Nils Lommen, Thomas Noll,
- Abstract要約: 本稿では,量化子自由な非線形実算術問題の解法を提案する。
従来の最先端ランタイムの1/20未満のインスタンスの5倍以上の満足度を示す。
特に、Sturm-MBOベンチマークでは、以前の最先端ランタイムの1/20未満のインスタンスの5倍以上の満足度を証明できます。
- 参考スコア(独自算出の注目度): 1.6682715542079578
- License: http://creativecommons.org/licenses/by/4.0/
- 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.
- Abstract(参考訳): 量化子なし非線形実算術(NRA)問題の解法は計算的に難しい課題である。
この問題に対処するため、先行研究は勾配降下に基づく有望なアプローチを提案した。
本研究では,それらのアイデアを拡張し,LLMとGPUアクセラレーションを組み合わせた効率的な手法を提案する。
我々は,SMTソルバであるGANRA (GPU Accelerated solve of non real Arithmetic problem) において,この結果を実装した。
GANRAを2つの異なるNRAベンチマークで評価し、従来の最先端よりも大幅に改善したことを示す。
特に、Sturm-MBOベンチマークでは、以前の最先端ランタイムの1/20未満のインスタンスの5倍以上の満足度を証明できます。
関連論文リスト
- SciML Agents: Write the Solver, Not the Solution [69.5021018644143]
敵の"ミスリーディング"問題の診断データセットと,1,000種類のODEタスクの大規模ベンチマークという,2つの新しいデータセットを紹介した。
オープンおよびクローズドソース LLM モデルについて, (i) 誘導型とガイド型, (ii) オフ・ザ・シェルフ対微調整型という2つの軸に沿って評価した。
予備的な結果は、慎重なプロンプトと微調整により、単純なODE問題を確実に解決できる特殊なLLMエージェントが得られることを示唆している。
論文 参考訳(メタデータ) (2025-09-12T02:53:57Z) - BEATS: Optimizing LLM Mathematical Capabilities with BackVerify and Adaptive Disambiguate based Efficient Tree Search [22.672130194493793]
大規模言語モデル(LLM)は、幅広いタスクやドメインで例外的なパフォーマンスを示している。
彼らは数学の厳密で論理的な性質のため、数学の問題を解くのに依然として困難に直面している。
本稿では,数学的問題解決能力を高めるための新しい手法BEATSを提案する。
論文 参考訳(メタデータ) (2024-09-26T15:47:42Z) - Deep Unrolling Networks with Recurrent Momentum Acceleration for Nonlinear Inverse Problems [3.9248546555042365]
本稿では,長期記憶リカレントニューラルネットワーク(LSTM-RNN)を用いて運動量加速過程をシミュレートするリカレント運動量加速(RMA)フレームワークを提案する。
RMAを学習勾配降下法(LPGD)と学習原始双対法(LPD)の2つの一般的なDuNetに適用し,それぞれLPGD-RMAとLPD-RMAとなる。
非線形デコンボリューション問題と境界値が制限された電気インピーダンストモグラフィ問題という2つの非線形逆問題に関する実験結果を提供する。
論文 参考訳(メタデータ) (2023-07-30T03:59:47Z) - Stochastic Gradient Methods with Preconditioned Updates [47.23741709751474]
このような問題に対するアルゴリズムはいくつかあるが、既存の手法は、スケールが悪く、あるいは条件が悪ければ、しばしばうまく機能しない。
ここではハッチンソンの対角ヘッセン近似のアプローチに基づく前提条件を含む。
我々は滑らかさとPL条件が仮定されるときの収束性を証明する。
論文 参考訳(メタデータ) (2022-06-01T07:38:08Z) - An Accelerated Variance-Reduced Conditional Gradient Sliding Algorithm
for First-order and Zeroth-order Optimization [111.24899593052851]
条件勾配アルゴリズム(Frank-Wolfeアルゴリズムとも呼ばれる)は、最近、機械学習コミュニティで人気を取り戻している。
ARCSは、ゼロ階最適化において凸問題を解く最初のゼロ階条件勾配スライディング型アルゴリズムである。
1次最適化では、ARCSの収束結果は、勾配クエリのオラクルの数で、従来のアルゴリズムよりも大幅に優れていた。
論文 参考訳(メタデータ) (2021-09-18T07:08:11Z) - Kernel methods through the roof: handling billions of points efficiently [94.31450736250918]
カーネル法は、非パラメトリック学習に対するエレガントで原則化されたアプローチを提供するが、今のところ大規模な問題ではほとんど利用できない。
最近の進歩は、最適化、数値線形代数、ランダム射影など、多くのアルゴリズム的アイデアの利点を示している。
ここでは、これらの取り組みをさらに進めて、GPUハードウェアを最大限に活用する解決器を開発し、テストする。
論文 参考訳(メタデータ) (2020-06-18T08:16:25Z) - MPLP++: Fast, Parallel Dual Block-Coordinate Ascent for Dense Graphical
Models [96.1052289276254]
この研究は、人気のあるDual Block-Coordinate Ascent原則に基づく新しいMAP-solverを導入している。
驚いたことに、性能の低い解法に小さな変更を加えることで、既存の解法を大きなマージンで大幅に上回る新しい解法MPLP++を導出します。
論文 参考訳(メタデータ) (2020-04-16T16:20:53Z) - Lagrangian Decomposition for Neural Network Verification [148.0448557991349]
ニューラルネットワーク検証の基本的なコンポーネントは、出力が取ることのできる値のバウンダリの計算である。
ラグランジアン分解に基づく新しい手法を提案する。
ランニングタイムのごく一部で、既成の解法に匹敵するバウンダリが得られることを示す。
論文 参考訳(メタデータ) (2020-02-24T17:55:10Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。