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 the proof assistant, where users can freely quantify over new variables, to queries much more challenging.

So the question is, is there any existing research/implementations that offloads proofs to solvers with similar limitations?

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?