Python API

Loss functions

vehicle_lang.load_loss_function(path: str | Path, property_name: str, *, target: DifferentiableLogic = DifferentiableLogic.Vehicle, samplers: Dict[str, Callable[[Dict[str, Any]], Iterator[Any]]] = {}) → Any

Load a loss function from a property in a Vehicle specification.

Parameters:

  • path (str | Path) – The path to the Vehicle specification file.

  • property_name (str) – The name of the Vehicle property to load.

  • target (DifferentiableLogic) – The differentiable logic to use for interpreting the Vehicle property as a loss function, defaults to the Vehicle logic.

  • samplers (Dict[str, Callable[[Dict[str, Any]], Iterator[Any]]]) – A map from quantified variable names to samplers for their values. See Sampler for more details.

Returns:

A function that takes the required external resources in the specification as keyword arguments and returns the loss corresponding to the property.

Return type:

Any

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.VehicleBuiltinUnsupported(builtin_name: str)
exception vehicle_lang.error.VehicleError
exception vehicle_lang.error.VehicleInternalError
exception vehicle_lang.error.VehiclePropertyNotFound(property_name: str)
exception vehicle_lang.error.VehicleSessionClosed
exception vehicle_lang.error.VehicleSessionUsed