Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency

Summary

This paper designs two self-consistency methods for formalizing mathematical statements in natural language into Isabelle --- symbolic equivalence and semantic consistency. In particular, symbolic equivalence measures whether the formalized statements are equivalent (judged by the Isabelle’s built-in automated theorem provers), and semantic consistency measures the similarity of the natural language translation of the formalized statement and its original statement (In other words, semantic consistency measures whether the formalized statement keeps the semantic meaning.) Tested with various base models, this paper shows that the combination of the two proposed methods improves the success rate of the autoformalization process.

Strengths

- This paper studies an interesting topic, self-consistency for autoformalization, which is non-trivial because the target is not unique. To the best of my knowledge, this is the first paper to study the self-consistency methods for autoformalization. - Figure 2 shows that self-consistency methods for autoformalization have great potential because the pass@k accuracy keeps increasing with more trails.

Weaknesses

- The major weakness of this paper is the scope of the autoformalization --- the symbolic equivalence method only applies to the formalization of theorem statements instead of their proofs. Autoformalization of theorem statements is an arguably less significant problem since it cannot be used to verify any informal proofs.

Questions

- Definition 1 looks unnecessarily complicated to me. For two theorems A and B, does the symbolic equivalence just mean that A and B are equivalent (which can be checked by the Isabelle solve_direct tool)? - The variable misalignment example is confusing to me. In particular, do the authors suggest that the No. 2 and No.3 outputs in Figure 1 should be equivalent? It seems to me that in output No. 3, the variables x and y are untyped but x, y in output No. 2 have type real. In addition, it is even unclear to me whether output No. 3 is provable. - Is the phenomenon in Figure 2 true for models finetuned for autoformalization such as MMA? In addition, does SymEq/SemCo still improve the performance over MMA models?

Rating

5

Confidence

4

Soundness

2

Presentation

4

Contribution

2

Limitations

The authors adequately addressed the limitations and potential negative societal impact.

Summary

This paper targets the task of autoformalization for mathematics, which inputs an informal theorem statement (in English) and outputs a formal theorem statement (inside an interactive theorem prover). Prior work has used LLMs in-context to produce autoformalizations. The work is motivated by a disparity between top-1 accuracy and top-k accuracy when sampling formalizations from LLMs. The proposed method works atop any generative model of formalized statements. Their approach is to refine the k samples to a final choice via a voting mechanism. The approach is twofold - first a symbolic equivalence method uses automated theorem provers (ATPs) to check for equivalence between two formalized statements. The k-samples are then clustered by equivalence, and then they perform semantic consistency: measuring the embedding similarity between the original informal statement and the informalized formal statement. They indicate improvements over the baselines.

Strengths

1. The idea to compare formalization candidates via symbolic equivalence is interesting. It is a nice strategy to impose additional structure on the k-autoformalization samples. The use of the semantic consistency is a natural extension of the distilled backpropogation idea presented in (https://arxiv.org/abs/2302.12433). While measuring alignment with the informal statement is not automatable, the symbolic equivalence is a nice intermediate which I believe will be further explored in the future. 2. The results indicate that their approach is effective. As the approach can be placed atop any autoformalization strategy sampling > 1 candidates from a generative model, the idea is generally applicable and should be useful for all such future work.

Weaknesses

1. The semantic consistency alone does not appear to perform much better, I wonder if this is due to the choice of BERT for the embeddings. Perhaps you can use a newer model to judge its efficacy? 2. The formulae for combining the semantic consistency score do not seem to have any motivation for the particular choice of $f(x) = x, x^2, \log x$. Can the authors explain the rationale for these choices? 3. The definition of $\tau$-semantic consistency is not used elsewhere. In particular, it is unclear the purpose of the incorporation of $\tau$ as it is not mentioned again.

Questions

1. The BERT model is used for measuring embedding similarity. How do the results change if using better models? BERT is quite outdated at this point. 2. Can you provide analysis as to why the log-combination is better than the other two? 3. On line 308 you indicate that on average about 2 symbolic equivalences are proven for k = 10 samples, this is lower than I had expected. What is the average cluster size per problem? Is it often the case that the models output candidates which are not symbolically equivalent (or at least, cannot be proven to be)? Does the chosen formalization end up coming from a larger cluster, even with semantic consistency being used? 4. In algorithm 1 you mentioned you standardize candidates $\Psi_i, \Psi_j$. What is the protocol for performing this operation? Do all hypotheses go in P_i, P_j? Typos: 1. On line 164 you mentioned that prior works commonly assign scores based on cluster size. Could you include a reference? 2. On line 166 you mentioned the self-consistency is the similarity between the autoformalized version and its informalization. Did you mean the informalized version and the informal statement? Line 34: Cover -> Recover? Line 261: wining -> winning Line 301: autoformalizaiton -> autoformalization Line 578: "Some motivation examples -> "Some motivational examples" or "Motivating examples"

Rating

6

Confidence

4

Soundness

3

Presentation

3

Contribution

3

Limitations

I believe the authors have adequately addressed the potential limitations of their work in the limitations section in the appendix.

Summary

This paper introduces two methods metrics, symbolic equivalence and semantic consistency, to determine the equivalence relation between formal statements. They design novel technical solutions to measure each method and show that this improves autoformalization by allowing self-consistency-based clustering.

Strengths

1. The paper addresses an important and novel problem of improving autoformalization with more test-time compute. 2. The methods used are very intuitive and easy to understand. 3. The evaluation is sound and shows good performance gain. 4. The writing is clear and easy to follow.

Weaknesses

Since the authors investigated 5 models of different sizes, I wish they investigated the models' performances with the same amount of test-time compute. I.e., given the same amount of FLOP (as measured by cost, since Codex and GPT-4 did not reveal their parameter count), which model is preferred. This helps the reader understand which model they should choose for their workload.

Questions

How are the numbers supporting Figure 2 obtained? How many datapoints from MATH and miniF2F did you evaluate?

Rating

8

Confidence

4

Soundness

4

Presentation

4

Contribution

4

Limitations

In the conclusions, the authors did mention the things they wish to leave for future work, but it feels somewhat vague. It would be good if the authors can be more concrete and lay out future ideas they'd like to try or would like the community to carry out.

Summary

The paper presents a novel framework aimed at enhancing the accuracy of autoformalization in mathematics using LLMs. It addresses the challenge of translating natural language mathematical statements into formal language by introducing a two-pronged approach based on symbolic equivalence and semantic consistency. Symbolic equivalence leverages automated theorem provers to ensure logical homogeneity among autoformalization candidates, while semantic consistency evaluates the preservation of the original statement's meaning by comparing embeddings of the re-informalized text and the original. The framework scores and selects the best result from multiple autoformalization candidates, significantly improving accuracy across various LLMs and datasets like MATH and miniF2F. The extensive experiments demonstrate the synergistic effect of the two consistency methods, achieving relative improvements in autoformalization accuracy and reducing the need for manual verification.

Strengths

1. Clear Presentation and Structure: The paper is well-organized, with a nice logical flow. I really like the figures and tables in the paper. 2. Open Source: The authors submit the implementation of the proposed methods, which is beneficial for the research community. 3. Innovative Framework: Introduces a new approach that combines symbolic equivalence and semantic consistency to improve the accuracy of autoformalization. Symbolic equivalence and semantic consistency are mutually complementary, with their combination further enhancing performance. 4. Comprehensive Evaluation: The authors conduct extensive experiments on two mathematical datasets, MATH and miniF2F, demonstrating the efficacy of the proposed methods. 5. Wide Applicability: The proposed framework is effective across various model sizes and is not limited to a specific LLM, indicating broad applicability.

Weaknesses

This paper makes a valuable contribution to the field of formal mathematics. While I'm new to autoformalization and not an expert in this area, I believe the paper is well-written and presents a strong argument. However, due to my limited experience, my confidence level is relatively low as I might have missed some key points.

Questions

I only have a few questions as below. 1. According to Table 1, It seems to me that semantic consistency is not working alone. It has to be used with Symbolic Equivalence. Could you provide more insights into why this is the case? On the other hand, the default settings of semantic consistency use representation from BERT and cosine similarity. Did you try other alternative methods to compute semantic consistency? I am not sure if the bottleneck is the idea of semantic consistency or the method used. 2. I am wondering if the proposed method also works for "low-resource autoformalization". The community is switching from Lean 3 to Lean 4, but existing LLMs are not performing well on Lean 4 as they have not been pretrained on enough Lean 4 corpus (also because of the limited availability).

Rating

7

Confidence

2

Soundness

3

Presentation

3

Contribution

3

Limitations

The authors adequately addressed the limitations