任务定义
研究离散时间随机动力系统上的 infinite-horizon reach-avoid 问题，核心是目标集、危险集和概率阈值。
Problem setting
这个问题具体是什么
如果只看一句话，那就是：在给定初始集、目标集、危险集和概率要求之后，怎样得到一个既能控制系统、又能给出明确概率下界的控制器。
候选控制器
先用强化学习得到一个可用的参考控制器，让系统先具备足够好的控制表现。
可求证近似
再把神经控制器改写成更适合推理和优化求解的多项式形式，同时处理近似误差和置信度。
概率保证
通过随机障碍证书与 SOS / SDP 求解概率下界，并据此决定下一步还要不要继续迭代。
现在的方法主线
1. 先把规格写清楚
确定初始集、目标集、危险集和希望满足的概率要求。
2. 用 RL 学参考策略
当前用 SAC 训练候选控制器，为后续求证提供一个性能较好的起点。
3. 做 PAC 多项式近似
把神经控制器转成多项式控制器，让它能进入更可控的形式化求解环节。
4. 求证书和下界
通过 stochastic barrier-like certificates 和 SOS / SDP 得到形式化的概率下界。
5. 根据需要继续更新
如果第一次结果偏保守，就回到控制器或证书模板继续调整，而不是停在第一次求解上。
我更关注什么
- 不是单独做一个控制器，也不是只做验证，而是让学习、近似、求证和更新连起来。
- 最终关心的不只是“能不能跑”，还包括“下界能不能说清楚”“哪里还需要继续改”。
- 这也是为什么我会同时看控制器复杂度、证书复杂度和后续迭代方向，而不是只看一次仿真的效果。
和已有验证工作的关系
像 Policy Verification in Stochastic Dynamical Systems Using Logarithmic Neural Certificates 这类工作，更偏向“给定一个神经网络控制器以后，怎样把高概率的 reach-avoid 规格验证下来”。这条线对我很重要，因为它说明高概率验证本身是可以做得很细的。
我现在更靠前一步
我现在关心的不只是“一个现成策略怎么验证”，而是“策略先怎么学出来、再怎么转成可求证形式、最后怎样进入证书求解和后续更新”。也就是说，我更在意整条研究流程怎样真正接起来。
Next step
接下来准备怎么推进
继续做控制器更新
对第一次求证后仍偏保守的区域继续做控制器更新，而不是停在当前状态。
改进 PAC 近似
继续平衡多项式次数、样本规模和近似误差，让控制器复杂度和求解代价更稳定。
增强证书表达能力
当系统维数更高、几何结构更复杂时，需要更有表达力的证书模板和更稳的求解策略。
扩展到更复杂系统
继续考虑非多项式动力学、更高维环境，以及学习与验证之间更自动化的配合方式。