Skip to content

Latest commit

 

History

History
114 lines (94 loc) · 3.74 KB

README.md

File metadata and controls

114 lines (94 loc) · 3.74 KB
Raw

Formal Verifications of Bayesian Network Classifiers

Setup

  1. Cloning the repository

    git clone --recursive git@github.com:autonlab/bn-sat-verification.git

  2. Check if submodules are cloned There should be directory src/bnc_sdd. If not, run

    git submodule update --init --recursive

  3. Install dependencies Note: Tested on Python 3.10.11

    python -m pip install --index-url https://support.bayesfusion.com/pysmile-A/ pysmile
python3 -m pip install -r requirements.txt

  4. Create pysmile_license.py under src/ directory and paste your license key. The license key can be obtain free of charge for academic usage on BayesFusion website. It should look like this:

    import pysmile

pysmile.License((
	b"SMILE LICENSE XXXXXXXX XXXXXXXX XXXXXXXX "
	b"THIS IS AN ACADEMIC LICENSE AND CAN BE USED "
	b"SOLELY FOR ACADEMIC RESEARCH AND TEACHING, "
	b"AS DEFINED IN THE BAYESFUSION ACADEMIC "
	b"SOFTWARE LICENSING AGREEMENT. "
	b"Serial #: .................. "
	b"Issued for: Michael Jackson (mjackson@la.edu) "
	b"Academic institution: Some Institution "
	b"Valid until: 2023-12-04 "
	b"Issued by BayesFusion activation server"
	),[
	XXXX,XXXX,XXXX,XXXX,XXXX,XXXX,XXXX,XXXX,XXXX,XXXX,XXXX,XXXX,XXXX,XXXX,XXXX,XXXX,
	XXXX,XXXX,XXXX,XXXX,XXXX,XXXX,XXXX,XXXX,XXXX,XXXX,XXXX,XXXX,XXXX,XXXX,XXXX,XXXX,
	XXXX,XXXX,XXXX,XXXX,XXXX,XXXX,XXXX,XXXX,XXXX,XXXX,XXXX,XXXX,XXXX,XXXX,XXXX,XXXX,
	XXXX,XXXX,XXXX,XXXX,XXXX,XXXX,XXXX,XXXX,XXXX,XXXX,XXXX,XXXX,XXXX,XXXX,XXXX,XXXX])

Reproducibility

cd src

# Experiment 1: (each script generates different part of the table)
python experiment1_1paper.py
python experiment1_2paper.py
python experiment1_paper.py


# Experiment 2:
# generating models and rules
python experiments_fall/train.py
python experiments_fall/generate_fmo_rules.py
python experiments_fall/extract_rules.py
python experiments_fall/create_config.py

# running verification
python experiment2_paper.py

# for mdd visualization, quantitative analysis: experiment2_paper.ipynb
# for counterexamples, results: experiments_fall/artifacts_visualisation.ipynb

Call specific parts of the repository from shell

(Assuming that you're in the /src directory.)

To convert a Bayesian Network that is saved in pysmile format .xdsl to .net format, run

This requires:

  1. A .xdsl file that contains the Bayesian Network
python3 scripts/convert_to_shih.py --input_file <input_file> --output_file <output_file> (optional: --verbose)
# e.g. python scripts/convert_to_shih.py --input_file models/simple_weather_model.xdsl --output_file bnc_networks/weather.net

To build Multivalued Decision Diagrams (MDDs) from a .net file, run:

This requires:

  1. A .net file that contains the Bayesian Network
  2. A .json file that contains the configuration of the Bayesian Network
python3 convert_net_to_odd.py --netconfigpath <netconfigpath> --netfilepath <netfilepath> (optional: --verbose)
# e.g. python convert_net_to_odd.py --netconfigpath "bnc_configs/weather.json" --netfilepath bnc_networks/weather.net

To parse and display MDD from .odd file, run:

This requires:

  1. A .odd file that contains the MDD
python3 odd_parser.py --filepath <filepath> (optional: --plot <True/False, default=True>, --verbose)
# e.g. python odd_parser.py --filepath odd_models/weather/weather_1.odd

To convert MDD into CNF, run:

This requires:

  • A .odd file that contains the MDD
python3 tseitin_encoding.py --odd <odd_file> --cnf <cnf_file> (optional: --verbose)
# e.g. python3 tseitin_encoding.py --odd odd_models/test/test_diagram.odd --cnf cnf_files/test_diagram.json --verbose

Test queries

To test a query, while being in top directory, run:

pytest -v