Para abordar la falta de garantías verificables para la salida de los modelos de lenguaje a gran escala (LLM), este artículo propone una capa de contrato que aprovecha los principios de Diseño por Contrato (DbC) y la teoría de tipos. Esta capa de contrato media todas las invocaciones de LLM, especifica los requisitos semánticos y de tipo para las entradas y salidas, y proporciona correcciones probabilísticas para garantizar el cumplimiento. Presentamos el LLM como un analizador semántico de doble perspectiva y un componente probabilístico de caja negra, donde la satisfacción del contrato es probabilística y la verificación semántica se define operativamente mediante condiciones especificadas por el programador en estructuras de datos bien definidas. En términos más generales, argumentamos que dos agentes que satisfacen el mismo contrato son funcionalmente equivalentes con respecto a dicho contrato.
