כתבה
arXiv cs.LG ·
האצת פתרון סימטריה נוזלית על ידי תיקון גרדיאנטים
Accelerating Floating-Point Satisfiability Solving via Gradient Normalization
מאמר חדש עוסק באצת פתרון סימטריה נוזלית על ידי תיקון גרדיאנטים. המחברים מציגים פרקטיקה חדשה שמשתמשת בלמידה משולבת לפתרון בעיות סימטריה. הם מציעים פתרון חדש, GradSAT, שמשתמש בשיטת תיקון גרדיאנטים דינמי לאצת פתרון. המאמר כולל תיאור של הפרקטיקה והפתרון, כמו גם תוצאות ניסויים.
תקציר מקורי באנגליתarXiv:2610.08808v1 Announce Type: cross 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 satis
קרא במקור המקורי
arxiv.org
פתח כתבה מקורית