Para abordar la falta de verificabilidad de la salida de los modelos de lenguaje a gran escala (LLM), este artículo propone una capa de contrato que aplica principios de diseño por contrato (DbC) y 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 el cumplimiento. Esto presenta al LLM como un punto de vista dual: un analizador semántico y un componente probabilístico de caja negra. El cumplimiento del contrato es probabilístico, y la verificación semántica se define operativamente mediante condiciones especificadas por el programador en estructuras de datos bien definidas. Además, este artículo argumenta que dos agentes que satisfacen el mismo contrato son funcionalmente equivalentes para dicho contrato.
