論文の概要: Accelerating Floating-Point Satisfiability Solving via Gradient Normalization
- arxiv url: http://arxiv.org/abs/2610.08808v1
- Date: Mon, 14 Sep 2026 13:22:32 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-10-12 09:53:32.093706
- Title: Accelerating Floating-Point Satisfiability Solving via Gradient Normalization
- Title（参考訳）: 勾配正規化による浮動小数点満足度解の高速化
- Abstract要約: We present GradSAT, a novel framework that bridges optimization-based SMT solve with Multi-Task Learning (MTL)。
GradSATは、それぞれのSMT節を独立したMTLタスクとして扱うことにより、制約満足度プロセスを再構築する。
高度に最適化された2段階のハイブリッドパイプラインを通じてこれを実装している。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Satisfiability Modulo Theories (SMT) solvers are foundational to software verification, program analysis, and compiler testing, particularly over the theory of Quantifier-Free Floating-Point (QF_FP). While recent optimization-based SMT solvers have successfully applied gradient descent to continuous relaxations of logical formulas, they are fundamentally bottlenecked by gradient domination, a phenomenon where a small subset of difficult clauses hijacks the optimization trajectory, preventing the solver from satisfying the broader formula and trapping it in local minima. To overcome this, we present GradSAT, a novel framework that bridges optimization-based SMT solving with Multi-Task Learning (MTL). GradSAT reformulates the constraint satisfaction process by treating each SMT clause as an independent MTL task. By applying dynamic gradient normalization (GradNorm), GradSAT actively balances the gradient magnitudes across all clauses at runtime, systematically penalizing dominant gradients and accelerating lagging clauses to ensure uniform convergence. GradSAT implements this through a highly optimized, two-stage hybrid pipeline. First, a GPU-accelerated PyTorch backend leveraging symbolic compilation and operator fusion navigates the continuous relaxation to a high-quality basin. Second, the candidate assignment is handed off to a bit-precise local search engine to rapidly resolve the exact, rigorous assignment. By stabilizing the continuous search dynamics, GradSAT mitigates the brittleness of prior gradient-based solvers and provides a robust, highly parallelizable architecture for complex constraint solving.
- Abstract（参考訳）: Satisfiability Modulo Theories (SMT) は、ソフトウェア検証、プログラム分析、コンパイラテスト、特に量子自由浮動小数点(QF_FP)の理論に基礎を置いている。
最近の最適化ベースのSMTソルバは、論理式の連続緩和に勾配勾配を適用できたが、それらは基本的に勾配支配によってボトルネックになっている。
そこで我々は,Multi-Task Learning (MTL)による最適化に基づくSMT問題解決を橋渡しする新しいフレームワークであるGradSATを提案する。
GradSATは、それぞれのSMT節を独立したMTLタスクとして扱うことにより、制約満足度プロセスを再構築する。
動的勾配正規化(GradNorm)を適用することで、GradSATは実行時に全節にわたる勾配の等級を積極的にバランスさせ、系統的に支配的な勾配を罰し、ラギング節を加速して一様収束を保証する。
GradSATは高度に最適化された2段階のハイブリッドパイプラインを通じてこれを実装している。
まず、シンボリックコンパイルと演算子融合を活用したGPUアクセラレーションのPyTorchバックエンドが、継続的緩和を高品質な盆地へとナビゲートする。
次に、候補割当をビット精度のローカル検索エンジンに渡して、正確で厳密な割当を迅速に解決する。
連続探索のダイナミクスを安定化することにより、GradSATは事前勾配に基づく解法の脆さを軽減し、複雑な制約解決のための堅牢で高並列化可能なアーキテクチャを提供する。
関連論文リスト
- Scalable Floating-Point Satisfiability via Staged Optimization [4.212975258164135]
この研究は浮動小数点満足度を解くための新しいアプローチであるStageSATを導入している。
StageSATは、浮動小数点公式を、精度の向上の3段階における一連の最適化問題として再設定する。
論文 参考訳（メタデータ） (2026-01-08T01:51:46Z) - Gradient Descent with Provably Tuned Learning-rate Schedules [14.391648046717073]
そこで我々は,勾配に基づくアルゴリズムにおいて,因子を確実にチューニングするための新しい解析ツールを開発した。
我々の分析は、一般的に使用される活性化関数を持つニューラルネットワークに適用される。
論文 参考訳（メタデータ） (2025-12-04T18:49:58Z) - Decentralized Nonconvex Composite Federated Learning with Gradient Tracking and Momentum [78.27945336558987]
分散サーバ(DFL)はクライアント・クライアント・アーキテクチャへの依存をなくす。
非滑らかな正規化はしばしば機械学習タスクに組み込まれる。
本稿では,これらの問題を解決する新しいDNCFLアルゴリズムを提案する。
論文 参考訳（メタデータ） (2025-04-17T08:32:25Z) - Gradient-Variation Online Learning under Generalized Smoothness [56.38427425920781]
勾配変分オンライン学習は、オンライン関数の勾配の変化とともにスケールする後悔の保証を達成することを目的としている。
ニューラルネットワーク最適化における最近の取り組みは、一般化された滑らかさ条件を示唆し、滑らかさは勾配ノルムと相関する。
ゲームにおける高速収束と拡張逆最適化への応用について述べる。
論文 参考訳（メタデータ） (2024-08-17T02:22:08Z) - Optimal Algorithms for Stochastic Bilevel Optimization under Relaxed
Smoothness Conditions [9.518010235273785]
両レベル最適化のための完全リリップループ・ヘシアン・インバージョンフリーなアルゴリズム・フレームワークを提案する。
我々は、我々のアプローチを少し修正することで、より汎用的な多目的ロバストな双レベル最適化問題に対処できることを示した。
論文 参考訳（メタデータ） (2023-06-21T07:32:29Z) - Independent Component Alignment for Multi-Task Learning [2.5234156040689237]
マルチタスク学習(MTL)では、複数のタスクに共同で取り組むために単一のモデルを訓練する。
MTL最適化の安定性基準として線形勾配系の条件数を用いる。
本稿では,提案基準に基づく新しいMTL最適化手法であるAligned-MTLを提案する。
論文 参考訳（メタデータ） (2023-05-30T12:56:36Z) - Convergence of ease-controlled Random Reshuffling gradient Algorithms under Lipschitz smoothness [0.0]
非常に多くのスムーズで可能な非サイズの関数の平均を考慮し、この問題に対処するために2つの広く最小限のフレームワークを使用します。
IG/RRスキームの簡易制御による修正を定義する。
我々は、完全なバッチ勾配(L-BFGS)とIG/RR手法の実装の両方で実装を証明し、アルゴリズムが同様の計算作業を必要とすることを証明した。
論文 参考訳（メタデータ） (2022-12-04T15:26:36Z) - Faster One-Sample Stochastic Conditional Gradient Method for Composite
Convex Minimization [61.26619639722804]
滑らかで非滑らかな項の和として形成される凸有限サム目標を最小化するための条件勾配法(CGM)を提案する。
提案手法は, 平均勾配 (SAG) 推定器を備え, 1回に1回のサンプルしか必要としないが, より高度な分散低減技術と同等の高速収束速度を保証できる。
論文 参考訳（メタデータ） (2022-02-26T19:10:48Z) - Balancing Rates and Variance via Adaptive Batch-Size for Stochastic
Optimization Problems [120.21685755278509]
本研究は,ステップサイズの減衰が正確な収束に必要であるという事実と,一定のステップサイズがエラーまでの時間でより速く学習するという事実のバランスをとることを目的とする。
ステップサイズのミニバッチを最初から修正するのではなく,パラメータを適応的に進化させることを提案する。
論文 参考訳（メタデータ） (2020-07-02T16:02:02Z) - Towards Better Understanding of Adaptive Gradient Algorithms in
Generative Adversarial Nets [71.05306664267832]
適応アルゴリズムは勾配の歴史を用いて勾配を更新し、深層ニューラルネットワークのトレーニングにおいてユビキタスである。
本稿では,非コンケーブ最小値問題に対するOptimisticOAアルゴリズムの変種を解析する。
実験の結果,適応型GAN非適応勾配アルゴリズムは経験的に観測可能であることがわかった。
論文 参考訳（メタデータ） (2019-12-26T22:10:10Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。