| Name | reinfier JSON |
| Version |
0.5.3
JSON |
| download |
| home_page | None |
| Summary | Reinfier - A verification framework for deep reinforcement learning |
| upload_time | 2024-05-22 22:17:36 |
| maintainer | None |
| docs_url | None |
| author | None |
| requires_python | >=3.10 |
| license | None |
| keywords |
drl
dnn
verification
interpretation
|
| VCS |
 |
| bugtrack_url |
|
| requirements |
No requirements were recorded.
|
| Travis-CI |
No Travis.
|
| coveralls test coverage |
No coveralls.
|
# Reinfier
A general verification and interpretability framework for deep reinforcement learning, which combines the formal verification of deep neural network with bounded model checking algorithm and k-induction algorithm to verify the properties of deep reinforcement learning or give counterexamples.
Source code is available at [Reinfier](https://github.com/Kurayuri/Reinfier).
## Installation
Reinfier takes [DNNV](https://github.com/dlshriver/dnnv) as the external DNN verification framework now, which requrires verifiers of DNN ([Reluplex](https://github.com/guykatzz/ReluplexCav2017), [planet](https://github.com/progirep/planet), [MIPVerify.jl](https://github.com/vtjeng/MIPVerify.jl), [Neurify](https://github.com/tcwangshiqi-columbia/Neurify), [ERAN](https://github.com/eth-sri/eran), [BaB](https://github.com/oval-group/PLNN-verification), [marabou](https://github.com/NeuralNetworkVerification/Marabou), [nnenum](https://github.com/stanleybak/nnenum), [verinet](https://vas.doc.ic.ac.uk/software/neural/)).
For DRL verification, Reinfier now supports Marabou, Neurify, nnenum and Planet well. For DNN verifcation, Reinfier supports ones as same as DNNV.
Building above verifers requires following packages of system:
```shell
cmake
python-is-python3
python3.8-venv
```
DNNV and Reinfier are recommended to install with a python virtual environment.
```shell
python -m venv testenv
cd testenv
source ./bin/activate
```
Currently, DNNV main branch on [PyPI](https://pypi.org/project/dnnv/0.5.1/) has bug caused by dependency. It is better to intall it from source code. Run:
```shell
pip install git+https://github.com/dlshriver/DNNV.git@develop
```
```shell
docker pull dlshriver/dnnv:latest
docker run --name dnnv dlshriver/dnnv:latest tail -f /dev/null
docker exec -it dnnv bash
```
To install any of the supported verifiers, run:
```shell
dnnv_manage install reluplex planet mipverify neurify eran bab marabou nnenum verinet
```
Reinfier requires python>=3.8. To install Reinfier, run:
```shell
pip install reinfier
```
Usage sample files to test:
```python
import reinfier as rf
network, property = rf.res.get_example()
print(rf.verify(network, property))
```
The result should be:
```python
(False, 2, an instance of <numpy.ndarray>)
```
which means the property is False (SAT, Invalid) with verification depth is 2, and a violation (counterexample) is given.
## Usage
A **DRLP** object storing a property in DRLP format and an **NN** object storing an ONNX DNN are required for a basic DRL verification query in Reinfier.
```python
import reinfier as rf
network = rf.NN("/path/to/ONNX/file")
# or
network = rf.NN(ONNX_object)
property = rf.DRLP("/path/to/DRLP/file")
# or
property = rf.DRLP(DRLP_str)
rf.verify(network, property) # Verify API (default k-induction algorithm, Recommended)
# or
rf.k_induction(network, property) # k-induction algorithm
# or
rf.bmc(network, property) # bounded model checking algorithm
```
## DRLP
DRLP, i.e. Deep Reinforcement Learning Property, is a Pyhton-embedded DSL to describe property of DRL.
### Reserved Keywords
| Parameter | Variable Keyword | Type |
|--------------------------|:----------------:|:---------------:|
| Input of NN $x$ | $x$ | $numpy.ndarray$ |
| Output of NN $y$ | $y$ | $numpy.ndarray$ |
| Input size of NN | $x\_size$ | $int$ |
| Output size of NN | $y\_size$ | $int$ |
| Verification depths $k$ | $k$ | $int$ |
### Example
```python
_a = [0,1]
@Pre
[[-1]*2]*k <= x <= [[1]*2]*k
[a]*2 == x[0]
for i in range(0,k-1):
Implies(y[i] > [0], x[i]+0.5 >= x[i+1] >= x[i])
Implies(y[i] <= [0], x[i]-0.5 <= x[i+1] <= x[i])
@Exp
y >= [[-2]]*k
```
Such DRLP text describe an Environment and an Agent:
Becouse of Initial state 𝐼 consists of two situtions in fact, such DRLP describes two concrete properties.
1. State boundary S: Each input value is within $[−1,1]$
2. Initial state 𝐼: Each input value is $0$ or Each input value is $1$
3. State transition 𝑇: Each input value of the next state increases by at most $0.5$ when output is greater than $0$, and each input value of the next state decreases by at most $0.5$ when output is not greater than $0$
4. Other constraints 𝐶: None
5. Post-condition 𝑄: Output is always not less than $-2$
### Defination
The dinfination of DRLP:
```BNF
<drlp> ::= (<statements> NEWLINE '@Pre' NEWLINE)
<io_size_assign> NEWLINE <statements> NEWLINE
'@Exp' NEWLINE <statements>
<io_size_assign> ::= ''
| <io_size_assign> NEWLINE <io_size_id> '=' <int>
<io_size_id> = 'x_size' | 'y_size'
<statements> ::= ''
| <statements> NEWLINE <statement>
<statement> ::= <compound_stmt> | <simple_stmts>
<compound_stmt> ::= <for_stmt> | <with_stmt>
<for_stmt> :: = 'for' <id> 'in' <range_type> <for_range> ':' <block>
<with_stmt> :: = 'with' <range_type> ':' <block>
<block> ::= NEWLINE INDENT <statements> DEDENT
| <simple_stmts>
<range_type> ::= 'range' | 'orange'
<for_range> ::= '('<int>')'
| '('<int> ',' <int> ')'
| '('<int> ',' <int> ',' <int>')'
<simple_stmts> ::= ""
| <simple_stmts> NEWLINE <simple_stmt>
<simple_stmt> ::= <call_stmt> | <expr>
<call_stmt> ::= 'Impiles' '(' <expr> ',' <expr> ')'
| 'And' '(' <exprs> ')'
| 'Or' '(' <exprs> ')'
<exprs> ::= <expr>
| <exprs> ',' <expr>
<expr> ::= <obj> <comparation>
<comparation> ::= ''
| <comparator> <obj> <comparation>
<obj> ::= <constraint> | <io_obj>
<io_obj> ::= <io_id>
| <io_id> <subscript>
| <io_id> <subscript> <subscript>
<io_id> ::= 'x' | 'y'
<subscript> ::= '[' <int> ']'
| '[' <int>':'<int> ']'
| '[' <int>':'<int> ':'<int>']'
<int> ::= <int_number>
| <id>
| <int> <operator> <int>
<constraint> :: = <int>
| <list>
| <constraint> <operator> <constraint>
```
Raw data
{
"_id": null,
"home_page": null,
"name": "reinfier",
"maintainer": null,
"docs_url": null,
"requires_python": ">=3.10",
"maintainer_email": null,
"keywords": "DRL, DNN, verification, interpretation",
"author": null,
"author_email": "Kurayuri <Kurayuri@outlook.com>",
"download_url": "https://files.pythonhosted.org/packages/e7/42/07f69efb5017dd25c5416a0f2dbf5e59ba93217e471fe4441b7de2143751/reinfier-0.5.3.tar.gz",
"platform": null,
"description": "# Reinfier\nA general verification and interpretability framework for deep reinforcement learning, which combines the formal verification of deep neural network with bounded model checking algorithm and k-induction algorithm to verify the properties of deep reinforcement learning or give counterexamples. \nSource code is available at [Reinfier](https://github.com/Kurayuri/Reinfier).\n## Installation\nReinfier takes [DNNV](https://github.com/dlshriver/dnnv) as the external DNN verification framework now, which requrires verifiers of DNN ([Reluplex](https://github.com/guykatzz/ReluplexCav2017), [planet](https://github.com/progirep/planet), [MIPVerify.jl](https://github.com/vtjeng/MIPVerify.jl), [Neurify](https://github.com/tcwangshiqi-columbia/Neurify), [ERAN](https://github.com/eth-sri/eran), [BaB](https://github.com/oval-group/PLNN-verification), [marabou](https://github.com/NeuralNetworkVerification/Marabou), [nnenum](https://github.com/stanleybak/nnenum), [verinet](https://vas.doc.ic.ac.uk/software/neural/)). \n\nFor DRL verification, Reinfier now supports Marabou, Neurify, nnenum and Planet well. For DNN verifcation, Reinfier supports ones as same as DNNV.\n\nBuilding above verifers requires following packages of system: \n```shell\ncmake\npython-is-python3\npython3.8-venv\n```\n\nDNNV and Reinfier are recommended to install with a python virtual environment. \n```shell\npython -m venv testenv\ncd testenv\nsource ./bin/activate\n```\nCurrently, DNNV main branch on [PyPI](https://pypi.org/project/dnnv/0.5.1/) has bug caused by dependency. It is better to intall it from source code. Run: \n```shell\npip install git+https://github.com/dlshriver/DNNV.git@develop\n```\n\n```shell\ndocker pull dlshriver/dnnv:latest\ndocker run --name dnnv dlshriver/dnnv:latest tail -f /dev/null\ndocker exec -it dnnv bash\n```\n\n\n\nTo install any of the supported verifiers, run:\n```shell\ndnnv_manage install reluplex planet mipverify neurify eran bab marabou nnenum verinet\n```\n\nReinfier requires python>=3.8. To install Reinfier, run: \n```shell\npip install reinfier\n```\n\nUsage sample files to test: \n```python\nimport reinfier as rf\n\nnetwork, property = rf.res.get_example()\n\nprint(rf.verify(network, property))\n```\nThe result should be:\n```python\n(False, 2, an instance of <numpy.ndarray>)\n```\nwhich means the property is False (SAT, Invalid) with verification depth is 2, and a violation (counterexample) is given.\n\n## Usage\nA **DRLP** object storing a property in DRLP format and an **NN** object storing an ONNX DNN are required for a basic DRL verification query in Reinfier.\n\n```python\nimport reinfier as rf\n\nnetwork = rf.NN(\"/path/to/ONNX/file\")\n# or\nnetwork = rf.NN(ONNX_object)\n\nproperty = rf.DRLP(\"/path/to/DRLP/file\")\n# or\nproperty = rf.DRLP(DRLP_str)\n\nrf.verify(network, property) # Verify API (default k-induction algorithm, Recommended)\n# or\nrf.k_induction(network, property) # k-induction algorithm \n# or\nrf.bmc(network, property) # bounded model checking algorithm\n```\n\n## DRLP\nDRLP, i.e. Deep Reinforcement Learning Property, is a Pyhton-embedded DSL to describe property of DRL.\n### Reserved Keywords\n| Parameter | Variable Keyword | Type |\n|--------------------------|:----------------:|:---------------:|\n| Input of NN $x$ | $x$ | $numpy.ndarray$ |\n| Output of NN $y$ | $y$ | $numpy.ndarray$ |\n| Input size of NN | $x\\_size$ | $int$ |\n| Output size of NN | $y\\_size$ | $int$ |\n| Verification depths $k$ | $k$ | $int$ |\n### Example\n```python\n_a = [0,1]\n\n@Pre\n[[-1]*2]*k <= x <= [[1]*2]*k\n\n[a]*2 == x[0]\n\nfor i in range(0,k-1):\n Implies(y[i] > [0], x[i]+0.5 >= x[i+1] >= x[i])\n Implies(y[i] <= [0], x[i]-0.5 <= x[i+1] <= x[i])\n\n@Exp\ny >= [[-2]]*k\n```\nSuch DRLP text describe an Environment and an Agent: \nBecouse of Initial state \ud835\udc3c consists of two situtions in fact, such DRLP describes two concrete properties.\n1. State boundary S: Each input value is within $[\u22121,1]$ \n2. Initial state \ud835\udc3c: Each input value is $0$ or Each input value is $1$\n3. State transition \ud835\udc47: Each input value of the next state increases by at most $0.5$ when output is greater than $0$, and each input value of the next state decreases by at most $0.5$ when output is not greater than $0$\n4. Other constraints \ud835\udc36: None\n5. Post-condition \ud835\udc44: Output is always not less than $-2$ \n\n### Defination\n\nThe dinfination of DRLP: \n```BNF\n<drlp> ::= (<statements> NEWLINE '@Pre' NEWLINE)\n <io_size_assign> NEWLINE <statements> NEWLINE \n '@Exp' NEWLINE <statements>\n\n<io_size_assign> ::= ''\n | <io_size_assign> NEWLINE <io_size_id> '=' <int>\n \n<io_size_id> = 'x_size' | 'y_size'\n\n<statements> ::= ''\n | <statements> NEWLINE <statement>\n\n<statement> ::= <compound_stmt> | <simple_stmts>\n\n<compound_stmt> ::= <for_stmt> | <with_stmt>\n\n<for_stmt> :: = 'for' <id> 'in' <range_type> <for_range> ':' <block>\n\n<with_stmt> :: = 'with' <range_type> ':' <block>\n\n<block> ::= NEWLINE INDENT <statements> DEDENT\n | <simple_stmts>\n\n<range_type> ::= 'range' | 'orange'\n\n<for_range> ::= '('<int>')'\n | '('<int> ',' <int> ')'\n | '('<int> ',' <int> ',' <int>')'\n\n<simple_stmts> ::= \"\"\n | <simple_stmts> NEWLINE <simple_stmt>\n\n<simple_stmt> ::= <call_stmt> | <expr>\n\n<call_stmt> ::= 'Impiles' '(' <expr> ',' <expr> ')'\n | 'And' '(' <exprs> ')'\n | 'Or' '(' <exprs> ')'\n\n<exprs> ::= <expr> \n | <exprs> ',' <expr>\n\n<expr> ::= <obj> <comparation>\n\n<comparation> ::= '' \n | <comparator> <obj> <comparation>\n\n<obj> ::= <constraint> | <io_obj>\n\n<io_obj> ::= <io_id> \n | <io_id> <subscript>\n | <io_id> <subscript> <subscript>\n \n<io_id> ::= 'x' | 'y'\n\n<subscript> ::= '[' <int> ']'\n | '[' <int>':'<int> ']'\n | '[' <int>':'<int> ':'<int>']'\n\n<int> ::= <int_number> \n | <id> \n | <int> <operator> <int>\n\n<constraint> :: = <int> \n | <list>\n | <constraint> <operator> <constraint>\n\n```\n",
"bugtrack_url": null,
"license": null,
"summary": "Reinfier - A verification framework for deep reinforcement learning",
"version": "0.5.3",
"project_urls": {
"Home": "https://github.com/Kurayuri/Reinfier"
},
"split_keywords": [
"drl",
" dnn",
" verification",
" interpretation"
],
"urls": [
{
"comment_text": "",
"digests": {
"blake2b_256": "08746dffc67057b41187b40c2fb3c188a4657743a925a992dcd9870eeea39f10",
"md5": "03e54282a5a04ee8a46bf1e4cb795d40",
"sha256": "1cd7f9b325616f31774ee5725d0b7da2e8b1c431cb7bb16d4847362f01d785a3"
},
"downloads": -1,
"filename": "reinfier-0.5.3-py3-none-any.whl",
"has_sig": false,
"md5_digest": "03e54282a5a04ee8a46bf1e4cb795d40",
"packagetype": "bdist_wheel",
"python_version": "py3",
"requires_python": ">=3.10",
"size": 52997,
"upload_time": "2024-05-22T22:17:34",
"upload_time_iso_8601": "2024-05-22T22:17:34.179923Z",
"url": "https://files.pythonhosted.org/packages/08/74/6dffc67057b41187b40c2fb3c188a4657743a925a992dcd9870eeea39f10/reinfier-0.5.3-py3-none-any.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": "",
"digests": {
"blake2b_256": "e74207f69efb5017dd25c5416a0f2dbf5e59ba93217e471fe4441b7de2143751",
"md5": "cc371745f7483d241e28a031d5cfec4d",
"sha256": "5a7c774f82d8eff3a22db08edea4b89337cc23fc58ec412017129d12dcffbff9"
},
"downloads": -1,
"filename": "reinfier-0.5.3.tar.gz",
"has_sig": false,
"md5_digest": "cc371745f7483d241e28a031d5cfec4d",
"packagetype": "sdist",
"python_version": "source",
"requires_python": ">=3.10",
"size": 41485,
"upload_time": "2024-05-22T22:17:36",
"upload_time_iso_8601": "2024-05-22T22:17:36.812698Z",
"url": "https://files.pythonhosted.org/packages/e7/42/07f69efb5017dd25c5416a0f2dbf5e59ba93217e471fe4441b7de2143751/reinfier-0.5.3.tar.gz",
"yanked": false,
"yanked_reason": null
}
],
"upload_time": "2024-05-22 22:17:36",
"github": true,
"gitlab": false,
"bitbucket": false,
"codeberg": false,
"github_user": "Kurayuri",
"github_project": "Reinfier",
"travis_ci": false,
"coveralls": false,
"github_actions": false,
"lcname": "reinfier"
}
