diff --git a/autoverify/portfolio/hydra/hydra.py b/autoverify/portfolio/hydra/hydra.py index 2a2f1a6..c52b8b0 100644 --- a/autoverify/portfolio/hydra/hydra.py +++ b/autoverify/portfolio/hydra/hydra.py @@ -17,9 +17,11 @@ ) from autoverify.types import TargetFunction from autoverify.util.resources import ResourceTracker -from autoverify.util.target_function import get_pick_tf, get_verifier_tf +from autoverify.util.target_function import get_verifier_tf +from autoverify.util.verification_instance import VerificationInstance from autoverify.util.verifiers import verifier_from_name -from autoverify.verifier.verifier import CompleteVerifier, Verifier +from autoverify.util.vnncomp import inst_bench_to_kwargs +from autoverify.verifier.verifier import CompleteVerifier logger = logging.getLogger(__name__) @@ -74,20 +76,22 @@ def _remap_rh_keys( def _get_init_kwargs( - verifier: str, scenario: PortfolioScenario + verifier: str, scenario: PortfolioScenario, instance: VerificationInstance ) -> dict[str, Any]: init_kwargs: dict[str, Any] = {} # TODO: Type - if ( - scenario.verifier_kwargs is not None - and verifier in scenario.verifier_kwargs - ): - init_kwargs = scenario.verifier_kwargs[verifier] + if scenario.vnn_compat_mode: + assert scenario.benchmark is not None + init_kwargs = inst_bench_to_kwargs( + scenario.benchmark, verifier, instance + ) return init_kwargs -# TODO: Refactor this to use a more "Strategy"-like pattern +# TODO: Refactor this to use a more Strategy-like pattern +# Should be able to pass different strategies for components +# such as the configurator and updater class Hydra: """_summary_.""" @@ -136,7 +140,7 @@ def _configurator( run_name = f"pick_{self._iter}_{i}" logger.info("Picking verifier") - verifier = self._pick(run_name) + verifier = self._pick(run_name, pf) logger.info(f"Picked {verifier}") logger.info(f"Tuning {verifier}") @@ -149,38 +153,56 @@ def _configurator( return new_configs - # TODO: fix type errors - def _pick(self, run_name: str) -> str: + def _pick(self, run_name: str, pf: Portfolio) -> str: if self._scenario.pick_budget == 0: logging.info("Pick budget is 0, selecting random verifier.") return random.choice(self._scenario.verifiers) - verifier_insts: list[Verifier] = [] + verifiers: list[str] = self._ResourceTracker.get_possible() - for name in self._ResourceTracker.get_possible(): - verifier_class = verifier_from_name(name) - alloc = _get_cpu_gpu_alloc(name, self._ResourceTracker) - init_kwargs = _get_init_kwargs(name, self._scenario) - verifier_insts.append( - verifier_class(cpu_gpu_allocation=alloc, **init_kwargs) + def hydra_tf(config: Configuration, instance: str, seed: int) -> float: + seed += 1 # silence warning + verifier = verifiers[config["index"]] + assert isinstance(verifier, str) + + verifier_class = verifier_from_name(verifier) + init_kwargs = _get_init_kwargs( + verifier, + self._scenario, + VerificationInstance.from_str(instance), ) + alloc = _get_cpu_gpu_alloc(verifier, self._ResourceTracker) + verifier_inst = verifier_class( + cpu_gpu_allocation=alloc, **init_kwargs + ) + + verifier_tf = get_verifier_tf(verifier_inst) + + assert isinstance(verifier_inst, CompleteVerifier) + cost = verifier_tf(verifier_inst.default_config, instance, seed) + + if self._iter == 0: + return cost + else: + pf_cost = pf.get_cost(instance) + + return float(min(cost, pf_cost)) + + walltime_limit = ( + self._scenario.seconds_per_iter + * self._scenario.pick_budget + / self._scenario.configs_per_iter + ) - target_func = get_pick_tf(verifier_insts) pick_cfgspace = ConfigurationSpace() pick_cfgspace.add_hyperparameter( Categorical( "index", - [i for i in range(len(verifier_insts))], + [i for i in range(len(verifiers))], default=0, ) ) - walltime_limit = ( - self._scenario.seconds_per_iter - * self._scenario.pick_budget - / self._scenario.configs_per_iter - ) - smac_scenario = Scenario( pick_cfgspace, walltime_limit=walltime_limit, @@ -189,21 +211,21 @@ def _pick(self, run_name: str) -> str: **self._scenario.get_smac_scenario_kwargs(), ) - smac = ACFacade(smac_scenario, target_func, overwrite=True) + smac = ACFacade(smac_scenario, hydra_tf, overwrite=True) inc = smac.optimize() # Not dealing with > 1 config assert isinstance(inc, Configuration) key_map: dict[Configuration, Configuration] = {} - for i in range(len(verifier_insts)): + for i in range(len(verifiers)): cfg = Configuration(pick_cfgspace, {"index": i}) - key_map[cfg] = verifier_insts[i].default_config + key_map[cfg] = verifier_from_name(verifiers[i])().default_config rh = _remap_rh_keys(key_map, smac.runhistory) self._cost_matrix.update_matrix(rh) - return str(verifier_insts[inc["index"]].name) + return str(verifiers[inc["index"]]) def _tune( self, verifier: str, run_name: str, target_func: TargetFunction @@ -239,20 +261,26 @@ def _get_target_func(self, verifier: str, pf: Portfolio) -> TargetFunction: """If iteration > 0, use the Hydra target function.""" verifier_class = verifier_from_name(verifier) name = str(verifier_class.name) - init_kwargs = _get_init_kwargs(name, self._scenario) - alloc = _get_cpu_gpu_alloc(verifier, self._ResourceTracker) - verifier_inst = verifier_class(cpu_gpu_allocation=alloc, **init_kwargs) - verifier_tf = get_verifier_tf(verifier_inst) - - if self._iter == 0: - return verifier_tf def hydra_tf(config: Configuration, instance: str, seed: int) -> float: seed += 1 # silence warning + init_kwargs = _get_init_kwargs( + name, self._scenario, VerificationInstance.from_str(instance) + ) + alloc = _get_cpu_gpu_alloc(verifier, self._ResourceTracker) + verifier_inst = verifier_class( + cpu_gpu_allocation=alloc, **init_kwargs + ) + verifier_tf = get_verifier_tf(verifier_inst) + assert isinstance(verifier_inst, CompleteVerifier) cost = verifier_tf(config, instance, seed) - pf_cost = pf.get_cost(instance) + + if self._iter == 0: + return cost + else: + pf_cost = pf.get_cost(instance) return float(min(cost, pf_cost)) diff --git a/autoverify/portfolio/portfolio.py b/autoverify/portfolio/portfolio.py index 602a608..85273da 100644 --- a/autoverify/portfolio/portfolio.py +++ b/autoverify/portfolio/portfolio.py @@ -1,5 +1,8 @@ """_summary_.""" +from __future__ import annotations + import datetime +import json import math from collections.abc import Iterable, Mapping, MutableSet, Sequence from dataclasses import dataclass @@ -7,12 +10,13 @@ from typing import Any import numpy as np -from ConfigSpace import Configuration +from ConfigSpace import Configuration, ConfigurationSpace from autoverify.util.instances import verification_instances_to_smac_instances from autoverify.util.resource_strategy import ResourceStrategy from autoverify.util.smac import index_features from autoverify.util.verification_instance import VerificationInstance +from autoverify.util.verifiers import get_verifier_configspace @dataclass(frozen=True, eq=True, repr=True) @@ -21,6 +25,7 @@ class ConfiguredVerifier: verifier: str configuration: Configuration + resources: tuple[int, int] | None = None @dataclass @@ -37,10 +42,11 @@ class PortfolioScenario: configs_per_iter: int = 2 alpha: float = 0.5 # tune/pick split added_per_iter: int = 1 - stop_early = True - resource_strategy = ResourceStrategy.Auto + stop_early: bool = True + resource_strategy: ResourceStrategy = ResourceStrategy.Auto output_dir: Path | None = None - verifier_kwargs: Mapping[str, dict[str, Any]] | None = None + vnn_compat_mode: bool = False + benchmark: str | None = None def __post_init__(self): """_summary_.""" @@ -63,6 +69,10 @@ def __post_init__(self): if self.added_per_iter > self.length: raise ValueError("Entries added per iter should be <= length") + if self.vnn_compat_mode: + if not self.benchmark: + raise ValueError("Use a benchmark name if vnn_compat_mode=True") + self.n_iters = math.ceil(self.length / self.added_per_iter) self._verify_resources() @@ -73,6 +83,9 @@ def _verify_resources(self): if r[0] in seen: raise ValueError(f"Duplicate name '{r[0]}' in resources") + if r[0] not in self.verifiers: + raise ValueError(f"{r[0]} in resources but not in verifiers.") + seen.add(r[0]) if self.resource_strategy == ResourceStrategy.Auto: @@ -190,3 +203,63 @@ def discard(self, cv: ConfiguredVerifier): raise ValueError(f"{cv} is not in the portfolio") self._pf_set.discard(cv) + + def to_json(self, out_json_path: Path): + """Write the portfolio in JSON format to the specified path.""" + json_list: list[dict[str, Any]] = [] + + for cv in self._pf_set: + cfg_dict = dict(cv.configuration) + to_write = { + "verifier": cv.verifier, + "configuration": cfg_dict, + "resources": cv.resources, + } + json_list.append(to_write) + + with open(out_json_path, "w") as f: + json.dump(json_list, f, indent=4, default=str) + + @classmethod + def from_json( + cls, + json_file: Path, + config_space_map: Mapping[str, ConfigurationSpace] | None = None, + ) -> Portfolio: + """Instantiate a new Portfolio class from a JSON file.""" + with open(json_file) as f: + pf_json = json.load(f) + + pf = Portfolio() + + for cv in pf_json: + if config_space_map is None: + cfg_space = get_verifier_configspace(cv["verifier"]) + else: + cfg_space = config_space_map[cv["verifier"]] + + cv["configuration"] = Configuration(cfg_space, cv["configuration"]) + + if cv["resources"]: + cv["resources"] = tuple(cv["resources"]) + + pf.add(ConfiguredVerifier(**cv)) + + return pf + + def str_compact(self) -> str: + """Get the portfolio in string form in a compact way.""" + cvs: list[str] = [] + + for cv in self: + cvs.append( + "\t".join( + [ + str(cv.verifier), + str(hash(cv.configuration)), + str(cv.resources), + ] + ) + ) + + return "\n".join(cvs) diff --git a/autoverify/portfolio/portfolio_runner.py b/autoverify/portfolio/portfolio_runner.py new file mode 100644 index 0000000..fbfe3a3 --- /dev/null +++ b/autoverify/portfolio/portfolio_runner.py @@ -0,0 +1,31 @@ +"""_summary_.""" +from typing import TypeVar + +from autoverify.portfolio.portfolio import Portfolio +from autoverify.util.instances import VerificationDataResult +from autoverify.util.verification_instance import VerificationInstance + +_T = TypeVar("_T", VerificationInstance, str) + + +class PortfolioRunner: + """_summary_.""" + + def __init__(self, portfolio: Portfolio): + """_summary_.""" + self._portfolio = portfolio + # TODO: santiy check and fix all resources + + def verify_instances( + self, instances: list[_T] + ) -> dict[_T, VerificationDataResult]: + """_summary_.""" + # TODO: + # - launch all verifiers in parallel + # - as soon as one finds a result: + # - save result + # - stop all verifiers + # - go to next instance + results: dict[_T, VerificationDataResult] = {} + + return results diff --git a/autoverify/tune/tune_hydra.py b/autoverify/tune/tune_hydra.py new file mode 100644 index 0000000..a6cfad7 --- /dev/null +++ b/autoverify/tune/tune_hydra.py @@ -0,0 +1,49 @@ +"""_summary_.""" +from collections.abc import Sequence +from pathlib import Path + +from autoverify.portfolio.hydra.hydra import Hydra +from autoverify.portfolio.portfolio import PortfolioScenario +from autoverify.util.resource_strategy import ResourceStrategy +from autoverify.util.verification_instance import VerificationInstance + + +def tune_hydra_portfolio( + instances: Sequence[VerificationInstance], + verifiers: Sequence[str], + resources: list[tuple[str, int, int]], + alpha: float, + length: int, + sec_per_iter: int, + output_dir: Path, + portfolio_out: Path, + *, + configs_per_iter: int = 1, + added_per_iter: int = 1, + stop_early: bool = False, + resource_strategy: ResourceStrategy = ResourceStrategy.Auto, + vnn_compat_mode: bool = False, + benchmark: str | None = None, +): + """_summary_.""" + pf_scen = PortfolioScenario( + verifiers, + # TODO: Resources, + resources, + instances, + length, + sec_per_iter, + configs_per_iter, + alpha, + added_per_iter, + stop_early, + resource_strategy, + output_dir, + vnn_compat_mode, + benchmark, + ) + + hydra = Hydra(pf_scen) + portfolio = hydra.tune_portfolio() + portfolio.to_json(portfolio_out) + print(portfolio.str_compact()) diff --git a/autoverify/types.py b/autoverify/types.py index ae02537..4b4d657 100644 --- a/autoverify/types.py +++ b/autoverify/types.py @@ -1,6 +1,6 @@ """_summary_.""" # from dataclasses import dataclass, field -from typing import Callable, Sequence +from typing import Callable from ConfigSpace import Configuration @@ -15,4 +15,4 @@ VerifierResources = tuple[str, int, int] -ResourceList = Sequence[VerifierResources] +ResourceList = list[VerifierResources] diff --git a/autoverify/util/instances.py b/autoverify/util/instances.py index f44f92a..cee732d 100644 --- a/autoverify/util/instances.py +++ b/autoverify/util/instances.py @@ -5,7 +5,7 @@ from collections.abc import Sequence from dataclasses import dataclass from pathlib import Path -from typing import Callable, Literal, overload +from typing import Callable, Iterable, Literal, overload import pandas as pd @@ -107,12 +107,33 @@ def verification_instances_to_smac_instances( return [inst.as_smac_instance() for inst in instances] +_InstancePredicate = Callable[[VerificationInstance], bool] + + +def _passes_at_least_1( + predicates: Iterable[_InstancePredicate], instance: VerificationInstance +) -> bool: + for pred in predicates: + if pred(instance): + return True + return False + + +def _passes_all( + predicates: Iterable[_InstancePredicate], instance: VerificationInstance +) -> bool: + for pred in predicates: + if not pred(instance): + return False + return True + + @overload def read_vnncomp_instances( # type: ignore benchmark: str, vnncomp_path: Path, *, - predicate: Callable[[VerificationInstance], bool] | None = None, + predicate: _InstancePredicate | Iterable[_InstancePredicate] | None = None, as_smac: Literal[False] = False, resolve_paths: bool = False, ) -> list[VerificationInstance]: @@ -124,7 +145,7 @@ def read_vnncomp_instances( benchmark: str, vnncomp_path: Path, *, - predicate: Callable[[VerificationInstance], bool] | None = None, + predicate: _InstancePredicate | Iterable[_InstancePredicate] | None = None, as_smac: Literal[True] = True, resolve_paths: bool = False, ) -> list[str]: @@ -135,7 +156,7 @@ def read_vnncomp_instances( benchmark: str, vnncomp_path: Path, *, - predicate: Callable[[VerificationInstance], bool] | None = None, + predicate: _InstancePredicate | Iterable[_InstancePredicate] | None = None, as_smac: bool = False, resolve_paths: bool = False, ) -> list[VerificationInstance] | list[str]: @@ -171,6 +192,9 @@ def read_vnncomp_instances( verification_instances = [] + if predicate and not isinstance(predicate, Iterable): + predicate = [predicate] + with open(str(instances)) as csv_file: reader = csv.reader(csv_file) @@ -186,7 +210,7 @@ def read_vnncomp_instances( int(float(timeout)), # FIXME: Timeouts can be floats ) - if predicate and not predicate(instance): + if predicate and not _passes_at_least_1(predicate, instance): continue if as_smac: diff --git a/autoverify/util/resource_strategy.py b/autoverify/util/resource_strategy.py index 5c4700c..aa9fc0e 100644 --- a/autoverify/util/resource_strategy.py +++ b/autoverify/util/resource_strategy.py @@ -1,6 +1,9 @@ """_summary_.""" from enum import Enum +from autoverify.types import ResourceList +from autoverify.util.verifiers import uses_gpu + # HACK: Can't put this in `resources.py` because # it results in a circular import @@ -9,3 +12,18 @@ class ResourceStrategy(Enum): Auto = "auto" Exact = "exact" + + +def resources_from_strategy( + rs: ResourceStrategy, verifiers: list[str] +) -> ResourceList: + """_summary_.""" + resources: ResourceList = [] + + if rs == ResourceStrategy.Auto: + for verifier in verifiers: + resources.append((verifier, 0, 1 if uses_gpu(verifier) else 0)) + else: + raise NotImplementedError(f"ResourceStrategy {rs} not supported yet.") + + return resources diff --git a/autoverify/util/target_function.py b/autoverify/util/target_function.py index ab8ca2e..2c56c1f 100644 --- a/autoverify/util/target_function.py +++ b/autoverify/util/target_function.py @@ -5,7 +5,8 @@ from autoverify.types import Cost, Instance, Seed, TargetFunction from autoverify.util.verification_instance import VerificationInstance -from autoverify.util.vnncomp import inst_bench_to_verifier +from autoverify.util.verifiers import verifier_from_name +from autoverify.util.vnncomp import inst_bench_to_kwargs, inst_bench_to_verifier from autoverify.verifier.verification_result import CompleteVerificationResult from autoverify.verifier.verifier import CompleteVerifier, Verifier @@ -115,7 +116,7 @@ def target_function( def get_pick_tf( - verifiers: list[Verifier], *, timeout_penalty: int = _DEFAULT_PAR + verifiers: list[str], benchmark: str, *, timeout_penalty: int = _DEFAULT_PAR ) -> TargetFunction: """_summary_.""" @@ -124,8 +125,16 @@ def target_function( ) -> Cost: """_summary_.""" seed += 1 # silence warning, cant rename the param to _ or smac errors + + verifier = verifiers[config["index"]] + verifier_inst = verifier_from_name(verifier) + result = _run_verification_instance( - verifiers[config["index"]], + verifier_inst( # type: ignore + **inst_bench_to_kwargs( + benchmark, verifier, VerificationInstance.from_str(instance) + ) + ), None, instance, ) diff --git a/autoverify/util/verifiers.py b/autoverify/util/verifiers.py index 913bd9b..fc5e78d 100644 --- a/autoverify/util/verifiers.py +++ b/autoverify/util/verifiers.py @@ -1,8 +1,32 @@ """_summary_.""" +from ConfigSpace import ConfigurationSpace + from autoverify.verifier import AbCrown, MnBab, Nnenum, OvalBab, Verinet from autoverify.verifier.verifier import Verifier +# HACK: Should be an attribute of the verifier +# Ideally something that specifies wether it can or +# always uses the GPU. This is mainly needed for +# resource allocation in portfolios. +def uses_gpu(verifier: str) -> bool: + """Returns if this verifier uses the GPU.""" + verifier = verifier.lower() + + if verifier == "abcrown": + return True + elif verifier == "nnenum": + return False + elif verifier == "verinet": + return True + elif verifier == "ovalbab": + return True + elif verifier == "mnbab": + return True + + raise ValueError(f"Invalid verifier name: {verifier}") + + # TODO: Dont hardcode this def get_all_complete_verifier_names() -> list[str]: """Return a list of all complete verifier names.""" @@ -15,6 +39,11 @@ def get_all_complete_verifier_names() -> list[str]: ] +def get_verifier_configspace(verifier: str) -> ConfigurationSpace: + """Get the Configuration Space of a verifier by name.""" + return verifier_from_name(verifier)().config_space + + # TODO: Dont hardcode this def verifier_from_name(name: str) -> type[Verifier]: """Return the class type from the verifier name.""" diff --git a/autoverify/util/vnncomp.py b/autoverify/util/vnncomp.py index e0f98ea..c10a709 100644 --- a/autoverify/util/vnncomp.py +++ b/autoverify/util/vnncomp.py @@ -4,49 +4,64 @@ benchmark + instance. """ from pathlib import Path +from typing import Any from ConfigSpace import Configuration from autoverify.util.verification_instance import VerificationInstance -from autoverify.verifier import AbCrown, Nnenum, OvalBab, Verinet +from autoverify.util.verifiers import verifier_from_name +from autoverify.verifier import Verinet from autoverify.verifier.verifier import CompleteVerifier -def inst_bench_to_verifier( - benchmark: str, instance: VerificationInstance, verifier: str -) -> CompleteVerifier: +# HACK: +def inst_bench_to_kwargs( + benchmark: str, + verifier: str, + instance: VerificationInstance, +) -> dict[str, Any]: """_summary_.""" if verifier == "nnenum": - return Nnenum(use_auto_settings=True) - elif verifier == "abcrown": # NOTE: Not complete + return {"use_auto_settings": True} + elif verifier == "abcrown": # TODO: All benchmarks if benchmark == "acasxu": - return AbCrown(yaml_override={"data__num_outputs": 5}) + return {"yaml_override": {"data__num_outputs": 5}} elif benchmark.startswith("sri_resnet_"): - return AbCrown( - yaml_override={ + return { + "yaml_override": { "model__onnx_quirks": "{'Reshape': {'fix_batch_size': True}}" # noqa: E501 } - ) - return AbCrown() + } + return {} elif verifier == "ovalbab": - return OvalBab() + return {} elif verifier == "verinet": if benchmark == "acasxu": - return Verinet(transpose_matmul_weights=True) + return {"transpose_matmul_weights": True} elif benchmark == "cifar2020": if instance.network.name.find("convBigRELU") >= 0: - return Verinet(dnnv_simplify=True) + return {"dnnv_simplify": True} elif benchmark == "cifar100_tinyimagenet_resnet": - return Verinet(dnnv_simplify=True) + return {"dnnv_simplify": True} elif benchmark == "nn4sys": if instance.network.name == "lindex.onnx": - return Verinet(dnnv_simplify=True) - - return Verinet() + return {"dnnv_simplify": True} + return {} raise ValueError("Invalid verifier") +def inst_bench_to_verifier( + benchmark: str, instance: VerificationInstance, verifier: str +) -> CompleteVerifier: + """_summary_.""" + verifier_inst = verifier_from_name(verifier)( + **inst_bench_to_kwargs(benchmark, verifier, instance) + ) + assert isinstance(verifier_inst, CompleteVerifier) + return verifier_inst + + def _get_abcrown_config(benchmark: str, instance: VerificationInstance) -> str: net_name = instance.network.name diff --git a/autoverify/verifier/complete/abcrown/abcrown_yaml_config.py b/autoverify/verifier/complete/abcrown/abcrown_yaml_config.py index 429d103..1901f52 100644 --- a/autoverify/verifier/complete/abcrown/abcrown_yaml_config.py +++ b/autoverify/verifier/complete/abcrown/abcrown_yaml_config.py @@ -56,7 +56,7 @@ def from_config( yaml_override: dict[str, Any] | None = None, ): """Initialize the YAML file based on the configuration.""" - dict_config: dict[str, Any] = config.get_dictionary() + dict_config: dict[str, Any] = dict(config) abcrown_dict: dict[str, Any] = {} for key, value in dict_config.items(): diff --git a/autoverify/verifier/complete/ovalbab/ovalbab_json_config.py b/autoverify/verifier/complete/ovalbab/ovalbab_json_config.py index af8d16e..049665e 100644 --- a/autoverify/verifier/complete/ovalbab/ovalbab_json_config.py +++ b/autoverify/verifier/complete/ovalbab/ovalbab_json_config.py @@ -29,7 +29,7 @@ def from_json(cls, json_file: Path): @classmethod def from_config(cls, config: Configuration): """_summary.""" - dict_config: dict[str, Any] = config.get_dictionary() + dict_config: dict[str, Any] = dict(config) ovalbab_dict: dict[str, Any] = { "bounding": { "nets": [ diff --git a/pyproject.toml b/pyproject.toml index 7bc93de..92510f8 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -91,3 +91,6 @@ push = false "pyproject.toml" = ['version = "{version}"'] "README.md" = ["{version}"] "autoverify/__init__.py" = ['__version__ = "{version}"'] + +[tool.setuptools] +py-modules = ["autoverify"] diff --git a/scripts/tuning/hydra.py b/scripts/tuning/hydra.py new file mode 100644 index 0000000..5294dc5 --- /dev/null +++ b/scripts/tuning/hydra.py @@ -0,0 +1,133 @@ +import argparse +from pathlib import Path + +from autoverify.tune.tune_hydra import tune_hydra_portfolio +from autoverify.util.instances import read_vnncomp_instances +from autoverify.util.resource_strategy import ( + ResourceStrategy, + resources_from_strategy, +) +from autoverify.util.vnncomp_filters import filters + + +def build_argparser() -> argparse.ArgumentParser: + parser = argparse.ArgumentParser() + + parser.add_argument( + "--verifiers", + nargs="+", + type=str, + help="Verifiers to consider", + required=True, + ) + parser.add_argument( + "--benchmark", + type=str, + help="Name of the VNNCOMP benchmark", + required=True, + ) + parser.add_argument( + "--vnncomp_path", + type=Path, + help="Path to VNNCOMP benchmarks", + required=True, + ) + parser.add_argument( + "--filter", + type=str, + help="Name of filter for instances", + ) + parser.add_argument( + "--length", + type=int, + help="Length of the portfolio", + required=True, + ) + parser.add_argument( + "--sec_per_iter", + type=int, + help="Walltime limit per Hydra iteration", + required=True, + ) + parser.add_argument( + "--alpha", + type=float, + help="Alpha (in [0, 1]), tune/pick split", + required=True, + ) + parser.add_argument( + "--output_dir", + type=Path, + help="Hydra output directory", + required=True, + ) + parser.add_argument( + "--portfolio_out", + type=Path, + help="Portfolio output file", + required=True, + ) + parser.add_argument( + "--configs_per_iter", + type=int, + help="Configurations to tune per Hydra iteration", + default=1, + ) + parser.add_argument( + "--added_per_iter", + type=int, + help="Number of configs added to the portfolio per Hydra iteration", + default=1, + ) + parser.add_argument( + "--stop_early", + type=bool, + help="Wether to stop early when performance stagnates", + default=False, + ) + parser.add_argument( + "--resource_strategy", + type=str, + choices=[v.value for v in ResourceStrategy], + help="Resource allocation strategy", + default="auto", + ) + parser.add_argument( + "--vnn_compat", + action=argparse.BooleanOptionalAction, + default=False, + help="Use VNNCOMP compatible mode", + ) + + return parser + + +if __name__ == "__main__": + parser = build_argparser() + args = parser.parse_args() + + instances = read_vnncomp_instances( + args.benchmark, + vnncomp_path=args.vnncomp_path, + predicate=filters.get(args.filter), + ) + + args.resource_strategy = ResourceStrategy(args.resource_strategy) + resources = resources_from_strategy(args.resource_strategy, args.verifiers) + + tune_hydra_portfolio( + instances, + args.verifiers, + resources, + args.alpha, + args.length, + args.sec_per_iter, + args.output_dir, + args.portfolio_out, + configs_per_iter=args.configs_per_iter, + added_per_iter=args.added_per_iter, + stop_early=args.stop_early, + resource_strategy=args.resource_strategy, + vnn_compat_mode=args.vnn_compat, + benchmark=args.benchmark, + ) diff --git a/scripts/tuning/tune_verifier_vnncomp.py b/scripts/tuning/tune_verifier_vnncomp.py index be7a350..24531cb 100644 --- a/scripts/tuning/tune_verifier_vnncomp.py +++ b/scripts/tuning/tune_verifier_vnncomp.py @@ -2,7 +2,6 @@ import argparse from pathlib import Path -from autoverify.tune import smac_tune_verifier from autoverify.tune.tune_verifier import vnn_smac_tune_verifier from autoverify.util.instances import read_vnncomp_instances from autoverify.util.verifiers import verifier_from_name @@ -102,16 +101,6 @@ def build_argparser() -> argparse.ArgumentParser: rh_csv_path=args.rh_csv_path, ) - # config = smac_tune_verifier( - # verifier, - # instances, - # args.time, - # output_dir=output_dir, - # config_out=config_out, - # run_name=args.run_name, - # rh_csv_path=args.rh_csv_path, - # ) - print("*" * 80) print("Incumbent:") print(config) diff --git a/tests/test_portfolio/test_portfolio.py b/tests/test_portfolio/test_portfolio.py index 7d068b6..87cb186 100644 --- a/tests/test_portfolio/test_portfolio.py +++ b/tests/test_portfolio/test_portfolio.py @@ -68,8 +68,14 @@ def test_to_json(portfolio: Portfolio, tmpdir: Path): assert all(v for v in seen.values()) -def test_from_json(portfolio_json: Path): - pf = Portfolio.from_json(portfolio_json) +def test_from_json( + portfolio_json: Path, simple_configspace: ConfigurationSpace +): + cfg_space_map = { + "foo": simple_configspace, + "hello": simple_configspace, + } + pf = Portfolio.from_json(portfolio_json, cfg_space_map) assert len(pf) == 2 cvs = list(pf) @@ -77,3 +83,4 @@ def test_from_json(portfolio_json: Path): assert cvs[0].verifier == "foo" assert cvs[1].verifier == "hello" + assert isinstance(cvs[0].configuration, Configuration) # TODO: diff --git a/tests/test_util/test_instances.py b/tests/test_util/test_instances.py index 9080a11..f94fef2 100644 --- a/tests/test_util/test_instances.py +++ b/tests/test_util/test_instances.py @@ -233,7 +233,15 @@ def _check_path(p: Path) -> bool: def _nano_filter(inst: VerificationInstance) -> bool: return inst.network.name == "test_nano.onnx" + def _sat_filter(inst: VerificationInstance) -> bool: + return inst.network.name == "test_sat.onnx" + instances = read_vnncomp_instances( bench_name, vnncomp_path, predicate=_nano_filter ) assert len(instances) == 2 + + instances = read_vnncomp_instances( + bench_name, vnncomp_path, predicate=[_nano_filter, _sat_filter] + ) + assert len(instances) == 4