Library for creating circuits that encode discrete distributions.
Project description
py-aiger-coins
Library for creating circuits that encode discrete distributions and Markov Decision Processes. The name comes from the random bit model of drawing from discrete distributions using coin flips.
Table of Contents
Install
To install this library run:
$ pip install py-aiger-coins
Note that to actually compute probabilities, one needs to install with the bdd option.
$ pip install py-aiger-coins[bdd]
For developers, note that this project uses the poetry python package/dependency management tool. Please familarize yourself with it and then run:
$ poetry install
Usage
Note this tutorial assumes py-aiger-bdd
has been installed (see the
Install section).
Biased Coins
We start by encoding a biased coin and computing its bias. The primary
entrypoint for modeling coins is the coin
function.
from fractions import Fraction
import aiger_coins
bias = Fraction(1, 3)
coin1 = aiger_coins.coin(bias)
coin2 = aiger_coins.coin((1, 3)) # or just use a tuple.
assert coin1.prob() == coin2.prob() == prob
Distributions on discrete sets
We now illustrate how to create a set of mutually exclusive coins that represent distribution over a finite set. For example, a biased three sided dice can be 1-hot encoded with:
dice = aiger_coins.dist([1, 3, 2], name='x')
dice = aiger_coins.dist([(1, 6), (3, 6), (2, 6)], name='x') # equivalent
dice = aiger_coins.dist([Fraction(1, 6), Fraction(3, 6), Fraction(2, 6)], name='x') # equivalent
print(dice.freqs())
# (Fraction(1, 6), Fraction(1, 2), Fraction(1, 3))
Letting, ⚀ = dice[0]
, ⚁ = dice[1]
, ⚂ = dice[2]
,
one, two, three = dice[0], dice[1], dice[2]
We can ask the probability of drawing an element of {⚀, ⚁}
with:
assert (one | two).prob() == Fraction(2, 3)
assert (~three).prob() == Fraction(2, 3)
Distributions and Coins
Distribution
s and Coin
s are really just wrappers around two
aiger_bv.UnsignedBVExpr
objects stored in the expr
and valid
attributes.
The attributes expr
and valid
encode an expression over fair coin
flips and which coin flips are "valid" respectively. Coins is a
special type of Distribution
where the expression is a predicate
(e.g. has one output).
Note that accessing the ith element of a Distribution
results in a
Coin
encoding the probability of drawing that element.
Manipulating Distributions
In general Distribution
s can me manipulated by manipulating the
.expr
attribution to reinterpret the coin flips or manipulating
.valid
to condition on different coin flip outcomes.
Out of the box Distribution
s support a small number of operations:
+, <, <=, >=, >, ==, !=, ~, |, &, ^, .concat
, which they inherit
from aiger_bv.UnsignedBVExpr
. When using the same .valid
predicate
(same coin flips), these operations only manipulate the .expr
attribute.
More generally, one can use the apply
method to apply an arbitrary
function to the .expr
attribute. For example, using the dice from
before:
dice2 = dice.apply(lambda expr: ~expr[2])
assert dice2[0].freqs() == Fraction(2, 3)
One can also change the assumptions made on the coin flips by using
the condition method, for example, suppose we condition on the coin
flips never being all False
. This changes the distribution
as follows:
coins = dice.coins # Bitvector Expression of coin variables.
dice3 = dice.condition(coins != 0)
print(dice3.freqs())
# [Fraction(0, 5), Fraction(3, 5), Fraction(2, 5)]
Binomial Distributions
As a convenience, py-aiger-coins
also supports encoding Binomial
distributions.
x = binomial(3)
print(x.freqs())
# (Fraction(1, 8), Fraction(3, 8), Fraction(3, 8), Fraction(1, 8))
Markov Decision Processes and Probablistic Circuits
aiger_coins
also supports modeling Probablistic Circuits, Markov
Decision Process (MDPs), and Markov Chains (MDPs with no inputs).
Internally, the MDP
object is simply an AIGBV
bitvector circuit
with some inputs annotated with distributions over their inputs.
The primary entropy point to modeling a Markov Decision Process is
the circ2mdp
function.
from aiger_bv import atom
from aiger_coins import circ2mdp
x = atom(3, 'x', signed=False)
y = atom(3, 'y', signed=False)
expr = (x & y).with_output('x&y')
mdp1 = circ2mdp(expr)
mdp1 = circ2mdp(expr.aigbv) # equivalent
Composition
MDP
can be composed using an API analogous to aiger_bv.AIGBV
and
aiger.AIG
sequential circuits. In addition, MDP
support being feed
actions from a distribution via sequential composition.
# Put a distribution over the y input.
dist = aiger_coins.dist((0, 1, 2), name='y')
mdp2 = dist >> mdp1
mdp2 = mdp1 << dist # equivalent
mdp2 = circ2mdp(expr, {'y': dist}) # equivalent
assert mdp1.inputs == {'x', 'y'}
assert mdp2.inputs == {'x'}
mdp3 = mdp2 | circ2mdp(aiger_bv.identity_gate(4, 'z'))
assert mdp3.inputs == {'x', 'z'}
assert mdp3.outputs == {'x&y', 'z'}
mdp4 = mdp3.feedback(inputs=['z'], outputs=['x&y'], keep_outputs=True)
assert mdp4.inputs == {'x'}
assert mdp4.outputs == {'x&y', 'z'}
Extracting Circuit
One can transform an MDP
into an AIG
or AIGBV
object using
.aig
and .aigbv
attributes. This adds as the coinflips explicitly
as inputs and also adds a special output ##valid
that monitors if
the sequence of inputs and coin flips was valid.
assert mdp.aigbv.outputs == mdp.outputs | {'##valid'}
assert '##valid[0]' in mdp.aig.outputs
Encoding and Decoding Traces
Often times, one is interested in analyzing traces, sequences of states and actions, through a Markov Decision Process.
In order to map this to an execution of an MDP
object, one needs to
find a sequence of coin flip inputs such that feeding the actions and
the coin flip inputs into the circuit generated by MDP.aigbv
.
This (and its inverse) can be done via the MDP.encode_trc
and
MDP.decode_trc
methods.
For example, consider the simple MDP modeled by:
from aiger_bv import atom
from aiger_coins import circ2mdp
action = atom(1, 'action', signed=False)
x_prev = atom(1, 'x_prev', signed=False)
c = atom(1, 'c', signed=False)
x_next = (x_prev & c & action).with_output('x_next')
sys = circ2mdp(x_next).feedback(
keep_outputs=True,
inputs=['x_prev'], outputs=['x_next'], initials=[(True,)],
)
sys <<= coin((1, 2), name='c')
assert sys.inputs == {'action'}
assert sys.outputs == {'x_next'}
We can encode and decode traces into this model as follows:
# Encoding and Decoding
sys_actions = 3*[{'action': (True,)}]
states = 3*[{out: (True,)}]
actions = sys.encode_trc(sys_actions, states)
assert not any(v['c'][0] for v in actions)
sys_actions2, states2 = sys.decode_trc(actions)
assert sys_actions2 == sys_actions
assert states2 == states
Project details
Release history Release notifications | RSS feed
Download files
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.
Source Distribution
Built Distribution
Hashes for py_aiger_coins-1.2.0-py3-none-any.whl
Algorithm | Hash digest | |
---|---|---|
SHA256 | 1eca823e1c6c21adb566053082d6241a7f0b69c68d6ae4852ff7849c800b589e |
|
MD5 | 3c99a12f0cbbed6ada8a127e20aa8221 |
|
BLAKE2b-256 | 64115d95c7dae65e3ec8f79ab202f2d3fd4196f1d3a75160816762efca998b99 |