Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency

Dear Reviewer GLbW

Thank you for your review and detailed feedback. In the following, please let us address the concerns and questions you've pointed out.

[Weakness #1] The scope of our framework and the significance of statement autoformalization

First, we would like to clarify that, the symbolic equivalence could be adapted to the proof autoformalization. Formally speaking, a formal proof is nothing but a sequence of formal subgoals logically connected (e.g., see Figure 2 in DSP [1]). Since there is no clear difference between the autoformalization for the final goal and the intermediate subgoals, the symbolic equivalence should be still effective in proof autoformalization. We leave the exploration of this direction as the future work.

Next, while we do recognize the importance of automatic verification of informal proofs and regard it as our future work, we respectfully disagree with the comment that “Autoformalization of theorem statements is an arguably less significant problem since it cannot be used to verify any informal proofs”. Elaborately, automatic verification of informal proofs can be achieved by autoformalizing each subgoals in the informal proof, and the validity of the formal proof can be verified with a proof assistant such as Isabelle or Lean. Hence, we do believe the statement autoformalization capability is the foundation for verifying informal proofs.

Moreover, technically, proof autoformalization requires not only the informal statement and proof as input but also the formal statement [1, 2]. Therefore, having a correct formal statement for the informal statement is a crucial precondition for the success of proof autoformalization.

Finally, for theorem proving, proof autoformalization is not necessary. For example, the recent AlphaProof project [3] by Google DeepMind uses statement autoformalization to generate approximately 100 million problems and trains its solver network using the AlphaZero algorithm.

[1] Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs. ICLR 2023

[2] Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalization. ICLR 2024

[3] https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/

[Question #1] Compared with solve_direct tactic

It is quite hard to formally define the equivalence between two theorems, and hence we try to define the symbolic equivalence as a metric of the consistency between two formal statements. Continue the example shown in Figure 1, given a formal statement,solve_direct can successfully detect its duplicate version, but cannot detect its variant although it is still a correct formalization.

theorem first_statement : 
fixes a b :: real
assumes "a = 2/3"
and "b = 6"
shows "a * b = 4"
  using assms(1) assms(2) by force

theorem second_statement : 
fixes x y :: real
assumes "x = 2/3"
and "y = 6"
shows "x * y = 4"
  solve_direct
  
(* solve_direct: the current goal can be solved directly with
  Scratch.first_statement: ?a = 2 / 3 ⟹ ?b = 6 ⟹ ?a * ?b = 4 *)
  
theorem first_statement : 
fixes a b :: real
assumes "a = 2/3"
and "b = 6"
shows "a * b = 4"
  using assms(1) assms(2) by force

theorem second_statement : 
fixes y :: real
assumes  "y = 6"
shows "(2 / 3) * y = 4"
  solve_direct

(* No proof found *)

Empirically, we also replace the symbolic equivalence with solve_direct tactic and conduct a comparison experiment using GPT-4 autoformalization results. The 1@k results shown in the following indicate that the symbolic equivalence still outperforms solve_direct either when solely used or combined with the semantic consistency.

[Question #2] A mistake in Figure 1

We apologize for the mistake made in Figure 1. The No.3 output in Figure 1 is provable and it should be

theorem
fixes x y :: real
assumes "x = 2/3"
and "y = 6"
shows "x * y = 4"

[Question #3] Is the proposed methods still effective on MMA fine-tuned models?

Thanks for the comment. We trained a Mistral 7B model using the Isabelle data in MMA, and evaluate our framework using this model on 60 MATH problems. The pass@k (k=1,2,3,10) are 23.3%, 31.6%, 35%, 46.6%, respectively, indicating the curve in Figure 1 is still effective for this model. In addition, the n@k results are provided as follows, and we can observe that our framework also works well.

Dear Reviewer LZ2a

Thank you for the insightful feedback on our paper. We appreciate the time and effort you have put into reviewing our work, and we are grateful for encouraging comments such as interesting idea, effective results, and general applicability. We have carefully read your review and addressed your concerns as follows.

[Weakness #1 & Question #1] Newer model for the semantic consistency

Thanks for the comment. As suggested, we use e5-Mistral [1] instead of the BERT as a new embedding model. The results are shown as follows. It appears that the embedding model update makes a minimal impact on performance. This may due to that the effectiveness of informalization may be more critical than the embedding model for the semantic consistency.

[Weakness #1 & Question #2] The rationale of combination strategy

The choice of combination strategy (linear, quadratic, or logarithmic) is determined empirically. Curves of three combination strategies are shown in Figure 4 and Figure 7, and we can observe that the log-combination is the most stable. A potential reason for this result may due to that the log transformation numerically imposes a heavier penalty on candidates with lower scores, thereby reducing their likelihood of being selected. We will present a comprehensive analysis about combination strategy in our revision.

[Weakness #3] The definition of $\tau$-semantic consistency

The definition of $\tau$-semantic consistency is included for the completeness and serves as a counterpart to the symbolic equivalence. In the implementation, we directly use the embedding similarity as the score of semantic consistency.

[Question #3.1] What is the average cluster size per problem?

We apologize for the confusion. In the paper (line 308), “2.13 vs. 2.33” is computed by the average size of symbolic equivalence classes across ALL problems, i.e., $\sum$ sizes of all classes on all problems / $\sum$ Number of classes on all problems. For example, given two problems and their symbolic class sizes are 10 and 1 (i.e., all problem are symbolically equivalent and none problem are symbolically equivalent). Then the average size is calculated by (10 + 10 $\times$ 1) / (1 + 10). Following your suggestion, we list the average and maximum cluster size per problem (using GPT-4 outputs) as follows. We will clarify this and include the results in the revision.

[Question #3.2] Is it often the case that the models output candidates which are not symbolically equivalent?

From the above results, the model frequently produces candidates that are symbolically equivalent.

[Question #3.3] Does the chosen formalization end up coming from a larger cluster, even with semantic consistency being used?

Yes. Generally, the efficacy of log-combination is derived from that (1) the symbolic equivalence determines multiple large clusters, and then (2) the semantic consistency distinguishes the best one from them.

[Question #4] The protocol for performing standardization

The standardization is employed to align variables and it does put all hypothesis into $P_i$ and $P_j$. Elaborately, given two formal statements, if their conclusions are in the form of the numerical relation, the standardization introduces new variables $\alpha$, and identifies other variable as auxiliary variables. For other cases, the standardization conduct the bipartite matching for the alignment.

[Typos #1]

Thanks for the comments. We will include Self-Consistency [2], CodeT [3], and Multi-Perspective Self-Consistency [4], as references.

[Typos #2]

Yes, the self-consistency in the context refers to the similarity between the informalized version and the informal statement.

[1] https://huggingface.co/intfloat/e5-mistral-7b-instruct

[2] Self-Consistency Improves Chain of Thought Reasoning in Language Models, ICLR 2023

[3] CodeT: Code Generation with Generated Tests, ICLR 2023

[4] Enhancing Large Language Models in Coding Through Multi-Perspective Self-Consistency, ACL 2024

Equivalence checking solely up to variable naming is not considered the general case. In fact, the primary challenge in autoformalization lies in accurately modeling mathematical concepts. Therefore, symbolic reasoning that extends beyond mere variable matching is essential when language models represent the same concept in various ways.

We list four examples in the following.

(*A standard six-sided die was rolled 50 times, and the outcomes are shown in the table. What is the average of the 50 outcomes? Express your answer as a decimal to the nearest hundredth. \\begin{tabular}{|c|c|}\n\\hline\nOutcome&$\\#$ of Occurrences\\\\\\hline\n1&14\\\\\\hline\n2&5\\\\\\hline\n3&9\\\\\\hline\n4&7\\\\\\hline\n5&7\\\\\\hline\n6&8\\\\\\hline\n\\end{tabular}*)

theorem
fixes outcome :: "nat \<Rightarrow> nat"
assumes h0 : "outcome 1 = 14"
and h1 : "outcome 2 = 5"
and h2 : "outcome 3 = 9"
and h3 : "outcome 4 = 7"
and h4 : "outcome 5 = 7"
and h5 : "outcome 6 = 8"
and h6 : "sum outcome {1..6} = 50"
shows "(sum (\<lambda>i. i * outcome i) {1..6}) / 50 = 3.24"

theorem
fixes avg :: real
assumes h0 : "avg = (14*1 + 5*2 + 9*3 + 7*4 + 7*5 + 8*6) / 50"
shows "avg = 3.24"

(* Problem : The sum of the $x$-coordinates of the vertices of a triangle in the Cartesian plane equals $\\sqrt{13}$.  
	Let $S$ equal the sum of the $x$-coordinates of the midpoints of the sides of the triangle. 
	Find $S^2$.*)

theorem
fixes A B C M1 M2 M3 :: "real * real"
assumes h0 : "fst A + fst B + fst C = sqrt 13"
and h1 : "M1 = ((fst A + fst B) / 2, (snd A + snd B) / 2)"
and h2 : "M2 = ((fst B + fst C) / 2, (snd B + snd C) / 2)"
and h3 : "M3 = ((fst A + fst C) / 2, (snd A + snd C) / 2)"
and h4 : "S = fst M1 + fst M2 + fst M3"
shows "S powr 2 = 13"

theorem
fixes A B C M1 M2 M3 :: "real * real"
assumes h0 : "fst A + fst B + fst C = sqrt 13"
and h1 : "M1 = midpoint A B"
and h2 : "M2 = midpoint B C"
and h3 : "M3 = midpoint C A"
and h4 : "\<forall> P Q. midpoint P Q = ((fst P + fst Q)/2, (snd P + snd Q)/2)"
and h5 : "S = fst M1 + fst M2 + fst M3"
shows "S^2 = 13"

(* What is the least common multiple of all positive integers smaller than 8? *)
	
theorem
fixes n :: nat and lcm :: "nat \<Rightarrow> nat \<Rightarrow> nat"
assumes h0 : "n < 8"
and h1 : "\<forall> a b. lcm a b = (a * b) div (gcd a b)"
shows "fold lcm [1..<8] 1 = 420"

theorem
fixes lcm :: "nat \<Rightarrow> nat \<Rightarrow> nat"
assumes h0 : "\<forall> a b. lcm a b = (a * b) div (gcd a b)"
shows "lcm (lcm (lcm (lcm (lcm (lcm (lcm 1 1) 2) 3) 4) 5) 6) 7 = 420"


(* Daniel works at an electronics store, and he claims that the popularity of a television (measured in number of sales) is inversely proportional to its cost. 
If 15 customers buy a television that costs $\\$$1500, according to Daniel's theory, how many customers would buy a television that costs $\\$$2500? *)

theorem
fixes cost1 cost2 sales1 sales2 :: real
assumes h0 : "cost1 = 1500"
and h1 : "cost2 = 2500"
and h2 : "sales1 = 15"
and h3 : "cost1 * sales1 = cost2 * sales2"
shows "sales2 = 9"

theorem
fixes x y k :: real and f :: "real \<Rightarrow> real"
assumes h0 : "f 1500 = 15"
and h1 : "f 2500 = y"
and h2 : "\<forall> x. x * f x = k"
shows "y = 9"

Dear Reviewer zk1U

Thank you for the insightful feedback on our paper. We appreciate the time and effort you have put into reviewing our work, and we are grateful for the recognition of the importance of our research problem and encouraging comments such as clear writing, easy-to-understand, and good performance. We have carefully read your review and addressed your concerns as follows.

[Question #1] Autoformalization cost of different LLMs

Thank you for the suggestion. To assess the autoformalization cost of various LLMs, we calculate the number of output tokens generated per problem and present the results in the following. Considering the pricing for LLM generation, CodeX offers superior cost-effectiveness, since it not only achieves comparable performance with GPT-4 but also incurs a cost that is less than one-fifth of GPT-4's expense. We will include these results in the revision.

[Question #2] Data sizes used in Figure 1 and evaluation

For the MATH dataset, we randomly selected a subset of 400 problems. As to the miniF2F dataset, we use the whole 488 problems. Figure 1 is obtained under the same setting. More details regarding the experimental setup are included in Section 4.1.

[Limitation] Vague future work

We appreciate your suggestion. The future work along with the proposed framework may lie in (1) adapting the proposed framework to the LEAN prover; (2) incorporating better large language models such as ProofGPT [1] and MMA [2] to further improve the performance of the framework; (3) generating more high-quality aligned informal and formal data using our framework; (4) generalizing our framework to proof autoformalization. We will update our paper to further specify these future directions.

[1] ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics

[2] Multilingual Mathematical Autoformalization

Dear Reviewer 37Eh:

Thank you for the insightful feedback on our paper. We appreciate the time and effort you have put into reviewing our work, and we are grateful for encouraging comments such as clear presentation, comprehensive evaluation, and wide applicability. We have carefully read your review and addressed your concerns as follows.

[Question #1.1] Illustration of the semantic consistency

The performance of semantic consistency relies on the informalization process, which is relatively sensitive to the category and difficulty of the problem (see Table 2 and Table 4). While semantic consistency can work well for certain problems, this sensitivity can lead to inconsistent performance when used alone. On the other hand, symbolic equivalence provides a more stable performance by computing the score based on the size of the derived equivalence class, as seen in Figure 6. When combined, semantic consistency and symbolic equivalence complement each other effectively. Semantic consistency helps identify the optimal version among multiple large symbolic equivalence classes, thereby enhancing overall performance.

[Question #1.2] Alternative methods to compute semantic consistency

We appreciate your suggestion to explore alternative methods. As suggested, we use e5-Mistral [1] as an alternative to BERT for our embedding model. The results are detailed below. We can observe that the new embedding model does not make a significant impact on the results. This observation suggests that the quality of informalization is more critical for semantic consistency than the specific embedding model used.

[Question #2] Low-resource autoformalization

Although we have not yet adapted our framework to LEAN (this is planned for future work). However, the results from Table 1 and Figure 5 demonstrate that our framework remains effective even with models exhibiting low autoformalization performance (e.g., a significant improvement from 18.1% to 42.6% and from 7.5% to 18.0% for Mistral 7B on MATH and MiniF2F, respectively). Therefore, the efficacy of our framework could be expected even if the low-resource degrades the model performance.

[1] https://huggingface.co/intfloat/e5-mistral-7b-instruct