Venue: NeurIPS 2021 Track Datasets_and_Benchmarks Round1

Reviews:

final_score: rating: 8: Top 50% of accepted papers, clear accept
review_content: summary and contributions: The authors developed NATURALPROOFS, a multi-domain corpus of mathematical statements and their proofs, written in natural mathematical language. Using the developed model, the authors benchmarked strong neural methods on mathematical reference retrieval and generation tasks which test a system’s ability to determine key results that appear in proof. NATURALPROOFS allows for evaluating in-domain performance and out-of-domain generalization in broad and deep coverage mathematics, as well as real-world, low-resource settings.
strengths: The dataset is a large-scale, multi-domain dataset for studying mathematical reasoning in natural language, consisting of 32k theorem statements and proofs, 14k definitions and 2k other types of pages—the multiple domains open opportunities for investigating domain transfer and methods for low-resource settings. The use of open-source maths textbooks with theorems and proofs is interesting.
weaknesses: The author should have not clearly explained the theoretical background of the work. Some crucial points like training the BERT model with the title and content were missing in the paper; the authors should have explained why they did not attempt this.
correctness: The experiment was properly documented.
clarity: The paper is clearly written. However, more details should be given in the methodology section; this will enhance reproducibility. 
relation to prior work: Some effort was made with regard to related work. 
additional feedback: The author introduced a work that can have a positive impact on mathematics education. More effort should be made to discuss this or other potential social impacts of NaturalProof.
review_title: NATURALPROOFS: Mathematical Theorem Proving in Natural Language

final_score: rating: 7: Good paper, accept
review_content: summary and contributions: The study presented an interesting corpus called NATURALPROOFS written in natural mathematical language, which is vital in multi-application domains, for example in education. This work provides a new direction in abstracting complex mathematical problems and challenging tasks

Indeed, creating and formalizing mathematical problems using natural mathematical language itself is challenging.

I believe the paper has made a new contribution, given the following points:
•	Well written, clear and nicely structured. It is self-contained with background to the study and methods used.
•	The notations used are consistent.
•	The ablation to the study is clearly exposed.


strengths: 
Indeed, creating and formalizing mathematical problems using natural mathematical language itself is challenging.

I believe the paper has made a new contribution, given the following points:
•	Well written, clear and nicely structured. It is self-contained with background to the study and methods used.
•	The notations used are consistent.
•	The ablation to the study is clearly exposed.

weaknesses: The only demerits would be to include full set of assumptions of theoretical results which was not shown in the paper. Although, the checklist indicated that.
correctness: The submission fits the theme.
clarity: Clear and concise
relation to prior work: Clearly mentioned
additional feedback: None.
review_title: Feedback on NaturalsProof - Mathematical Theorem Proving in Natural Language

final_score: rating: 8: Top 50% of accepted papers, clear accept
review_content: summary and contributions: This paper presents a dataset and a benchmark for the domain of mixed symbolic and natural language mathematical proving, namely the NATURALProofs dataset. The samples from the dataset come from different sources and more specifically ProofWiki, the Stacks project and a few mathematical textbooks available in LaTeX and that can be parsed to create a dataset for the purpose at hand. Additionally, the authors present baselines and evaluation metrics for two tasks: 

(i) mathematical reference retrieval: given a mathematical claim (theorem + proof) the goal is identifying the set of *references*, i.e. theorems, lemmas, definitions, that are relevant in the proof.

(ii) mathematical reference generation: given a mathematical claim (theorem + proof) the goal is to generate an ordered sequence of the references used for the proof. This model can be also used as a retrieval model (although as the experiments show (and as expected) it will perform poorer than the models specifically designed for retrieval). 

strengths: 1. The work is very complete: it presents a dataset, a benchmark and also models for two different tasks. The number of experiments is very extensive.

2. The task is interesting and challenging, and although I have some doubts about the true utility of the task as it is proposed (see Weakness), the dataset seems to have been created carefully and in a curated way.

3. As I mention in the Correctness, the paper is soundless and the proposed methodology and benchmarks seems correct, IMO.

weaknesses: 1.a I have some concerns on the use the authors make about the word ‘reasoning’, how they introduce the concept of ‘mathematical proving’, and what the dataset is intended for. Specially, for the case of the retrieval task, I’m not convinced whether this can be considered as a reasoning problem (such as for instance problems where multi-hop architectures are used) or on the contrary this is simply about finding references whose (BERT) representation will be close to the target claim (BERT) representation. 

1.b Also, if I’m understanding correctly, at least for the retrieval task (and the models), the set of references R is known and fixed at inference time. If so, how is this connected to concepts such as ‘reasoning’ and ‘generalization’?

Could you share your thoughts on these?


2. As I mention in detail in the Clarity section, I found the paper a bit hard to follow.

correctness: Yes. The paper is soundless.
clarity: 1. This is a dense paper, and that makes things harder to explain. Yet, I felt the paper was a bit harder to follow than what I expected. One of the problems I had is that some information that is required to understand the paper is described in the Appendix. For instance, the process of the annotation/construction of the corpus (in this particular case it’s mostly collecting and parsing data) is blurry until the moment you check the Appendix. As the paper has been submitted to the Datasets and Benchmark tracks, I think this should be a central part of the work.
relation to prior work: 1. The novelty of the work is not perfectly clear to me at the moment. The authors clarify this is an early work on mathematical proving that combines symbolic and natural language text content, but it is not clear whether this is also one of the first works on mathematical reference retrieval and generation, and I felt the current Related Work section couldn’t clarify as it should. Would it be possible to rephrase this bit in a future version of the paper?

additional feedback: 1. Lines 34-35/80-86 discuss about different sources of the dataset being broad-coverage, deep-coverage and low-resource, however I would appreciate if more context could be given for these terms (specially w.r.t to what it is considered low-resource in the context of mathematical proving). This is a paper describing a dataset and submitted to a Datasets and Benchmark track, and so it’s content should be presented in a very detailed and specific way.

2. Lines 87-88 mention that the corpus is multi-domain, however little is said about the specific domains we can find in the dataset unless the Appendix is read. I feel it’s necessary for a piece of work introducing a dataset. I feel this is also relevant to have a better understanding of the in-domain versus the out-of-domain experiments.

3. The pairwise approach uses a small set of negative references as a tractable alternative to the parallel strategy, could you expand on how that small set of negative references is selected?

4. For the mathematical reference generation, what guarantees do we have that the reference order from a given claim is unique?

5. I felt some parts of the paper include some over-claims. For instance:
Lines 126-127, would it be possible to soft them?
Lines 19-20, at this point, it gives the impression the paper will be doing mathematical proving, which is not truly the case.

6. Are the many references that are unique or not-frequent? If so, I wonder how the performance varies depending on their frequency?

7. I might be missing something, but, why is the average length ratio (line 242) an order-aware metric?
review_title: A dataset to select definitions that are relevant to prove a mathematical claim.

Meta-review: Reviewers univocally argue for acceptance of this paper that provides a carefully crafted, large-scale, multi-domain dataset for studying mathematical reasoning in NLP. Reviewers are also impressed, extensive number of experiments in this challenging domain. A few minor points raised by reviewers are responded to by the authors with proposed edits. 

Decision: Accept