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.
翻译:生成模型(尤其是大语言模型)能够产生流畅的输出,但缺乏可验证的保证。我们借鉴契约式设计与类型论原理,引入一个契约层来中介所有大语言模型调用。契约规定了输入输出的语义与类型要求,并结合概率性修正机制引导生成过程趋向合规。该层揭示了大语言模型的双重视角:既可作为语义解析器,也可视为概率性黑盒组件。契约满足具有概率特性,语义验证通过程序员在良类型数据结构上指定的条件进行操作性定义。更广泛而言,本研究提出:任何满足相同契约的两个智能体,就这些契约而言具有功能等价性。