Probabilistic Equivalence Verification Approach for Automatic Mathematical Solution Assessment

1 Introduction

In an e-learning environment, it is important to assess the knowledge proficiency of learners in order to provide relevant feedback and suggestion to enhance their learning process [Guzman and Conejo, 2007]. Most of the current e-learning systems such as Coursera [2013] and Edventure [2013] have provided support for automatic assessment, but only with multiple choice questions as it is a great challenge to support other question formats. In addition, it also takes lots of effort to convert an open-ended math question into a multiple choice question [Hyman, 2012]. Recently, there has been a growing interest in intelligent tutoring systems for supporting mathematical learning such as geometry construction [Gulwani et al., 2011], algebra problem generation [Singh et al., 2012] and automatic solution assessment [Rasila et al., 2007; 2010]. For mathematical solution assessment, it checks the equivalence of mathematical expressions in the user answer and standard solution. It is a challenging problem as the semantics of mathematical expressions are highly symbolic and equivalent mathematical expressions can be expressed in different forms.

Alvis C.M. Fong

School of Computing and Math Sciences Auckland University of Technology New Zealand

Automatic mathematical solution assessment is different from other similarity-based solution assessment problems such as automatic essay grading [Hearst, 2000] and short text marking [Mohler et al., 2011]. It is an exact verification problem which aims to verify whether the mathematical expressions in the user answer and the standard solution are equivalent or not, whereas similarity-based solution assessment aims to measure the similarity between the user answer and the standard solution according to a similarity threshold. The current techniques and Computer Algebra Systems such as Maple and Mathematica provide support for mathematical equivalence checking. However, these techniques have generated many false negative errors if the mathematical expressions are written in a different form from the standard solution.

In this paper, we propose a novel and effective Probabilistic Equivalence Verification (PEV) approach for automatic mathematical solution assessment. The proposed PEV approach is a randomized method based on probabilistic numerical equivalence testing of two mathematical expressions. It can avoid false negative errors completely while guaranteeing a small probability of false positive errors to occur. For the rest of this paper, we will discuss the related work, present the proposed PEV approach and its performance results, and give the conclusion.

2 RelatedWork

Currently, there are 3 main approaches for automatic mathematical solution assessment, namely computer algebraic approach, rule-based approach and structural approach. The computer algebraic approach is based on symbolic algebraic computation [Cohen, 2003; Von Zur Gathen and Gerhard, 2003] for automatic mathematical solution assessment. This technique is implemented in commercial Computer Algebra Systems such as Mathematica [2011] and Maple [2011]. The rule-based approach [Buchberger and Loos, 1982; Moses, 1971] is based on mathematical rules for equivalence assessment. Starting with a mathematical expression, this approach transforms it into another equivalent expression and compares it with the intended target expression for equivalence verification. The structural approach [Shatnawi and Youssef, 2007; Youssef and Shatnawi, 2006] is based on the tree representation of a mathematical expression. In this approach, two mathematical expressions are first represented as two mathematical expression trees. Then, tree matching algorithm [Apostolico and Galil, 1997] is used to compare the two trees using dynamic programming [Zhang and Shasha, 1989] for equivalence verification.

Due to the nature of symbolic computation [Yap, 2000; Cohen, 2003], all these approaches can avoid false positive errors completely. However, these approaches may generate false negative error if the provided correct answer is written in a different form from the given standard solution.

3 Problem Statement

In most mathematics questions, mathematical expressions are the most common form of the required answers. The mathematical equivalence verification problem is specified as follows. Given 2 mathematical functions f(x1, x2, .., xn) and g(x1, x2, .., xn), mathematical equivalence verification aims to verify the equivalence of the two mathematical functions f and g. Mathematically, two functions f and g are said to be equivalent (f ≡ g), if and only if they have the same value at every point in the domain D (e.g., Zn ,Rn , etc.). Note that f ≡ g iff h = f - g ≡ 0. Therefore, mathematical equivalence verification can be considered as equivalent to check whether function h is equivalent to zero, i.e., h(x1, .., xn) ≡ 0, ∀x1, .., xn ∈ D. Table 1 shows some examples of mathematical answer and solution expressions.

4 Probabilistic Equivalence Verification

Probabilistic or randomized algorithms [Alon and Spencer, 2008; Motwani and Raghavan, 1996] have been studied quite extensively for the last 30 years. As compared with purely deterministic algorithms, probabilistic algorithms are generally faster, simpler, and easier to implement. In particular, probabilistic algorithms are the most effective and efficient algorithms for a class of semantic or equivalence verification problems such as fingerprinting [Rabin, 1981], DNA screening [Ngo and Du, 2000], primality testing [Agrawal et al., 2004] and boolean expression equivalence testing [Blum et al., 1980]. In this paper, we propose a novel Probabilistic Equivalence Verification (PEV) approach for equivalence verification of two mathematical expressions. As a mathematical expression is analogous to a programming function, we can verify the equivalence of two mathematical expressions by borrowing the idea of testing methods in software engineering [Beizer, 2002]. More specifically, the proposed PEV approach is based on probabilistic numerical testing method [Alon and Spencer, 2008] and algebraic properties of mathematical expressions. Figure 1 shows the proposed PEV approach, which consists of four main steps: Mathematical Expression Categorization, Query Point Selection, Function Evaluation and Probabilistic Numerical Testing.

Before discussing these steps in details, we need to define the following definition.

Let D be a set in a finite field F and R be the real number field. In the mathematical verification problem, we aim to determine probabilistically how close a test function f : F → R is to a target function g according to a well-defined measure. We introduce the concept of distance to formalize the notion of "closeness".

Definition 1 (Distance). Let f be the test function and g be the target function. The closeness of the two functions f and g is measured in terms of the Hamming distance over D as follows:

The distance function is needed to determine the minimal number of testing points that guarantees the likelihood of false positive errors. Although it is difficult to derive the distance Δ(f, g) explicitly, we can estimate the Hamming distance Δ(f, g) of f and g by sampling random points of x ∈ D such that f(x) ̸= g(x).

Algorithm 1 presents the high level description of the PEV approach. It repeatedly evaluates the value of f at random points r1, r2, .., rn of the corresponding multivariate variable x = x1, x2, .., xn, which are sampled uniformly from a sufficiently large range. If the evaluation result is equal to 0, it returns true. Otherwise, it returns false. Different from CASs such as Maple and Mathematica, PEV can avoid false negative errors completely while guaranteeing small possibility for false positive errors to occur. As such, the proposed PEV algorithm is effective for verifying the equivalence of 2 mathematical expressions which are equivalent but may be expressed in different forms.

Algorithm 1: Probabilistic Equivalence Verification

Input: f(x), g(x) - test and target functions Output: True if f ≡ g, False if f ̸≡ g Process: 1 Identify the expression category of f and g; 2 Select a set of trial points V ⊂ D randomly such that |V | is sufficiently large; 3 Select a variable domain x ∈ V ⊂ D and a function target value range T for evaluating f and g; 4 repeat 5 Select a random point x from V uniformly and independently; 6 Test f(x) ̸= g(x) and Update Δ(f, g); until |V |; 7 if Δ(f, g) ≥ 1- ϵ then return False; 8 else return True;

4.1 Mathematical Expression Categorization

It categorizes a given pair of mathematical expressions based on the Latex representation format. The category will be used for selecting an appropriate algorithm for equivalence verification. Each mathematical expression is categorized according to the following 5 expression categories based on the increasing order of complexity for equivalence verification: Constant (CO), Univariate Polynomial (UP), Multivariate Polynomial (MP), Univariate General Function (UF) and Multivariate General Function (MF). Before discussing the details, we need to distinguish the different expression categories. As the constant, univariate polynomial and univariate general function are straightforward, we only discuss the multivariate polynomial and multivariate general function.

Definition 2 (Multivariate Polynomial). Let F be a finite field and |F| = q and d < q. A function f : Fm ← R is said to be a multivariate polynomial with degree d if it can be expressed as follows:

The degree of a particular monomial in a multivariate polynomial f is defined as the sum of the exponent of each variable in that monomial. The degree of f, denoted as deg(f), is defined as the maximum degree of all the monomials in f. For example, the degree of the monomial x61x2x53 is 12, and the degree of f = x31x22 + x61x2x53 is deg(f) = 12.

Multivariate general function f is basically a multivariate polynomial with fractional functions or transcendental functions applied on a variable x such as x3-1 x+1 , sinx, √x and ex .

The category of a pair of expressions is categorized according to the highest order of the two. Table 2 gives some examples of answers and solutions for the different mathematical expression categories.

In this research, mathematical expressions are represented in the Latex format. For example, the expression (a+b)2 has its Latex format of (a+b)ˆ2. Similarly, the expression e2+lnx has its Latex format of eˆ{2+\ln x}. To categorize a mathematical expression, content features of the Latex format of the mathematical expression is used. There are four main types of content features: constant, univariate variable, multivariate variable and elementary function. Table 3 shows some examples of the content features of answers and solutions. Based on the extracted content features, we can categorize a mathematical expression according to the decision table given in Table 4.

4.2 Query Point Selection

It aims to select random points according to a geometric structure such as axis or line, and determine the query point size for efficient equivalence verification.

Borrowing the strategies [Ibarra and Moran, 1983] used in software program testing, we use the following two strategies to select query points: axis-based selection and linebased selection. The axis-based selection strategy is used for univariate function verification, whereas the line-based selection strategy is used for multivariate function verification. The axis-based selection strategy chooses random points along the axis of a variable. The line-based selection strategy chooses random points along a line l = {x1 + th}, where t = 1, 2, .., k, which passes through x1 with a constant slope h: x1 ∈ Fm, h ∈ Fm. Figure 2 gives an illustration of the two strategies.

In our proposed probabilistic approach, the query point size, i.e., the number of distinguishing query points, is very important as it determines the correctness of the equivalence verification results. In Section 5, our theoretical investigation will show that the query point size can be determined based on the degree of f and g. In short, the query point size |V | is determined by |V | = max{deg(f), deg(g)}.

Gathen et al. [2003] showed that any elementary function can be expressed in terms of a quotient of two polynomials. Hence, the above discussion is also applicable for general functions even though their degrees are not defined explicitly.

4.3 Function Evaluation

In this research, we assume that the functions f(x) and g(x) can be evaluated accurately by using a computer algebra system. Thus, this assumption simplifies the computational implementation issues to obtain fixed point accuracy. However, in some situations, it is possible that the functions f and g may have high degree terms such as xd or consist of exponents such as ax . Hence, evaluating these terms would result in infinite values due to large values of either d or x. Thus, it will generate false negative results and degrade the performance.

To overcome this, we also observe that it is sufficient to map the final result f(x) to f(x) mod p, p ≥ |V |, where p is a prime number and V is the size of random sampling points which will be discussed in the next section. Often, the sampling size |V | is small and it is easy to find a prime number p ≥ |V |. As such, we can avoid the issue on computing large values. For efficiency, we apply the Multiply-And-Square algorithm [Yap, 2000] to compute the value of f(x) mod p when f(x) contains high degree terms or exponents.

4.4 Probabilistic Numerical Testing

It aims to estimate the distance Δ(f, g) between two mathematical expressions f and g based on the point selection strategy and function evaluation discussed in the previous steps. Specifically, it repeatedly selects a random point x ∈ V in the query point set uniformly and independently, and verifies whether f(x) ̸= g(x) or not. Then, it estimates the distance Δ(f, g) based on the fraction of number of successful points such that f(x) ̸= g(x) and the query point size. Lastly, the equivalence of two mathematical expressions f and g is determined based on whether Δ(f, g) ≥ 1 - ϵ. Note that the query point size depends on both of the mathematical expression category and the desired error bound ϵ, i.e., |V | = d+2 ϵ for univariate polynomials. In other words, the query point size determines the trade-off between the correctness of verification result and computational time.

5 Theoretical Analysis

This section aims to study the correctness of the PEV approach. The correctness property ensures that the algorithm will return True with a high probability if the two expressions have the same value on sufficiently large number of random points of x. In this case, the correctness property determines the false negative error. To guarantee the correctness property, we need to prove that the Hamming distance Δ(f, g) is small. In additon, the correctness property also guarantees that the algorithm will return False with a high probability if the two expressions do not agree on sufficiently large number of random points of x. The correctness property determines the false positive error. To guarantee the correctness property, we need to prove that the Hamming distance Δ(f, g) is high. We aim to design an effective and efficient equivalence verification algorithm, which can minimize the false positive error, false negative error and query size. Depending on the mathematical category of the two expressions f(x) and g(x), we have developed different appropriate verification algorithms accordingly. These algorithms differ on the number of query points, the strategy to select query points and the domain values of query points.

Here, we provide some theoretical analysis on the correctness of our approach. The basic idea of our proof is that if f is not equivalent to g, then the existent probability of x such that f(x) = g(x) is small. Figure 3 gives 2 examples of equivalence verification for a pair of expressions with univariate polynomials and another pair of expressions with univariate general functions. It can be seen that when the complexity of the expressions increases, the probability of false positive errors to occur also increases. It also explains why the query point size for equivalence verification of higher complexity mathematical categories is larger.

Theorem 1 (Univariate Polynomial). Let d be the maximum degree of the univariate test polynomial g(x) : V → R and the univariate target polynomial g(x) : V → R, where V ⊂ Z is a set of at least d + 2 integer points of x. If there exists a function f(x) satisfying that f(xi) = g(xi), xi ∈ V, ∀i = 1, .., d+2, then f(x) ≡ g(x). In other words, the two polynomials f(x) and g(x) are equivalent, i.e., Δ(f, g) = 0. In addition, if f(x) ̸≡ g(x), then f(x) agrees with g(x) at at most d + 1 points. Hence, we have the probability of false positive error:

By definition, we have Δ(f, g) ≥ 1 - ϵ. Therefore, it means that f(x) is not close to g(x) with a high probability. Moreover, the minimal query size of V such that the correctness property is guaranteed is d + 2.

Proof: This proof is straightforward due to the wellknown Lagrange Interpolation Polynomial Theorem [Hardy and Wright, 1980], which states that two univariate polynomials g(x) and f(x) with degree at most d can coincide at most d + 1 points of x.

Theorem 2 (Multivariate Polynomial). Let d be the maximum degree of the multivariate test polynomial f(x) : V → R and the multivariate target polynomial g(x) : V → R, where V ⊂ Z is a set of at least d multivariate integer points of x ∈ Zm. If f(x) ̸≡ g(x), then the probability that the PEV algorithm has false positive error is bounded by

By definition, we have Δ(f, g) ≥ 1 - ϵ. Therefore, it means that f(x) is not close to g(x) with a high probability. In addition, the minimal query size of V such that the correctness property is guaranteed is d + 1.

Proof: It is straightforward that the PEV algorithm has no false negative error as it is a trial-and-error method. The false positive error bound can be proved using mathematical induction on the number of variables n of the polynomial. Let P(x) = f(x)-g(x) be a multivariate polynomial. It is equivalent to prove that Pr[P(r1, r2, .., rn) = 0] ≤ d |V | .

For the case n = 1, if P ̸≡ 0, then P is a univariate variable polynomial with degree d. Thus, it has at most d roots. Hence, Pr[P(r1, r2, .., rn) = 0] ≤ d |V | .

For the inductive step, we can solve the multivariate case by fixing n - 1 variables x2, .., xn to r2, .., rn and apply the result from the univariate case. Assume that P ̸≡ 0, we compute Pr[P(r1, .., rn) = 0]. First, let k be the highest power of x1 in P . We can rewrite P as

for some polynomials A and B. Let X1 be the case that P(r1, .., rn) is evaluated to 0, and X2 be the case that A(r2, .., rn) is evaluated to 0. Using Bayes rule, we can rewrite the probability that P(r1, .., rn) = 0 as

Consider the probability of X2 (or A(r2, .., rn) = 0), the polynomial A has degree d - k with n - 1 variables. So, by inductive hypothesis on the number of variables, we obtain

Similarly, if ¬X2 (or A(r2, .., rn) ̸= 0), P is a univariate polynomial degree k. By inductive hypothesis, we have

Finally, we can substitute the results from Equations (1) and (2) into Equation (3) to complete the inductive step.

Theorem 3 (General Function). Let d = max{2deg(f) , 2deg(g) } + 1 be the maximum degree of the test function f(x) : V → R and the target function g(x) : V → R, where V ⊂ Z is a set of at least d multivariate integer points x ∈ Z or x ∈ Zm. If f(x) ̸≡ g(x), then the probability that the PEV algorithm has false positive error is bounded by

By definition, we have Δ(f, g) ≥ 1 - ϵ. Therefore, it means that f(x) is not close to g(x) with a high probability. In addition, the minimal query size of V such that the correctness property is guaranteed is max{2deg(f) , 2deg(g) } + 1.

Proof: Gathen et al. [Von Zur Gathen and Gerhard, 2003] showed that every mathematical expression f(x) can be represented as a quotient of two polynomials, i.e., f(x) = f1(x) f2(x) for some polynomials f1 (x) and f2 (x). Let f(x) and g(x) be represented in terms of quotients of polynomials, i.e., f(x) = f1(x) f2(x) and g(x) = g1(x) g2(x) . By equating the denominators of the 2 quotients, the problem becomes verifying the equivalence of two polynomials, which is similar to the previous proof.

6 Performance Evaluation

To evaluate the proposed PEV approach, we have devised 100 answer-solution pairs with 50 correct (positive) answers, and 50 incorrect (negative) answers for 100 test questions based on the undergraduate mathematics course contents. The test questions are general questions selected according to some standard mathematical functions. The 100 test cases are representative, completely different and well-selected to cover all possible function types and different levels of complexity for equivalent verification. Table 5 shows some examples of the pairs of answers and solutions for the test questions. As we are unable to obtain the codes for the existing techniques, we only evaluate the performance of PEV and compare it with Maple and Mathematica whose performance outperformed other techniques for mathematical expression equivalence verification. In addition, we also used SimPy [2013], which is a Python library for symbolic mathematics and computer algebra system, for processing Latex represented mathematical expressions.

We use the precision measure to evaluate the performance of the proposed PEV algorithm. Precision is defined as the percentage of total correct verifications from all verifications. In addition, we also measure the false negative errors and false positive errors. Note that the performance evaluation is based on the final verification result of all steps in the PEV approach. Figure 4 shows the performance results based on precision. It shows that the proposed PEV algorithm has consistently outperformed Maple and Mathematica. PEV can achieve 100% performance in precision while Maple and Mathematica can only achieve about 65% and 58% respectively. This is because PEV can avoid false negative errors and it can also reduce false positive errors to as small as possible by using many trials. Theoretically, there may occur false positive errors. However, PEV can guarantee the possibility of the false positive errors to be closed to zero by sampling a sufficiently large number of points such that the two expressions will disagree on some of these points if they are not equivalent. Table 6 gives the performance results based on the false negative error and false positive error for Maple, Mathematica and PEV. As shown from the table, both commercial CAS systems produce false negative errors with 70% in Maple and 84% in Mathematica. This has shown the effectiveness of the proposed PEV algorithm in verifying the equivalence of two mathematical expressions numerically rather than symbolically.

7 Conclusion

In this paper, we have proposed a novel approach for automatic mathematical solution assessment in Web-based mathematics testing. The proposed approach is an effective Probabilistic Equivalence Verification algorithm for mathematical solution assessment. In this paper, we have discussed and analyzed the correctness of our approach for most of the typical mathematical function types. In addition, we have also analyzed the efficiency of the proposed approach by determining the minimal number of testing points such that the small likelihood of false positive errors is guaranteed. The performance results have shown that the proposed PEV approach is very effective for mathematical answer verification and assessment. For future work, we intend to investigate Webbased testing techniques for other subjects such as physics and chemistry which contain mathematical and chemical expressions as the required answer type.