给大模型加契约层，让输出可验证、可信赖。
A DbC Inspired Neurosymbolic Layer for Trustworthy Agent Design
- 用契约机制约束大模型输入输出的语义和类型
- 通过概率修复使生成结果更符合契约要求
- 适合需要高可靠性智能体的系统设计者
生成模型（尤其是大语言模型）虽能生成流畅文本，但缺乏可验证的保证。本文借鉴设计契约（DbC）与类型理论思想，引入一个契约层，中介所有大模型调用。契约规定输入输出的语义与类型要求，并结合概率修复机制引导生成向合规方向演进。该层揭示了大模型作为语义解析器与概率黑箱的双重属性。契约满足为概率性，语义验证通过程序员定义的、在良类型数据结构上的条件实现。更广泛地，本工作提出：任何满足相同契约的两个智能体，在这些契约下具有功能等价性。
原文摘要 · Abstract (English)
Generative models, particularly Large Language Models (LLMs), produce fluent outputs yet lack verifiable guarantees. We adapt Design by Contract (DbC) and type-theoretic principles to introduce a contract layer that mediates every LLM call. Contracts stipulate semantic and type requirements on inputs and outputs, coupled with probabilistic remediation to steer generation toward compliance. The layer exposes the dual view of LLMs as semantic parsers and probabilistic black-box components. Contract satisfaction is probabilistic and semantic validation is operationally defined through programmer-specified conditions on well-typed data structures. More broadly, this work postulates that any two agents satisfying the same contracts are \emph{functionally equivalent} with respect to those contracts.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。