Venue: NeurIPS 2022 Conference

Reviews:

final_score: rating: 6: Weak Accept: Technically solid, moderate-to-high impact paper, with no major concerns with respect to evaluation, resources, reproducibility, ethical considerations.
review_content: summary: The paper investigates the interesting problem of learning formal task specifications (i.e., a DFA) from (expert) demonstrations in a MDP. The main motivation is that symbolic structures (DFAs in this case) offer better properties (e.g., non-Markovian goals, goal composition, less sensitive to perturbations in the environment, etc.) compared to previous "inverse control" reward-based approaches like IRL. The main difficulty is the large search space of DFAs (even for the small toy example considered in the paper). The paper proposes the DISS (demonstration informed specification search) as an approximate solution to learning DFAs from demonstration. The key idea is to construct a structured search space over labeled examples and tasks. A knowledge-injected hill-climbing algorithm can operate efficiently in this search space to uncover the task that best "explains" the demonstrations. The key algorithmic contribution in DISS is the "surprise-guided sampler" which constructs labeled examples. Experiments are conducted on a gridworld and show the proposed method outperforming 2 baselines. 

----------

UPDATE: I thank the authors for their detailed responses and being open to suggestions. I generally agree with Reviewer Y88L's comments, especially regarding the experimental aspects (baselines, user studies) and overall clarity of the paper. The authors have addressed most reviewer feedback, incorporated a number of reviewer comments into the paper and have included some more empirical data in the Appendix. I'm more positively inclined towards the paper although I think it remains difficult to assess impact with the current set of experiments. I've revised my score upwards to incorporate all the new information.
strengths_and_weaknesses: Strengths
  + The problem of learning formal representations of goals directly from expert trajectories (without reward functions) is challenging and important. The proposed approach seems to extend the state of the art in this area. The primary contribution of the paper is algorithmic with the introduction of the DISS algorithm for identifying specifications and the SGS component for selecting labeled examples.
  + The algorithmic ideas seem rigorously developed and novel (although I'm not sure I fully understood the details in Section 4.).
  + Experiments show that the method does perform better than reasonably strong baselines (enumeration and mutation-based).

Weaknesses
  - I found the paper to be a bit hard to read (especially compared to the closely related work in [21], which was much clearer). This paper assumes or omits important definitions (e.g., $\varphi(\xi)$, LSE). Combined with the large amount of new notation, interchangeable terminology (e.g., specification vs task) and typos, I found it challenging to grasp the key ideas on my first reading. Overall, I'd suggest this paper be edited to be more self-contained and clearer.
  - The experiments are somewhat limited. I was looking forward to a deeper analysis into the learned DFAs and in particular their correctness. For example, how "close to optimal" are the DFAs (compared to an optimal DFA)? The DFA for a single example is somewhat analyzed but a more detailed "error" analysis would strengthen the paper.
  - Given the use of grid worlds in this paper and previous works [21, 22] and the above concerns, the overall impact of the paper is somewhat unclear to me. (That said, I'm open to revising my score based on the feedback and other reviewers.)
questions:   1. What's the definition of $\varphi(\xi)$? (I'm assuming the same as [21].)
  2. What's the correctness / optimality of the final DFAs wrt to ground truth?
  3. Are there any non-grid-world applications or domains in which these methods can be evaluated?
  4. What's the computational complexity of DISS? How does it compare with the baselines?
limitations: Yes.
review_title: null

final_score: rating: 6: Weak Accept: Technically solid, moderate-to-high impact paper, with no major concerns with respect to evaluation, resources, reproducibility, ethical considerations.
review_content: summary: Continuing the tradition of making the powerful goal modeling language LTL amendable to end-user usability, this paper gives an efficient approach to solve for LTL formulas (expressed using a DFA) from expert demonstrations. The crux of their algorithm is incorporating in the fact that the optimal planner is an maximum-entropy planner, using this knowledge to derive an algorithm more efficient than an enumerator agnostic to this fact.

strengths_and_weaknesses: ## str

This paper shows a promising inference algorithm that is efficient in converting expert-demonstration trajectories into DFA specifications over an MDP environment. Most importantly, it does so by considering fewer numbers of DFAs than prior algorithms. The crux of their algorithm is incorporating in the fact that the optimal planner is an maximum-entropy planner, and leveraging this information to derive an algorithm that is more efficient than enumerating a DFA and using the maximum-entropy planner afterwards to check.

## weakness

### additional baselines are required

This task can be formulated as a straight-forward program synthesis task, and one should seriously consider standard neural-symbolic approaches on it. 
Here are few suggestions:
1. For instance, in this simulated environment, one can easily generate paired data of the form (Env, DFA, Traj_from_max_ent_planner) and use supervised learning to learn a mapping from (Env,Traj_from_max_ent_planner)->DFA. One can use hugginface API on a pre-trained language model (gpt-neo) and fine tune it over some structured/textual representation of these abstract objects. Then at inference time simply use the top-k sampling to generate DFA from this fine-tuned language model, and see if it works
2. You can also develop a PCFG capable of generating DFA, then, using a learned neural network, predict the probability distributions of this PCFG, then sample top-k DFA from this grammar, and see if it works

I wouldn't be surprised there will be some very strong patterns in the datapoints (Env, DFA, Traj_from_max_ent_planner) so that a learned neural model can pick it up, and can generate some fairly good (low energy) DFAs. And you won't even have to worry about having a train/test data split since the space of DFA (like you said) is very large, so the likelihood of encountering the same DFA from training to testing is unlikely.

### motivation can be better

Synthesizing a DFA in this manner is very different from synthesizing a DFA for (for instance) regular expression matching. The key difference lies in the evaluation of the DFA, whereas in regex synthesis it is trivial to check if it is consistent with a set of accept/reject input strings, to validate if a DFA is good for specifying a goal, we need to check whether a maximum-entropy planner would produce similar trajectories as the ones given by the expert. This is important and sets this task apart from many other program synthesis tasks, where checking the validity of a program is cheap.

### few writing changes

running example 1.1 is a good attempt (I'm happy to see ML papers are adopting more of a PL paper convention with a running example section), but is still confusing. I still do not know what is the DSL that governs the "goal space" of the robot. For instance, I can infer the robot's trajectory as simply "reach the yellow square as soon as possible, but do so while using as many horizontal movements as vertical movements, while not changing directions too much" <-- is this in the goal space? probably not, as DFA cannot do counting, but how would I know that? In general conter-factuals are easier to describe if the reader knows of the space of hypothesis beforehand. Instead example 1.1 did not explain what this space is, and the reader is lost. Figure 1 has no caption, and Figure 2 has no caption. I have to guess that figure 2 is in fact the solution that explains the behaviour of the robot, i.e. it cannot visit yellow directly after visiting blue, or it will be in the "death" state. A short sentence describe the overall hypothesis space, something like "The goal space of the robot is formulated as a DFA, where edges denote traversing through multiple same-colored blocks (i.e. a blue means visiting multiple blues in succession)...". . . Okay I just took a glance at reference [21], "learning task specification from demonstrations". They explained the problem so much better. The agent moved in the way it moved because it accidentally touched water (due to wind), so it has to dry itself (brown) before touching yellow (electricity), or else it'll be zapped. That is a wonderful story and made much more sense. I don't know why you took their example and removed the most reader-friendly affordance (fire, zap, water, drying) from it. Having to go read that [21] personally only to find out an easier explanation was already there is frustrating at best.
questions: line53 : where is the light blue dotted path?


limitations: it is discussed well
review_title: null

final_score: rating: 3: Reject: For instance, a paper with technical flaws, weak evaluation, inadequate reproducibility and incompletely addressed ethical considerations.
review_content: summary: The authors introduce a method, Demonstration Informed Specification Search (DISS), for learning DFAs from examples. Their method consists of simulated annealing over DFAs and labeled examples simultaneously, with a very complex proposal distribution they call the "surprise guided sampler" (SGS) that involves among other things defining an analogue of "gradient" and incrementally conjecturing paths likely to be mislabeled by candidate DFAs. They compare against a SAT-based algorithm and a more random ablation of DISS on a toy synthetic grid-world domain and find their method performs best.
strengths_and_weaknesses: The method introduced is very complicated and the toy results are extremely meager. This ratio is highly unfavorable. In general, the paper seems unmotivated. The paper is also highly symbolic and more generally does not seem relevant to the NeurIPS community.
questions: Why is this an important problem? Also, could the kernel of the main SGS idea be demonstrated more clearly in a more abstract setting?
limitations: Yes
review_title: null

Meta-review: metareview: The paper presents a new approach for synthesizing automata-based specifications from sample behaviors. In some ways, this is very related to the problem of generating DFAs from examples, but there are important differences related to this planning context that make it more constrained. I think this is an interesting problem and there is a solid contribution in this work that the evaluation clearly demonstrates.
There is significant scope for improvement in the presentation as expressed in many of the comments in the reviews that I think are fixable in a camera ready version of the paper. I think there is a bigger question of fit with the NeurIPS community that is reflected in the low scores that the paper received. The paper reads much more like a CAV paper than a NeurIPS paper, and that might limit its impact in this community. 
confidence: Less certain
Decision: Reject