# Sound Logical Explanations for Mean Aggregation Graph Neural Networks

# Installation
These instructions are written for Linux.

From the root of the code (the folder `code`), create a new `python3` virtual environment with:
```
python3 -m venv ./venv
```
Then activate the environment with:
```
source venv/bin/activate
```
Then install the following required packages using `pip`. If difficulties are encountered, instructions for installing `torch` can be found [here](https://pytorch.org/get-started/locally/) and instructions for `torch_geometric` can be found [here](https://pytorch-geometric.readthedocs.io/en/latest/notes/installation.html).
```
pip3 install torch torchvision torchaudio
pip3 install torch_geometric
pip3 install pyg_lib torch_scatter torch_sparse torch_cluster torch_spline_conv -f https://data.pyg.org/whl/torch-2.0.0+cpu.html
pip3 install networkx==3.0
pip3 install wandb
pip3 install matplotlib
```

A different version of CUDA can be used, depending on your system.

# File Structure
- `data/` - datasets
- `src/` - source code. All of our code for checking rule soundness and producing explanatory rules is found in `monotonic_rule_extraction.py`.
- Other folders are used for saved models, checkpoints, encoders / decoders, etc.

# Running Experiments
All experiments should be run from within the `src` directory. A full description of all hyperparameters available can be found in the argument parser in `main.py`.

## Training
The following code will train a mean-GNN with non-negative weights for 8000 epochs, stopping training if performance deteriorates for 50 epochs, with a learning rate of 0.001, a random seed of 1, 2 GNN layers, and on the LogInfer-WN-hier dataset.
```
python main.py --early-stop 50 --epochs 8000 --layers 2 --lr 0.001 --seed 1 --aggregation mean --dataset LogInfer-WN-hier --log-interval 100 --non-negative-weights 1 --train 1
```

## Validation
To set the threshold of the model, you must next run it on the validation dataset. For example, with the following command:
```
python main.py --early-stop 50 --epochs 8000 --layers 2 --lr 0.001 --seed 1 --aggregation mean --dataset LogInfer-WN-hier --log-interval 100 --non-negative-weights 1 --test 1 --evaluation-set valid
```

## Testing
To check the model on the test set, the following command should be run, using `--evaluation-set test`:
```
python main.py --early-stop 50 --epochs 8000 --layers 2 --lr 0.001 --seed 1 --aggregation mean --dataset LogInfer-WN-hier --log-interval 100 --non-negative-weights 1 --test 1 --evaluation-set test
```

## Testing and Sound Rule Extraction
Finally, to check for sound monotonic rules, use the `--search-rule-check 1` argument. When this is done on the `lubm` dataset, explanations for all predictions will also be computed on the provided `evaluation-set`. For example:
```
python main.py --early-stop 50 --epochs 8000 --layers 2 --lr 0.001 --seed 1 --aggregation mean --dataset LogInfer-WN-hier --log-interval 100 --non-negative-weights 1 --evaluation-set test --search-rule-check 1
```

Use the `--reduce-rule-size 1` argument to reduce the size of the explanatory rules.