Skip to main content
Proof Assistants Beta

You are not logged in. Your edit will be placed in a queue until it is peer reviewed.

We welcome edits that make the post easier to understand and more valuable for readers. Because community members review edits, please try to make the post substantially better than how you found it, for example, by fixing grammar or adding additional resources and hyperlinks.

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