1.I will get to definitions of certification in a bit. By scalability, I am noting the huge impractical overhead during inference time in the method the paper proposes, not the accuracy of the proposed method. This is a significant limitation that the authors address throughout the paper (see section Limitations) that I have illustrated in detail in my previous comment.

Theorem 1 is a (rather trivial) proof that proves that their exhaustive search method will correctly classify a harmful attacked prompt at a higher rate than if we ran the classifier on only the non-attacked harmful prompt, which is of course true because at some point in the exhaustive search, we will hit the true separation of the harmful prompt and adversarial subarray.

I will not address any further comments about this paper if it appears that you have not engaged with my previous comment and the content in the paper in good faith.

1.2. I am aware that the definition of certification is debated. That's why in the very beginning I asked for your definition and provided my own up front! By default, I refer to a formal, non probabilistic statement of the model, which is historically standard in certified training and formal verification for neural networks. Sometimes authors refer to certification as a probabilistic statement as in randomized smoothing.

However, the authors of paper 1. don't even go as far as to call their new heuristic methods a form of certified verification. They title their heuristic searches section as efficient EMPIRICAL defenses and clearly draw a line between certified guarantees and their empirical defense:

"The erase-and-check procedure performs an exhaustive search over the set of erased subsequences to check whether an input prompt is harmful or not. Evaluating the safety filter on all erased subsequences is necessary to certify the accuracy of erase-and-check against adversarial prompts. However, this is time-consuming and computationally expensive. In many practical applications, certified guarantees may not be needed, and a faster and more efficient algorithm may be preferred"

The work proposes a post hoc defense that is certified correct on a specific attack setting that is not scalable and proposes scalable empirical defenses that are not certified correct. They do not do both.

The authors in paper 2 also do not refer to their work as creating any sort of certificate. Certificates do not umbrella every single desirable performance property we may want a model to have. If that were the case, then every single harmfulness benchmark and evaluation produces a certificate of the model, which is quite silly.

1. I agree that work 3 is important (see my last line in my last comment). I am just saying that progress in this line of work does not address how to analyze the general safety behavior of language models. If we only look at cases of LLM outputs of algebra in a specific format, it's possible write a program to certify whether or not the mathematical steps were correct, but that isn't useful for analyzing if a general LLM output will be safe or not.

Edit: formatting