Can Proof Assistants Verify Multi-Agent Systems?
作者: Julian Alfredo Mendez, Timotheus Kampik
发布时间: 2025-03-11
来源: arxiv
研究方向: 多智能体系统（MAS）的工程与形式化验证
主要内容
本文研究了如何使用Soda语言来验证多智能体系统。Soda是一种支持函数式和面向对象编程的语言，可以编译为Scala（主流编程语言）和Lean（形式化验证工具）。通过这种方式，Soda可以用于实现MAS，并支持与主流软件生态系统的集成以及使用Lean进行形式化验证。
主要贡献
1. 提出了一种使用Soda语言设计、实现和验证MAS的方法。
2. 展示了如何将Soda代码编译为Scala，以便与主流编程生态系统集成。
3. 展示了如何将Soda代码编译为Lean，以便使用形式化验证工具进行验证。
4. 通过一个简单的交互协议验证示例，证明了该方法的可行性和有效性。
研究方法
1. 使用Soda语言设计MAS组件。
2. 将Soda代码编译为Scala和Lean。
3. 使用Lean进行形式化验证，包括定义和证明性质。
4. 通过实验评估系统的效率。
实验结果
实验结果表明，该系统能够以可接受的速度执行大量交易，并证明了其可行性。
未来工作
未来的工作将包括将该方法扩展到更复杂的MAS场景，提供更详细的关于使用证明辅助工具而非模型检查器进行MAS验证的分析，以及将该方法应用于现实世界问题，如确保复杂社会技术系统中的公平性属性。