Compositional Policy Learning in Stochastic Control Systems with Formal Guarantees

Summary

This paper proposes a verifiable RL framework that learns a composition of NN policies for stochastic control systems, along with a formal supermartingale certificate for the safety probability of satisfying the reach-avoid specification. It decomposes the global reach-avoid task into a DAG with edges denoting subtasks which are solved by policy+RASM. Finally, it composes the low-level subtask's policy into a global safe policy with probability guarantees. The authors evaluate this framework in a relatively simple Stochastic Nine Room environment.

Strengths

This paper is greatly written and easy to follow. The authors did a good job on the paper presentation. They study an important safe RL problem with step-wise safety chance constraint, which is suitable for safety-critical systems. The proposed compositional safe RL framework is novel to me. The proposed algorithm and approach are sound. Control policy learning with formal guarantees in probability is significant.

Weaknesses

1. My biggest concern is the scalability problem of this paper, which might originate from the DAG representation. If the global RL task is too complex, the graph might be too huge to handle. 2. Because of the scalability problem, the experiments in this paper look much simpler than other RL papers. 3. The authors may miss a few recent papers addressing a similar safe RL problem with chance constraints, as in a) Enforcing Hard Constraints with Soft Barriers: Safe Reinforcement Learning in Unknown Stochastic Environments, as far as I can tell, this reference also considers continuous control problems with safety probability chance constraints, and its guarantees are also based on the supermartingale property, although the approaches are quite different.

Questions

1. What are the relations between (either additive or multiplicative) RASM and barrier certificate for stochastic (either continuous or discrete) systems? The definition of the barrier certificate can be found in the following references. b) Stochastic safety verification using barrier certificates. c) A Barrier Function Approach to Finite-Time Stochastic System Verification and Control. 2. What's the complexity of the proposed algorithm? It should be feasible to conduct the big O complexity analysis as the algorithm is built on top of topologic sorting, binary searching, etc.

Rating

6: Weak Accept: Technically solid, moderate-to-high impact paper, with no major concerns with respect to evaluation, resources, reproducibility, ethical considerations.

Confidence

5: You are absolutely certain about your assessment. You are very familiar with the related work and checked the math/other details carefully.

Soundness

4 excellent

Presentation

4 excellent

Contribution

2 fair

Limitations

This paper may face a scalability problem.

Summary

This paper introduces CLAPS (Compositional Learning for Probabilistic Specifications), a new method for learning a composition of neural network policies in stochastic environments, together with a formal certificate which guarantees that a reach-avoid specification over the policy's behavior is satisfied with the desired probability. The proposed approach is evaluated empirically on a stochastic Nine Rooms environment.

Strengths

1) Different to previous works discussed by the authors, the CLAPS method is applicable to stochastic control systems, that may be defined via non-linear dynamics functions. 2) The approach is compositional. Complex tasks are analysed and solved in terms of simple tasks, that are then combined in order to achieve the overall goal. 3) The literature is discussed in detail. The bibliography, at 61 items, is an excellent overview of current methods in safe RL.

Weaknesses

1) A lot of material appears in the appendix. I did not check it, but the paper appears to be consistent. 3) This work builds on top of [61] as regards the use of supermartingales. However, the bounds obtained are stricter, which seems to justify the claims to novelty (together with the compositional approach). Minor, p. 3: When discussing the equation for the stochastic feedback loop system, u_t is described as the control action even though no u_t appears in the equation. On the other hand, function \pi is not described. I understand that \pi: X -> U is the policy and \pi(x_t) = u_t.

Questions

p. 4: When the authors say "if the probability of a random trajectory...", do they actually mean "if the probability of any trajectory..."

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.

Confidence

4: You are confident in your assessment, but not absolutely certain. It is unlikely, but not impossible, that you did not understand some parts of the submission or that you are unfamiliar with some pieces of related work.

Soundness

4 excellent

Presentation

4 excellent

Contribution

3 good

Limitations

p. 9: The authors mention that "the systematic decomposition used in our algorithm has advantages over manual task decompositions". They might discuss these advantages further.

Summary

This paper introduces CLAPS, a compositional method designed for learning and verifying neural network policies in stochastic control systems. By considering control tasks with specifications expressed in the SPECTRL language, CLAPS decomposes the task into an abstract graph of reach-avoid tasks. It utilizes reach-avoid supermartingales to offer formal guarantees on the probability of reach-avoidance in each subtask. Additionally, the paper establishes proof demonstrating that RASMs (Reach-Avoid Supermartingales) provide a significantly more stringent lower bound on the probability of reach-avoidance compared to prior approaches. The experimental evaluation conducted in the Stochastic Nine Rooms environment showcases the ability of CLAPS to derive guarantees for global compositional policies.

Strengths

+ Compositional Learning is an important research direction. The approach presented in this paper provides correctness guarantees for individual sub-policies that can be used to collectively ensure the correctness of the global policy, making the learning and verification approach valuable for applications where safety and reliability are critical. The ability to verify and validate each component of the policy offers a robust and trustworthy framework for developing complex control systems. + Taking inspiration from exponential barrier certificates developed in the control theory community, the paper introduces a conceptually similar concept to improve Reach-Avoid Supermartingales, which provides a more strict lower bound on the probability of reach-avoidance guarantees (compared with prior work [61]). + The main algorithm is easy to understand, follow, and implement.

Weaknesses

The proposed approach falls short of advancing the state-of-the-art in compositional learning and verification. While Reach-Avoid Supermartingales in prior work makes sense for providing probabilistic correctness guarantees for infinite time horizon systems, the expectation for a global policy composed of sub-policies is that each sub-policy terminates within a finite time horizon. Simpler techniques such as statistical verification, which relies on drawing a large number of samples and employing concentration inequalities, can achieve high-probability correctness guarantees for finite horizons. Consequently, the paper lacks a compelling argument showcasing why their probabilistic verification approach surpasses a straightforward statistical verification approach for compositional policies. Strengthening the paper would involve demonstrating that the probabilistic verification approach indeed outperforms stochastic verification in practice. In the specific context of the Stochastic Nine Rooms environment examined in this paper, it seems that the robot can reach the goal within a finite time horizon. Given the convergence of PPO sub-policies, it is reasonable to anticipate that stochastic verification methods can yield substantially higher probabilistic guarantees compared to the reported result of 33% in the paper's probabilistic verification approach.

Questions

+ Can the proposed Reach-Avoid Supermartingales (RASMs) approach be formally characterized in relation to exponential barrier certificates? + Have you considered applying Statistical Verification of Learning-Based Cyber-Physical Systems (https://cpsl.pratt.duke.edu/sites/cpsl.pratt.duke.edu/files/docs/zarei_hscc20.pdf) to the Nine Rooms environments?

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.

Confidence

4: You are confident in your assessment, but not absolutely certain. It is unlikely, but not impossible, that you did not understand some parts of the submission or that you are unfamiliar with some pieces of related work.

Soundness

3 good

Presentation

3 good

Contribution

2 fair

Limitations

The paper would benefit from a more comprehensive discussion and extensive experimentation regarding the advantages of the probabilistic verification approach over stochastic verification within the context of compositional policy learning.

Summary

The paper presents CLAPS, a compositional RL algorithm that also ensures guarantees of correctness when learning from temporal specifications. The core contribution of this work revolves around guarantees. Prior works in compositional RL with guarantees apply to deterministic environments and/or ones with linear dynamics. This work presents an algorithm that is suitable for stochastic environments with non-linear dynamics. The algorithm builds on two prior works., namely [61] that learns policies for control systems with non-linear dynamics with reach-avoid guarantees and [30] that compositionally learns policies (without guarantees) from temporal specifications. An empirical evaluation on 9-rooms environment over a suite of source and target states shows the efficacy of the approach in learning long-horizon tasks with guarantees.

Strengths

RL from temporal logic to learn long-horizon tasks is a promising and thriving research community. This paper makes a strong contribution in that space by learning policies with guarantees in stochastic systems with non-linear dynamics.

Weaknesses

The empirical evaluation can be strengthened. Please find concrete comments below: 1. The evaluations have been presented for one environment only. The 9-room environment is somewhat low-dimensional. I am curious about how the approach may scale to higher dimensional environments. 2. Is there a comparison between the sample complexity of CLAPS with prior compositional approaches such as DiRL? This could offer a study of tradeoffs for guarantees. 3. Would it be possible to compare CLAPS to [27] on the benchmarks that would be common to both? It would be interesting to see how the formal guarantees of both approaches compare.

Questions

I am quite unclear as to how the guarantee extends compositionally. From my understanding, a critical challenge in obtaining guarantees from compositional approaches such as [27] is that one needs to ensure the guarantee at the transition point between two edges, ie., in the region where one policy ends and the other begins. Could you clarify how that is accounted for in the proof of Theorem 5? The example I have in mind is as follows: Say, one of the subgoal regions is split by a wall such that a learn policy entering the subgoal region ends before the wall and the policy exiting the subgoal region exits from the other side of the wall. The probability of connecting these two policies is clearly not 1. How is the guarantee in CLAPS accounting for such scenarios?

Rating

5: Borderline accept: Technically solid paper where reasons to accept outweigh reasons to reject, e.g., limited evaluation. Please use sparingly.

Confidence

4: You are confident in your assessment, but not absolutely certain. It is unlikely, but not impossible, that you did not understand some parts of the submission or that you are unfamiliar with some pieces of related work.

Soundness

2 fair

Presentation

3 good

Contribution

2 fair

Limitations

See above. I can change my score based on the clarification of the question above.

Still confused about the experiment settings

I thank the authors' response. However, I am still confused about the experiment settings and the argument made in the rebuttal. In this paper > Our method learns a policy along with a formal certificate which guarantees that a specification is satisfied with the desired probability. In the rebuttal > We clarify that, while satisfaction of a reach-avoid specification (and, more generally, any SpectRL specification) can be witnessed by a finite trace, one needs infinite traces to witness that a reach-avoid specification is not satisfied. Does your argument retain its validity if I'm only concerned about verifying whether a specification is **satisfied** with a certain desired probability? I concur with your assessment that your work has strength in providing probabilistic correctness assurances for systems with infinite time horizons, such as verifying the balance of a pendulum. However, in the context of a global policy composed of sub-policies, it's expected that each sub-policy concludes within a finite time horizon. Expecting a sub-policy to run infinitely seems unreasonable. Upon reaching a sub-goal, why not transition to the subsequent sub-policy for the next sub-goal? What's the rationale behind verifying a sub-policy that **satisfies** its specification with the desired probability over an infinite time horizon? While statistical methods are only suited for and effective in finite time horizon systems, they seamlessly align with your scenario if your objective is to ensure that a specification is **satisfied** with the desired probability, and each sub-policy is anticipated to reach a known sub-goal. Even if traces longer than a certain threshold are treated as violating a specific reach-avoid specification, stochastic verification methods could conceivably provide significantly higher probabilistic assurances than the reported 33% result. In this context, why can this experimental outcome be used to validate the effectiveness of your approach?