TrustAI/DeepConcolic

About the running time of ssclp

Closed this issue · 1 comments

Hello~ When I ran this command (python deepconcolic.py —model ../saved_models/mnist_complicated.h5 —criterion ssclp —mnist-data —outputs outs) to run Concolic Sign-sign-coverage (MC/DC) for DNNs on the MNIST model, I ran it for two days and still stuck in the place where the constraints were solved, as shown in the figure below.

屏幕快照 2020-04-23 下午2 46 09

Hi,

The size of the LP problems can be quite large indeed; also the performance of LP solvers may vary significantly on those problems. By default, DeepConcolic selects a solver (CBC) that requires dumping each LP problem to a file in order to solve it, and this makes the whole process even more time and resource heavy.

DeepConcolic offers several possibilities to select a solver among a pre-defined list, like CPLEX for instance. Yet, using that solver requires installing and a bit of configuration. The first step for starts here, and after that normally setting PYTHONPATH to some value that depends on where you install CPLEX should suffice.