2
$\begingroup$

I don't know complexity class theory well so I might make some categorical errors, but I will try to ask this question anyways.

Suppose you have written a function in some programming language which solves an NP-complete problem. There must exist an algorithm which can verify the correctness of an (input, output) pair in polynomial time. Does there exists an algorithm which takes the code of your solution function and produces code for a verification function? In other words, can a efficient polynomial time verification program be constructed from any solution program?

Alternatively, if this is impossible, suppose the solution function is written in a strongly typed language like Lean or Agda which can formalize mathematics. Now suppose you are given not only a function which solves an NP-complete problem, but also a formalization of the problem as well as a proof of correctness of the function. Can you construct a polynomial time verification function from that?

My motivation is that it would be interesting if one could "super-compile" a program in such a way that it is enriched with verification functions. Then one may attempt to skip certain parts of the program during execution by guessing the output of a function and using the generated verification to check.

$\endgroup$
1
  • 2
    $\begingroup$ Is 'solution function' a deterministic algorithm (e.g., a SAT solver) or a nondeterministic algorithm? What are your goals, in writing a verifier? Is your purpose to check for bugs in the implementation of the 'solution function'? $\endgroup$
    – D.W.
    Commented Jan 2 at 17:23

2 Answers 2

2
$\begingroup$

Yes: The certificate (checked by the verifier) simply encodes the non-deterministic choices made by the non-deterministic program. You then run the original non-deterministic program, resolving the non-determinism using the certificate.

Remember that each "NP verifier" receives two inputs: The original problem instance, and a certificate. The verifier must always output "no" when given a no-instance; when given a yes-instance, it must output "yes" for at least one certificate.

If you are still confused why this certificate is needed, see e.g. this anwer: Certificates and NP?


However, the way your question is written makes me fear that you mean something very non-standard when you say "verifier." What do you mean by "verifier"? And how should dependent types help here? (Executing the correctness proof is usually not more meaningful than executing the original solver..)

$\endgroup$
5
  • $\begingroup$ Yes I think I used verifier incorrectly. What by meant by a verifier is a program which takes a pair (input, output) and returns True if it is a solution to the NP-complete problem and False if not. My question is whether such a "check if problem is solved" program can be constructed from a program that solves the problem, or possibly as additional data a formalization of the problem and a proof that said progran does solve the problem. $\endgroup$ Commented Jan 2 at 16:52
  • $\begingroup$ So as an example suppose I have written a function that solves linear systems of equations (LSE). Does there exist an algorithm which can take my code and produce a function that takes in a vector v and tells me if it solves the LSE? Obviously it would be a function that checks if L v = 0. $\endgroup$ Commented Jan 2 at 16:58
  • 2
    $\begingroup$ In general, NP problems are decision problems. They have no output. $\endgroup$ Commented Jan 2 at 18:29
  • $\begingroup$ Yet, they are often (but not always) formulated as "there exists a thing such that ..." (eg. there exists an assignment that satisfies this CNF). If so, then there is a straightforward way to construct a NP-solver from a program checking whether a formula satisfies a CNF. But you can also write a solver that does a bunch of weird, unnecessary stuff in order to find a solution. Turning this back into a something taking CNFs as input seems hard since finding what part of the program corresponds to the CNF being checked might be non-trivial. Formally, it is an ill-posed question. @RobertWegner $\endgroup$ Commented Jan 2 at 18:33
  • 2
    $\begingroup$ This answer seems to be assuming the original solver program is a polynomial-time algorithm running on a nondeterministic machine. The question reads more to me like the solver is running on a deterministic machine, with no runtime bound. $\endgroup$ Commented Jan 3 at 3:16
2
$\begingroup$

Generally speaking, we don't need compiler support to implement the verifier. Implementing a verifier for a NP-problem is usually easy; far easier than implementing an efficient solver. So I doubt that your idea is going to prove very useful.

That said, if you want to do it, if you have a formal specification of a NP problem, it should be possible to auto-generate a verifier. If you look at the formal definition of NP, you will see that the way we specify a NP problem is by specifying the verification method. If you look at informal definitions of NP problems, typically they specify a list of conditions for a solution $y$ to count as a valid solution to a problem instance $x$. Those conditions are the verifier; all that you need to do to build a verifier is to write code to check all of those conditions. Given a formal specification of those conditions, I expect it will typically be trivial to synthesize code that checks those conditions (you basically just have to execute the specification).

I don't know of any good way to automatically generate a verifier given code for a deterministic solver, like a SAT solver or ILP solver.

It's not clear why you want a verifier. If your goal is to use the verifier to check the output of the solver, because you are worried that the solver might have bugs, then you don't want to auto-generate the verifier from the solver code anyway, because then bugs in the solver would imply bugs in the verifier. If you want to check for bugs in the solver, then you should independently implement the verifier, not auto-generate it from the solver.

Most NP-complete problems are hard to solve, so typically there isn't any good solver. Many of the problems we solve in practice are not NP-complete, but rather are in P. In that case, you might be interested in the CS literature on "program checking". That literature devises algorithms to check whether the results of a program are correct, for certain specific problems (which typically are not NP-complete). See, e.g., https://en.wikipedia.org/wiki/Freivalds%27_algorithm for one example.

$\endgroup$
3
  • $\begingroup$ Thank your reply. My mofivation for wanting auto-generated verifiers is the following. Suppose you could write a special compiler for, say, C, that decomposes your program into sections (for example functions) that correspond to solvers of certain problems which are easier to verify. For exampel the compiler detects that this piece of code is solving a linear system of equations. Then the compiler additionally generates verifiers which can determine if for one of these sections a certain output (change in the memory) is correct for a given input. $\endgroup$ Commented Jan 2 at 18:49
  • $\begingroup$ Then you can now attempt to skip the execution of your code by using heutistics to guess the output amd check if your guess is correct. This may give speedups in expectation. $\endgroup$ Commented Jan 2 at 18:50
  • $\begingroup$ @RobertWegner, Got it. Thanks for elaborating on that! My opinion: The software engineering cost of coming up with and implementing the heuristic is vastly higher than the cost of implementing the verifier. Therefore, even if you had compiler support to build the verifier, it would not make an appreciable difference to the software engineering cost of such an approach. Therefore, I don't think it's a useful direction. In any case, my answer explains what is and isn't possible, for compiler-generated verification. $\endgroup$
    – D.W.
    Commented Jan 2 at 19:02

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.