Log-Derivative Trick for Parametric Markov Chains

Arthur Gall; Ichiro Hasuo; Thomas Seiller

cs.LGOct 27, 2026

Log-Derivative Trick for Parametric Markov Chains

Authors: Arthur Gall, Ichiro Hasuo, Thomas Seiller

Organizations: National Institute of Informatics, Tokyo, Japan · SOKENDAI (The Graduate University for Advanced Studies), Kanagawa, Japan · Imiron Co., Ltd., Tokyo, Japan · CNRS, France

Abstract

Optimizing expected rewards and reachability probabilities in parametric Markov chains (pMCs) is central to the analysis and synthesis of probabilistic systems with loops. While traditional symbolic synthesis approaches--such as parameter lifting and rational function generation--suffer from scalability bottlenecks, gradient-based optimization emerges as an effective alternative. However, existing gradient-based techniques still rely on symbolic gradient computation--such as solving large linear systems--over the global state space, inheriting scalability limits. Finite-horizon approximation is possible but introduces uncontrollable bias. In this paper, we introduce a scalable Monte Carlo gradient estimator based on a measure-theoretic generalization of the log-derivative trick. We prove that our estimator provides unbiased gradient estimates under almost-sure termination and standard regularity conditions. Crucially, our method avoids global state-space materialization and linear system solving entirely: it operates purely along sampled trajectories, requiring only black-box evaluations of local transition probabilities (or densities) and their derivatives. Unlike existing pMC techniques that are fundamentally restricted to finite discrete systems, our measure-theoretic framework naturally extends to continuous and general $σ$ -finite state spaces. Empirical evaluations on synthetic discrete pMCs and continuous-state case studies demonstrate that our method scales to state spaces far beyond the reach of existing solvers, significantly reducing execution time without introducing bias.

Figures & tables

Panel of Figure 4 — Figure 4: Experiments for RQ1: impact of the number of parameters $k$ on gradient estimation runtime, and average precision. Values are averaged over 25 synthetic pMC benchmarks, each generated with 10 times more states than parameters.

Panel of Figure 5 — Figure 5: Experiments for RQ2: gradient descent with a strict 100-second timeout, averaged over 100 pMCs with 5,000 states and 100 parameters, comparing optimizers.

Panel of Figure 6 — Figure 6: Experiments for RQ2: gradient descent with a strict 100-second timeout, averaged over 100 pMCs with 5,000 states and 100 parameters, comparing gradient computation methods.

Panel of Figure 7 — Figure 7: Experiments for RQ3: impact of the sample size $N$ on gradient estimation runtime, cosine similarity, and normalized distance. Results are averaged over 100 pMC benchmarks.

Panel of Figure 8 — Figure 8: Experiments for RQ4: Execution time and gradient approximation precision across varying state-space sizes. Values are averaged over 25 synthetic pMC benchmarks, each with $10^{2}$ parameters.

Panel of Figure 9 — Figure 9: Evaluation for RQ5: Gradient-based optimization on continuous pMCs ( $10^{4}$ path samples per step over $10^{3}$ iterations). (a) Benchmark $T_{3}$ initialized at $p=1$ ; (b) Benchmark $T_{4}$ initialized at $(p,q)=(0.5,0.5)$ . The analytically computed optimal rewards are indicated by closed-form expressions in bold.

Markov Chains

See all 31 papers

PAC Approximation and DIRECT Optimization for Parametric Markov Models
Aug 3, 2026Zhiming Chi, Ying Liu, Andrea Turrini +2Robust Markov Decision Processes Markov Decision Processes
Key Laboratory of System Software (Chinese Academy of Sciences), Beijing, China · Institute of Software, Chinese Academy of Sciences, Beijing, China · University of Chinese Academy of Sciences, Beijing, China +2
GradInf: Gradient Estimation as Probabilistic Inference
Jul 8, 2026Gaurav Arya, Mathieu Huot, Moritz Schauer +2Probabilistic Programming
Carnegie Mellon University, Pittsburgh, USA · Massachusetts Institute of Technology, Cambridge, USA · Chalmers University of Technology & University of Gothenburg, Gothenburg, Sweden +1
Exact Discrete Stochastic Simulation with Deep-Learning-Scale Gradient Optimization
Feb 23, 2026Jose M. G. Vilar, Leonor SaizStraight-Through Estimator Markov Chains
Biofisika Institute (CSIC, UPV/EHU), University of the Basque Country (UPV/EHU), P.O. Box 644, 48080 Bilbao, Spain · IKERBASQUE, Basque Foundation for Science, 48011 Bilbao, Spain · Department of Biomedical Engineering, University of California, 451 E. Health Sciences Drive, Davis, CA 95616, USA

Aug 3, 2026J/K move · Enter open · S save

PAC Approximation and DIRECT Optimization for Parametric Markov Models

Zhiming Chi, Ying Liu, Andrea Turrini, Lijun Zhang+1

Key Laboratory of System Software (Chinese Academy of Sciences), Beijing, China · Institute of Software, Chinese Academy of Sciences, Beijing, China · University of Chinese Academy of Sciences, Beijing, China+2

Robust Markov Decision Processes Markov Decision Processes Markov Models Formal Verification

Open paper AskPDF arXiv

In this paper, we consider the parameter synthesis and optimization problem for parametric Markov decision processes (pMDPs), the extension of classical MDPs where exact probability values are replaced by parametric expressions. Computing the rational function

f_{\lsf}

that maps parameter valuations to the satisfaction value of a PRCTL property

\lsf

is a computationally expensive task, particularly for pMDPs where the optimal policy may vary across the parameter space. We adopt the scenario approach to efficiently synthesize a probably approximately correct (PAC) approximation

\ApproxFunOfProperty{f}

f_{\lsf}

: by sampling parameter configurations and solving a linear program, we obtain a polynomial approximation whose error margin

\margin

is guaranteed, with prescribed confidence, for all but an

\errorRate

-fraction of the parameter domain under the sampling distribution. We further show how this PAC framework can be combined with statistical model checking (SMC), enabling the analysis of black-box parametric models. Building on the PAC approximation, we integrate the DIRECT (DIviding RECTangles) algorithm for derivative-free global optimization over the parameter space. We establish conditional optimality-gap guarantees: under explicit Lipschitz and PAC-good-set assumptions, the difference between the true optimum

f_{\lsf}(\parameters^{*})

and the value found by DIRECT is bounded by a partition-diameter term and, in the PAC case, an additional approximation-error term. An empirical evaluation on 2997 benchmarks focuses on the new DIRECT-based optimization component. The results show that DIRECT variants solve fewer instances than the scenario optimizer, but on their common successful instances they often return slightly better objective values and usually run faster, while remaining close to the scenario values within the PAC margin.

Abstract

Markov Chains

Explore similar work

PAC Approximation and DIRECT Optimization for Parametric Markov Models

GradInf: Gradient Estimation as Probabilistic Inference

Exact Discrete Stochastic Simulation with Deep-Learning-Scale Gradient Optimization