📜 ⬆️ ⬇️

"What is proof?": A look from theoretical informatics

Theoretical computer science is one of the areas of study at the Department of Mathematical and Information Technologies of the Academic University. We are often asked what theoretical informatics does. Theoretical computer science is an actively developing scientific field that includes both fundamental areas: algorithms, computational complexity, cryptography, information theory, coding theory, algorithmic game theory, and more applied ones: artificial intelligence, machine learning, programming language semantics, verification, automatic proof of theorems and much more. We will devote this article to a review of only a small plot, namely, we will tell about unusual approaches to the concept of proof, which theoretical informatics considers.



To explain what kind of evidence will be discussed, consider an example: there is a computer program whose authors claim that the program does something definite (specific examples will be a little later). The program can be run and get an answer. And how can you make sure that the program does what it should do? It would be nice if, in addition to the answer, the program would give proof that this answer is correct.
')
Consider a more specific example: we want to have a program that, in a bichromatic graph, finds a matching maximum size together with proof of its maximum.



Recall that a graph is called bichromatic if its vertices can be colored in two colors so that the edges of the graph connect the vertices of different colors. A matching in a graph is such a set of edges that no two of them have a common end. A set of vertices of a graph is called covering if each edge of the graph has at least one end in this set. Koenig's theorem states that in a bichrophic column the size of the maximum matching matches the size of the minimal covering set. Thus, in order to prove that the matching is maximal, one can present a covering set whose size coincides with the size of the given matching. Indeed, this covering set will be minimal, since each covering set must cover at least one end of each edge of this matching. For example, in the graph in the figure, the matching (M1, G3), (M2, G2), (M4, G1) will be maximal, since there is a covering set of size 3, which consists of G2, G3 and M4. Note that it is much easier to verify such a proof than to calculate the maximum matching: it suffices to verify that the matching size coincides with the size of the covering set and verify that all edges are covered.

Consider another example, suppose we need a program that checks a system of non-strict linear inequalities with rational coefficients for consistency (recall that a system of inequalities is called joint if you can pick up such values ​​of variables that all inequalities are satisfied).



How can you prove the correctness of the result? If the system is consistent, then the solution of this system can be a proof of consistency (it is easy to prove that if such a system has a solution, then there is a rational solution, that is, it can be written down). And how to prove that the system is incompatible? It turns out that this can be done with the help of the Farkas Lemma, which states that if the system of non-strict linear inequalities is incompatible, then these inequalities can be added with non-negative coefficients and a contradictory inequality 0≥1 can be obtained. For example, the system in the figure is incompatible, and if you add the first equation with a factor of 1, the second with a factor of 2, and the third with a factor of 1, you get 0≥1. The proof of incompatibility is just a set of non-negative coefficients.

In this article we will talk about whether evidence is needed, or verifying evidence is not always easier than solving a problem on your own. (In the example of maximum matching, we did not prove that there is no algorithm that solves the problem for the same time as proof checking takes.) If we do not limit the size of the proof, then it turns out that evidence is needed, and if we demand that the proof be short, the question of the need for proof is equivalent to the most important open question of the equality of the classes P and NP. Then we will talk about interactive evidence (evidence in dialogue). We will discuss cryptographic evidence that does not disclose unnecessary information, except for the correctness of the proved statement. And we end with a discussion of probabilistically verifiable proofs and the famous PCP theorem, which is used to prove the difficulty of approximating optimization problems.

In this article we will not touch on the automatic proof of theorems and the proof of the correctness of programs, although these topics are also quite interesting.


Do you need proof?


A language is a set of strings over some finite alphabet. In theoretical computer science, evidence is usually considered for statements of the form x∈L, where L is a language and x is a certain string. Statements of this kind generalize mathematical theorems, since any mathematical theorem states that a statement written in a formal language belongs to the set of true statements.

The proof system for the language L is the algorithm A (x, w), which receives two lines as input: x and w and verifies that the string w is a proof of the membership of x∈L. From the system of evidence require two properties: correctness and completeness. Correctness states that if for some rows x and w the algorithm A (x, w) returns 1, then x∈L. Completeness asserts that for each x∈L there exists a string w such that the algorithm A (x, w) yields 1.

Languages ​​for which evidence systems exist are called enumerable languages. If you come across a different definition of an enumerable language, then as an exercise, prove their equivalence.

A language L is called solvable if there exists an algorithm B such that when x∈L, the algorithm B (x) returns 1, and when x∉L it returns 0. Any soluble language has a proof system in which the proof is empty. The natural question is whether it is necessary that for any language for which there is a system of evidence, there exists a resolving algorithm. The answer to this question is known, there are languages ​​for which there are systems of evidence, but for which there is no resolving algorithm. To invent an example of such a language is not difficult, it is more difficult to invent a natural example. Consider a language that consists of polynomials with integer coefficients in many variables that vanish at least for some integer value of the variables. The proof system for such a language is constructed simply: the proof is the integer value of the variables in which the polynomial vanishes. The DPRM theorem (named for the authors: Davis, Putnam, Robinson, and Matiyaesevich) states that this language is not solvable, that is, there is no algorithm that checks whether the polynomial vanishes at integer points. The last step in the proof of this theorem belongs to Academician Yu. V. Matiyasevich, and this theorem gives a negative answer to the 10th Hilbert problem.

Short evidence


So far we have not imposed any restrictions on the algorithm that verifies the proof and on the size of the proof. Would it be useful to prove the correctness of the result of a program if the time it takes to check the proof is more than the time it takes to execute the program? It seems that such proofs are meaningless, therefore, we will require that the algorithm A (x, w) in the definition of the proof system works polynomially on the length of the string x and on the length of the proof w time, such proof systems will be called effective.


We say that the language L belongs to the class NP if there is an effective system of proofs for it and the polynomial p, that for any x∈L there is a proof that x∈L is of length not greater than p (| x |). The language L belongs to the class P if there exists an algorithm polynomial in time that checks whether the input string belongs to the language L. The class P is contained in the class NP, because for each language L of P, the algorithm checking the belonging of L itself will be a proof system if that he ignores evidence. At the moment, it is not known whether there exist languages ​​from the class NP, which do not belong to the class P. The question of the equality of the classes P and NP is on the list of seven millennium problems compiled by the Clay Institute; for the solution of this problem a prize of one million dollars has been announced. Many have heard about the list of tasks of the millennium in connection with the proof of the Poincare hypothesis by G. Ya. Perelman. Most experts believe that the classes P and NP do not match.

Consider examples of languages ​​from the NP class:


Interactive evidence


Until now, the evidence that we considered was very similar to our usual ones, namely, evidence is some text that, although it is not clear how to invent, but it is easy to verify, there is an algorithm that verifies the correctness of the evidence. That is, to come up with a proof, you need to have some special abilities, and everyone can check the proof. In fact, not all the evidence of modern mathematics has this property. Firstly, the evidence is not written in a formal language convenient for automatic verification, and secondly, in order to understand the evidence in some areas, you need to spend several years studying this area.

Mathematics classes for schoolchildren often practice this format of classes: children are given a set of tasks, when the child believes that he has solved the problem, he verbally tells the solution to the teacher. And there is a dialogue between the teacher and the student, who either convinces the teacher that the problem is solved or does not convince.

Consider an example of interactive proof: there is a program that solves the problem of isomorphism of graphs. In the case when the graphs are isomorphic, the program can prove the correctness of its answer by issuing a permutation defining isomorphism. We show how it is possible in the dialogue to prove that graphs are non-isomorphic. Let the user ask the program if the graphs G 0 and G 1 are isomorphic and get the answer that they are non-isomorphic. After that, the user throws a coin (selects a random element i from the set {0,1}) and selects a random permutation of the n-element set (all the permutations are considered to be equally probable) σ. He asks the program whether the graphs are isomorphic to G 0 , σ (G i ). If i = 0, then the program is expected to answer that the graphs are isomorphic, and if i = 1, then the program is expected to graph non-isomorphic. If the graphs G 0 and G 1 were indeed non-isomorphic, then the program will easily give the correct answer to this question. And if G 0 and G 1 were isomorphic, then the graph σ (G i ) with equal probability can be either a permutation of G 0 or a permutation of G 1 , therefore the program will produce the expected response with a probability not greater than 1/2. The error probability can be reduced by repeating the algorithm n times and deciding that the algorithm works correctly if in each of the n launches the correct answer was given; the probability of error in this case does not exceed 1/2 n .

In the example just considered, the proof is a dialogue between the proving (the program) and the verifier (the user), while the proving can be very complicated, and the verifier can only do simple things (produce polynomial time calculations). If x∈L, then the prover must convince the verifier with probability 1, and if x∉L, then the verifier must accept such proof with a probability of no more than 1/10. Shamir's theorem states that such interactive proof systems with short dialogues exist for all L languages ​​for which there are recognition algorithms using polynomial memory. In particular, it is possible to prove in polynomial time that there is no Hamiltonian path in the graph.

Evidence with zero disclosure




The concept of proof is found not only in mathematics and computer science, but also in jurisprudence. For example, a person is accused of a crime, he can prove that he was not at the crime scene, but does not want to tell where he was in fact (for example, he could have a mistress or wants to hide his whereabouts from competitors). Alibi is not a crime, but its announcement is very undesirable. It turns out that it is theoretically possible to prove in such a way as not to communicate unnecessary information, except for the statement being proved.

Consider an example: some firms write programs that quickly solve the problem of graph isomorphism, but the free version of this program simply says whether graphs are isomorphic or not, without giving a permutation in the case that graphs are isomorphic. To get a permutation, you need to buy a paid version of the program. But meanwhile, the developers want the user to make sure that the graphs are indeed isomorphic, but that this information does not help the user to find this isomorphism on his own. This can be done as follows: if the graphs G 0 and G 1 are isomorphic, then you can choose a random permutation π and produce the graph G 2 = π (G 1 ) and ask the user to decide which graph isomorphism he wants to get G 0 and G 2 or G 1 and G 2 . The program will respond to exactly one of these requests. If the program knows isomorphism, then it will easily respond to the user's request, but if there is no isomorphism, then at least one of the user's request options for issuing an answer will fail. And if the user selects the query randomly, then the probability that there is an isomorphism between the options selected by the user does not exceed 1/2. The error can be reduced by repeating this process: choosing a new permutation and prompting the user to choose a new option.

It turns out that for each language from the NP class, with a certain cryptographic assumption, it is possible to construct such an interactive proof of ownership that will not give any information about the classic proof of membership (which exists for any language from the NP class). The cryptographic assumption mentioned is the existence of one-way functions, i.e. functions that are easy to calculate but hard to reverse. For example, many believe that a function that gives out their product by two n-bit numbers is one-sided.

Probability testable evidence


Let a math teacher give his students homework, they hand him notebooks with a solution. Any math teacher wants to check the solution without reading it completely. The option to check the decision only by the answers is bad, since the answer can be written off or guessed and also this does not help in the tasks on the proof, in which there are no answers as such. It turns out that this dream of teachers is achievable and any proof can be rewritten in such a way that to check it it would be enough to look at the constant number of bits of proof.

We give an example for the language of pairs of non-isomorphic GNI graphs. In our example, the proof will be exponential length, namely, for graphs on n vertices, the proof will be 2 n (n-1) / 2 , here n (n-1) / 2 is the maximum number of edges that a graph can have on n tops. The proof of the non-isomorphism of a pair of graphs G 0 and G 1 is a bit string w of length 2 n (n-1) / 2 , which is indexed by all different graphs on n vertices. The bit of the string w corresponding to the graph H is zero if H is isomorphic to G 0 , unity if the graph is isomorphic to G 1 , and equal to anything if the graph H is not isomorphic to neither G 0 nor G 1 . The figure shows an example of such a string w for two non-isomorphic graphs on three vertices:



The verification of such a proof is similar to an interactive proof: you must throw a coin (take random i from {0,1}), random permutation σ and look at the bit of proof corresponding to the column σ (G i ), if it coincides with i, then accept such proof , if it does not coincide with i, then reject. In the case when the graphs G 0 and G 1 are non-isomorphic, then such a proof will be accepted. If the graphs G 0 and G 1 are isomorphic, then the graph σ (G i ) with equal probability can be a permutation of G 0 and G 1 , therefore, the proof will be accepted with a probability not greater than 1/2. By repeating such a check 10 times for independent random choices i and σ, it is possible to lower the error probability to 1/1024.

The disadvantage of the above proof is that it has an exponential size. However, the famous PCP theorem (PCP is short for probabalistically checkable proofs) states that for each language from class NP there is evidence of belonging to a language of polynomial size, and to verify this proof, it is enough to read the constant number of bits of this proof. Moreover, the usual proof (which exists by definition of the class NP) can be transformed in polynomial time into a proof that can be checked probabilistically.

PCP-theorem is not only a fun fact, but also a powerful tool for proving the difficulty of approximate solutions for optimization problems. Recall that an independent set in a graph is a set of vertices of the graph, between which there are no edges of the graph. It is known that the task of finding the maximum independent set in a graph is NP-hard, which, in particular, means that if there is an algorithm that is polynomial in the number of vertices of the graph that finds the maximum independent set in the graph, then P = NP. Using the PCP theorem, it can be proved that the NP-hard problem is to find not only the maximal independent set, but also the approximately maximal set (with a constant approximation). In particular, if there exists an algorithm which, during polynomial time in the graph, finds an independent set that is not more than 1000 times smaller than the maximum, then it follows that P = NP.

Links


Literature in which you can find rigorous wording and evidence of all the statements mentioned in the article:


Those interested in theoretical computer science are advised to pay attention to the magistracy of the Academic University.

Source: https://habr.com/ru/post/217215/


All Articles