Automated Proof Generation for Rust Code via Self-Evolution

We sincerely thank Reviewer hvY6 for the insightful comments.  Our response is the following and our revision in the revised paper is highlighted in blue:

W1. “I find that the paper tries a little bit too hard to sell the novelty of this SAFE approach … expert iteration … I would encourage the authors to tone down the language a bit more”

Thanks for your suggestion about the writing of our paper. We have made the following revision in the revised paper following your suggestion:

a) Our original submission had a short discussion comparing “expert iteration” and SAFE in Section 2. We have elaborated that discussion in the revised version.

Basically, indeed, our work applies the self-evolving / expert-iteration approach to a new task:

synthesizing correctness proof for Rust code. This new target task raises some unique challenges and hence require different designs:

• Data scarcity challenge in Verus. We do not have millions of manually-written mathematical theorems for bootstrapping, which is why we had to rely on GPT-4o for bootstrapping. We also have no access to a large quantity of proof problems and hence must synthesize problems (i.e., Rust-code transpilation + specification synthesis) by itself.

• The underlying verification engine. Math-proof synthesis can be decomposed to many small steps or tactics thanks to the interactive theorem prover, LEAN. In contrast, Verus leverages SMT-solver to prove the correctness of a function as a whole. Consequently, step-wise search strategies used in prior work do not apply here. Instead, whole-proof debugging is crucial for SAFE.

b) We have toned down the language a bit more in Introduction. Particularly, we moved the last paragraph originally in the Introduction, which summarizes the reason-of-success of SAFE and how it can help future research, to the end of Section 2 and rephrased it in the context of prior self-evolving/expert-iteration work.

c) We replaced some appearance of "SAFE" with more precise phrases (e.g., “GPT-4”) at those places you pointed out.

W2. pass@k metrics for self-debugging is unfair

Thanks for pointing out this issue. In the revised paper, we made several changes to the evaluation section, especially Table 1, to address this fairness concern.

At the end of Section 4.1.2, we explain the number of samples produced under SAFE+

We re-organized Table 1: in the revised version, SAFE+ has no Accuracy@1 result now. Instead, the generate once + debug once setting of SAFE+ is now presented in a newly added row of Accuracy@2, so that it is compared with taking two samples from other non-debugging models in a fair way. Similarly, we moved SAFE+ Accuracy@10 results in our original submission down to the Accuracy@100 row, as that is fairer as suggested by the reviewer.

We have revised the text in Section 4.2.1, so that we present a fairer statement of SAFE+’s capability.

Since Table 2 and Table 3 do not compare SAFE+ with SAFE, instead they are designed to show the differences across rounds and different specification settings, we did not reorganize them in the revised paper. But, we added the annotation of “(K + K*K)” right after the “Self-Debugging” column name to remind readers that SAFE+ produces many more than K samples.

Q1. Table 2’s “total” column

The “total” column is the mean Accuracy over all of the proof tasks in the entire VerusBench dataset. They are not the mean of the other columns in Table 2, because there are different numbers of proof tasks in SV, MBPP, and Tutorial.

Q2. “When constructing training data for the repair task, are you doing any filtering to make sure the ‘incorrect program’ is actually similar to the ‘correct program’?”

We do not filter based on the similarities between “incorrect program” and “correct program”.   For each proof task (i.e., a Rust program with a specification), we first divide its incorrect proofs into subgroups where each group's proofs have the same number of verification errors and then randomly sample at most 10 errors in each subgroup. Our target is to ensure the diversity of debugging data for training.

Q3. “the difference between SAFE and expert iteration”

Please refer to the response to W1 and Section 2 in the revised paper.

We sincerely thank the insightful comments from Reviewer K5mr. The following is our response, and we have highlighted our revisions in blue in the revised paper:

W1. “In Table 1 the Accuracy of GPT-4o on VerusBench@100 is unfortunately missing. Similarly, the result of DeepSeekCoder RAW @100 is missing”

Thanks for pointing out this issue. We have added the evaluation results of the Accuracy@100 on two raw models and GPT-4o in Table 1. Naturally, these models are all able to prove more tasks with 100 tries, comparing with only 10 or fewer tries. However, even with 100 tries, they still perform much worse than SAFE models with 10 or fewer tries even without SAFE’s self-debugging feature.

W2. “In Table 2, Round 3 appears to severely degrade performance of the resulting model on the Tutorial dataset”

The degradation only occurs for Accuracy@1 for the Tutorial dataset. The main reason is that proofs generated by LLMs might be vulnerable to minor issues --- e.g., using an integer type with bit-width (i32) instead of an integer type without bit-width (int) may cause the whole proof to break down. The occurrence of these issues is rather random and typically goes away when more samples are synthesized. For example, if we look at Accuracy@10, Round 3 model’s accuracy is consistently better than that of Round 2 for every part of VerusBench, as shown in Table 2.

Our iterative process should stop when the accuracy improvement becomes marginal. As shown in Table 6, the improvement between Round 2 and Round 3 is not significant in most settings, so we stop our self-evolution at Round 3.

W3. “There is no discussion of Limitations”

We have added a “Discussion and Limitation” section in Section D (in Appendix). Specifically, we explain two limitations of our SAFE approach and potential future work, scaling to real-world software projects and designing a fine-grained self-debugging strategy.

Thank you for providing the requested additional details. I will further read through points raised in other reviews but don't expect to adjust my score.

We sincerely thank Reviewer aKrU for the insightful comments.  We provide our response below and highlight our revisions in blue in the revised paper:

 W1.“What could be potential approach for improving the self-debugging ability in the following rounds”

This is a very good question, and definitely worth future research to look into.

We feel the potential approach likely needs to change the formation of our current self-debugging training data. Currently, the training data for self-debugging includes many pairs of incorrect proof Yx and a corresponding correct proof Y. Sometimes, the incorrect proof Yx

may contain many mistakes, causing many different verification errors. If future research can break-down the difference between Yx and Y, figuring out which edit in Y is used to fix which verification error in Yx, the resulting data can probably train a model that is better at fixing deeply flawed proof through multiple rounds of debugging.

We have added this discussion into the revised paper (Section D.2 in Appendix).

 W2.“ SAFE’s ability on smaller LLMs”

We have conducted a new experiment with DeepSeekCoder-1.3B as backbone (Section E.4 and Table 8 in Appendix).

We use the same experimental setting as in the original submission on bigger LLMs, bootstrapping DSCoder-1.3B with GPT-4o's predictions.

After the same rounds of self-evolving specification generation and proof generation. The results on the VerusBench are as below.

The results demonstrate that even when the model size is small, our self-evolution approach can still improve its capability of proof generation.

 Q1.“ What's the data input used to let the generation model generate data for the next round? … Are these data the same programs as those used in the generating round 0 data? Would the training data in each round kind of repetitive and lack of diversity”

When SAFE trains the proof-generation model, all the proof tasks (each proof task is a Rust function associated with a specification) that have not yet been proved by earlier rounds’ models are input used to let the generation model produce data. If any previously unproved task is now proved by the latest model, the proof is then added to the training set for the next round.

In each round, we fine-tune our model based on the raw model, e.g., DeepSeekCoder-33b, using all the correct proofs generated so far in all previous rounds. Following the discussion above, if Round k manages to prove many proof tasks that were not proved in earlier rounds, the training data for Round K+1 will be much richer than the training data used for Round-k and all the earlier rounds. On the other hand, if Round-k only manages to prove few tasks not proved before, the training data for Round k+1 will indeed be kind of repetitive comparing with the training data used for Round k. In that case, the self-evolving process should stop.

When SAFE trains the spec-generation model, the situation is a little bit different. At each round, all the 21K Rust programs are data input used to let the spec-generation model generate specifications. This part of the details is discussed in Section C.2 in the Appendix.

Q2. “Self-debugging is quite effective and improves the accuracy, how does the model obtain the ability of self-debugging? does the fine-tuning procedure contains self-debugging training data?”

In our proof-generation step, we fine-tune our model on two tasks simultaneously, proof generation and self-debugging; the self-debugging training data for each round comes from the correct and incorrect proofs synthesized by our models in earlier rounds. We have revised Section 3.3 (self-evolving proof-synthesis) to make this clear, together with formal definitions of our two fine-tuning tasks.

Q3. “Why are the baseline models prompted with 4 examples instead of more examples?”

These 4 examples have included the main language features of Verus proof annotations, and hence are sufficient for GPT-4o to conduct in-context learning. When we designed the GPT-4o prompt, we found that adding more examples does not clearly improve GPT-4o’s output quality. Furthermore, more examples, which means longer context, would lead to longer GPT-4o inference cost and time, which we cannot afford --- our current bootstrapping round already requires one month of non-stop GPT-4o invocation.

We sincerely thank Reviewer 73u5 for the insightful comments.  We provide our response below and highlight related revisions in blue in the revised paper:

W1. “discussion on how to scale the approach to real-world software projects”

We have added a discussion in Section D.1 (in Appendix) on this topic.

Since every function is the unit for Verus verification, we believe the LLM fine-tuned by SAFE on functions in small programs would continue to be useful for functions in large projects. Of course, if we apply SAFE to synthesize proof for large Rust projects, we expect a key challenge in how to resolve code dependencies across functions: a function may call other executable functions or specification functions, and the callee functions may exist in a different file and/or belong to a different class. How to resolve all the code dependency and provide LLM with all the needed information may require support that goes beyond machine learning.

W2.“It would strengthen the paper if more evaluation can be done on the specification generation task and how it can be combined with proof generation to automate end-to-end verification”

We have added further evaluation results and related discussion in Section E.2 and Figure 4 (in Appendix of the revised paper) that show the distribution of the correctness-score and the completeness-score of all the specifications synthesized during the self-evolving process of SAFE.

In our original submission, we designed two baselines to show how the quality of specification generation would affect the end-to-end verification and hence the effectiveness of our proof generation training: this result was shown in Table 3 (and P-values in Table 7). As the reviewer pointed out, our original presentation in Table 3 was unclear; so, we have cleaned up Table 3 in the revised paper. In general, Table 3 shows that the quality-decrease in specification substantially decreases the effectiveness of end-to-end verification for the Rust programs in our training dataset and hence the accuracy of the final proof-generation model.

W3. “The paper lacks a study on the choice of the correctness and completeness thresholds for the specification metric”

As explained in Section 3.2, SAFE needs specifications that have reasonably high scores, but not perfect scores (i.e., 1.0). Beyond the reasons that are already presented in Section 3.2, an extra reason for the relatively low Completeness threshold (0.6) is that a mutated test case might still be correct and hence should not be rejected. For example, Listing 7 illustrates a test case for “sharedElements” while it does not require the order of output list to be the same as its inputs. If we change the target output from [13, 14] to [14, 13], it is still correct and hence will lower the Completeness score of some good specifications.

We apologize that we did not have time to re-run the whole training process using different specification-filtering thresholds. We hope that the newly added Figure 4 in the revised paper (it shows the score-distribution of synthesized specifications) and the newly cleaned-up Table 3 (how proof-synthesis accuracy drops when different sets of specification are used) will help readers see how our specification filtering has helped SAFE.

W4. Writing issues

4.1 “The text in Section 3 is sometimes ad-hoc and contains low-level details”

In the revised paper, we have deleted some ad-hoc discussion in Section 3, moved some ad-hoc discussion into Appendix (e.g., the now early part of Section C.1 Specification Filtering), and added formal definitions about our task target and specification metrics (Formula (1), (2), and (3) in Section 3).

4.2 “The paper says `much previous work relies on running many test cases’ without providing any references”

We have added reference to this sentence. It is Lines 271-272 now.

4.3 “Table 2 should be Table 3”

We have changed the incorrect reference. It is Line 521 now.

4.4 “Table 3: The split of model names to multiple lines is confusing … The delta rows look redundant as well”

We have changed the model names in Table 3 and removed $\Delta$ rows.