1
$\begingroup$

We're currently looking at how to integrate neural network solvers into general proof assistants. One of the issues we're running into is that, unlike general SAT/SMT solvers like Z3, queries for neural network solvers may only reference a fixed, finite set of variables. This makes compilation from expressions in the proof assistant, where users can freely quantify over new variables, to the queries for the solver much more challenging.

So the question is, is are there any existing tools that offload proofs to solvers with similar limitations?

Improve this question
$\endgroup$
7
  • 1
    $\begingroup$ How hard is it to rename the variables? $\endgroup$
    – Andrej Bauer
    Commented Dec 5, 2023 at 7:56
  • $\begingroup$ “queries for neural network solvers may only reference a fixed, finite set of variables”. What does this mean? What “neural network solvers” are you talking about? $\endgroup$
    – Jason Rute
    Commented Dec 5, 2023 at 14:22
  • $\begingroup$ So you have one variable for every input and output value for the neural network, i.e. if your neural network has 3 inputs and 2 outputs, your query can only refer to 5 variables in total. It's impossible to rename these variables. For some solvers (e.g. Marabou) this is an artificial limitation, but for most solvers (e.g. alpha-beta-crown) it is a pretty hard limitation. $\endgroup$
    – Matthew Daggitt
    Commented Dec 5, 2023 at 14:54
  • 1
    $\begingroup$ I think you and I have a very different definition of what a “neural network solver” means. For me it is a NN-based tool for solving theorems. For you I think it is a SAT-based tool for verifying neural network properties, right? If renaming the variables like Andre suggested isn’t an option, then I think you need to explain more about the domain and how this limitation comes up. $\endgroup$
    – Jason Rute
    Commented Dec 5, 2023 at 15:02
  • $\begingroup$ Yes, they're essentially SAT-solver like tools for verifying properties of neural networks. I'm not really keen to go into the specifics of why they have these limitations. I was just wondering if anyone was aware of any other domains where solvers with fixed, finite sets of variables have been integrated in proof assistants? $\endgroup$
    – Matthew Daggitt
    Commented Dec 5, 2023 at 15:21

0

Reset to default

Browse other questions tagged or ask your own question.