Verification tool for machine learning models in R
ml-vRtool is a dedicated machine learning model verification tool designed specifically for R users. It aims to bridge the accessibility gap by providing robust verification capabilities across various machine learning models. The tool focuses on verifying the robustness property, particularly
There's a critical need for accessible and comprehensive machine learning model verification tools, especially for R-using researchers. Existing verification techniques, largely implemented in Python and C++, often have limitations in accessibility and scope, particularly beyond neural networks. Our work addresses this gap by introducing a tool specifically tailored for R users, offering robust verification capabilities across diverse machine learning models.
The core focus of ml-vRtool lies in verifying the robustness property, specifically targeting
-
Z3 Theorem Prover: An SMT solver integrated and tailored within ml-vRtool to handle the verification of machine learning models.
-
Marabou Integration for Neural Networks: For neural network models, ml-vRtool converts them into the ONNX (Open Neural Network Exchange) format. This standard format enables compatibility with various state-of-the-art verification tools. Marabou, an SMT-based tool specialized in verifying neural network models, is integrated within ml-vRtool to effectively handle and verify these complex models.
By employing these solvers, ml-vRtool offers a robust means to verify the
ml-vRtool provides support for various machine learning classification models using specific libraries in R:
-
Decision Tree
- Supported Library:
rpart
- Supported Library:
-
Random Forest
- Supported Library:
randomForest
- Supported Library:
-
Support Vector Machine (SVM)
- Linear Binary SVM
- Linear Multiclass SVM
- Supported Library:
Kernlab
- Supported Library:
-
Neural Networks (NN)
- Supported Library:
keras
- Supported Library:
To utilize ml-vRtool for verifying machine learning models in R, follow these steps:
-
Clone the Repository:
git clone https://github.com/rahulps33/ml-vRtool.git
-
Open the Project:
- Open the project using RStudio by navigating to the cloned directory and opening
ml-vRtool.Rproj
. - Alternatively, double-click on
ml-vRtool.Rproj
to open it with RStudio.
- Open the project using RStudio by navigating to the cloned directory and opening
-
Example Usage: For a detailed example of how to use ml-vRtool, refer to the
example.R
file in this repository. Here's a brief overview:-
Installing Requirements for ML Solvers: Run the following command in R to install requirements for ML solvers:
source("requirements/requirements_ml.R")
-
Verifying ML Models: For decision tree, random forests, and SVM models, utilize the solver scripts provided in the
ml_solvers
directory as exemplified in theexample.R
file. For instance, for a decision tree model:# Run the decision tree solver code source("ml_solvers/dt_solver.R") # Call the function for decision tree solver dt_solver_r(model, ref_input, epsilon_value)
Parameters:
-
model
: Corresponding trained machine learning model -
ref_input
: A 1-row dataframe with features i.e., the reference input and its corresponding class (class should be the last column). For example:iris[1,] Sepal.Length Sepal.Width Petal.Length Petal.Width Species 1 5.1 3.5 1.4 0.2 setosa
-
epsilon_value
: User-defined value used to verify the$\varepsilon$ -robustness of the provided reference input.
-
-
Installing Requirements for NN Solvers: Marabou tool integrated here supports Linux or MacOS for verifying neural network models. Follow these steps:
- Activate the virtual environment used for training your neural network model. For example, if the environment is "r-keras", use:
use_virtualenv("r-keras")
- Install required Python packages to convert the neural network model to ONNX format:
py_install(c("onnx", "tf2onnx", "h5py", "onnxruntime"))
- Install Marabou tool in this environment. Instructions are available in their GitHub repository: Marabou
- Activate the virtual environment used for training your neural network model. For example, if the environment is "r-keras", use:
-
Verifying Neural Network Models:
-
To call Marabou from
nn_solvers
directory, run:source("nn_solvers/nn_solver.R") marabou_solver_r(model, epsilon, ref_input, class)
For neural network models, different considerations apply compared to other models. Ensure the input matches the model's expected shape, especially when dealing with images.
Parameters:
-
model
andepsilon
: Trained neural network model and epsilon value for verifying$\varepsilon$ -robustness of the provided reference input. -
ref_input
andclass
: Reference input and its corresponding class for neural network models. If dealing with images, ensure the input image matches the model's expected input shape (e.g., 28x28 for MNIST).
-
-
-
Contributions to ml-vRtool are welcome! Feel free to submit issues, feature requests, or pull requests. Help us improve and expand the capabilities of this verification tool to serve the community better.
Special thanks to the contributors and supporters of ml-vRtool for their valuable input and efforts in making this tool accessible and efficient for R-using researchers.
Note: This tool is a work-in-progress and may have limitations or ongoing developments. Your feedback and contributions are highly appreciated!