Portfolio Interface

[kw-corne]

Portfolio Interface

Portfolios are constructed using hydra-smac.

The only two things needed for constructing a portfolio must be:

1. A set of verifier configuration spaces
2. A set of networks and properties to construct the portfolio on

Properties

• Set of verifier configurations

Construction

A function with the following shape must be exposed:

def construct_portfolio(self,
    verifier_configuration_spaces,
    instances,
    *,
    hydra_parameters, # e.g. iterations, time limits, par-n scores
) -> Portfolio: ...

Note: File format (json) might change depending on if it is suitable or not. Notably we might not be able to express more complex relations between parameters using ConfigSpace, because those will not be serializable. In that case we could still try to export configuration using pickle. However using json is more transparent as un-pickling allows for arbitrary code execution.

def save_as_json(self, out_file: Path): ...

def load_from_json(self, file: Path): ...

Running

If a portfolio contains at least one verifier configuration, then the portfolio can be run to perform parallel verification. (Note: Since every verifier exposes methods for verifying properties non-parallel verification is also implementable).

Current plan is to use Dask Distributed for running a portfolio in parallel, which should (in theory) work anywhere from a single machine to a large cluster.

Portfolio should expose a method of the following shape:

def verify(self,
    network_property_structure: ???,
    dask_parameters: ???,
) -> ???[VerificationResult]: ...

Still need to decide on how to group properties and networks together, as well as grouping the VerificationResults in an nice manner.

Note: This is very much subject to change depending on how we end up implementing Dask for this task