vehicle-lang

A toolkit for enforcing logical specifications on neural networks

Science Score: 64.0%

This score indicates how likely this project is to be science-related based on various indicators:

✓
CITATION.cff file
Found CITATION.cff file
✓
codemeta.json file
Found codemeta.json file
✓
.zenodo.json file
Found .zenodo.json file
○
DOI references
✓
Academic publication links
Links to: arxiv.org
✓
Committers with academic emails
1 of 9 committers (11.1%) from academic institutions
○
Institutional organization owner
○
JOSS paper metadata
○
Scientific vocabulary similarity
Low similarity (12.8%) to scientific vocabulary

Keywords

agda haskell neural-network specification verification

Keywords from Contributors

energy-system-model mesh interpretability parallel optimizer yolov5s pipeline-testing datacleaner data-profilers particles

Last synced: 6 months ago · JSON representation ·

Repository

A toolkit for enforcing logical specifications on neural networks

Basic Info

Host: GitHub
Owner: vehicle-lang
License: other
Language: Haskell
Default Branch: dev
Homepage: https://vehicle-lang.readthedocs.io/
Size: 25 MB

Statistics

Stars: 110
Watchers: 7
Forks: 12
Open Issues: 107
Releases: 24

Topics

agda haskell neural-network specification verification

Created almost 5 years ago · Last pushed 6 months ago

Metadata Files

Readme Changelog Contributing License Citation Codeowners

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

ONNX

Dataset formats

Verifier backends

Marabou

Interactive Theorem Prover backends

Agda
Rocq

Related papers

Owner

Name: vehicle-lang
Login: vehicle-lang
Kind: organization
Location: United Kingdom

Repositories: 3
Profile: https://github.com/vehicle-lang

Citation (CITATION.cff)

cff-version: "1.2.0"
message: "If you use this software, please cite it using these metadata."
title: "Vehicle"
authors:
  - family-names: "Daggitt"
    given-names: "Matthew"
  - family-names: "Kokke"
    given-names: "Wen"
  - family-names: "Ślusarz"
    given-names: "Natalia"
  - family-names: "Atkey"
    given-names: "Robert"
  - family-names: "Casadio"
    given-names: "Marco"
  - family-names: "Komendantskaya"
    given-names: "Ekaterina"
version: "0.19.0"
date-released: "2025-08-26"
license: "BSD-3-Clause"
type: "software"
repository-artifact: "https://github.com/vehicle-lang/vehicle/releases/tag/v0.19.0"
repository-code: "https://github.com/vehicle-lang/vehicle"
references:
  - authors:
      - family-names: "Daggitt"
        given-names: "Matthew"
      - family-names: "Kokke"
        given-names: "Wen"
      - family-names: "Atkey"
        given-names: "Robert"
      - family-names: "Ślusarz"
        given-names: "Natalia"
      - family-names: "Arnaboldi"
        given-names: "Luca"
      - family-names: "Komendantskaya"
        given-names: "Ekaterina"
    doi: "10.48550/arXiv.2401.06379"
    month: 1
    status: "submitted"
    title: "Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs"
    type: "conference-paper"
    year: "2024"
    url: "https://arxiv.org/abs/2401.06379"
  - authors:
      - family-names: "Daggitt"
        given-names: "Matthew"
      - family-names: "Kokke"
        given-names: "Wen"
      - family-names: "Atkey"
        given-names: "Robert"
    doi: "10.48550/arXiv.2402.01353"
    month: 1
    status: "submitted"
    title: "Efficient compilation of expressive problem space specifications to neural network solvers"
    type: "conference-paper"
    year: "2024"
    url: "https://arxiv.org/abs/2402.01353"
  - authors:
      - family-names: "Daggitt"
        given-names: "Matthew"
      - family-names: "Kokke"
        given-names: "Wen"
      - family-names: "Atkey"
        given-names: "Robert"
      - family-names: "Arnaboldi"
        given-names: "Luca"
      - family-names: "Komendantskaya"
        given-names: "Ekaterina"
    doi: "10.48550/arXiv.2202.05207"
    keywords:
      - Neural networks
      - verification
      - Interactive Theorem Provers
      - Agda
      - Marabou
    month: 2
    title: "Vehicle: Interfacing Neural Network Verifiers with Interactive Theorem Provers"
    type: "unpublished"
    year: "2022"
    url: "https://arxiv.org/abs/2202.05207"
identifiers:
  - type: url
    value: "https://github.com/vehicle-lang/vehicle/releases/tag/v0.17.0"
    description: "The GitHub release URL of tag v0.17.0."
  - type: url
    value: "https://gpypi.org/project/vehicle-lang/0.17.0/"
    description: "The PyPI release URL of version 0.17.0."
  - type: url
    value: "https://github.com/vehicle-lang/vehicle/releases/tag/v0.16.1"
    description: "The GitHub release URL of tag v0.16.1."
  - type: url
    value: "https://gpypi.org/project/vehicle-lang/0.16.1/"
    description: "The PyPI release URL of version 0.16.1."
  - type: url
    value: "https://github.com/vehicle-lang/vehicle/releases/tag/v0.16.0"
    description: "The GitHub release URL of tag v0.16.0."
  - type: url
    value: "https://gpypi.org/project/vehicle-lang/0.16.0/"
    description: "The PyPI release URL of version 0.16.0."
  - type: url
    value: "https://github.com/vehicle-lang/vehicle/releases/tag/v0.15.0"
    description: "The GitHub release URL of tag v0.15.0."
  - type: url
    value: "https://pypi.org/project/vehicle-lang/0.15.0/"
    description: "The PyPI release URL of version 0.15.0."
  - type: url
    value: "https://github.com/vehicle-lang/vehicle/releases/tag/v0.14.1"
    description: "The GitHub release URL of tag v0.14.1."
  - type: url
    value: "https://pypi.org/project/vehicle-lang/0.14.1/"
    description: "The PyPI release URL of version 0.14.1."
  - type: url
    value: "https://github.com/vehicle-lang/vehicle/releases/tag/v0.14.0"
    description: "The GitHub release URL of tag v0.14.0."
  - type: url
    value: "https://pypi.org/project/vehicle-lang/0.14.0/"
    description: "The PyPI release URL of version 0.14.0."
  - type: url
    value: "https://github.com/vehicle-lang/vehicle/releases/tag/v0.13.0"
    description: "The GitHub release URL of tag v0.13.0."
  - type: url
    value: "https://pypi.org/project/vehicle-lang/0.13.0/"
    description: "The PyPI release URL of version 0.13.0."
  - type: url
    value: "https://github.com/vehicle-lang/vehicle/releases/tag/v0.11.1"
    description: "The GitHub release URL of version 0.11.1."
  - type: url
    value: "https://pypi.org/project/vehicle-lang/0.11.1/"
    description: "The PyPI release URL of version 0.11.1."
  - type: url
    value: "https://github.com/vehicle-lang/vehicle/releases/tag/v0.11.0"
    description: "The GitHub release URL of version 0.11.0."
  - type: url
    value: "https://pypi.org/project/vehicle-lang/0.11.0/"
    description: "The PyPI release URL of version 0.11.0."
  - type: url
    value: "https://github.com/vehicle-lang/vehicle/releases/tag/v0.10.0"
    description: "The GitHub release URL of version 0.10.0."
  - type: url
    value: "https://pypi.org/project/vehicle-lang/0.10.0/"
    description: "The PyPI release URL of version 0.10.0."
  - type: url
    value: "https://github.com/vehicle-lang/vehicle/releases/tag/v0.9.0"
    description: "The GitHub release URL of version 0.9.0."
  - type: url
    value: "https://pypi.org/project/vehicle-lang/0.9.0/"
    description: "The PyPI release URL of version 0.9.0."
  - type: url
    value: "https://github.com/vehicle-lang/vehicle/releases/tag/v0.8.0"
    description: "The GitHub release URL of version 0.8.0."
  - type: url
    value: "https://pypi.org/project/vehicle-lang/0.8.0/"
    description: "The PyPI release URL of version 0.8.0."
  - type: url
    value: "https://github.com/vehicle-lang/vehicle/releases/tag/v0.7.0"
    description: "The GitHub release URL of version 0.7.0."
  - type: url
    value: "https://pypi.org/project/vehicle-lang/0.7.0/"
    description: "The PyPI release URL of version 0.7.0."
  - type: url
    value: "https://github.com/vehicle-lang/vehicle/releases/tag/v0.6.0"
    description: "The GitHub release URL of version 0.6.0."
  - type: url
    value: "https://pypi.org/project/vehicle-lang/0.6.0/"
    description: "The PyPI release URL of version 0.6.0."
  - type: url
    value: "https://github.com/vehicle-lang/vehicle/releases/tag/v0.5.1"
    description: "The GitHub release URL of version 0.5.1."
  - type: url
    value: "https://pypi.org/project/vehicle-lang/0.5.1/"
    description: "The PyPI release URL of version 0.5.1."
  - type: url
    value: "https://github.com/vehicle-lang/vehicle/releases/tag/v0.5.0"
    description: "The GitHub release URL of version 0.5.0."
  - type: url
    value: "https://pypi.org/project/vehicle-lang/0.5.0/"
    description: "The PyPI release URL of version 0.5.0."
  - type: url
    value: "https://github.com/vehicle-lang/vehicle/releases/tag/v0.4.1"
    description: "The GitHub release URL of version 0.4.1."
  - type: url
    value: "https://pypi.org/project/vehicle-lang/0.4.1/"
    description: "The PyPI release URL of version 0.4.1."
  - type: url
    value: "https://github.com/vehicle-lang/vehicle/releases/tag/v0.4.0"
    description: "The GitHub release URL of version 0.4.0."
  - type: url
    value: "https://pypi.org/project/vehicle-lang/0.4.0/"
    description: "The PyPI release URL of version 0.4.0."
  - type: url
    value: "https://github.com/vehicle-lang/vehicle/releases/tag/v0.3.3"
    description: "The GitHub release URL of version 0.3.3."
  - type: url
    value: "https://pypi.org/project/vehicle-lang/0.3.3/"
    description: "The PyPI release URL of version 0.3.3."
  - type: url
    value: "https://github.com/vehicle-lang/vehicle/releases/tag/v0.3.0"
    description: "The GitHub release URL of version 0.3.0."
  - type: url
    value: "https://pypi.org/project/vehicle-lang/0.3.0/"
    description: "The PyPI release URL of version 0.3.0."
  - type: url
    value: "https://github.com/vehicle-lang/vehicle/releases/tag/v0.2.0"
    description: "The GitHub release URL of version 0.2.0."
  - type: url
    value: "https://pypi.org/project/vehicle-lang/0.2.0a4/"
    description: "The PyPI release URL of version 0.2.0-alpha4."
  - type: url
    value: "https://pypi.org/project/vehicle-lang/0.2.0a1/"
    description: "The PyPI release URL of version 0.2.0-alpha1."
  - type: url
    value: "https://github.com/vehicle-lang/vehicle/releases/tag/v0.1.0"
    description: "The GitHub release URL of tag v0.1.0."

GitHub Events

Total

Create event: 76
Release event: 4
Issues event: 43
Watch event: 28
Delete event: 72
Member event: 1
Issue comment event: 118
Push event: 243
Pull request review comment event: 65
Pull request review event: 75
Pull request event: 90
Fork event: 5

Last Year

Create event: 76
Release event: 4
Issues event: 43
Watch event: 28
Delete event: 72
Member event: 1
Issue comment event: 118
Push event: 243
Pull request review comment event: 65
Pull request review event: 75
Pull request event: 90
Fork event: 5

Committers

Last synced: about 2 years ago

All Time

Total Commits: 1,184
Total Committers: 9
Avg Commits per committer: 131.556
Development Distribution Score (DDS): 0.368

Past Year

Commits: 306
Committers: 5
Avg Commits per committer: 61.2
Development Distribution Score (DDS): 0.598

Top Committers

Name	Email	Commits
=	m**t@g**m	748
Wen Kokke	w****e	329
dependabot[bot]	4****]	46
pre-commit-ci[bot]	6****]	29
Bob Atkey	b**y@g**m	12
nslusarz	n**1@h**k	7
Natalia Ślusarz	7****z	7
Marco Casadio	1****0	5
Ekaterina Komendantskaya	k**a@g**m	1

Committer Domains (Top 20 + Academic)

hw.ac.uk: 1

Issues and Pull Requests

Last synced: 6 months ago

All Time

Total issues: 94
Total pull requests: 291
Average time to close issues: about 1 year
Average time to close pull requests: 4 days
Total issue authors: 9
Total pull request authors: 10
Average comments per issue: 1.15
Average comments per pull request: 0.43
Merged pull requests: 227
Bot issues: 0
Bot pull requests: 78

Past Year

Issues: 24
Pull requests: 106
Average time to close issues: 7 days
Average time to close pull requests: 3 days
Issue authors: 6
Pull request authors: 9
Average comments per issue: 1.17
Average comments per pull request: 0.96
Merged pull requests: 64
Bot issues: 0
Bot pull requests: 11

View more stats

Top Authors

Issue Authors

MatthewDaggitt (62)
wenkokke (17)
BenCoke12 (3)
Allenator1 (3)
developing-ar (3)
ckessler2 (2)
tflinkow (2)
kiczaaa (1)
GuilhermeMBP (1)

Pull Request Authors

MatthewDaggitt (151)
dependabot[bot] (52)
pre-commit-ci[bot] (26)
wenkokke (26)
developing-ar (20)
Allenator1 (8)
joshua-smart (3)
2XUID (2)
faezs (2)
laurenpudz (1)

Top Labels

Issue Labels

bug (33) refactoring (13) backend:verifiers (12) enhancement (12) compiler:type-checker (12) documentation (10) backend:loss (7) backend:itps (6) upstream (5) compiler:error-messages (5) performance (5) CI (5) language (4) test-suite (4) python (3) build-system (3) soundness (3) UX (3) error-messages (3) compiler:verifier-backend (2) status:invalid (1) compiler:normalisation (1) errors-and-warnings (1) discussion (1) compiler:other (1)

Pull Request Labels

refactoring (79) dependencies (52) github_actions (39) enhancement (35) backend:loss (34) backend:verifiers (34) bug (30) python (18) compiler:type-checker (15) documentation (11) compiler:normalisation (10) test-suite (10) CI (8) language (8) errors-and-warnings (7) error-messages (5) performance (5) backend:itps (5) UX (3) compiler:error-messages (2) compiler:verifier-backend (2) compiler:other (1) compiler:loss-backend (1) compiler:evaluation (1)

Packages

Total packages: 1
Total downloads:
- pypi 1,906 last-month

Total dependent packages: 0
Total dependent repositories: 0
Total versions: 24
Total maintainers: 1

pypi.org: vehicle-lang

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

Documentation: https://vehicle-lang.readthedocs.io/
License: Copyright Matthew Daggitt, Wen Kokke, University of Strathclyde, Heriot-Watt University, University of Western Australia (c) 2021-2024 All rights reserved. Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met: * Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer. * Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution. * Neither the name of Wen Kokke nor the names of other contributors may be used to endorse or promote products derived from this software without specific prior written permission. THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
Latest release: 0.19.0
published 6 months ago

Versions: 24
Dependent Packages: 0
Dependent Repositories: 0
Downloads: 1,906 Last month

Rankings

Dependent packages count: 7.0%

Average: 18.7%

Dependent repos count: 30.4%

Maintainers (1)

wenkokke

Last synced: 6 months ago

Dependencies

.github/actions/setup-haskell/action.yml actions

actions/cache v2 composite
haskell/actions/setup v2 composite

.github/actions/setup-python/action.yml actions

actions/setup-python v4 composite

.github/actions/setup-vehicle/action.yml actions

actions/download-artifact v3 composite

.github/workflows/build-vehicle-python.yml actions

./.github/actions/setup-python * composite
./.github/actions/setup-vehicle * composite
actions/checkout v3 composite

.github/workflows/build-vehicle.yml actions

./.github/actions/setup-haskell * composite
actions/checkout v3 composite
actions/upload-artifact v3 composite

.github/workflows/build.yml actions

actions/checkout v2 composite
mrkkrp/ormolu-action v9 composite

.github/workflows/test-editor-integration.yml actions

./.github/actions/setup-haskell * composite
actions/checkout v3 composite

docs-source/requirements.txt pypi

Sphinx ==6.1.3

scripts/benchmark-histogram/poetry.lock pypi

click 8.1.3
colorama 0.4.6
contourpy 1.0.6
cycler 0.11.0
dataclasses-json 0.5.7
fonttools 4.38.0
kiwisolver 1.4.4
marshmallow 3.19.0
marshmallow-enum 1.5.1
matplotlib 3.6.2
mypy-extensions 0.4.3
numpy 1.24.1
packaging 22.0
pandas 1.5.2
pillow 9.3.0
pyparsing 3.0.9
python-dateutil 2.8.2
pytz 2022.7
seaborn 0.12.2
six 1.16.0
typing-extensions 4.4.0
typing-inspect 0.8.0

scripts/benchmark-histogram/pyproject.toml pypi

click ^8.1.3
dataclasses-json ^0.5.7
matplotlib ^3.6.2
pandas ^1.5.2
python ^3.10
seaborn ^0.12.2

tools/networks/requirements.txt pypi

keras >=2.7.0
matplotlib >=3.5.1
numpy >=1.22.0
sklearn >=0.0
tensorflow >=2.7
tf2onnx >=1.9.3

vehicle-python/poetry.lock pypi

black 22.12.0 develop
chardet 5.1.0 develop
click 8.1.3 develop
colorama 0.4.6 develop
distlib 0.3.6 develop
filelock 3.9.0 develop
flake8 5.0.4 develop
isort 5.12.0 develop
mccabe 0.7.0 develop
mypy 0.971 develop
mypy-extensions 0.4.3 develop
pathspec 0.10.3 develop
platformdirs 2.6.2 develop
pluggy 1.0.0 develop
pycodestyle 2.9.1 develop
pyflakes 2.5.0 develop
pyproject-api 1.5.0 develop
tomli 2.0.1 develop
tox 4.4.5 develop
virtualenv 20.17.1 develop
absl-py 1.4.0
astunparse 1.6.3
cachetools 5.3.0
certifi 2022.12.7
charset-normalizer 3.0.1
flatbuffers 23.1.4
gast 0.4.0
google-auth 2.16.0
google-auth-oauthlib 0.4.6
google-pasta 0.2.0
grpcio 1.51.1
h5py 3.7.0
idna 3.4
importlib-metadata 6.0.0
keras 2.11.0
libclang 15.0.6.1
markdown 3.4.1
markupsafe 2.1.2
numpy 1.24.2
oauthlib 3.2.2
opt-einsum 3.3.0
packaging 23.0
protobuf 3.19.6
pyasn1 0.4.8
pyasn1-modules 0.2.8
requests 2.28.2
requests-oauthlib 1.3.1
rsa 4.9
setuptools 66.0.0
six 1.16.0
tensorboard 2.11.2
tensorboard-data-server 0.6.1
tensorboard-plugin-wit 1.8.1
tensorflow 2.11.0
tensorflow-estimator 2.11.0
tensorflow-io-gcs-filesystem 0.29.0
termcolor 2.2.0
typing-extensions 4.4.0
urllib3 1.26.14
werkzeug 2.2.2
wheel 0.38.4
wrapt 1.14.1
zipp 3.11.0

vehicle-python/pyproject.toml pypi

numpy ^1.24
python ^3.8,<3.11
tensorflow ^2.10

vehicle-lang

Science Score: 64.0%

Keywords

Keywords from Contributors

Repository

Basic Info

Statistics

Topics

Metadata Files

README.md

Vehicle

Documentation

Examples

Support

Neural network formats

Dataset formats

Verifier backends

Interactive Theorem Prover backends

Related papers

Owner

Citation (CITATION.cff)

GitHub Events

Total

Last Year

Committers

All Time

Past Year

Top Committers

Committer Domains (Top 20 + Academic)

Issues and Pull Requests

All Time

Past Year

Top Authors

Issue Authors

Pull Request Authors

Top Labels

Issue Labels

Pull Request Labels

Packages

pypi.org: vehicle-lang

Rankings

Maintainers (1)

Dependencies