A high-level functional language for writing mathematically-precise specifications for neural networks.

Navigation

Verified details

These details have been verified by PyPI
Maintainers
Avatar for matthewdaggitt from gravatar.com matthewdaggitt Avatar for wenkokke from gravatar.com wenkokke

Unverified details

These details have not been verified by PyPI
Meta
  • License Expression: MIT
    SPDX License Expression
  • Author: Wen Kokke
  • Requires: Python <3.14, >=3.10
  • Provides-Extra: test , mypy , pygments , numpy , jax , dev , wheel , tensorflow , pytorch
Report project as malware

Project description

PyPI GitHub tag (latest by date) GitHub Workflow Status readthedocs status pre-commit.ci status

Vehicle

Vehicle is a system for embedding logical specifications into neural networks. At its heart is the Vehicle specification language, a high-level, functional language for writing mathematically-precise specifications for your networks. For example, the following simple specification says that a network's output should be monotonically increasing with respect to its third input.

Example specification

These specifications can then automatically be compiled down to loss functions to be used when training your network. After training, the same specification can be compiled down to low-level neural network verifiers such as Marabou which either prove that the specification holds or produce a counter-example. Such a proof is far better than simply testing, as you can prove that the specification holds for all inputs. Verified specifications can also be exported to interactive theorem provers (ITPs) such as Agda. This in turn allows for the formal verification of larger software systems that use neural networks as subcomponents. The generated ITP code is tightly linked to the actual deployed network, so changes to the network will result in errors when checking the larger proof.

Documentation

Examples

Each of the following examples comes with an explanatory README file:

  • ACAS Xu - The complete specification of the ACAS Xu collision avoidance system from the Reluplex paper in a single file.

  • Car controller - A neural network controller that is formally proven to always keep a simple model of a car on the road in the face of noisy sensor data and an unpredictable cross-wind.

  • MNIST robustness - A classifier for the MNIST dataset that is proven to be robust around the images in the dataset.

In addition to the above, further examples of specifications can be found in the test suite and the corresponding output of the Vehicle compiler can be found here.

Support

If you are interested in adding support for a particular format/verifier/ITP then open an issue on the Issue Tracker to discuss it with us.

Neural network formats

Dataset formats

Verifier backends

Interactive Theorem Prover backends

Related papers

Project details

Verified details

These details have been verified by PyPI
Maintainers
Avatar for matthewdaggitt from gravatar.com matthewdaggitt Avatar for wenkokke from gravatar.com wenkokke

Unverified details

These details have not been verified by PyPI
Meta
  • License Expression: MIT
    SPDX License Expression
  • Author: Wen Kokke
  • Requires: Python <3.14, >=3.10
  • Provides-Extra: test , mypy , pygments , numpy , jax , dev , wheel , tensorflow , pytorch

Release history Release notifications | RSS feed

This version

0.23.0

0.22.0

0.21.0

0.20.0

0.19.0

0.18.0

0.17.0

0.16.1

0.15.0

0.14.1

0.13.0

0.11.1

0.10.0

0.9.0

0.8.0

0.7.0

0.6.0

0.5.1

0.4.1

0.3.3

Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Source Distributions

No source distribution files available for this release.See tutorial on generating distribution archives.

Built Distributions

If you're not sure about the file name format, learn more about wheel file names.

vehicle_lang-0.23.0-cp313-cp313-win_amd64.whl (13.4 MB view details)

Uploaded CPython 3.13Windows x86-64

vehicle_lang-0.23.0-cp313-cp313-musllinux_1_1_x86_64.whl (22.6 MB view details)

Uploaded CPython 3.13musllinux: musl 1.1+ x86-64

vehicle_lang-0.23.0-cp313-cp313-manylinux_2_28_x86_64.whl (22.1 MB view details)

Uploaded CPython 3.13manylinux: glibc 2.28+ x86-64

vehicle_lang-0.23.0-cp313-cp313-macosx_11_0_arm64.whl (17.8 MB view details)

Uploaded CPython 3.13macOS 11.0+ ARM64

vehicle_lang-0.23.0-cp313-cp313-macosx_10_13_x86_64.whl (18.3 MB view details)

Uploaded CPython 3.13macOS 10.13+ x86-64

vehicle_lang-0.23.0-cp312-cp312-win_amd64.whl (13.4 MB view details)

Uploaded CPython 3.12Windows x86-64

vehicle_lang-0.23.0-cp312-cp312-musllinux_1_1_x86_64.whl (22.6 MB view details)

Uploaded CPython 3.12musllinux: musl 1.1+ x86-64

vehicle_lang-0.23.0-cp312-cp312-manylinux_2_28_x86_64.whl (22.1 MB view details)

Uploaded CPython 3.12manylinux: glibc 2.28+ x86-64

vehicle_lang-0.23.0-cp312-cp312-macosx_11_0_arm64.whl (17.8 MB view details)

Uploaded CPython 3.12macOS 11.0+ ARM64

vehicle_lang-0.23.0-cp312-cp312-macosx_10_13_x86_64.whl (18.3 MB view details)

Uploaded CPython 3.12macOS 10.13+ x86-64

vehicle_lang-0.23.0-cp311-cp311-win_amd64.whl (13.4 MB view details)

Uploaded CPython 3.11Windows x86-64

vehicle_lang-0.23.0-cp311-cp311-musllinux_1_1_x86_64.whl (22.6 MB view details)

Uploaded CPython 3.11musllinux: musl 1.1+ x86-64

vehicle_lang-0.23.0-cp311-cp311-manylinux_2_28_x86_64.whl (22.1 MB view details)

Uploaded CPython 3.11manylinux: glibc 2.28+ x86-64

vehicle_lang-0.23.0-cp311-cp311-macosx_11_0_arm64.whl (17.8 MB view details)

Uploaded CPython 3.11macOS 11.0+ ARM64

vehicle_lang-0.23.0-cp311-cp311-macosx_10_10_x86_64.whl (18.3 MB view details)

Uploaded CPython 3.11macOS 10.10+ x86-64

vehicle_lang-0.23.0-cp310-cp310-win_amd64.whl (13.4 MB view details)

Uploaded CPython 3.10Windows x86-64

vehicle_lang-0.23.0-cp310-cp310-musllinux_1_1_x86_64.whl (22.6 MB view details)

Uploaded CPython 3.10musllinux: musl 1.1+ x86-64

vehicle_lang-0.23.0-cp310-cp310-manylinux_2_28_x86_64.whl (22.1 MB view details)

Uploaded CPython 3.10manylinux: glibc 2.28+ x86-64

vehicle_lang-0.23.0-cp310-cp310-macosx_11_0_arm64.whl (17.8 MB view details)

Uploaded CPython 3.10macOS 11.0+ ARM64

vehicle_lang-0.23.0-cp310-cp310-macosx_10_10_x86_64.whl (18.3 MB view details)

Uploaded CPython 3.10macOS 10.10+ x86-64

File details

Details for the file vehicle_lang-0.23.0-cp313-cp313-win_amd64.whl.

File metadata

File hashes

Hashes for vehicle_lang-0.23.0-cp313-cp313-win_amd64.whl
Algorithm Hash digest
SHA256 b298a1256cb371a7e9ea42da7c940b87d5e3dca35fa92f36133bf51ed4c14b83
MD5 f42cb2bbd8f957cbbae0497e8041e7b7
BLAKE2b-256 63fbbafb9f2881c0c739ea68918c842ea7089562f7842cd26270bc6428e62d54

See more details on using hashes here.

Provenance

The following attestation bundles were made for vehicle_lang-0.23.0-cp313-cp313-win_amd64.whl:

Publisher: ci.yml on vehicle-lang/vehicle

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file vehicle_lang-0.23.0-cp313-cp313-musllinux_1_1_x86_64.whl.

File metadata

File hashes

Hashes for vehicle_lang-0.23.0-cp313-cp313-musllinux_1_1_x86_64.whl
Algorithm Hash digest
SHA256 af0d47a56bf35db550fe4a57ea8cfdb354f1c789952420f2731dc6cf659bda1b
MD5 ca19adea7c0b586d90a544914256e926
BLAKE2b-256 ccd99535e166716a7ebcd9d4b11abe99959cbfa9e0a780d4b3f95803b113778c

See more details on using hashes here.

Provenance

The following attestation bundles were made for vehicle_lang-0.23.0-cp313-cp313-musllinux_1_1_x86_64.whl:

Publisher: ci.yml on vehicle-lang/vehicle

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file vehicle_lang-0.23.0-cp313-cp313-manylinux_2_28_x86_64.whl.

File metadata

File hashes

Hashes for vehicle_lang-0.23.0-cp313-cp313-manylinux_2_28_x86_64.whl
Algorithm Hash digest
SHA256 26730a759147422705a5f6f4e33defef82ce1c7fe311fa9871e7618a8f280da0
MD5 4868cffdb0ad185c1a3af68360815233
BLAKE2b-256 cb9d6d2f0b25dfd51a754f9eac5099cb19f1a6679aa56fad3aa79abb76bb1399

See more details on using hashes here.

Provenance

The following attestation bundles were made for vehicle_lang-0.23.0-cp313-cp313-manylinux_2_28_x86_64.whl:

Publisher: ci.yml on vehicle-lang/vehicle

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file vehicle_lang-0.23.0-cp313-cp313-macosx_11_0_arm64.whl.

File metadata

File hashes

Hashes for vehicle_lang-0.23.0-cp313-cp313-macosx_11_0_arm64.whl
Algorithm Hash digest
SHA256 7f69a70a4ba49101b2e6594d4585f5b9e463677758d19274f7eaaa65d2c9454a
MD5 d0bf979ae2e16656d387b2138fc00064
BLAKE2b-256 a7cd6fba691646e6a3fa206576a48a06a6fe1cd747bc32ce6f8ea096d27c2265

See more details on using hashes here.

Provenance

The following attestation bundles were made for vehicle_lang-0.23.0-cp313-cp313-macosx_11_0_arm64.whl:

Publisher: ci.yml on vehicle-lang/vehicle

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file vehicle_lang-0.23.0-cp313-cp313-macosx_10_13_x86_64.whl.

File metadata

File hashes

Hashes for vehicle_lang-0.23.0-cp313-cp313-macosx_10_13_x86_64.whl
Algorithm Hash digest
SHA256 58d038a51be53899666a2b7be674315736b4255be16078c206cf4e5847985a79
MD5 9c96cb5c859b0c3d605c5fa15cdf84cc
BLAKE2b-256 22488dcd64ac41f5dff26aed88eab29c2702cf709d5e35ec07fb73aabda39d4c

See more details on using hashes here.

Provenance

The following attestation bundles were made for vehicle_lang-0.23.0-cp313-cp313-macosx_10_13_x86_64.whl:

Publisher: ci.yml on vehicle-lang/vehicle

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file vehicle_lang-0.23.0-cp312-cp312-win_amd64.whl.

File metadata

File hashes

Hashes for vehicle_lang-0.23.0-cp312-cp312-win_amd64.whl
Algorithm Hash digest
SHA256 b2ee4089db9645ba4fd1cd63d97f5cafa31c029d318d05f883267ad2556ba996
MD5 ffb82e1a531f9b0010d7c3a3913105d8
BLAKE2b-256 83c1c866f35b1bc8eba369dbf50aba4ef4c356e6690a4f2e935b35c2119c81bc

See more details on using hashes here.

Provenance

The following attestation bundles were made for vehicle_lang-0.23.0-cp312-cp312-win_amd64.whl:

Publisher: ci.yml on vehicle-lang/vehicle

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file vehicle_lang-0.23.0-cp312-cp312-musllinux_1_1_x86_64.whl.

File metadata

File hashes

Hashes for vehicle_lang-0.23.0-cp312-cp312-musllinux_1_1_x86_64.whl
Algorithm Hash digest
SHA256 a558682a8d745eb61bd7cca5c3168b246040bddbb3996828ab1d397c08904fdf
MD5 6aa86d7f6a6d838dba824f2b6b5db548
BLAKE2b-256 6f28d68f39732605e3f04ffd619c8c1001ebe10b91dfb0256af74180f0335063

See more details on using hashes here.

Provenance

The following attestation bundles were made for vehicle_lang-0.23.0-cp312-cp312-musllinux_1_1_x86_64.whl:

Publisher: ci.yml on vehicle-lang/vehicle

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file vehicle_lang-0.23.0-cp312-cp312-manylinux_2_28_x86_64.whl.

File metadata

File hashes

Hashes for vehicle_lang-0.23.0-cp312-cp312-manylinux_2_28_x86_64.whl
Algorithm Hash digest
SHA256 9a450ddcffde31e57ccad2f15d4e32266c2ab80107daa699e5c1268d2199f51c
MD5 f551f790c8d77222d4cb9b331c218c1a
BLAKE2b-256 d15f42246dc85148b41b1aea0c8cdf9b81ea851a27cccbf9f6c4b180086e6ad2

See more details on using hashes here.

Provenance

The following attestation bundles were made for vehicle_lang-0.23.0-cp312-cp312-manylinux_2_28_x86_64.whl:

Publisher: ci.yml on vehicle-lang/vehicle

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file vehicle_lang-0.23.0-cp312-cp312-macosx_11_0_arm64.whl.

File metadata

File hashes

Hashes for vehicle_lang-0.23.0-cp312-cp312-macosx_11_0_arm64.whl
Algorithm Hash digest
SHA256 b8af263f8b0308594e9cac4b915da3648001c411faacf1779135101fda0ea30b
MD5 93e65c2d9fd42b9406defabc5307f6f2
BLAKE2b-256 61b051cac9e21600de875197271b02c886bf8c89dc09866ce271ac07c5a7fbbc

See more details on using hashes here.

Provenance

The following attestation bundles were made for vehicle_lang-0.23.0-cp312-cp312-macosx_11_0_arm64.whl:

Publisher: ci.yml on vehicle-lang/vehicle

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file vehicle_lang-0.23.0-cp312-cp312-macosx_10_13_x86_64.whl.

File metadata

File hashes

Hashes for vehicle_lang-0.23.0-cp312-cp312-macosx_10_13_x86_64.whl
Algorithm Hash digest
SHA256 fbdd9828daff7d01b35b75c9d170e3b952b60963b6baa40b753a023f0672a2e0
MD5 a24619b24964649f2eb7b7ac94a7b919
BLAKE2b-256 4642fd22d04155f0e26cf6376016875c0e0dfda3cc6ab3d1c62416e0aaaddd02

See more details on using hashes here.

Provenance

The following attestation bundles were made for vehicle_lang-0.23.0-cp312-cp312-macosx_10_13_x86_64.whl:

Publisher: ci.yml on vehicle-lang/vehicle

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file vehicle_lang-0.23.0-cp311-cp311-win_amd64.whl.

File metadata

File hashes

Hashes for vehicle_lang-0.23.0-cp311-cp311-win_amd64.whl
Algorithm Hash digest
SHA256 0e87e864126385c963d785cf2b817e8aead93a211304916d5d1b68b9ecba5859
MD5 6ca80b6e9e8b0c39c80b53a1871eac87
BLAKE2b-256 9dd9450fe0f9d0dbeea67391f908d2e9046bc8f8cd4b5791a68b2834102ade88

See more details on using hashes here.

Provenance

The following attestation bundles were made for vehicle_lang-0.23.0-cp311-cp311-win_amd64.whl:

Publisher: ci.yml on vehicle-lang/vehicle

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file vehicle_lang-0.23.0-cp311-cp311-musllinux_1_1_x86_64.whl.

File metadata

File hashes

Hashes for vehicle_lang-0.23.0-cp311-cp311-musllinux_1_1_x86_64.whl
Algorithm Hash digest
SHA256 5c8a9c3d725740d0dd12d7fb83a4366cfb3b8be0d2a8cae16c3ab67a60b4b767
MD5 1ab020ebd93fe3b5fc19dffbdb21edeb
BLAKE2b-256 7847891eb62c2f40f5152d4a199ee3a00522754ee0da81c3b6fbfb0cf8321179

See more details on using hashes here.

Provenance

The following attestation bundles were made for vehicle_lang-0.23.0-cp311-cp311-musllinux_1_1_x86_64.whl:

Publisher: ci.yml on vehicle-lang/vehicle

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file vehicle_lang-0.23.0-cp311-cp311-manylinux_2_28_x86_64.whl.

File metadata

File hashes

Hashes for vehicle_lang-0.23.0-cp311-cp311-manylinux_2_28_x86_64.whl
Algorithm Hash digest
SHA256 a5deedc8c670322dd54e53ed9e00d746518c4a05a48a7636490df3a3f6854187
MD5 f2f77c2e01a1f85c6d8c8cb5b2514dfa
BLAKE2b-256 ae6a8ed647b07e917b03ff487b3638c62de0ae57ec3cda52bfbbe337b75acf20

See more details on using hashes here.

Provenance

The following attestation bundles were made for vehicle_lang-0.23.0-cp311-cp311-manylinux_2_28_x86_64.whl:

Publisher: ci.yml on vehicle-lang/vehicle

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file vehicle_lang-0.23.0-cp311-cp311-macosx_11_0_arm64.whl.

File metadata

File hashes

Hashes for vehicle_lang-0.23.0-cp311-cp311-macosx_11_0_arm64.whl
Algorithm Hash digest
SHA256 62de785f3348928de293592eff03cc7d6e40e2d2e8ac770da83f4832c0aa83da
MD5 8b27d63bfb5222afefb920c194d45802
BLAKE2b-256 b1fb5af406a620a08a51bb19c3a8cfa4b7cebf73f4f271a3d3dda14848261d11

See more details on using hashes here.

Provenance

The following attestation bundles were made for vehicle_lang-0.23.0-cp311-cp311-macosx_11_0_arm64.whl:

Publisher: ci.yml on vehicle-lang/vehicle

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file vehicle_lang-0.23.0-cp311-cp311-macosx_10_10_x86_64.whl.

File metadata

File hashes

Hashes for vehicle_lang-0.23.0-cp311-cp311-macosx_10_10_x86_64.whl
Algorithm Hash digest
SHA256 cdc56a34c22e9978d81499999726e71a742d75a2135edacbd587dba697fd6b94
MD5 3c0aabb1962f0bd8f9b8bddc6e3aa7b6
BLAKE2b-256 3686d5205a4801b58c3991b4cc6011c1b706428355fb13a4184390dcad414eba

See more details on using hashes here.

Provenance

The following attestation bundles were made for vehicle_lang-0.23.0-cp311-cp311-macosx_10_10_x86_64.whl:

Publisher: ci.yml on vehicle-lang/vehicle

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file vehicle_lang-0.23.0-cp310-cp310-win_amd64.whl.

File metadata

File hashes

Hashes for vehicle_lang-0.23.0-cp310-cp310-win_amd64.whl
Algorithm Hash digest
SHA256 e8de20d4de7edbe5ea29829e02c3a7c947c1ac5fa9e2aa90486cd1988c8c7149
MD5 01594db643d10e334dcc64e7a1e43905
BLAKE2b-256 5f9e9f50e99adbef8c8bb07e19b824691ba9df019d2fb3c58247649c8d3de7a1

See more details on using hashes here.

Provenance

The following attestation bundles were made for vehicle_lang-0.23.0-cp310-cp310-win_amd64.whl:

Publisher: ci.yml on vehicle-lang/vehicle

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file vehicle_lang-0.23.0-cp310-cp310-musllinux_1_1_x86_64.whl.

File metadata

File hashes

Hashes for vehicle_lang-0.23.0-cp310-cp310-musllinux_1_1_x86_64.whl
Algorithm Hash digest
SHA256 8e384645de41814aaae2dd9e9f197bde5ded5a0b2a308f2cc256f1b31db11250
MD5 59d3d149660f7ce3e1e7ee7d9fae317c
BLAKE2b-256 9df846a9f4dd8d0b519a99f41d9a2e110c6864bfbc586339de727529d3a22007

See more details on using hashes here.

Provenance

The following attestation bundles were made for vehicle_lang-0.23.0-cp310-cp310-musllinux_1_1_x86_64.whl:

Publisher: ci.yml on vehicle-lang/vehicle

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file vehicle_lang-0.23.0-cp310-cp310-manylinux_2_28_x86_64.whl.

File metadata

File hashes

Hashes for vehicle_lang-0.23.0-cp310-cp310-manylinux_2_28_x86_64.whl
Algorithm Hash digest
SHA256 a1435b575e225f585dc845ba6b83310e97afaac9518ae3d11533f52e38e80d44
MD5 6e4f5454ccd222668d814b19c153db10
BLAKE2b-256 e221d08e8b3f7c5dc6a2dcb4189f882596413377e1b4024a50a486aea8be8e41

See more details on using hashes here.

Provenance

The following attestation bundles were made for vehicle_lang-0.23.0-cp310-cp310-manylinux_2_28_x86_64.whl:

Publisher: ci.yml on vehicle-lang/vehicle

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file vehicle_lang-0.23.0-cp310-cp310-macosx_11_0_arm64.whl.

File metadata

File hashes

Hashes for vehicle_lang-0.23.0-cp310-cp310-macosx_11_0_arm64.whl
Algorithm Hash digest
SHA256 5b11ae9f0ed41480edd3fd4e9b7fbe9ec880c5b4697f5a925ea23657e68d34cd
MD5 329a8cf34e41c310a68bf266821c6f6d
BLAKE2b-256 99ac7ce1c65f14944d77f8fdfc4c0dda2b2129b3e7dc3ec1e10bcea6d970beda

See more details on using hashes here.

Provenance

The following attestation bundles were made for vehicle_lang-0.23.0-cp310-cp310-macosx_11_0_arm64.whl:

Publisher: ci.yml on vehicle-lang/vehicle

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file vehicle_lang-0.23.0-cp310-cp310-macosx_10_10_x86_64.whl.

File metadata

File hashes

Hashes for vehicle_lang-0.23.0-cp310-cp310-macosx_10_10_x86_64.whl
Algorithm Hash digest
SHA256 0cd2dedf2462f550c3b94e89f49da45c0d60f63751a95a3a6c2a2de6b5d08e82
MD5 9ddc80548f74516cf1573775e4dafac0
BLAKE2b-256 7cd8c1cd70d81552981e233095cb1c70cec1e7fc0ba17113bc4f4b747024f971

See more details on using hashes here.

Provenance

The following attestation bundles were made for vehicle_lang-0.23.0-cp310-cp310-macosx_10_10_x86_64.whl:

Publisher: ci.yml on vehicle-lang/vehicle

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

Supported by

AWS Cloud computing and Security Sponsor Datadog Monitoring Depot Continuous Integration Fastly CDN Google Download Analytics Pingdom Monitoring Sentry Error logging StatusPage Status page