Skip to content

Expand Solver Adapter Ecosystem #18

@fraware

Description

@fraware

Title: Implement Additional Neural Network Verification Adapters

Description:
Provability Fabric currently supports Marabou for neural network verification and DryVR for hybrid systems. The project would benefit from additional solver adapters to support a wider range of verification scenarios.

Current Adapters:
Marabou (neural networks)
DryVR (hybrid systems)

Proposed New Adapters:

  • NeuralSAT - For satisfiability-based neural network verification
  • α-β-CROWN - For complete neural network verification with improved scalability
  • Planet - For verification of neural networks with ReLU activations
  • Sherlock - For reachability analysis of neural networks

Technical Requirements:

  • Implement adapter interface following existing patterns in adapters/ directory
  • Include comprehensive test suites with benchmark comparisons
  • Provide documentation with usage examples
  • Ensure compatibility with existing specification bundle format

Expected Deliverables:

  • New adapter implementation in adapters/ directory
  • Test suite with verification benchmarks
  • Documentation updates
  • Integration tests

Skills Needed:

  • Neural network verification expertise
  • Python/Rust development
  • Understanding of formal verification concepts

Difficulty: Intermediate to Advanced

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions