10:02
官方账号arXiv cs.LG@Matthias Cosler, Cas Cremers, Bernd Finkbeiner, Mohamed Ghanem, Niklas Medinger
推荐理由：做安全协议验证的团队终于有了减少人工的利器——RL框架自动生成更短证明，Tamarin用户可以直接集成到现有工作流中，值得一试。
自动证明
共 1 条相关 AI 资讯
5月25日
10:02
本文提出一个基于强化学习的框架，借鉴AlphaZero和AlphaProof的思路，为安全协议分析工具Tamarin实现新的证明搜索方式。该框架通过无状态API将Tamarin转化为经典RL环境，并用蒙特卡洛树搜索结合神经网络启发式，从已完成子证明中学习。在16个案例研究中，该方法比Tamarin标准搜索找到更多自动证明，且生成的证明比标准及人工设计的启发式更短。该框架可直接用于辅助Tamarin用户，减少人工工作量，展示了RL方法在协议验证领域的潜力。