Review for NeurIPS paper: Neurosymbolic Reinforcement Learning with Formally Verified Exploration

Weaknesses: (-) I have two majors concerns, one regarding the (theoretical) analysis and the other empirical evaluations. Speaking on the first point, it seems like all the safety guarantees boil down to the fact that the initial shields are safe and verifiable. However, when it gets transformed into the neural space, we use imitation learning and based my understanding, there is no guarantee that by imitation learning, the neural network would exactly reproduce what would happen in the shield. Granted, the initial symbolic-form shield is safe. Yet this transformation step seems to raise the possibility of unsafety.