Gradient-based search for properties

[kksnowy]

This PR is a preliminary implementation of a gradient-based search for witnesses/adversarial examples for properties. It contains the following changes (still WIP):

• Updates to the Vehicle compiler:
  • A compiler pass for search to lift quantifiers to the top of a property AST and convert properties of the form forall x. P(x) to not exists x. not P(x).
  • Updates to the JSON loss structure outputted by the compiler e.g. it can now output a map indicating whether a search on a property will produce witnesses or adversarial examples.
• Updates to the Python backend:
  • Quantifiers (which are now at the top level for search) are separated from a loss AST and the AST is restructured to enable loss functions to be evaluated at network inputs.
  • Common functions supporting loading/translating a loss AST are refactored to make them more modular for training and search.
  • A PyTorch PGD algorithm has been implemented to search for witnesses for properties containing existential quantifiers, and adversarial examples for properties containing universal quantifiers.

Python unit tests have been added to test the search for properties involving a single input and multiple inputs. They can be run using uv run --extra test --extra pygments python -m pytest -s tests/test_search.py

[kksnowy]

As discussed last meeting, I removed the functionaliseResources step in compileToSearchLoss and removed the changes I made in FunctionaliseResources.hs (please see commit 52224bb) but this now results in the below error when compiling to a loss function for search.

This error can be reproduced by running uv run --extra test --extra pygments python -m pytest -s tests/test_search.py

[MatthewDaggitt]

Okay I have merged the latest changes 🎉 . Nothing major - we now have to call forceValue before pattern matching using toRatTensorValue/toBoolTensorValue etc.

I have also fixed the functionaliseResources bug by handling free variables that now still exist in the fromJSON methods.

@kksnowy it looks like you don't have your pre-commit hooks properly configured (for code formatting etc.). Can you follow the instructions for installing the pre-commit hooks in the CONTRIBUTING.md file?

[kksnowy]

@MatthewDaggitt Sorry for the delay, I have done that now, and the formatting issues should now be fixed.

Also, I think there's now an issue with compiling to loss functions for search using the VehicleLoss differentiable logic. I have mentioned this in this issue #1211 which has all of the remaining to-do's for my project.