Stochastic constraints, which incorporate both deterministic parameters and random variables, extend classical deterministic constraints by explicitly accounting for uncertainty. These constraints are increasingly prevalent in data science, artificial intelligence, and bioinformatics; however, solving them requires addressing quantitative satisfaction problems that remain a significant challenge in computer science. In this paper, we propose a novel framework for deciding deterministic parameters that maximize the satisfaction probability. Our approach features a unique synergy between stochastic optimization and symbolic techniques: at the high level, it employs \emph{oracle-based stochastic gradient descent} to identify high-quality parameter candidates, while at the low level, it utilizes \emph{interval arithmetic} to compute rigorously certified lower bounds. This framework produces a sequence of sound and increasingly tight lower bounds for the true maximum satisfaction probability, supported by a high-probability convergence guarantee. We demonstrate the effectiveness and efficiency of our approach through its application to Stochastic Satisfiability Modulo Theories (SSMT) problems and a stochastic trajectory planning task.
翻译:随机约束融合了确定性参数与随机变量,通过显式建模不确定性扩展了经典确定性约束。这类约束在数据科学、人工智能和生物信息学中日益常见,然而求解此类问题需要处理定量满意度问题,这仍是计算机科学领域的重要挑战。本文提出一种新颖框架,用于确定最大化满足概率的确定性参数。该方法的独特之处在于将随机优化与符号技术有机结合:在高层采用基于Oracle的随机梯度下降识别高质量候选参数,在低层利用区间算术严格计算经认证的下界。该框架可为真实最大满足概率生成一系列可靠且逐步紧化的下界,并具有高概率收敛保证。通过将其应用于随机可满足性模理论问题和随机轨迹规划任务,我们验证了该方法的高效性与有效性。