PyDSMC

Statistical Model Checking for Neural Agents Using the Gymnasium Interface

PyDSMC is an open-source Python library for statistical model checking of neural agents on arbitrary Gymnasium environments. It is designed to be lightweight and easy-to-use while being based on established statistical methods to provide guarantees on the investigated agents' performances on various properties. Implementing the Gymnasium interface, PyDSMC is widely applicable and fully agnostic to the environments underlying implementation. It works out of the box with Stable-Baselines3 agents and any policy exposed as a predict callable.

PyDSMC is based on Deep Statistical Model Checking and aims to facilitate greater adoption of statistical model checking by simplifying its usage.

Please consult the accompanying paper for more details.

Why Deep Statistical Model Checking?

• The training and evaluation curves can differ greatly throughout training (see figure below)
  → Just inspecting the training curves leads to suboptimal policy extraction.
• Reporting an arbitrary number of seeds does not provide (statistical) guarantees
• Reporting min/max or standard deviation is much less informative than a confidence interval

Therefore, - PyDSMC advocates performing statistically backed model evaluations periodically throughout training to ensure a good extraction point, - and then analyzing the extracted policy post-training to provide unbiased and accurate performance results.

Feature highlights

• Environment-agnostic — evaluate any Gymnasium environment.
• Sound guarantees — confidence intervals from established statistical methods (Clopper–Pearson, Wilson, Hoeffding, DKW, Empirical Bernstein Stopping, …).
• Automatic method selection — PyDSMC picks a suitable statistical method from your property's parameters.
• Arbitrary properties — analyze return, crash probability, or any custom trajectory-based metric you define.
• Parallel evaluation — vectorized environments to speed up evaluations
• High-level interface — property definition and evaluation in only a few lines of code.

Quickstart

import gymnasium as gym
from pydsmc import Evaluator, create_predefined_property

# Any Gymnasium environment works.
env = gym.make("CartPole-v1")
evaluator = Evaluator(env=env)

# Analyze the achieved return with a sound confidence interval.
evaluator.register_property(
    create_predefined_property(
        property_id="return",
        epsilon=0.05,         # half-width of the confidence interval
        kappa=0.05,           # 1 - kappa is the confidence level
        relative_error=True,  # epsilon relative to the mean
        bounds=(0, 500),      # CartPole-v1 return is in [0, 500]
        sound=True,           # request a sound statistical method (expensive)
        gamma=0.99,           # discount factor for the return
    ),
)

# `predict_fn` returns an action for a batch of observations.
results = evaluator.eval(
    # This `predict_fn` would be replaced with your trained agent's policy.
    predict_fn=lambda obs, **_: (env.action_space.sample(), None),
    stop_on_convergence=True,  # Stop evaluating on property convergence
    episode_limit=2_000,       # Stop if not converged after 2,000 episodes
)

See Usage for a full walkthrough and Examples for end-to-end scripts on real trained agents.

Where to next?

• Installation — install from PyPI and set up a dev environment.
• Usage — properties, the evaluator, and statistical-method selection.
• Examples — complete scripts on trained agents.
• API Reference — the full public API.
• Citation — the paper and BibTeX entry.