Venue: NeurIPS 2022 Conference

Reviews:

final_score: rating: 4: Borderline reject: Technically solid paper where reasons to reject, e.g., limited evaluation, outweigh reasons to accept, e.g., good evaluation. Please use sparingly.
review_content: summary: This work presents a self-supervised method that trains a teacher to generate theorems and a solver to prove them.
The method applies to the special case of single-loop programs and an assertion that requires proof.

strengths_and_weaknesses: Strengths:
1. Problem formulation of validation assertion is precise.
2. The method uses vast augmentation to generate data.
3. A high-performance implementation of AlphaZero and search.

Weaknesses:
1. The paper is not clearly written.
2. Limited to a very special case of a single-loop.
3. Doesn't generalize, for example to nested loops and does not scale.
questions: 1. Is the model overfitting the generated data?
2. Is there a method that generalizes to different types of problems without intensive augmentation or overfitting?

limitations: The work does not address the limitation of solving one problem type that is too specific and overfitting.
review_title: null

final_score: rating: 7: Accept: Technically solid paper, with high impact on at least one sub-area, or moderate-to-high impact on more than one areas, with good-to-excellent evaluation, resources, reproducibility, and no unaddressed ethical considerations.
review_content: summary: This paper proposes an AlphaZero-like approach to loop invariant synthesis. Specifically, a teacher agent is first trained to generate programs, which are then used to train a solver agent. To incorporate domain knowledge, both agents are modeled as non-deterministic programs, which can be refined by implementing certain operators. The solver agent is a non-deterministic program with the _choose_ operator to be learned and the _reward_ operator to be designed, while the teacher agent is designed to fill a single-loop program template. In order to generate a diverse set of training programs, a number of teacher constraints are introduced. Different from the standard AlphaZero setting, both agents are trained to not only predict the value of a state but also the associated events. The implementation includes a domain-specific language for writing strategies, a graphical interface for inspecting neural network predictions, and an efficient implementation of AlphaZero algorithm. The evaluation performed on the benchmark from Code2Inv shows that Looprl (this work) significantly outperforms Code2Inv. 
strengths_and_weaknesses: Strengths:
- although fairly technical, this paper is well-writen -- the motivation is clearly illustrated and the proposed methodology of learning teacher and solver agents looks very promising
- modeling search strategies as non-deterministic programs and then reducing strategy learning into refining programs are very novel
- the implementation (including domain specific language design, graphical ainterface, high-performance MCTS search, etc.) is very solid
- the evaluation shows significant improvement compared with Code2Inv

Weaknesses:
- the title makes a very general claim of finding proofs and theorems, however, only loop invariant synthesis (for single-loop programs) is concerned in the paper. The design of teacher and solver agents are also specialied for the loop invariant synthesis problem. It might be better to adjust the title to reflect what the paper is actually trying to address
- as hinted by CLN2INV [29], the Code2Inv benchmarks are very easy to solve when domain knowledge like templates (either explicit or implict) are used.  Verification tasks from [SV-COMP](https://sv-comp.sosy-lab.org/2022/index.php) would be a much better benchmark to test the full strength of Looprl. 

questions: 
In Figure-2, operation (e.g., abduct) and operator (e.g., choose/reward) are highlighted differently. What are the key differences betweem them? 

Can you illustrate the rationality of $r_e min(n_e, m_e)$ in the reward design? What is the difference between _number of occurrences_ ($m_e) and _number of calls_ ($n_e)?

How are the set of teacher constraints designed? Are the tuned for the chosen benchmark? What needs to be done to add a new constraint?
limitations: The current evaluation is relatively weak because the Code2Inv benchmark is a simple set of small single-loop programs. Evaluations on relatively large programs like the ones used in [SV-COMP](https://sv-comp.sosy-lab.org/2022/index.php) will make this work much stronger.
review_title: null

final_score: rating: 5: Borderline accept: Technically solid paper where reasons to accept outweigh reasons to reject, e.g., limited evaluation. Please use sparingly.
review_content: summary: This paper proposes an approach to synthesizing loop invariants with reinforcement learning. The idea is to leverage abductive reasoning for which search strategies can be treated as non-deterministic programs. An AlphaZero-style RL algorithm is in turn used to refined the strategies. The paper also proposes a method to generate problems of invariant synthesis using RL. To automate some of the processes described in the paper, the authors also implemented the Looprl theorem prover consisting of features that ease the burden of customising the approach. The evaluation clearly shows the benefits of including the teacher process in this approach.
strengths_and_weaknesses: Originality and clarity:

- The idea of using RL for invariant synthesis itself is not new. However, to my knowledge the proposed method to generate new problems (i.e., the teacher process) is indeed novel. Even better, the generation of new problems uses the same methodology used to solve the problems, which leads to a uniform AlphaZero-style solution to the problem of invariant synthesis. The Looprl theorem prover clearly embodies a significant amount of work which makes the proposed approaches practical. The paper is well written and easy to follow. Overall, it is a good attempt to find loop invariants using a combination of abductive reasoning and reinforcement learning.

Quality and significance:

- My main concern is the significance. It is true that abductive reasoning is closer to the way human experts reason about invariants, but the proposed approach is conceivably insufficient for the general task of theorem proving. The crucial part of this approach is the abduct procedure, which requires intensive domain-specific expert knowledge to engineer. 

    In the case of loop invariant synthesis studied in this paper, inventing such an abduct procedure is relatively easy because the domain is mostly linear arithmetic and we have the Fourier-Motzkin elimination. However, it is unclear how an abduct procedure can be engineered for more advanced mathematics, say, algebraic geometry. I can imagine that inventing these procedures requires deep analysis of human mathematical activities, which essentially makes the proposed approach relies heavily on hand-engineered procedures.

- For the above reasons, I think that the title and the claims of this paper are perhaps too general. Invariant synthesis is a narrow instance of theorem proving (i.e., generating cut-formulae satisfying certain conditions), and the paper only shows that the approach is promising for invariant synthesis.

- The evaluation confirms the contribution of the teacher process, but is rather unconvincing in terms of absolute performance. The fact that looprl with the vanilla MCTS can solve all the problems of Code2inv benchmarks means that the expert knowledge is perhaps too strong, or that the problems are too easy, possibly both. In fact, a modern state-of-the-art invariant synthesizer such as [Spacer](https://arxiv.org/abs/1405.4028) should also be able to solve all the problems in the Code2inv benchmarks. The reviewer suggests adding more problems to the test set, such as problems from recent [SyGuS competitions](https://sygus.org).

questions: I would consider raising the scores if the authors weaken the claims, or provide convincing reasons why the approach would work for general automated or interactive theorem proving.
limitations: Yes, the authors adequately addressed the limitations.
review_title: null

Meta-review: metareview: This work presents an approach to learning to prove loop-invariant theorems, organized around jointly training teacher and solver models. Reviewers praised its originality and creativity, as well as the quality of the software artifacts produced. Both the ideas and the code could be valuable for the community.

At the same time, there is a consensus (which I agree with) that the work oversells itself by claiming to be a general framework for learning to prove theorems. Might be true that you could in principle apply the framework to other kinds of theorems, but that would have to be shown empirically. Ditto for the claim that this can be applied to program synthesis, which the paper makes in the very first sentence of the abstract.

Given these overreaches, the camera ready version of this paper _needs_ to soften its claims about its broad applicability for theorem proving and program synthesis. The authors also need to change the title so that it has "Loop Invariant" in it or something similar, which they are receptive to in the rebuttal. The paper can talk about these loftier ambitions in the conclusion, but should clearly demarcate the actual extent of the empirical results.
confidence: Less certain
Decision: Accept