提出可安全扩展的智能体通信语言，防止语言膨胀失控。
CBCL: Safe Self-Extending Agent Communication
- 用确定性上下文无关语言约束通信内容与扩展
- 三重安全机制确保资源不超限、词汇不丢失
- 适合需要可验证通信的自主系统开发
智能体通信语言（ACL）使异构智能体能在多领域共享知识并协同工作。这种多样性要求语言具备可扩展性，但高表达力的扩展机制可能使输入语言超出可有效验证的复杂度类别。本文提出CBCL（通用商业通信语言），将所有消息，包括运行时语言扩展，均限制在确定性上下文无关语言（DCFL）类中。CBCL允许智能体以第一类消息定义、传输和采用特定领域的“方言”扩展；三个安全不变量（R1–R3）在Lean 4中机器验证，并在Rust参考实现中强制执行，防止无限扩展、应用声明的资源限制并保持核心词汇完整。我们在Lean 4中形式化语言及其安全属性，使用属性测试和差分测试实现Rust参考解析器与方言引擎，并提取出经验证的解析器二进制文件。结果表明，同像协议设计（即扩展定义与普通消息使用相同表示）可以实现可证明的安全性。随着自主智能体不断扩展自身通信能力，对它们能表达的内容进行形式化边界控制，是实现可控监管的前提。
原文摘要 · Abstract (English)
Agent communication languages (ACLs) enable heterogeneous agents to share knowledge and coordinate across diverse domains. This diversity demands extensibility, but expressive extension mechanisms can push the input language beyond the complexity classes where full validation is tractable. We present CBCL (Common Business Communication Language), an agent communication language that constrains all messages, including runtime language extensions, to the deterministic context-free language (DCFL) class. CBCL allows agents to define, transmit, and adopt domain-specific "dialect" extensions as first-class messages; three safety invariants (R1--R3), machine-checked in Lean 4 and enforced in a Rust reference implementation, prevent unbounded expansion, applying declared resource limits, and preserving core vocabulary. We formalize the language and its safety properties in Lean 4, implement a reference parser and dialect engine in Rust with property-based and differential tests, and extract a verified parser binary. Our results demonstrate that homoiconic protocol design, where extension definitions share the same representation as ordinary messages, can be made provably safe. As autonomous agents increasingly extend their own communication capabilities, formally bounding what they can express to each other is a precondition for oversight.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。