Showing 1–2 of 2 results for author: Oyabu, Y

Control-Data Separation and Logical Condition Propagation for Efficient Inference on Probabilistic Programs

Authors: Ichiro Hasuo, Yuichiro Oyabu, Clovis Eberhart, Kohei Suenaga, Kenta Cho, Shin-ya Katsumata

Abstract: We present a novel sampling framework for probabilistic programs. The framework combines two recent ideas -- \emph{control-data separation} and \emph{logical condition propagation} -- in a nontrivial manner so that the two ideas boost the benefits of each other. We implemented our algorithm on top of Anglican. The experimental results demonstrate our algorithm's efficiency, especially for programs… ▽ More We present a novel sampling framework for probabilistic programs. The framework combines two recent ideas -- \emph{control-data separation} and \emph{logical condition propagation} -- in a nontrivial manner so that the two ideas boost the benefits of each other. We implemented our algorithm on top of Anglican. The experimental results demonstrate our algorithm's efficiency, especially for programs with while loops and rare observations. △ Less

Submitted 29 September, 2023; v1 submitted 5 January, 2021; originally announced January 2021.

Ranking and Repulsing Supermartingales for Reachability in Probabilistic Programs

Authors: Toru Takisaka, Yuichiro Oyabu, Natsuki Urabe, Ichiro Hasuo

Abstract: Computing reachability probabilities is a fundamental problem in the analysis of probabilistic programs. This paper aims at a comprehensive and comparative account on various martingale-based methods for over- and under-approximating reachability probabilities. Based on the existing works that stretch across different communities (formal verification, control theory, etc.), we offer a unifying acc… ▽ More Computing reachability probabilities is a fundamental problem in the analysis of probabilistic programs. This paper aims at a comprehensive and comparative account on various martingale-based methods for over- and under-approximating reachability probabilities. Based on the existing works that stretch across different communities (formal verification, control theory, etc.), we offer a unifying account. In particular, we emphasize the role of order-theoretic fixed points---a classic topic in computer science---in the analysis of probabilistic programs. This leads us to two new martingale-based techniques, too. We give rigorous proofs for their soundness and completeness. We also make an experimental comparison using our implementation of template-based synthesis algorithms for those martingales. △ Less

Submitted 14 September, 2018; v1 submitted 27 May, 2018; originally announced May 2018.

Journal ref: Automated Technology for Verification and Analysis. ATVA 2018. Lecture Notes in Computer Science, vol 11138. Springer, Cham