Learning to Find Proofs and Theorems by Learning to Refine Search Strategies: The Case of Loop Invariant Synthesis
Authors: Jonathan Laurent
Andre Platzer
Venue: NeurIPS 2022 Accept (2022)
Keywords: Theorem Proving
Program Synthesis
AlphaZero
Reinforcement Learning

Abstract: We propose a new approach to automated theorem proving where an AlphaZero-style agent is self-training to refine a generic high-level expert strategy expressed as a nondeterministic program. An analogous teacher agent is self-training to generate tasks of suitable relevance and difficulty for the learner. This allows leveraging minimal amounts of domain knowledge to tackle problems for which training data is unavailable or hard to synthesize. As a specific illustration, we consider loop invariant synthesis for imperative programs and use neural networks to refine both the teacher and solver strategies.


Learning to Find Proofs and Theorems by Learning to Refine Search Strategies
The Case of Loop Invariant Synthesis
Jonathan Laurent Carnegie Mellon University Karlsruhe Institute of Technology
André Platzer Carnegie Mellon University
Karlsruhe Institute of Technology
Abstract
We propose a new approach to automated theorem proving where an AlphaZero- style agent self-training refine a generic high-level expert strategy expressed nondeterministic program. An analogous teacher agent is self-training to generate tasks of suitable relevance and difficulty for the learner. This allows leveraging minimal amounts of domain knowledge to tackle problems for which training data is unavailable or hard synthesize. As specific illustration, we consider loop invariant synthesis for imperative programs and use neural networks to refine both the teacher and solver strategies.
1 Introduction
Augmenting tactic-based interactive theorem provers with neural guidance has been the focus of increased attention in recent years 2 5 The dominant approach uses imitation learning on corpora of formalized mathematics. However, despite recent efforts involving self-supervised pre-training [ or auta-auummenttiion (6) this approach is limited by the conspicuous scarcity of numan-producee training data. An alternative approach inspired by the success of AlphaZero [7] is to use reinforcement learning and let agent self-train to interact with theorem prover via trial and error [8. [9. However, previous attempts doing so have been hampered by two fundamental issues:
First, existing tactic-based theorem provers offer infinite action spaces not amenable to random exploration. Also, they are optimized for formalizing the outcome of human insights concisely but often fail to define tractable search space for deriving those insights in the first place [10]. For example, using tactics effectively often requires providing insights in advance that are more easily found later in the search process (e.g. constructing term to instantiate an existential quantifier [IT). More generally. most of the human process of discovering proofs, which involves trial and error, sketching. and abductive reasoning not captured by standard prover tactics and so we can hardly expect a reinforcement learning agent to learn this process through sheer interaction with tactic-based prover.
Second, although reinforcement learning alleviates the need for human proofs during training, the agent must still be provided learning tasks of suitable relevance, diversity, difficulty, and generalizability in the form of theorem statements be proved. This is in contrast with applications of AlphaZero in board games, where the symmetric nature of games such as Chess or Go enables leveraging symmetric self-play as an infinite source of training tasks.
In this paper, suggest novel approach to learning automated theorem proving that does not rely on human-prou provided proofs and theorems. Instead, a teacher agent is trained to generate interesting and relevant tasks while solver agent is co-trained to solve them. Our insight is that both agents be implemented by using reinforcement learning to refine high-level search strategies [10] written by
36th Conference on Neural Information Processing Systems (NcurIPS 2022).

---

assume >= 1;
A desirable invariant is formula [2, y) such that:
y 0; while (y < <1000) {
x 1 = + [[x yl y < 1000 A /x. vl
(holds initially)
x = x yi
VE, y
- 1x 3.y +
(preserved) (implies post)
y= y 1;
y 2 1000 A 1 1z, vl
+ z I
assert yi
Such an invariant is 12, y] = (x z y A x M
Figure 1: An example program and an associated loop invariant
experts in the form of nondeterministic programs. Our paper also defines novel design principles and language constructs for expressing such strategies. These include conditional generative strategies as a template for implementing teachers, abductive reasoning as a design principle that is made scalable by self-learned guidance, and strategy events an abstraction that enables easier reward engineering and better sumple-efficinny: This paper introduces our new framework and also evaluates it in a well-containe' yet challenging setting, namely the automatic verification of imperative programs with loops. We frame our contributions in a way to emphasize general applicability. An empirical evaluation in other application domains is left to future work.
2 Approach
2.1 Background: Verifying Imperative Programs with Loops
Suppose we are given a program such as the one in Figure I and we want to prove that the final assertion always holds. The way to proceed is find predicate called loop invariant with the following properties: i) it is true before the loop is entered, ii) it is preserved by the loop body when the loop guard holds and iii) it implies the final assertion when the loop guard does not hold. By "preserved", we mean that if the invariant is true before executing the loop body then it is also true afterwards. Finding loop invariants is the most crucial aspect of program verification 12 and still resists automation [14].
Despite the difficulty of automatically synthesizing loop invariants, humans do routinely using well-understood search strategies. For example, in the case of the example in Figure I one would first try to prove the postcondition x: 2 y itself as invariant and then note that it is not preserved by the loop body as the following implication does not hold: y < 1000 A x 2 y A x + 2 y + However, simplifying the right-hand side, we see that the proof works if invariant itself. Using a similar form of abductive reasoning, we find that this in turn requires 2 0 to be an invariant and we end up proposing y Ax x 2 1 A y 2 0 as a loop invariant.
show 2 1 to be an
2.2 Expressing Search Strategies as Nondeterministic Programs
The search strategy we followed for the example above can be formalized as nondeterministic program, which is shown in Figure 2 As a nondeterministic program, it features choose operator that takes a list of objects as an input and selects one of them nondeterministically, A nondeterministic program can be refined into a deterministic one by providing an external oracle to implement the choose operator. It also defines search tree that can be explored with or without guiding heuristic. In this work, we use neural networks to implement such oracles and guiding heuristics.
In addition, key aspect of this strategy is to infer missing assumptions under which a currently failing proof obligation would hold. This form of reasoning is called abductive reasoning and is fundamental in the way humans search for proofs [16] 17]. It is implemented in separate abduct procedure that takes a formula as an input and returns either Valid or list of abduction candidates. For example, the abduct procedure fails to prove the implication x 2 0 + x + 2 1 but may suggest x + y > 1, x < and y 2 as possible missing assumptions. The use of abductive reasoning for theorem proving and loop invariant synthesis specifically has been proposed in the past 19. However, abduction procedures are hard to implement (20) and typically only available for specific decidable theories. Also, using them in proof search tends to scale poorly in the absence of

---

def solver(
init: Formula, guard: Formula,
3
body: Program, post: Formula) Formula:
4
def prove_inv irve_nnv(ing (inv: Formula) <> List[Formula]:
assert valio(Implies(nit, inv)) inductive
7
(nddeess(((gurr) inv), wlp(body,, inv)) match abduct (iduuc((nttttive):
case Valid:
return [inv]
case [ssuggestions]:
aux choose suggestions)
return [inv] prove_inv(aux)
inv_cand (impee(aabccc(mttteee(((oooooo inv_conjuncts prove_ prove_inv(inv, inv(iiv__ann) reward(max(-11, -0.2 len(inv_comm (on(iiv_conjunets) return And( son(<inn__ooo) wttiiiiycconntsss 18
post)))
17
Figure 2: A simple strategy for finding loop invariants, described in Python-like pseudocode syn- tax. In this strategy, an initial invariant candidate is selected nondeterministically that implies the postcondition (line 15). One ensures that this candidate holds initially (line(6), without which the strategy fails immediately. Then, one attempts to prove that is preserved by the loop body (lines] 7 and where wlp denotes Hoare's weakest liberal precondition operator (SS). If the candidate not preserved, the abduct function suggests list of assumptions that make it so. One then uses the choose operator to nondeterministically select one of them, which we try and prove invariant recursively (line 13). Because the number of abduction candidates to choose from can be large, successfully using such a strategy depends on having an effective oracle guide search. To provide sufficient context to such an oracle, calls to choose must provide some extra information that is omitted here for brevity. In this case, we would pass special token indicate the call site, the program being analyzed and the value of inv in the case of line 12 See Appendix A for more details and for a full listing of the invariant synthesis strategy that we use in our experiments.
good heuristics rank and filter abduction candidates. Our proposed framework makes abductive reasoning practical by addressing both issues: it allows leveraging self-learned guidance to select abduction candidates and it allows implementing abduction procedures nondeterministic programs that are amenable to learning themselves.
Another notable feature of the strategy in Figure 2 is the use of the reward operator on line 17 to incentivize finding short invariants (short proofs are desirable in general as they tend be easier to check, interpret and generalize). The reward operator can be used multiple times and at any point of the strategy execution. An implicit reward of or -1 is emitted when the strategy successfully returns or fails respectively. An optimal execution of nondeterministic strategy is one that maximizes the cumulative amount of collected rewards. In this example, we bound the maximal invariant size penalty in such way to ensure that finding proof is always rewarded more than failing doing so.
As argued by Selsam 10 defining search strategies as nondeterministic programs provides a natural and flexible way for experts to leverage domain-specife knowledge while outsourcing difficult proof decisions to search algorithms and learned heuristies. This paradigm differs from the standard paradigm of tactic-based theorem provers in which an external entity must orchestrate stateless tactics that do not call for any form of interactive guidance internally. In contrast, the nondeterministic programming approach inverts control and has strategies call external oracles rather than the other way around, which allows for a much tighter control of the resulting search space.
2.3 Refining Nondeterministic Strategies with Reinforcement Learning
A nondeterministic program induces (deterministic) Markov Decision Process (MDP) where intermediate states are choice points and final states are either success states (the program returns successfully) or failure states (an assertion is violated choose is called on empty list of choices).

---

Standard search algorithms can be used to navigate this MDP but doing so in an efficient and scalable way requires strong heuristics for guiding search.
In this work, we propose to learn such heuristics in a self-supervised fashion using the AlphaZero algorithm 77 21]. In AlphaZero, neural network is trained to map any state to probability distribution over available actions along with a value estimate (i.e. an estimate of the expected sum of future rewards). The neural network alone can be used as policy for navigating the MDP. However, a stronger policy results from combining the network with a tree search algorithm such as Monte-Carlo Tree Search (MCTS) [22]. The key insight underlying AlphaZero is that the network can be trained via an iterative improvement process where it is successively i) used as an MCTS heuristic to try and solve problems and then ii) updated using gradient descent so as to better predict the outcome of each attempt along with the action selected by MCTS on all states encountered along the way. More details on AlphaZero can be found in the literature 77].
Using AlphaZeero, we can refine nondeterministic proof search strategies without external proof examples to learn from. However, AlphaZero must still be provided with a set of training problems to be solved. Training problems should be diverse, relevant and numerous enough to allow proper generalization. They should also be of varied difficulty to allow for learning to bootstrap.
2.4 Generating Training Problems with Conditional Generative Strategies
In theorem proving, high-quality training problems produced by humans are often not available in quantities even remotely matching the needs of reinforcement learning to properly generalize across problem instances. A possible solution is use procedural generation techniques assemble large datasets of synthetic problems. This works well in some specific areas (23) and particularly for problems that can be framed as inverse problems such as symbolic integration [24]. In other areas, generating interesting problems is as hard as solving existing ones, possibly harder.
This is the case in partieular with the problem of loop invariant synthesis. Here, natural idea for generating problem instances would be to use a probabilistic grammar for repeatedly sampling triples consisting of program, loop invariant and an assertion and then reject all triples in which the properties defining valid invariants do not hold. Unfortunately, not only would doing so naively lead very high rejection rate, but the resulting dataset would be heavily biased towards trivial samples that are hardest to reject (e.g. programs where the final assertion is the negation of the loop guard and where the invariant does not even matter). In contrast, many classes of interesting problems from standard human-writtee written benchmarks would only be sampled with an infinitesimal probability.
In this work, we propose to generate problems using the same methodology we use to solve them: by leveraging reinforcement learning to refine nondeterministic search strategies.
Specifically, experts can define teacher strategies in the form of stochastic and nondeterministic pro- grams, each run of which either fails or successfully returns with problem instance. Reinforcement learning can then be used to refine such programs with the two objectives of maximizing the diversity and interestingness of generated problems while avoiding rejection. However, these objectives are naturally in tension since agent may be locally incentivized to avoid generating particular types of problems that are casier to reject. We introduce a design template for a class of strategies that avoid this obstacle. We call such strategies conditional generative strategies.
conditional generative strategy generates a problem in three steps: i) it samples set of constraints that define desired features for the generated problem, ii) it nondeterministicaly generates problem that respects as many constraints as possible and gets rewarded for doing so and iii) it applies a sequence of random and calidity-preservingg problem transformations as way to further increase diversity. We provide a high-level description of such a teacher strategy for invariant synthesis in Figure 3. The interest of such an architecture is that it enables decoupling the two conflicting objectives of generating valid and diverse problems: diversity is guaranteed by the first and third steps while learning can focus on the second step. This also allows using the exact same learning algorithm for training both teacher and solver agents (AlphaZero in this work).
2.5 Predicting Events Rather Than Rewards
In the standard AlphaZero setting, the network is trained to predict the value of encountered states, that is the expected sum of future rewards. However, such a number conflates lot of valuable

---

def teacher(rng: RandGen) >> Prog:
19 p refine_invii cs)
cs campple_contts(rroe
refine_body(pp cs)
p generate_ generate_prog(cs)
assert valid(inv_ p
4 p transform(p, rng)
refine_post(p cs)
5
p hide see__jiaariatt(p))
23
assert valid(inv_post(p))
6 return
24
p refine refine_init(p, cs)
assert valid(inv_init(p)
def generate_ : Constrs);
num_ violatiossn,, cs)
9
p Prog("
27
reward(mmxx-11. -0.5 nv))
10
assume init;
28
return p
while (guard) {
invariant inv_lin;
def transform(p: Prog, rng: RandGen): fuuffle_formulaas( rng)
invariant inv_auxx
31
14
invariant inv mai_; body;
32
p shuffle insifree_sstss(pp rng)
33
add @id_useless_initte rng)
34
add pid__selessspostt(( rng)
assert post;") p refine_guard(p, es)
return p
Figure 3: Simplified teacher strategy. Problems are generated by nondeterministically refining the template in lines 10 17 in way to optimize random constraints (see examples in Table I In this template, the invariant expressed as conjunction of most three sub-invariants: inv lin is linear equality or inequality, inv _aw_miiin__a is a disjunction of atomic formulas (i.e. comparisons) and inv_aux is conjunction of atomic formulas that can be used in proving inv inv_main but post. These three formulas are refined nondeterministicalyy by the call to refine_ inv on line 19 After an invariant is chosen, loop body also generated nondeterministically (0ine20) that preserves the invariant (line 2T). Finally, the num violationn function penalizes the presence of useless or redundant problem components. For example, penalty applied if inv_main features disjunct that can be removed without invalidating the problem. Appendix B provides more details on how the ref refine_ * functions can implemented. The simplest way to so to have a grammar and use the choose operator to select rules recursively. However, fancier strategies the nondeterministic programming framework. In particular, our implementation uses the abduct procedure introduced in Figure to suggest values for constants and subformulas.
inv_lin
easily be implemented in
Name
Type
Description
an integer n., then inv __mamin is refined with disjunc- tion of atomic formulas.
nun-inv-mainnddiijjnnts
none 1/2
has-conditional
bool
Whether body must include a conditional statement.
Whether assuming the negation the loop guard useful in proving the postcondition post.
doo--guard-usefuut-foo-poot
bool
If true, then inv maim inv_main always holds after executing body regardless of whether or not it holds before.
body-implies-main--in
bool
eq-only-for-init
bool
Whether or not to use equalities only in init.
Table 1: Examples of teacher constraints. Some descriptions refer to names introduced in Figure
The full list of constraints used in our experiments is available in Appendix B
5

---

information. For example, suppose teacher state is assigned value of O. Does O mean that the teacher predicted to either fail or succeed with equal probability or that will certainly succeed in generating problem that violates two constraints? And if so, which two?
Although this information is not relevant to MCTS, there several reasons for having the network predict it anyway. First, doing so can result in an increased sample efficiency by providing the network with more detailed feedback on its mistakes. Such an effect has been previously demonstrated in the KataGo project [25]. Second, it is interesting from an interpretability point of view and makes it easier to diagnose problems and weaknesses in a given network. We found third reason that is more subtle, which has to do with getting the combined benefits of issuing intermediate and final rewards.
Indeed, in the teacher strategy showed in Figure 3] only penalize the agent for violating constraint at the very end. Intuitively, there is a lost opportunity here since many violations could be detected much earlier while the problem is still being refined. Emitting intermediate reward at this point would certainly improve learning efficiency. However, the same violation can be potentially detected several different points in time and we must ensure that reward is only issued the first time. This in turns makes the job of the value prediction network harder since it needs to keep track of whether or not each violation has been penalized already. Encoding this information alone can be costly, network architectures such as transformers with quadratic
and especially so for attention-base inference cost. Having the network predict constraint violations separately offers an elegant way out: all rewards are issued at the end but from the moment constraint violation is detected, the network's s predicted probability for this violation overridden whenever a value estimate computed.
More formally, we propose to introduce the concept of an event. Strategies can declare an arbitrary number of events e and each is associated with reward re along with maximal number of occurrences m. (me = for constraint violation events) that can be counted towards the final reward. The reward operator introduced in Figure 2 is replaced by an event operator. When strategy terminates, a reward is issued implicitly with a value of -1 in case of a failure and
max {1 [ + Σ re mn,, me), Tnin
in case of a success. In this expression, Th denotes the number of calls made to event(e) during the whole episode and setting Twin > -1 guarantees that successes are always rewarded more than failures. Note that is important not to issue event penalties after a failure. Otherwise, faced with a likely failure, agent may be incentivized to simply give up and fail immediately to avoid further penalties in search of success. Also, there are two reasons for bounding the maximal number of occurrences of event that are counted towards the final reward by constant quantity m.. First, this allows having a network with a finite softmax head predict the number of occurrences of e (as we see below). Second, the m 1 case is particularly useful model events such as constraint violations that can be detected multiple times but should only be penalized once.
In this framework, the value head of the network is tasked with predicting the following probabilities: i) the probability Pa of a failure, ii) the probability P1 of succeeding with minimal reward Mmin- di) the probability P2 1 Po Pi of succeeding with greater reward and iv) the probabilities p¹, that min(ne: me)) = i for events and 0 S i & me. A value estimate derives from these probabilities:
Poo + - Tnin + P2 ΣΣ
P' i
where 8 x i[ I i) P is a corrected probability estimate accounting for the number of times n. that event(e) was raised already. In our invariant synthesis experiments, teacher and solver strategics to represent constraint violations (m, = 1) and encourage short proofs by penalizing individual proof steps respectively (m, 1).
events in both the
3 Implementation and Engineering Contributions
This paper advocates for a hybrid approach to automated theorem proving where human experts from a variety of areas can formalize their knowledge succinetly in the form of nondeterministic proving and teaching strategies. Reinforcement learning leveraged fill in the blanks in all inevitable cases where the human intuition escapes formalization.

---

Loopri
Probe
Info
goal prove-inductive
obligation:
assune 1;
y
probe-size:
36
while (y 1000)
nex-action-sizee
invariant 2 'to-prove";
nsteps:
+ y; y 1;
prior-value:
0.46
events:
assert proved...';
abduction-event
Actions
prior
abduct+ < abduct* y
0.04
0.14
conjecture y < 2c
0.00
help.
Figure 4: Using the Looprl UI inspect the solver agent on the problem from Figure Additional commented screenshots are available in Appendix
However, for this vision be practical, writing strategies and iterating on them must be as frictionless as possible. New tools and abstractions are needed to automate the process of converting nondeter- ministic programs into reinforcement learning environments, ease debugging and foster code reuse. In this work, we accomplish a crucial step in this direction by introducing the Loopri theorem prover. Looprl consists of the following collection of features:
A domain specific language for writing strategies embedded in OCaml, with first-class support for neural-guided nondeterministic programming. Strategies are automatically compiled into reinforcement learning environments that can be explored in Python.
A graphical interface that can be used to interact with strategies manually while inspecting the neural network's predictions and the behavior of MCTS (see Figure
A library of utility functions for writing program verification strategies. This library includes an implementation the abduct function introduced in Figure for integer linear arithmetic (see details in Appendix
A parallel, high-performance implementation of the (Gumbel) AlphaZero algorithm 7 21 for refining search strategies. Our implementation uses Pytorch (26] and Ray (27] It
provides support for events (see Section 2.5) and unbounded, variable-size action spaces.
The first point on developing a domain domain-specific language for writing strategies is particularly important and deserves more discussion. In our experience, having such language is not just mere matter of convenience but one feasibility. In fact, we did try to implement an initial version of a teacher strategy for loop invariant synthesis by writing pseudocode an MDP implemented in Python. However, doing so resulted in a complexity explosion where any single-Iig line change to the pseudocode could take days of work to implement.
paper and manually compiling it into
The reason compiling a nondeterministic program into an MDP manually so tedious that the whole program state must be made explicit, which includes the program stack. A tempting alternative would be to write nondeterministic code as normal Python code parametrized by an arbitrary choose function. However, this does not allow using tree search the resulting program since doing so would require cloning the whole execution state of a Python program. Fortunately, there exists a solution to this problem in the field of programming languages using search monads [28] [00 and which essentially enables writing arbitrary nondeterministic code and then reifying it into a search tree that can be manipulated explicitly.
In Looprl, we implement domain specific language embedded in OCaml for expressing nondeter- ministic strategies. OCaml is natural choice because it is fast (about two orders of magnitude faster than Python for symbolic code such as proof inferences) and has good support for monads and Python interoperability. Our language provides built-in support for the choose and event operators.
7

---

Also, it defines an intermediate graph-based based format for representing data to be sent to neural networks in an architecture-agnosicc way. Any piece of information that is passed the choose operator must be convertible to this format and feature suitable metadata ensuring a seamless integration with the Looprl user interface and debugging tools.
Experiments
We tested Looprl the problem of synthesizing loop invariants for single-loop imperative programs and evaluated it on the standard Code2Inv [29] benchmark. This benchmark contains a set of 132 programs written in C. All programs feature a single loop along with final assertion to be proven. They feature linear integer arithmetic and sometimes involve conditionals, assumptions and nondeterministic tests (some Code2Inv problems are Appendix C. Most existing invariant generation tools can only solve a subset of these problems [30]. To the best of our knowledge, only one existing tool can solve them all [3I] However, it does not use learning and relies on specific optimization techniques that are not generalizable beyond the setting of purely numerical programs.
We used Looprl implement an invariant generation strategy, which we describe in Appendix [A] In nutshell, it generalizes the simple strategy described in Figure by adding features such as the ability to abduct disjunctive invariants or to conjecture invariant templates with placeholder constants to be refined later using abduction. To our surprise and although this generic strategy can be described in only one page of pseudocode, it sufficient to simply solve every Code2Inv benchmark problem in few seconds when combined with the vanilla MCTS algorithm [2]
(with no learned heuristic).
We therefore evaluate a self-trained solver agent on its ability to solve as many Code2Inv problems as possible without resorting to any search. At every decision point, it greedily takes the highest ranked action according the network's policy head and no backtracking is allowed. We argue that such a metric is of particular interest and significance. Indeed, finding an invariant for a single loop is of limited interest of its own. Rather, doing is typically useful subtask in hierarchy of increasingly complex and relevant problems. The next level of this hierarchy may be to prove a piece of code with nested loops, and then to synthesize a function respecting specification, which is still several levels away from writing full-fledged software systems. Complex problems cannot be solved if backtracking search is needed at every level of this deep hierarchy.
4.1 Training Protocol
We train a teacher agent and solver agent in sequence using the (Gumbel) AlphaZero algorithm. Both agents use similar 1.6M parameters Dynamic Graph Transformer network (32) (see architecture details in Appendix H). The teacher agent is trained first for 20 AlphaZero iterations. During each iteration, it goes through 8000 problem generation episodes, using 64 MCTS simulations per step. Then, the network is updated using samples from the k previous iterations with & increasing from I to during training. Each iteration simulates 800 additional episodes to generate validation samples that are not used to train the network but to control overfitting via early stopping. After the teacher agent is trained, a dataset of 50K problems is gathered for training the solver, which includes a mix of 40K problems generated during the last five training iterations and 10K new ones that are generated without Gumbel exploration noise [21]. The solver agent is also trained for 20 iterations. During each iteration, it attempts to solve 20K randomly selected problems using 32 MCTS simulations per step. In addition, 5K additional problems are solved to generate validation samples. See Appendix G for complete list and explanation of all training hyperparameters.
complete training run takes about 16h on single machine with a 10-core Intel 19-10900KF processor, 64GB of RAM and a NVIDIA GeForce RTX 3080 GPU.
4.2 Experimental Results
We show training curves for the solver and teacher agents in Figures 5 and respectivell... These curves record the evolution of the average reward collected by MCTS combined with the latest network during each iteration. Error intervals are estimated based on two random seeds. Note that the maximum theoretical reward obtainable by the teacher agent is <1 since problem generation constraints may be sampled that are mutually incompatible, in which case the agent simply does its best to minimize the number of violated constraints. The same holds for the solver agent since all
8

---

0.8
Averago roward
0.5
Average reward
0.7
0.6
-1.0
0.4
15
Iteration number
Iteration number
Figure 5: Teacher training curve
Figure 6: Solver training curve
Policy
% Problems solved
Random
18.4 + 0.0
Network (untrained teacher)
39.7
1.6
Network (trained teacher)
61.5 + 0.4
Table 2: Experimental results on the Code2Inv benchmark (using backtracking search). The score for the Random heuristic is computed as an average across 10K attempts. Standard deviations are computed based using two different random seeds for the full training experiment.
generated invariants are penalized proportionally to their size. The solver agent goes through more modest reward gain during training (the y-axis is rescaled in Figure emphasize the trend). This is reflective of the fact that most problems generated by the teacher can be solved by MCTS alone and so most of the training concentrates on learning to solve about 10% of hard problems.
We show the results of our evaluation the Code2Inv benchmark in Table Three different agents are compared on the average ratio of benchmark problems for which they can successfully generate an invariant of minimal size without search or backtracking. The first agent baseline that simply selects proof actions at random. The second agent is solver network that was trained using problems generated by an untrained teacher (i.e. using MCTS but no network heuristic). Finally, the third agent is solver network trained using the full protocol of Section 4.1 These results demonstrate the critical impact of learning for both the teacher and solver agents. Unsurprisingly, an inferior teacher leads to an inferior solver with decreased generalization capabilities.
Related Work
Leveraging nondeterministic programming for proof search. The idea of combining nondeter-
ministic expert strategies with neural oracles was proposed by Selsam [10 33] as possible angle for tackling the IMO Grand Challenge 34.. However, how to train such oracles remains open problem. One proposal the description of arbitrary search problems and therefore training data from large number of heterogeneous sources. In contrast, we propose using reinforcement learning with the insight that nondeterministic search strategies can be used to generate problems in addition solving them.
32 is to use supervised learning for training a universal oracle that is conditioned on
Learning to generate synthetic theorems. Procedural generation techniques have been used for producing synthetic theorems 33 generating random proof trees from a given set of axioms and rules. Wang et al. proposed to use supervised learning learn how to guide this process towards generating more interesting theorems that are similar to those of a reference dataset [6].
36
37
24 38). These usually proceed in a backwards fashion by
Using reinforcement learning for loop invariant synthesis. Reinforcement learning has already been applied to the problem loop invariant synthesis [0) albeit in a very different way. In the aforementioned work (which introduces the Code2Inv benchmark), separate reinforcement

---

learning agent is trained from scratch on every benchmark problem, using counterexamples from an SMT solver as a training signal. This process takes minutes hours for each problem to be solved. In contrast, we train a single agent to generalize across problem instances so that new problems can be solved in matter of milliseconds.
Using reinforcement learning for theorem proving. The HOList Zero [8] and TacticZero [ systems use reinforcement learning to learn how to interact with tactic-based theorem provers without relying on human proofs. However, they still rely on large numan-produces mathematical statements to be used as training tasks and are not yet competitive with approaches based on imitation learning. The use of reinforcement learning has also been explored in the context of saturation- based subleau-based provers for first-order logic [39 40]. However, learned heuristics in such settings must operate at very low-level and are subject to speed-accuracy tradeoff that is unfavorable to deep learning.
corpora of formalized
Conclusions and Future Work
This paper took bold stride toward the challenge of self-learning automated theorem proving without relying on example theorems and proofs. It advocates hybrid approach to theorem proving where experts are provided a flexible language to formalize their -opaiin-ppecific knowledge in the form of generic nondeterministic teacher and solver strategies, leaving blanks to be filled by learning.
We demonstrated our framework by applying solves all Code2Inv challenges. More importantly, it learns to solve majority of problems with no search all despite never seeing these problems during training.
the problem of loop invariant synthesis. Our agent
None our core contributions, however, are specific to invariant synthesis. These include: i) our key insight that nondeterministic programming and reinforcement learning can be similarly combined to implement solvers and teachers, ii) conditional generative strategies as a general template to write teachers, iii) abductive reasoning as a design principle that is made scalable by self-learned guidance, iv) strategy events for easier reward engineering and better sample-efficiency, and v) an implementation that establishes engineering foundations for making the whole approach practical.
We see this paper as a first step toward a broader vision where interactive theorem provers allow users to write teacher and solver strategies for domains of mathematics and programming in modular and distributed fashion. A unique neural network can then be trained as an oracle for all these strategies. allowing better generalization and sample efficiency. However, many challenges lie ahead. In particular, while there is some evidence already 100
that effective solver strategies be written at scale (interactive theorem provers already allow specifying custom search and we are merely suggesting a generalization of this popular feature), scaling up teacher strategies raises more questions. For example, writing conditional generative strategies can be engineering-intensiee since diversity is enforced extrinsically via manually-defined constraints. Future work will explore teachers that also integrate intrinsic reward signals, either via curiosity mechanism or by having the solver directly reward the teacher for producing problems of suitable novelty and difficulty.
tactics [42 43 4
Broader Impact
Automated theorem proving for program verification and program synthesis plays an important role for increasing the safety of critical pieces of software. More automatic theorem provers enable a wider user base to benefit from the advances to their software quality. But automating theorem provers is a highly sophisticated challenge. Learning from succinct expert advice in the form of strategies may be the sweet spot enabling more generic domain speciffc automation for theorem provers.
Acknowledgments and Disclosure of Funding
This work was supported by the Alexander von Humboldt Professorship program, the National Science Foundation under Award CNNS-173622) and by DARPA under Contract No. FA8750- 18 C-0092. We thank Ruben Martins, Paul Gölz, Vincent Hellendoorn, Léonard Blier along with the anonymous reviewers at NeurlPS 2022 for their helpful comments and feedback.
10

---

References
[1] Daniel Huang, Prafulla Dhariwal, Dawn Song, and Ilya Sutskever. GamePad: learning environment for theorem proving. In 7th International Conference Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. OpenReview.net. 2019.
[2] Kaiyu Yang and Jia Deng. Learning to prove theorems via interacting with proof assistants. In Kamalika Chaudhuri and Ruslan Salakhutdinov, editors, Proceedings of the 36th International Conference on Machine Learning, ICML. 2019, 9-15 June 2019, Long Beach, California, USA, volume 97 of Proceedings of Machine Learning Research, pages 6984-6994. PMLR, 2019.
[3] Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy, and Stewart Wilcox. HOList: an environment for machine learning of higher order logic theorem proving. In Kamalika Chaudhuri and Ruslan Salakhutdinov, editors, Proceedings of the 36th International Conference on Machine Learning, ICML 2019, 9-15 June 2019, Long Beach. California, USA, PMLR, 2019.
volume 97 of Proceedings of Machine Learning Research, pages
[4] Wenda Li, Lei Yu, Yuhuai Wu, and Lawrence Paulson. IsarStep: a benchmark for high-level mathematical reasoning. In 9th International Conference on Learning Representations, ICLR 2021, Virtual Event, Austria, May 3-7, 2021. OpenReview.net, 2021.
[5] Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W. Ayers, and Stanislas Polu. Proof artifact co-training for theorem proving with language models. In The Tenth International Conference on Learning Representations, ICLR 2022, Virtual Event, April 25-29, 2022. OpenReview.net, 2022.
[6] Mingzhe Wang and Jia Deng. Learning prove theorems by learning generate theorems. In Hugo Larochelle, Marc' Aurelio Ranzato, Raia Hadsell, Maria-Florina Balcan, and Hsuan-Tien Lin, editors, Advances in Neural Information Processing Systems 33: Annual Conference on Neural Information Processing Systems 2020, NeurlPS 2020. December 6- 12, 2020, virtual, 2020.
[7] David Silver, Thomas Hubert, Julian Schrittwieser, loannis Antonoglou, Matthew Lai, Arthur Guez, Marc Lanctot, Laurent Sifre, Dharshan Kumaran, Thore Graepel, et al. A general reinforcement learning algorithm that masters chess, shogi, and go through self-play. Science, 140-1144, 2018
[8] Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, and Christian Szegedy. Learning to reason in large theories without imitation. CoRR, 0tbs/1905.10500 2019.
[9] Minchao Wu, Michael Norrish, Christian Walder, and Amir Dezfouli. TacticZero: learning to prove theorems from scratch with deep reinforcement learning. In Mare' Aurelio Ranzato, Alina Beygelzimer, Yann N. Dauphin, Percy Liang, and Jennifer Wortman Vaughan, editors, Advances in Neural Information Processing Systems 34: Annual Conference on Neural Information Processing Systems 2021, NeurlPS 2021, December 6-14, 2021, viriual, pages 9330-9342, 2021.
[10] Daniel Selsam. Beyond the tactic-state automaton. Mathematical Reasoning in General Artificial Intelligence Workshop. ICIR, 2021.
[11) Reiner Hähnle and Peter H. Schmitt. The liberalized 8-rule in free variable semantic tableaux.
J. Autom. Reasoning, (3(2):211-2211 1994.
[12] Stephen A. Cook. Soundness and completeness of an axiom system for program verification.
SIAM J. Comput., 7(1):70-90, 1978.
[13] David Harel. First-Order Dynamic Logic, volume 68 of LNCS. Springer, 1979.
[14] Jean-Christophe Filliâtre. One logic use them all. In Maria Paola Bonacina, editor, Automated Deduction - CADE-24 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings, volume 7898 of LNCS, pages 1-20. Springer, 2013.
[15] C. A. Hoare. An axiomatic basis for computer programming. Commun. ACM, 12(10):576 580, 1969.
[16] Michael Meyer. Abduction a logical view for investigating and initiating processes of discovering mathematical coherences. Educational Studies Mathematics, 1852)55 2010.
11

---

[17] George Polya. How to solve it: A new aspect of mathematical method, volume 85. Princeton university press, 2004.
[18] Isil Dillig. Thomas Dillig, Boyang Li, and Kenneth L.. McMillan. Inductive invariant generation via abductive inference. In Antony L.. Hosking, Patrick Th. Eugster, and Cristina V. Lopes. editors, Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2013, part of SPLASH 2013, Indianapolis, IN, USA, October 26-31, 2013, pages 443-456. ACM, 2013.
[19] Mnacho Echenim, Nicolas Peltier, and Yanis Sellami. Ilinva: using abduction to generate loop invariants. In Andreas Herzig and Andrei Popescu, editors, Frontiers of Combining Systems- 12th International Symposium, FroCoS 2019, London, UK, September 4-6, 2019, Proceedings, volume 11715 of LNCS, pages 77-93. Springer, 2019.
[20] Thomas Eiter and Georg Gottlob. The complexity of logic-based abduction. ACM, 42(1):3 42, 1995.
[21] Ivo Danihelka, Arthur Guez, Julian Schrittwieser, and David Silver. Policy improvement by planning with Gumbel. In The Tenth International Conference on Learning Representations, ICLR 2022, Virtual Event, April 25-29, 2022. OpenReview.net, 2022.
[22] Cameron Browne, Edward Jack Powley, Daniel Whitehouse, Simon M. Lucas, Peter I. Cowling, Philipp Rohlfshagen, Stephen Tavener, Diego Perez Liebana, Spyridon Samothrakis, and Simon Colton. A survey of Monte Carlo Tree Search methods. IEEE Trans. Comput. Intell. Al Games, 4(1):1-43, 2012.
[23] Rudy Bunel, Matthew J. Hausknecht, Jacob Devlin, Rishabh Singh, and Pushmeet Kohli. Lever- aging grammar and reinforcement learning for neural program synthesis. In 6th International Conference on Learning Representations, ICLR 2018, Vancouver, BC, Canada, April 30 May
3, 2018, Conference Track Proceedings. OpenReview.net, 2018.
[24] Guillaume Lample and François Charton. Deep learning for symbolic mathematics. In 8th International Conference on Learning Representations, ICLR 2020, Addis Ababa, Ethiopia, April 26-30, 2020. OpenReview.net, 2020.
[25]
David J. Wu. Accelerating self-play learning in go. CoRR, abs/1992.11056 2019.
[26]
Adam Paszke, Sam Gross, Francisco Massa, Adam Lerer, James Bradbury, Gregory Chanan, Trevor Killeen, Zeming Lin, Natalia Gimelshein, Luca Antiga, Alban Desmaison, Andreas Köpf, Edward 7. Yang. Zachary Vito, Martin Raison, Alykhan Tejani, Sasank Chilamkurthy, Benoit Steiner, Lu Fang. Junjie Bai, and Soumith Chintala. Pytorch: An imperative style, high-performancee deep learning library. In Hanna M. Wallach, Hugo Larochelle, Alina Beygelz- imer, Florence d' Alché-Bus Buc, Emily B. Fox, and Roman Garnett, editors, Advances in Neural Information Processing Systems 32: Annual Conference Neural Information Processing Systems 2019, NeurlPS 2019, December 8-14, 2019, Vancouver, BC, Canada, pages 2019.
[27] Philipp Moritz, Robert Nishihara, Stephanie Wang, Alexey Tumanov, Richard Liaw, Eric Liang, Melih Elibol, Zongheng Yang, William Paul, Michael I. Jordan, and Ion Stoica. Ray: A distributed framework for emerging Al applications. In Andrea C. Arpaci-Dusseau and Geoff Voelker, editors, 13th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2018, Carlsbad, CA, USA, October 8-10, 2018, pages 561-577. USENIX Association, 2018.
[28] Jules Hedges. Monad transformers for backtracking search. In Paul Blain Levy and Neel Krishnaswami, editors, Proceedings 5th Workshop on Mathematically Structured Functional Programming, MSFP@ ETAPS 2014, Grenoble, France, 12 April 2014, volume 153 of EPTCS, pages 31-50, 2014.
[29] Xujie Si, Hanjun Dai, Mukund Raghothaman, Mayur Naik, and Le Song. Learning loop invariants for program verification. In Advances in Neural Informtion Processing Systems, pages 7762-7773, 2018
[30] Xujie Si, Aaditya Naik, Hanjun Dai, Mayur Naik, and Le Song. Code2inv: deep learning framework for program verification. In Shuvendu K. Lahiri and Chao Wang, editors, Computer Aided Verification 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II. volume 12225 of LNCS, pages 151-164. Springer, 2020.
12

---

[31]
Gabriel Ryan, Justin Wong, Jianan Yao, Ronghui Gu, and Suman Jana. CLN2INV: learning
loop invariants with continuous logic networks. In 8th International Conference on Learning Representations, ICLR 2020, Addis Ababa, Ethiopia, April 26-30, 2020. OpenReview.ner, 2020.
[32] Daniel Selsam, Jesse Michael Han, Leonardo de Moura, and Patrice Godefroid. Universal policies for software-defined MDPs. arXiv preprini ar0iv::000:22222214400000 2020.
[33]
Daniel Selsam. The IMO grand challenge. ottp://aattcccoofeerreee./////gp
DS. 2020. Talk at AITP 2020.
[34]
Daniel Selsam. The IMO grand challenge: A battle of ideas. https://dselsam.githhu/
IMO-GC 1et0-GCCbatlee of ideas/ 2020.
[35] Yuhuai Wu, Albert Q. Jiang, Jimmy Ba, and Roger Baker Grosse. INT: an inequality benchmark for evaluating generalization in theorem proving. In 9th International Conference on Learning Representations, ICLR 2021, Virtual Event, Austria, May 3-7, 2021. OpenReview.net, 2021,
[36] Eser Aygün, Zafarali Ahmed, Ankit Anand, Vlad Firoiu, Xavier Glorot, Laurent Orseau, Doina Precup, and Shibl Mourad. Learning to prove from synthetic theorems. CoRR, abs/2006. 1259, 2020.
[37] Yury Puzis, Yi Gao, and Geoff Sutcliffe. Automated generation of interesting theorems. In Geoff Sutcliffe and Randy Goebel, editors, Proceedings of the Nineteenth International Florida Artificial Intelligence Research Society Conference, Melbourne Beach, Florida, USA, May
11-13, 2006, pages 49-54. AAAI Press, 2006.
[38] Stanislas Polu and llya Sutskever. Generative language modeling for automated theorem proving. CoRR, abs/2009.03399, 2020.
[39] Cezary Kaliszyk, Josef Urban, Henryk Michalewski, and Miroslav Olsák. Reinforcement learning of theorem proving. In Samy Bengio, Hanna M. Wallach, Hugo Larochelle, Kristen Grauman, Nicolò Cesa-Bianchi and Roman Garnett, editors, Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurlPS 2018, December 3-8, 2018, Montréal, Canada, pages 8836-8847, 2018.
[40] Maxwell Crouse, Ibrahim Abdelaziz, Bassem Makni, Spencer Whitehead, Cristina Cornelio, Pavan Kapanipathi, Kavitha Srinivas, Veronika Thost, Michael Witbrock, and Achille Fokoue. deep reinforcement learning approach to first-order logic theorem proving. In Thirty-Fifth AAAI Conference on Artificial Intelligence, AAAI 2021, Thirty-Third Conference on Innovative Applications of Artificial Intelligence, IAAI 2021, The Eleventh Symposium on Educational Advances in Artificial Intelligence, EAAI 2021, Virtual Event, February 2-9, 2021, pages 2279-6287. AAAI Press, 2021.
[41] Timothy Gowers. How can it be feasible to find proofs? https://gowers..worde theorem pwwving-project..... pro 2022.
com/
2022/ http/////nnnnnninnn an- automateo -weeaattcttettee
[42] David Delahaye. A tactic language for the system Coq. In Michel Parigot and Andrei Voronkov, editors, Logic for Programming and Automated Reasoning, 7th International Conference, LPAR 2000, Reunion Island, France, November 11-12, 2000, Proceedings, volume 1955 of LNCS, pages 85-95. Springer, 2000.
[43] Adam Chlipala. Certified Programming with Dependent Types A Pragmatic Introduction to the Coq Proof Assistant. MIT Press, 2013.
[44] Nathan Fulton, Stefan Mitsch, Brandon Bohrer, and André Platzer. Bellerophon: Tactical theorem proving for hybrid systems. In Mauricio Ayala- Rincón and César A. Muñoz, editors, ITP, volume 10499 of LNCS, pages 207-224. Springer, 2017.
[45] George B. Dantzig and B. Curtis Eaves. Fourier-Motzkin elimination and its dual. J. Comb. Theory, Ser. A, (1)))2888277, 1973.
[46] Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N. Gomez, Lukasz Kaiser, and Illia Polosukhin. Attention is all you need. In Isabelle Guyon, Ulrike von Luxburg, Samy Bengio, Hanna M. Wallach, Rob Fergus, S. V. N. Vishwanathan, and Roman Garnett, editors, Advances in Neural Information Processing Systems 30: Annual Conference on Neural Information P Processing Systems 2017, December 4-9, 2017, Long Beach, CA, USA, pages 1998,6008, 2017.
[47] Matthias Fey and Jan E. Lenssen. Fast graph representation learning with Porchc Geometric. In ICLR Workshop on Representation Learning on Graphs and Manifolds, 2019.
13

---

[48] Vincent J. Hellendoomn, Charles Sutton, Rishabh Singh, Petros Maniatis, and David Bieber. Global relational models of source code. 8th International Conference on Learning Repre- sentations, ICIR 2020, Addis Ababa, Ethiopia, April 26-30, 2020. OpenReview.net, 2020.
[49] Vighnesh Leonardo Shiv and Chris Quirk. Novel positional encodings to enable tree-based transformers. In Hanna M. Wallach, Hugo Larochelle, Alina Beygelzimer, Florence d' Alché- Buc, Emily B. Fox, and Roman Garnett, editors, Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019, NeurIPS 2019, December 8-14, 2019, Vancouver, BC, Canada, pages 12058-12068, 2019.
[50] Christopher Hahn, Frederik Schmitt, Jens U. Kreber, Markus Norman Rabe, and Bernd Finkbeiner. Teaching temporal logics to neural networks. In 9th International Conference Learning Representations, ICLR 2021, Virtual Event, Austria, May 3-7, 2021. Openkeview.net, 2021.
14


Reviews:
[{"review_id": "qfpG2KQ2RaY", "reviewer": "Reviewer_xxib", "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.", "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.", "rating": 5, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 2, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "Originality and clarity:\n\n- 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.\n\nQuality and significance:\n\n- 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. \n\n    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.\n\n- 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.\n\n- 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).\n", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"ethics_review_area": ""}, "extra_text": {}}, {"review_id": "VpEjMRaGr6", "reviewer": "Reviewer_grDR", "summary": "This work presents a self-supervised method that trains a teacher to generate theorems and a solver to prove them.\nThe method applies to the special case of single-loop programs and an assertion that requires proof.\n", "questions": "1. Is the model overfitting the generated data?\n2. Is there a method that generalizes to different types of problems without intensive augmentation or overfitting?\n", "limitations": "The work does not address the limitation of solving one problem type that is too specific and overfitting.", "rating": 4, "confidence": 4, "soundness": 2, "presentation": 2, "contribution": 2, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "Strengths:\n1. Problem formulation of validation assertion is precise.\n2. The method uses vast augmentation to generate data.\n3. A high-performance implementation of AlphaZero and search.\n\nWeaknesses:\n1. The paper is not clearly written.\n2. Limited to a very special case of a single-loop.\n3. Doesn't generalize, for example to nested loops and does not scale.", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"ethics_review_area": ""}, "extra_text": {}}, {"review_id": "0r0dJ5214U4", "reviewer": "Reviewer_Hkk3", "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. ", "questions": "\nIn Figure-2, operation (e.g., abduct) and operator (e.g., choose/reward) are highlighted differently. What are the key differences betweem them? \n\nCan 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)?\n\nHow 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.", "rating": 7, "confidence": 5, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "Strengths:\n- 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\n- modeling search strategies as non-deterministic programs and then reducing strategy learning into refining programs are very novel\n- the implementation (including domain specific language design, graphical ainterface, high-performance MCTS search, etc.) is very solid\n- the evaluation shows significant improvement compared with Code2Inv\n\nWeaknesses:\n- 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\n- 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. \n", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"ethics_review_area": ""}, "extra_text": {}}]

Author rebuttal:

Decision: Accept