bounded-prescience

This repo contains code for the paper Shielding Atari Games with Bounded Prescience (https://arxiv.org/abs/2101.08153) by Mirco Giacobbe, Hosein Hasanbeig, Hjalmar Wijk and Daniel Kroening. In addition to replicating the experiments in the paper and the bounded prescience shield, the repo allows the creation of property-labelled versions of the standard Atari gym environments which can expose safety information for other agents and policies.

Installation

The prescience package needs to be installed through pip:

git clone https://github.com/HjalmarWijk/bounded-prescience.git
cd bounded-prescience
pip3 install .

or alternatively:

pip3 install git+https://github.com/HjalmarWijk/bounded-prescience.git

Properties

Game	Property	Description	Classification
Alien	death	Losing a life
Amidar	death	Losing a life
Assault	death	Losing a life
Assault	overheat	Losing a life from overheating	Shallow
Asterix	death	Losing a life
Asteroids	death	Losing a life
Atlantis	death	Losing a life
BankHeist	death	Losing a life
BankHeist	death	Losing a life
BattleZone	death	Losing a life
BeamRider	death	Losing a life
Berzerk	death	Losing a life
Berzerk	death	Losing a life
Bowling	no-hit	Missing all pins	Minimal
Bowling	no-strike	Missing at least one pin
Boxing	knock-out	Getting knocked out	Minimal
Boxing	lose	Losing the match	Minimal
Boxing	no-enemy-ko	Match ends without knocking out enemy
Breakout	death	Losing a life
Centipede	death	Losing a life
CrazyClimber	death	Losing a life
DemonAttack	death	Losing a life
DemonAttack	death	Losing a life
DemonAttack	death	Losing a life
DoubleDunk	out-of-bounds	Moves out of bounds	Shallow
DoubleDunk	shoot-bf-clear	Losing ball due to shooting before clearing*	Shallow
Enduro	crash-car	Crashing into another car
FishingDerby	lose	Not winning over the opponent
Freeway	hit	Being hit by car
Frostbite	death	Losing a life
Frostbite	freezing	Losing a life from time running out
Gopher	lose-carrot	Having a carrot eaten
Gravitar	death	Losing a life
Gravitar	fuel	Running out of fuel	Shallow
Hero	death	Losing a life
IceHockey	enemy-score	Opponent scores
Jamesbond	death	Losing a life

* See manual for details on this game rule.

To test properties use the test_property.py script with flags --env [Game name] --prop [Property name]

This simulates a random agent and logs violations. To evaluate properties with human play, use --human flag (requires pygame).

Verification

To check properties for the 9 pre-trained agents evaluated in the paper under a variety of settings see the script check_noops.py To run the ChainerRL agents you first need to download them by running download_models.py (the Atari Zoo agents download dynamically). The scripts chainer_no_shield.sh and atari_zoo_no_shield.sh run all the agents for all propertiesm and write results as a csv in the results folder. Note that Atari Zoo agents need Tensorflow 1 (and AtariZoo) installed, while ChainerRL agents needs Tensorflow 2 and ChainerRL.

Shielding

To check properties using prescience shielding use the --lookahead flag for check_noops.py The shield scripts run this check for all algorithms, properties and shield depths up to 5.

Reference

Please use this bibtex entry if you want to cite this repository in your publication:

@misc{bounded_prescience_repo,
  author = {Mirco Giacobbe, Mohammadhosein Hasanbeig, Daniel Kroening, and Hjalmar Wijk},
  title = {Shielding Atari Games with Bounded Prescience Code Repository},
  year = {2020},
  publisher = {GitHub},
  journal = {GitHub repository},
  howpublished = {\url{https://github.com/HjalmarWijk/bounded-prescience}},
}

License

This project is licensed under the terms of the BSD-3-Clause