Inductive Synthesis for Probabilistic Programs Reaches New Horizons

• URL: http://arxiv.org/abs/2101.12683v1
• Date: Fri, 29 Jan 2021 16:59:00 GMT
• Title: Inductive Synthesis for Probabilistic Programs Reaches New Horizons
• Authors: Roman Andriushchenko, Milan Ceska, Sebastian Junges, Joost-Pieter Katoen
• Abstract summary: We present a novel method for the automated synthesis of probabilistic programs. The starting point is a program sketch representing a finite family of finite-state Markov chains with related but distinct topologies, and a PCTL specification. The method builds on a novel inductive oracle that greedily generates counter-examples (CEs) for violating programs and uses them to prune the family.
• Score: 0.5505634045241288
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: This paper presents a novel method for the automated synthesis of probabilistic programs. The starting point is a program sketch representing a finite family of finite-state Markov chains with related but distinct topologies, and a PCTL specification. The method builds on a novel inductive oracle that greedily generates counter-examples (CEs) for violating programs and uses them to prune the family. These CEs leverage the semantics of the family in the form of bounds on its best- and worst-case behaviour provided by a deductive oracle using an MDP abstraction. The method further monitors the performance of the synthesis and adaptively switches between the inductive and deductive reasoning. Our experiments demonstrate that the novel CE construction provides a significantly faster and more effective pruning strategy leading to acceleration of the synthesis process on a wide range of benchmarks. For challenging problems, such as the synthesis of decentralized partially-observable controllers, we reduce the run-time from a day to minutes.

Related papers

• Lightning Grasp: High Performance Procedural Grasp Synthesis with Contact Fields [55.014365168982884]
  We present Lightning Grasp, a novel high-performance procedural grasp synthesis algorithm.<n>It achieves orders-of-magnitude speedups over state-of-the-art approaches.<n>We open-source our system to propel further innovation in robotic manipulation.
  arXiv  Detail & Related papers  (2025-11-10T18:59:44Z)
• Taming Imperfect Process Verifiers: A Sampling Perspective on Backtracking [54.43083499412643]
  Test-time algorithms that combine the generative power of language models with process verifiers offer a promising lever for eliciting new reasoning capabilities.<n>We introduce a new process-guided test-time sampling algorithm, VGB, which uses theoretically grounded backtracking to achieve provably better robustness to verifier errors.
  arXiv  Detail & Related papers  (2025-10-03T16:21:14Z)
• Learning Symbolic Persistent Macro-Actions for POMDP Solving Over Time [52.03682298194168]
  This paper proposes an integration of temporal logical reasoning and Partially Observable Markov Decision Processes (POMDPs)<n>Our method leverages a fragment of Linear Temporal Logic (LTL) based on Event Calculus (EC) to generate emphpersistent (i.e., constant) macro-actions.<n>These macro-actions guide Monte Carlo Tree Search (MCTS)-based POMDP solvers over a time horizon.
  arXiv  Detail & Related papers  (2025-05-06T16:08:55Z)
• SymRTLO: Enhancing RTL Code Optimization with LLMs and Neuron-Inspired Symbolic Reasoning [18.40402135952776]
  This paper presents SymRTLO, a novel neuron-symbolic RTL optimization framework. A symbolic module is proposed for analyzing and optimizing finite state machine (FSM) logic. Experiments on the RTL-Rewriter benchmark with Synopsys Design Compiler and Yosys show that SymRTLO improves power, performance, and area (PPA) by up to 43.9%, 62.5%, and 51.1%, respectively.
  arXiv  Detail & Related papers  (2025-04-14T16:15:55Z)
• BRiTE: Bootstrapping Reinforced Thinking Process to Enhance Language Model Reasoning [78.63421517563056]
  Large Language Models (LLMs) have demonstrated remarkable capabilities in complex reasoning tasks. We present a unified probabilistic framework that formalizes LLM reasoning through a novel graphical model. We introduce the Bootstrapping Reinforced Thinking Process (BRiTE) algorithm, which works in two steps.
  arXiv  Detail & Related papers  (2025-01-31T02:39:07Z)
• Tango*: Constrained synthesis planning using chemically informed value functions [1.6787839854263589]
  We introduce a simple guided search which allows solving the starting material-constrained synthesis planning problem. We find the Tango* cost function catalyses strong improvements for the bidirectional DESP methods. Our method achieves lower wall clock times while proposing synthetic routes of similar length, a common metric for route quality.
  arXiv  Detail & Related papers  (2024-12-04T16:14:02Z)
• Double-Ended Synthesis Planning with Goal-Constrained Bidirectional Search [27.09693306892583]
  We present a formulation of synthesis planning with starting material constraints. We propose Double-Ended Synthesis Planning (DESP), a novel CASP algorithm under a bidirectional graph search scheme. DESP can make use of existing one-step retrosynthesis models, and we anticipate its performance to scale as these one-step model capabilities improve.
  arXiv  Detail & Related papers  (2024-07-08T18:56:00Z)
• Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic [4.60607942851373]
  We consider the problem of automatically synthesizing formal specifications from system executions. Most of the classical approaches for synthesizing temporal logic formulas aim at minimizing the size of the formula. We formalize this notion and devise a learning algorithm that synthesizes concise formulas having bounded lookahead.
  arXiv  Detail & Related papers  (2023-10-26T14:13:15Z)
• Smoothing Methods for Automatic Differentiation Across Conditional Branches [0.0]
  Smooth interpretation (SI) approximates the convolution of a program's output with a Gaussian kernel, thus smoothing its output in a principled manner. We combine SI with automatic differentiation (AD) to efficiently compute gradients of smoothed programs. We propose a novel Monte Carlo estimator that avoids the underlying assumptions by estimating the smoothed programs' gradients through a combination of AD and sampling.
  arXiv  Detail & Related papers  (2023-10-05T15:08:37Z)
• INVICTUS: Optimizing Boolean Logic Circuit Synthesis via Synergistic Learning and Search [18.558280701880136]
  State-of-the-art logic synthesis algorithms have a large number of logic minimizations. INVICTUS generates a sequence of logic minimizations based on a training dataset of previously seen designs.
  arXiv  Detail & Related papers  (2023-05-22T15:50:42Z)
• Forward LTLf Synthesis: DPLL At Work [1.370633147306388]
  We propose a new AND-OR graph search framework for synthesis of Linear Temporal Logic on finite traces (LTLf) Within such framework, we devise a procedure inspired by the Davis-Putnam-Logemann-Loveland (DPLL) algorithm to generate the next available agent-environment moves. We also propose a novel equivalence check for search nodes based on syntactic equivalence of state formulas.
  arXiv  Detail & Related papers  (2023-02-27T14:33:50Z)
• Formal Controller Synthesis for Markov Jump Linear Systems with Uncertain Dynamics [64.72260320446158]
  We propose a method for synthesising controllers for Markov jump linear systems. Our method is based on a finite-state abstraction that captures both the discrete (mode-jumping) and continuous (stochastic linear) behaviour of the MJLS. We apply our method to multiple realistic benchmark problems, in particular, a temperature control and an aerial vehicle delivery problem.
  arXiv  Detail & Related papers  (2022-12-01T17:36:30Z)
• Revisiting GANs by Best-Response Constraint: Perspective, Methodology, and Application [49.66088514485446]
  Best-Response Constraint (BRC) is a general learning framework to explicitly formulate the potential dependency of the generator on the discriminator. We show that even with different motivations and formulations, a variety of existing GANs ALL can be uniformly improved by our flexible BRC methodology.
  arXiv  Detail & Related papers  (2022-05-20T12:42:41Z)
• Faster One-Sample Stochastic Conditional Gradient Method for Composite Convex Minimization [61.26619639722804]
  We propose a conditional gradient method (CGM) for minimizing convex finite-sum objectives formed as a sum of smooth and non-smooth terms. The proposed method, equipped with an average gradient (SAG) estimator, requires only one sample per iteration. Nevertheless, it guarantees fast convergence rates on par with more sophisticated variance reduction techniques.
  arXiv  Detail & Related papers  (2022-02-26T19:10:48Z)
• Process Discovery for Structured Program Synthesis [70.29027202357385]
  A core task in process mining is process discovery which aims to learn an accurate process model from event log data. In this paper, we propose to use (block-) structured programs directly as target process models. We develop a novel bottom-up agglomerative approach to the discovery of such structured program process models.
  arXiv  Detail & Related papers  (2020-08-13T10:33:10Z)
• Combining Deep Learning and Optimization for Security-Constrained Optimal Power Flow [94.24763814458686]
  Security-constrained optimal power flow (SCOPF) is fundamental in power systems. Modeling of APR within the SCOPF problem results in complex large-scale mixed-integer programs. This paper proposes a novel approach that combines deep learning and robust optimization techniques.
  arXiv  Detail & Related papers  (2020-07-14T12:38:21Z)
• Creating Synthetic Datasets via Evolution for Neural Program Synthesis [77.34726150561087]
  We show that some program synthesis approaches generalize poorly to data distributions different from that of the randomly generated examples. We propose a new, adversarial approach to control the bias of synthetic data distributions and show that it outperforms current approaches.
  arXiv  Detail & Related papers  (2020-03-23T18:34:15Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.