Project Topics

1. Topic 1:
   In this project, we will use the VerifAI toolkit to "learn" the parameters of a linear quadratic regulator (LQR) controller that minimizes the count of lane violations of an ego car. Subsequently, you are required to attempt a proof that the learnt controller results in no lane violations.
   The Scenic probablistic-program based sampler allows you to specify statistical variations of higher-level semantic features, based on which test samples are created. The simulator follows the control rules of the parameterized LQR controller and determines the trajectory of the ego car with the sampled values of the semantic features.
   You are required to learn key parameters of the controller using this setup, and then try to attempt a proof (any technique is fine) that these values of parameters lead to zero violations of lane crossings. If your "learned" LQR controller does not yield a proof of correctness, you must provide a statistical estimate (along with a confidence interval) of what percentage of inputs within the allowed variations will lead to lane violations.
   Please see here for extensive documentation on VerifAI, and also worked out examples, explained in tutorial style. This project will be building on the case study titled "Lane keeping with inbuilt simulator".
2. Topic 2
   In this project, we will use the VerifAI toolkit to re-train a simple convolutional neural network for detecting images of cars on roads. The re-training should happen in iterations. At the end of each iteration, when you have re-trained the network, you are required to use alpha-beta CROWN to determine the local robustness of the re-trained network for a given image (radius of L_p norm ball for a suitable "p" of your choice, for which the class label of the image doesn't change).
   The Scenic probabilistic-program based sampler allows you to specify statistical variations of higher-level semantic features of scenes of cars on roads, based on which test samples are created. As you re-train the convolutional network, the network is expected to become better at recognizing images of cars on roads. This should reflect in an improvement (increase) in the local robustness metric when analyzed using alpha-beta CROWN. As you go from one re-training iteration to the next, you are required to change the sampling distribution, informed by the results of using alpha-beta CROWN.
   Please see here for extensive documentation about VerifAI, and also worked out examples, explained in tutorial style. This project will be building on the case study titled "Data augmentation". Please see here for documentation and code of alpha-beta CROWN. A colab demo and instructions for some simple tutorials using alpha-beta CROWN are available here.
3. Topic 3
   In this project, we will try to find an MILP-based alternative to using weighted MaxSAT in the Synplicate tool for generating Pareto-optimal interpretations. The Synplicate tool can be accessed here.
   We are going to try to replace the weighted MaxSAT encoding used in Synplicate to obtain a single Pareto-optimal interpretation. As discussed in class, there is a straightforward way to convert a weighted MaxSAT encoding to an MILP encoding. Your first task would be try this out, and compare the performance of the two approaches. We will be using Gurobi to solve the MILP instances. We don't expect this naive translation of weighted MaxSAT to MILP to yield much (if at all any) improvement in performance. The meat of your project would be to come up with alternative MILP encodings that exploit the structure of the problem, for which we can obtain tangible improvements over the weighted MaxSAT approach.
   For purposes of this problem, we will directly use samples from the UCI Machine Learning Repository. In other words, we will use datasets from this repository as proxies for samples obtained from a black-box ML model, and construct Pareto-optimal interpretations of the black-box model.
4. Topic 4
   In this project, we will investigate formal logic-based explanations of data instances w.r.t. tree ensemble models, and compare them with some heuristic explanations (viz. using LIME, SHAP and Anchor). The relevant toolkit (XReason) is available here. The goal of the project is to use guidance from formal logic-based explanations to create data instances for which explanations by other heuristic methods (like LIME, SHAP or Anchor) are incorrect (i.e. admit counter-examples).
   The github repository already contains code to validate, and then either repair or refine heuristic explanations. The primary objective of this project would be to use formal logic-based explanations to accelerate this process and zoom down on data instances where a heuristic explanation is necessarily incorrect.
   The project should hopefully yield a method for generating explanations that is better than formal logic-based explaners performance-wise, and better than heuristic explainers accuracy-wise (i.e. count of counterexamples is reduced).