Python API
Loss functions
- class vehicle_lang.DifferentiableLogic(value)
The differentiable logics supported by Vehicle.
Verification
- vehicle_lang.verify(specification: str | Path, properties: Iterable[str] | None = None, networks: Dict[str, str | Path] = {}, datasets: Dict[str, str | Path] = {}, parameters: Dict[str, Any] = {}, verifier: Verifier = Verifier.Marabou, verifier_location: str | Path | None = None, cache: str | Path | None = None) None
Check whether properties in a Vehicle specification hold.
- Parameters:
specification (str | Path) – The path to the Vehicle specification file to verify.
properties (Iterable[str] | None) – The names of the properties in the specification to verify, defaults to all declarations.
networks (Dict[str, str | Path]) – A map from the network names in the specification to files containing the networks.
datasets (Dict[str, str | Path]) – A map from the dataset names in the specification to files containing the datasets.
parameters (Dict[str, Any]) – A map from the parameter names in the specification to the values to be used in verification.
verifier (Verifier) – The verifier to be used, defaults to Marabou.
verifier_location (str | Path | None) – The path to the verifier executable, defaults to searching the system path.
cache (str | Path | None) – The path to the proof cache used by Vehicle, defaults to not writing a proof cache.
- class vehicle_lang.Verifier(value)
The neural network verifiers supported by Vehicle.
- Marabou = 1
The Marabou verifier.
Exceptions
- exception vehicle_lang.error.VehicleError
- exception vehicle_lang.error.VehicleInternalError