JP6910228B2 - Automatic certification device and program - Google Patents

Description

The present invention relates to an automated theorem proving device and a program.

In recent years, in the design and verification of hardware such as large-scale integrated circuits (LSIs), verification of software programs, etc., the use of an automated theorem proving device that automatically infers without human intervention has been studied. For example, Non-Patent Document 2 discloses that the verifiable target can be expanded by verifying the hardware design by a method using Craig interpolation.

In response to such research, a solver that generates and outputs a polynomial representing Craig interpolation related to a given proof object has been developed (for example, Non-Patent Document 1). In such a solver, since the coefficients of the polynomial are obtained by numerical analysis, they are generally not expressed as a concise integer ratio. In addition, the coefficient includes a numerical error.

Dai, L., et. Al., Generating non-linear interpolants by semidefinite programming. In: Sharygina, N., Veith H. (eds.) Computer Aided Verification -25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings. Lecture Notes in Computer Science, vol. 8044, pp.364-380, Springer (2013) (http://dx.doi.org/10.1007/978-3-642-39799-8_25) ) McMillan, K. L., Interpolation and SAT-Based Model Checking, in Proc. Of 15th Conf. On Computer Aided Verification (CAV 2003), LNCS, Vol.2725, pp. 1-13, Springer (2003)

As described above, in the conventional technique, the coefficient of the polynomial is not generally expressed as a simple integer ratio and includes a numerical error. Therefore, the actual hardware design corresponding to the obtained interpolation and the operation of the program are to be proved. It is not easy to interpret what kind of program is, for example, in the case of program operation verification, what kind of program operation state is represented, and in the case of automated processing such as operation verification. There was a problem that it could be an obstacle.

The present invention has been made in view of the above circumstances, and one of its objects is to provide an automatic proof device and a program capable of facilitating the interpretation of an actual proof object corresponding to the obtained interpolation.

The present invention for solving the problems of the above-mentioned conventional example is an automatic proof device, which is a means for receiving an input from a solver that generates and outputs a polynomial representing Craig approximation related to a given proof target, and the above-mentioned. A plurality of approximated coefficient calculation means for obtaining a plurality of approximate coefficients such that the ratio of the coefficients included in the accepted polynomial is an integer ratio and the value corresponding to each coefficient is a smaller value, and the plurality of obtained approximate coefficients. Approximation coefficients are selected from among them in the order determined by a predetermined method, a trial polynomial is generated in which the coefficients of the accepted polynomial are replaced with the selected approximation coefficients, and the trial polynomial represents the Craig interpolation. When it is determined by the verification means that the verification means for verifying whether or not it is established as a polynomial and the trial polynomial based on any of the obtained approximation coefficients by the verification are established as a polynomial representing the Craig interpolation. , A generation means for generating the approximation coefficient as a solution, and the generation means, assuming that the trial polynomial based on any of the obtained approximation coefficients does not hold as a polynomial representing the Craig interpolation. When it is determined by the verification means, it is assumed that an error has occurred and a predetermined process is executed.

According to the present invention, it is possible to facilitate the interpretation of the actual proof object corresponding to the obtained interpolation.

It is a block diagram of the block of the automatic certification apparatus which concerns on an example of Embodiment of this invention. It is a functional block diagram of the automatic certification apparatus which concerns on an example of embodiment of this invention. It is a flowchart which shows the operation example of the solver part of the automatic certification apparatus which concerns on an example of embodiment of this invention. It is a flowchart which shows the processing example of the automatic certification apparatus which concerns on an example of embodiment of this invention. It is explanatory drawing which shows the setting example of the constraint processed by the automatic certification apparatus which concerns on an example of Embodiment of this invention.

Embodiments of the present invention will be described with reference to the drawings. As illustrated in FIG. 1, the automatic certification device 1 according to the embodiment of the present invention includes a control unit 11, a storage unit 12, an operation unit 13, and a display unit 14.

Here, the control unit 11 is a program control device such as a CPU, and operates according to a program stored in the storage unit 12. In an example of this embodiment, the control unit 11 accepts an input from a solver that generates and outputs a polynomial representing Craig interpolation related to a given proof object, and the ratio of the coefficients included in the accepted polynomial is , A plurality of sets of approximation coefficients that approximate the values of each coefficient are obtained so that the ratio of integers is obtained and the value corresponding to each coefficient is a smaller value.

Note that interpolation here refers to interpolation in a logical expression.
When X and Y are unsatisfiable expressions
If X, then Z is tautological,
Z and Y are unsatisfiable expressions, and
When the variable appearing in Z appears in both X and Y, it is called Craig interpolation in which Z is "X then Y".

Further, the control unit 11 selects a set of approximation coefficients from the plurality of sets of approximation coefficients obtained in the order determined by a predetermined method. As an example, the sum of the absolute values of the approximation coefficients may be selected in ascending order (in order from the one having the smallest 1 norm). In another example, the sum of squares of each coefficient is in ascending order (from the one with the smallest 2 norms), or the maximum absolute value of the coefficients is in ascending order (the infinite norm is the smallest). It may be selected in order from the one).

The control unit 11 generates a trial polynomial in which each of the coefficients of the accepted polynomial is replaced with a corresponding value included in the selected set of approximate coefficients, and whether the trial polynomial is established as a polynomial representing Craig interpolation. To verify. When the control unit 11 determines that the trial polynomial based on any of the obtained approximation coefficients is established as a polynomial representing Craig interpolation by the processing of this verification, the control unit 11 uses the approximation coefficient as a solution for a predetermined process. ..

Further, when it is determined that none of the trial polynomials based on any of the obtained approximation coefficients is established as a polynomial representing Craig interpolation, the control unit 11 executes a predetermined process assuming that an error has occurred. The detailed operation of the control unit 11 will be described later.

The storage unit 12 is a memory device or the like, and holds a program executed by the control unit 11. This program may be provided stored in a computer-readable and non-temporary storage medium and copied to the storage unit 12. In the present embodiment, the storage unit 12 also operates as a work memory of the control unit 11.

The operation unit 13 is a keyboard, a mouse, or the like, receives a user's instruction input, and outputs the content of the instruction input to the control unit 11. The display unit 14 is a display or the like, and displays and outputs information according to an instruction input from the control unit 11.

Here, the operation of the control unit 11 will be described. In the present embodiment, the control unit 11 functionally includes the solver output receiving unit 21 and the coefficient calculation unit 22 as illustrated in FIG. 2 by executing the program stored in the storage unit 12. , A verification processing unit 23, a solution generation unit 24, and an output unit 25 are included. Further, in the present embodiment, as shown in FIG. 2, the control unit 11 also operates as a solver that generates and outputs a polynomial representing Craig interpolation related to the given proof target, and further includes the solver unit 31. But it may be. However, the solver unit 31 may be realized by another computer, and in that case, the solver output receiving unit 21 described later receives the output of the solver from the other computer functioning as the solver. ..

The solver unit 31 according to an example of the present embodiment converts the problem of generating the Craig interpolation of the pair of constraints T and T'given as the proof target into the semidefinite programming problem.

に変換する。 That is, the solver unit 31 sets the constraints T and T ′ related to the proof target to at least one polynomial f, which is 0 or more with respect to an arbitrary variable value.
At least one polynomial g, greater than 0,
At least one polynomial h equal to 0
Expressions containing at least one of

Convert to.

In addition, the individual polynomial _{f 1, f 2, ... f} s, g 1, g 2 ..., g t, h 1, h 2 ... h u, f '1, f' 2 ..., f 's', g' _{1, g '2 ..., g} ' t ', h' 1, h '2 ... h' u ' in advance, restrictions T, T' previously arbitrarily defined as a polynomial of a variable X that appears in common to.

In this way, at least one polynomial f, in which each of the constraints T and T'related to the proof target is 0 or more with respect to an arbitrary variable value,
At least one polynomial g, greater than 0,
At least one polynomial h equal to 0
By expressing a numerical solution that includes at least one of It is easier to obtain interpolation than when describing with a set of polynomials including.

Specifically, as illustrated in FIG. 3, the solver unit 31 has _{constraints T and T'expressed by a semi-algebraic system with inequalities (SAS <} : Semialgebraic System with inequalities) and a maximum degree. Accepts the natural number b representing (S1).

とし、ｉ，ｊをそれぞれ

（すなわち、ｉをｓビットの２進数値、ｊをｔビットの２進数値…など）として、ベクトルα，α′，β，β′，γが

との条件を満足するものとする。 Then, the solver unit 31 finds a numerical solution of the vectors α, α', β, β', and γ that satisfies the following mathematical expression (S2). That is,

Let i and j be respectively

(That is, i is an s-bit binary value, j is a t-bit binary value, etc.), and the vectors α, α', β, β', and γ are

The condition of is satisfied.

Further, here, it is assumed that the following restrictions are defined between the vectors α, α', β, β', and γ.

The process of obtaining the vectors α, α', β, β', and γ may use a symbolic solution (for example, quantifier elimination), but here it can be relaxed as a semidefinite programming problem. In this case, the well-known semidefinite programming problem solver can be used.

Here, C (0) _{≤ b} means SOS (Sum of Squares: multiple polynomials p ₁ , p ₂ ... p _N squared sum, that is, p ₁ ² + p ₂ ² + ... + p _N ² ) of degree b or less. do. ^{Further, σ (b) is a set of t sets of natural numbers N t} such that the sum is b + 1 or less {(k ₁ , k ₂ , ... k _t ) ∈ ^{N t} | k ₁ + k ₂ + ... + k _t. It means ≦ b + 1}.

The solver unit 31 examines whether or not the vectors α, α', β, β', and γ, which are solutions (numerical solutions), have been obtained (S3), and if no solution can be found (S3: No), the solver unit 31 31 stops processing as an error (S4). In this case, the solver output receiving unit 21, which will be described later, does not accept any input.

として、多項式ｆ，ｇ，ｈを定める（Ｓ５）。 When a solution is found in the process S3 (S3: Yes), the solver unit 31

The polynomials f, g, and h are defined as (S5).

を解として出力する。 And the inequality

Is output as a solution.

Further, the solver output receiving unit 21 receives an input of a solution output by the solver, such as the solver unit 31.

The coefficient calculation unit 22 obtains at least one (preferably a plurality) integer ratios of the coefficients of the variables X included in the solution received by the solver output receiving unit 21. In an example of this embodiment, the coefficient calculation unit 22 obtains this integer ratio by using the method of continued fraction expansion. ^{That is, the coefficient calculation unit 22 multiplies the received solution by 10 n} so that all the coefficients of the variables X included in the solution received by the solver output receiving unit 21 are natural numbers. Here, n is the smallest positive integer in which all the coefficients are natural numbers.

The coefficient calculation unit 22 performs the following processing (referred to as continued fraction expansion (CFE) processing) for _{each coefficient x 1} , x ₂ ... x _{n (all are natural numbers and at least one is not 0) thus obtained.} To execute.

を求める（Ｓ１２）。 As shown in FIG. 4, first, the coefficient calculation unit 22 accepts the designation of the depth d (d is a positive integer) (S11). If the depth d is not specified, d = 1. Up The coefficient calculator 22, the minimum coefficient of the coefficients _{x 1, x} 2 ... _{x n} as _{x p,} the respective coefficients _{x 1, x} 2 ... _{x n,} does not exceed the number obtained by dividing the _{x p} Integer set of

(S12).

The coefficient calculation unit 22 examines whether or not d is "1" (S13), and if d is "1" (S13: Yes), obtains the greatest common divisor of the above set a, and each component of a is obtained. The value of is divided by the greatest common divisor gcd (a) to obtain a set of values (S14):

The coefficient calculation unit 22 stores y (the ratio of the values of each component is the desired integer ratio) obtained here in the storage unit 12 as a return value (S15), and returns (calls recursively). If so, it returns to the caller's process, and if it was called first, it ends the process).

If d is not "1" in the process S13, the coefficients are set to x ₁ −a ₁ x _p , ..., x _p-1 , a _p-1 x _p , x _p , x _{p + 1} −a _{p + 1} x _{p + 1} , ... , X _{n −} a _n x _p
Let the depth d be (d-1) (S16), the CFE process be recursively executed (from process S11), and the return value be r'(S17).

にてｙを求め（Ｓ１８）、ｙの各成分を、これらの最大公約数ｇｃｄ（ｙ）で除した結果を返り値として記憶部１２に格納し（Ｓ１９）、リターンする。 Further, the coefficient calculation unit 22

Y is obtained in (S18), and the result of dividing each component of y by these greatest common divisors gcd (y) is stored in the storage unit 12 as a return value (S19) and returned.

In the approximation coefficients obtained by the examples so far, the value corresponding to each coefficient is an integer, but the approximation coefficient obtained as the integer may be further divided by a common integer d to be a rational number. That is, the approximation coefficient is not limited to an integer.

The verification processing unit 23 replaces the coefficient of the polynomial, which is the solution received by the solver output receiving unit 21, with a coefficient (approximate coefficient) for each value of each integer ratio stored in the storage unit 12 by the coefficient calculation unit 22. To generate. Then, the verification processing unit 23 verifies whether or not the generated trial polynomial is established as a polynomial representing Craig interpolation. In this verification, the range of the polynomial corresponding to T'is compared with the range when the trial polynomial is replaced with the polynomial of the solution accepted by the solver output receiving unit 21, and if they do not overlap, Craig interpolation is expressed. It will be judged that it is established as a polynomial.

The verification processing unit 23 is a trial polynomial established as a polynomial representing Craig interpolation, and has the smallest coefficient integer (focusing on one of the variables and having the smallest coefficient of the variable). , Or a trial polynomial in which the sum of all coefficients is the smallest) is output to the solution generation unit 24.

When the verification processing unit 23 determines that none of the trial polynomials generated by the coefficient calculation unit 22 using each integer ratio stored in the storage unit 12 is established as a polynomial representing Craig interpolation, the coefficient calculation unit 23 calculates the coefficient. After the value of the depth d used by the unit 22 to obtain the current polynomial ratio is incremented (incremented by an integer value of "1" or more) and the coefficient calculation unit 22 is incremented. The depth d may be output and the integer ratio may be generated again. When the value of d after increment exceeds a predetermined threshold value, or when the value of d after increment also gives the same integer ratio as the integer ratio obtained before incrementing d. (When it has converged), a predetermined process is executed assuming that an error has occurred.

As an example, when the verification processing unit 23 determines that an error has occurred as described above, the verification processing unit 23 may instruct the output unit 25 to output the solution accepted by the solver output receiving unit 21 as it is as a predetermined process. ..

The solution generation unit 24 replaces the polynomial that is the solution accepted by the solver output receiving unit 21 with the trial polynomial output by the verification processing unit 23, and generates a solution to be output.

The output unit 25 displays and outputs the solution to be output generated by the solution generation unit 24 (or the solution itself received by the solver output receiving unit 21 according to the instruction input from the verification processing unit 23) as a solution to the display unit 14. do.

In addition to displaying and outputting the solution to the display unit 14, the output unit 25 may output the solution to a printer (not shown) for printing, or output the solution as data so as to be input to another program, and the other program. May be used for the processing of.

に変換されて、その数値解である多項式と、当該多項式が満足する不等式あるいは等式が解として得られる。 [motion]
The embodiment of the present invention has the above configuration and operates as follows. That is, in an example of the present embodiment, at least one polynomial f in which each of the constraints T and T'related to the proof target is 0 or more with respect to an arbitrary variable value,
At least one polynomial g, greater than 0,
At least one polynomial h equal to 0
Expressions containing at least one of

Is converted to, and the polynomial that is the numerical solution and the inequality or equation that the polynomial satisfies are obtained as the solution.

As an example, the constraints T, T'are
T: = (y ≧ x ² + 1)
^{T ': = (y ≦ -x} 2 -1)
(See FIG. 5), these constraints T and T'are not satisfied at the same time, that is, since T∧T' is inconsistent, only variables common to these T and T'are included. There exists a formula ε that is ε if T and ε∧T'contradictory (Craig's interpolation theorem). And this ε becomes Craig interpolation.

The solver obtains the Craig interpolation ε as a numerical solution from the constraints T and T'. Specifically, one of the numerical solutions is
871.465y + 348.560> 0
Obtained as.

The automated theorem proving apparatus 1 of the present embodiment rounds the coefficients 871.465 and 348.560 by the method of continued fraction expansion to obtain an approximation coefficient. In the example here, as a result of this rounding process,
5, 2
11, 4
A set of approximate coefficients is obtained such that the coefficients such as ... are ratios of integers.

The automatic proof device 1 starts from the smallest approximation coefficient (the one with the smallest sum of the absolute values of each of the included coefficients, that is, the one with the smallest one norm) among the obtained sets of approximation coefficients. It is examined whether or not the trial polynomial replaced with the corresponding coefficient in the polynomial of is the Craig interpolation ε of the constraints T and T'.

Here, the automated theorem proving device 1 replaces the coefficient 871.465 with the corresponding integer value 5 and the coefficient 348.560 with the corresponding integer value 2, an inequality 5y + 2> 0 using a trial polynomial.
Is the constraint T, T'
T: = (y ≧ x ² + 1)
^{T ': = (y ≦ -x} 2 -1)
Check if it is Craig interpolation ε for.

In the example here, the range y ≧ x ² + 1 represented by the constraint T is included in the range of the inequality 5y + 2> 0 using the trial polynomial.
"If the constraint T, it is ε."
Is established.

Further, since the range of inequality 5y + 2> 0 with trial polynomials are non-overlapping with the range y ≦ ^-x 2 -1 representing constrained T ',
"Ε and constraint T'contradiction"
Also holds.

That is, it can be determined that the inequality 5y + 2> 0 using this trial polynomial is Craig interpolation of the above constraints T and T'.

The automatic proof device 1 examines and determines whether or not the trial polynomial is Craig interpolation by comparing the range of each inequality (or equality) in this way. In the example here, as described above, since it can be determined that the inequality 5y + 2> 0 using the trial polynomial examined first is the Craig interpolation of the constraints T and T', the automatic proof device 1 is used. , The inequality 5y + 2> 0 using this trial polynomial is displayed and output to the display unit 14 as a solution.

According to the automated theorem proving device 1, the solution is shown by a simplified inequality as compared with the numerically obtained solution, so that a solution that can be easily interpreted as the corresponding actual condition can be obtained.

Further, by inputting the solution output by the automatic proof device 1 into the processing system of the program verification or theorem proving, the output of the automatic proof device 1 of the present embodiment is provided for the processing of the program verification or the theorem proving. be able to.

[Modification example (example of adopting Dai's method)]
In the above example of the present embodiment, the polynomial f, in which the solver (solver unit 31 or the like) is 0 or more with respect to an arbitrary variable value as a constraint relating to the proof target,
Polynomial g, greater than 0,
Polynomial h equal to 0
However, if an inequality or an equation using a polynomial representing Craig interpolation can be obtained as a numerical solution, the automated theorem proving device 1 of the present embodiment is used. , The example using this solver is not limited, and other solvers may be used.

For example, in the present embodiment, the solver for obtaining a numerical solution may adopt the method shown in Non-Patent Document 1. In this case, the polynomial f, whose constraint on the proof target is 0 or more for any variable value,
Polynomial g not equal to 0,
Polynomial h equal to 0
It will be set to include at least one of.

[Effect of Embodiment]
According to this embodiment, the numerically analyzed polynomial is re-expressed by a relatively simple integer ratio coefficient. As a result, it is possible to easily associate the operation of the actual program corresponding to the interpolation obtained as a numerical solution with the proof target, which not only makes it easier for the user to understand, but also for automatic verification. It will be useful.

Further, as the solver used for this processing, by using a solver in which the description of the constraint "not equal to 0" is replaced with "greater than 0", interpolation can be obtained for a relatively large number of constraints. ..

Since the present invention can output a relatively simple polynomial representation of Craig interpolation for various proof problems, Craig is used for hardware design and verification of large-scale integrated circuits (LSIs), software program verification, and the like. It is useful when adopting a method using interpolation and automating it.

1 Automatic certification device, 11 Control unit, 12 Storage unit, 13 Operation unit, 14 Display unit, 21 Solver output receiving unit, 22 Coefficient calculation unit, 23 Verification processing unit, 24 Solution generation unit, 25 Output unit, 31 Solver unit.

Claims (5)

A means of accepting input from a solver that generates and outputs a polynomial that represents Craig interpolation for a given proof object,
A coefficient calculation means for obtaining a plurality of approximate coefficients so that the ratio of the coefficients included in the accepted polynomial is an integer ratio and the value corresponding to each coefficient is a smaller value.
From the plurality of obtained approximation coefficients, the approximation coefficients are selected in the order determined by a predetermined method, a trial polynomial in which the coefficients of the accepted polynomial are replaced with the selected approximation coefficients is generated, and the trial polynomial is generated. Is a verification means for verifying whether or not is established as a polynomial representing the Craig interpolation.
When the trial polynomial based on any of the obtained approximation coefficients is established as a polynomial representing the Craig interpolation by the verification, the generation means for generating the approximation coefficient as a solution when determined by the verification means. When,
Including
When the verification means determines that none of the trial polynomials based on any of the obtained approximation coefficients is established as a polynomial representing the Craig interpolation, the generation means determines that an error has occurred. To execute,
Automatic certification device. The automatic certification device according to claim 1.
The solver has restrictions on the subject of certification.
Polynomial f, which is greater than or equal to 0 for any variable value,
Polynomial g, greater than 0,
Polynomial h equal to 0
Is set to include at least one of
An automated theorem proving device that is a solver that generates and outputs a polynomial that represents Craig interpolation of a pair of constraints T and T'. The automatic certification device according to claim 1 or 2.
An automated theorem proving device in which the output solution is subjected to program verification or theorem proving processing. The automatic certification device according to claim 1.
The solver has restrictions on the subject of certification.
Polynomial f, which is greater than or equal to 0 for any variable value,
Polynomial g not equal to 0,
Polynomial h equal to 0
Is set to include at least one of
An automated theorem proving device that is a solver that generates and outputs a polynomial that represents Craig interpolation of a pair of constraints T and T'. Computer,
A means of accepting input from a solver that generates and outputs a polynomial that represents Craig interpolation for a given proof object,
A coefficient calculation means for obtaining a plurality of approximate coefficients so that the ratio of the coefficients included in the accepted polynomial is an integer ratio and the value corresponding to each coefficient is a smaller value.
From the plurality of obtained approximation coefficients, the approximation coefficients are selected in the order determined by a predetermined method, a trial polynomial in which the coefficients of the accepted polynomial are replaced with the selected approximation coefficients is generated, and the trial polynomial is generated. Is a verification means for verifying whether or not is established as a polynomial representing the Craig interpolation.
When the trial polynomial based on any of the obtained approximation coefficients is established as a polynomial representing the Craig interpolation by the verification, the approximation coefficient is generated as a solution when determined by the verification means, and the calculation is performed. When the verification means determines that none of the trial polynomials based on any of the approximation coefficients is established as a polynomial representing the Craig interpolation, a generation means for executing a predetermined process as if an error has occurred, and a generation means.
A program that functions as.

Images