用Soda语言让多智能体系统既能运行又能形式化验证
Can Proof Assistants Verify Multi-Agent Systems?
- Soda是支持编译到Scala和Lean的高阶编程语言
- 能实现可集成到主流生态的多智能体系统
- 适合需要形式化验证的可信系统开发者
本文提出Soda语言，用于验证多智能体系统。Soda是一种高级函数式与面向对象语言，支持将其代码编译为强静态类型语言Scala，以及证明助手Lean。借助这一能力，Soda可构建多智能体系统或其部分组件，既可融入主流软件生态，又可通过先进工具进行形式化验证。文中简要介绍了Soda及其互操作性，并演示了如何设计与验证交互协议。过程中也指出了实际应用中的挑战。
原文摘要 · Abstract (English)
This paper presents the Soda language for verifying multi-agent systems. Soda is a high-level functional and object-oriented language that supports the compilation of its code not only to Scala, a strongly statically typed high-level programming language, but also to Lean, a proof assistant and programming language. Given these capabilities, Soda can implement multi-agent systems, or parts thereof, that can then be integrated into a mainstream software ecosystem on the one hand and formally verified with state-of-the-art tools on the other hand. We provide a brief and informal introduction to Soda and the aforementioned interoperability capabilities, as well as a simple demonstration of how interaction protocols can be designed and verified with Soda. In the course of the demonstration, we highlight challenges with respect to real-world applicability.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。