Search Techniques

VerifAI provides several techniques for exploring the semantic search space for verification, testing, and synthesis. These are largely based on sampling and optimization methods. In the tool, we refer to all of these as “samplers”.

There are three active samplers (i.e. cross entropy, simulated annealing, and bayesian optimization samplers) and two passive samplers (i.e. random and halton samplers) supported. The details of their implementation can be found in verifai/samplers directory.

How to add a new sampler?

First, add your python script of your sampler in verifai/samplers directory along with other sampler scripts. Second, add an API to call your sampler in verifai/samplers/feature_sampler.py

Sampling from a Scenic program

Defining the semantic feature space using a Scenic program (instead of the Feature APIs in VerifAI) requires the use of a special sampler, ScenicSampler.

class ScenicSampler(scenario, maxIterations=None, ignoredProperties=None)

Samples from the induced distribution of a Scenic scenario.

Created using the fromScenario and fromScenicCode class methods.

See Scene Generation in the Scenic documentation for details of how Scenic’s sampler works. Note that VerifAI’s other samplers can be used from within a Scenic scenario by defining external parameters.

classmethod fromScenario(path, maxIterations=None, maxSteps=None, ignoredProperties=None, **kwargs)

Create a sampler corresponding to a Scenic program.

The only required argument is path, and maxIterations may be useful if your scenario requires a very large number of rejection sampling iterations. See scenic.scenarioFromFile for details on optional keyword arguments used to customize compilation of the Scenic file.

Parameters:

• path (str) – path to a Scenic file.

• maxIterations (int) – maximum number of rejection sampling iterations (default 2000).

• ignoredProperties – properties of Scenic objects to not include in generated samples (see defaultIgnoredProperties for the default).

• kwargs – additional keyword arguments passed to scenic.scenarioFromFile; e.g. params to override global parameters or model to set the world model.

classmethod fromScenicCode(code, maxIterations=None, maxSteps=None, ignoredProperties=None, **kwargs)

As above, but given a Scenic program as a string.

pointForScene(scene)

Convert a sampled Scenic Scene to a point in our feature space.

The FeatureSpace used by this sampler consists of 2 features:

• objects, which is a Struct consisting of attributes object0, object1, etc. with the properties of the corresponding objects in the Scenic program. The names of these attributes may change in a future version of VerifAI: use the nameForObject function to generate them.

• params, which is a Struct storing the values of the global parameters of the Scenic program (use paramDictForSample to extract them).

static nameForObject(i)

Name used in the FeatureSpace for the Scenic object with index i.

That is, if scene is a Scene, the object scene.objects[i].

paramDictForSample(sample)

Recover the dict of global parameters from a ScenicSampler sample.