Imagina que estás intentando enseñar a un artista muy creativo e imaginativo (una IA) cómo esculpir una estatua de un bloque de mármol utilizando un brazo robótico. El artista es excelente entendiendo tu descripción ("Haz un pájaro") y puede escribir las instrucciones para el robot. Sin embargo, este artista nunca ha visto realmente el taller. No sabe dónde están las abrazaderas pesadas que sujetan el mármol, ni el tamaño del brazo del robot. Podría escribir instrucciones que parecen perfectas en el papel, pero que harían que el robot chocara directamente contra una abrazadera, rompiendo la máquina.

Este artículo propone una solución a ese problema uniendo al artista creativo con un inspector de seguridad estricto y matemáticamente perfecto.

Así es como funciona su asociación, desglosada en pasos simples:

1. Los dos socios

El Artista (La IA): Este es un Modelo de Lenguaje Grande llamado GLLM, traído de trabajos anteriores. El GLLM es excelente tomando tu solicitud en lenguaje natural ("Escribe un pájaro") y transformándola en una lista de instrucciones robóticas (código G). Maneja la Generación Aumentada por Recuperación (RAG) para traer contexto sobre la máquina y la tarea, y verifica que el código sea sintáctica y semánticamente razonable. Lo que NO hace, y para lo cual nunca fue diseñado, es evitar que el robot se estrelle físicamente contra las cosas; no tiene un sistema de prevención de colisiones integrado.
El Inspector (El Motor Lógico): Este es un demostrador de Lógica de Separación que los autores trajeron de su propio trabajo anterior, específicamente del artículo Separation Logic for Verifying Physical Collisions of CNC Programs (arXiv:2605.10437), donde se introdujeron por primera vez el modelo de "Montículo Espacial" y el demostrador. El único trabajo del Inspector es detectar colisiones físicas: situaciones donde la herramienta y un obstáculo intentarían ocupar el mismo espacio al mismo tiempo. No es un revisor de código de propósito general; no verifica si el código es "incorrecto" en un sentido amplio; es puramente un detector de accidentes.

Lo que este artículo realmente contribuye es el cableado entre estas dos herramientas existentes: un bucle de retroalimentación neuro-simbólico en el que los hallazgos de colisión del Inspector se traducen en una guía estructurada para el Artista.

2. El "Arena Digital" (El Montículo Espacial)

Para que las matemáticas funcionen, el sistema convierte el taller físico en una gigantesca cuadrícula 3D de cubos diminutos (como una versión 3D de Minecraft).

Algunos cubos están marcados como "Mármol" (el material a cortar).
Algunos están marcados como "Abrazaderas" (obstáculos).
Algunos están marcados como "Aire Vacío" (espacio seguro).
La herramienta del robot también es una forma específica de cubos.

El Inspector trata el movimiento del robot como un juego de "silla musical" con estos cubos. Importante: el Inspector nunca observa realmente cómo se mueve el robot ni ejecuta una simulación geométrica. Lee el script de G-code directamente, línea por línea, y determina qué cubos necesitaría ocupar cada movimiento de la herramienta. La regla que aplica es simple: los cubos reclamados por la herramienta no deben estar ya reclamados por una abrazadera o cualquier otro obstáculo.

3. El Colchón de Seguridad (El "Abrigo Peludo")

Los robots no son perfectos. Podrían tambalearse ligeramente, o la herramienta podría doblarse un poco. Para tener esto en cuenta, el sistema no verifica solo el tamaño exacto de la herramienta. Le da a la herramienta un "abrigo peludo" (un margen de seguridad matemático) a su alrededor.

Si la herramienta mide 5 mm de ancho, el sistema finge que mide 7 mm para estar seguro.
El Inspector verifica si esta "herramienta peluda" choca con algo. Si lo hace, el movimiento está prohibido.

4. La "Carrera de Datos" (La Alarma de Colisión)

En informática, una "carrera de datos" ocurre cuando dos programas intentan usar la misma memoria al mismo tiempo. Los autores llaman a una colisión física una "Carrera de Datos Espacial".

Cuando el Artista escribe un movimiento que causaría una colisión:

El Inspector examina la cuadrícula 3D basada en el código.
Ve los "Cubos de la Herramienta" superpuestos con los "Cubos de la Abrazadera".
La prueba matemática falla. El Inspector grita: "¡ALTO! ¡Estás intentando ocupar el mismo espacio!"

5. El Bucle de Retroalimentación (La Nota "No Vayas Allí")

En el pasado, si una IA cometía un error, quizás solo le decías: "Inténtalo de nuevo", y esperabas que tuviera suerte. Eso es ineficiente.

Este sistema es más inteligente. Cuando el Inspector encuentra una colisión, no solo dice "No". Señala la ubicación exacta de la colisión y dibuja una caja pequeña y precisa a su alrededor.

El Mensaje: "Intentaste moverte a las coordenadas X, Y, Z. Hay una abrazadera dentro de esta caja específica. No entres en esta caja."
La Corrección: Esta nota se envía de vuelta al Artista. El Artista lee la nota, se da cuenta del error y reescribe las instrucciones para ir alrededor de la caja.

6. El Resultado: "Correcto por Construcción"

Siguen haciendo este bucle: el Artista escribe, el Inspector verifica, el Inspector señala la colisión, el Artista lo corrige, hasta que el Inspector puede probar matemáticamente que la herramienta es altamente improbable que colisione con nada en el espacio de trabajo actual tal como fue descrito al demostrador.

Como el sistema solo se detiene cuando la prueba matemática es exitosa, el conjunto final de instrucciones es "Correcto por Construcción" para ese espacio de trabajo y esa descripción de obstáculos. La garantía es que, bajo el modelo espacial que el Inspector recibió, la trayectoria de la herramienta no produce una colisión física. (Ninguna prueba puede descartar colisiones causadas por cambios en el espacio de trabajo después de que se genera el código — fixtures movidos, nuevo material, un operador dejando una herramienta dentro de la celda —, por lo que esta es una garantía condicional al espacio de trabajo, no una incondicional).

Resumen

El artículo describe una forma de hacer seguras las instrucciones robóticas generadas por IA emparejando una IA creativa con un verificador de seguridad estricto basado en matemáticas. El verificador convierte el mundo físico en una cuadrícula, verifica superposiciones (colisiones) leyendo directamente el código, y envía advertencias precisas de "no entrar" de vuelta a la IA hasta que las instrucciones estén matemáticamente verificadas como libres de colisiones para el espacio de trabajo tal como fue descrito al demostrador.

Resumen Técnico: Generación de Código G Correcta por Construcción mediante Lógica de Separación

Enunciado del Problema

La integración de Modelos de Lenguaje Grandes (LLM) en el mecanizado de Control Numérico Computarizado (CNC) ofrece el potencial de automatizar la síntesis de instrucciones de máquina de bajo nivel (código G) a partir de lenguaje natural. Sin embargo, la implementación de modelos generativos directamente en sistemas ciberfísicos introduce desafíos críticos de seguridad. Aunque LLMs como el marco GLLM pueden generar código sintácticamente correcto que se alinea semánticamente con las geometrías objetivo, carecen de conciencia espacial inherente y garantías de seguridad deterministas.

Una limitación principal es la "alucinación" de trayectorias de herramienta que asumen espacios de trabajo infinitos y libres de obstáculos. Incluso trayectorias de herramienta lógicamente sólidas pueden resultar en colisiones físicas debido a variables ambientales dinámicas (por ejemplo, sujeciones actualizadas, dimensiones de la materia prima) y realidades mecánicas (por ejemplo, retraso del servomotor, excentricidad del husillo). Los mecanismos de seguridad tradicionales, como simulaciones geométricas o pruebas de margen de caso peor, son efectivos para la visualización pero carecen de las pruebas simbólicas y matemáticas requeridas para garantizar la seguridad frente a movimientos físicos continuos y colisiones de casos extremos. En consecuencia, existe la necesidad de un mecanismo de verificación independiente y determinista que pueda garantizar matemáticamente la disyunción espacial antes de la ejecución del código.

Metodología

Nota de Atribución: El formalismo del "Montón Espacial" (Spatial Heap) y el Probador de Lógica de Separación (SL Prover) utilizados aquí fueron introducidos en el trabajo previo de los autores (Lee, arXiv:2605.10437). El presente artículo integra ese probador existente con el GLLM en un pipeline neuro-simbólico de bucle cerrado.

El artículo propone un marco neuro-simbólico que une la generación probabilística de IA con la verificación formal determinista. La arquitectura consiste en un pipeline unidireccional e iterativo que involucra dos agentes principales: un Generador (GLLM) y un Verificador (Probador de Lógica de Separación).

1. La Arquitectura Generador-Verificador

Generador (GLLM): Utiliza un LLM ajustado (por ejemplo, StarCoder-3B) potenciado con Generación Aumentada por Recuperación (RAG). El sistema RAG inyecta contexto estático (límites cinemáticos de la máquina, topografía del espacio de trabajo, geometría de la herramienta) y márgenes de seguridad dinámicos en el prompt. Es crucial destacar que el GLLM es un marco publicado previamente cuyo rol aquí permanece inalterado: se encarga de la generación de código G asistida por RAG y la corrección semántica/sintáctica. El GLLM no realiza evitación de colisiones; la prevención de colisiones nunca formó parte de su alcance.
Verificador (Probador SL): Un probador de Lógica de Separación (SL) específico del dominio, reutilizado directamente del trabajo previo del autor. Este trata el espacio de trabajo físico del CNC como un "Montón Espacial" discreto. En este modelo, la ocupación física se gestiona como un recurso lógico, donde las coordenadas en una red entera 3D discreta ( $\mathbb{Z}^3$ ) se mapean a estados como Herramienta, Entorno, Materia Prima o Vacío.

2. El Bucle Neuro-Simbólico

El marco opera a través de un ciclo iterativo continuo:

Inicialización y RAG: Se procesan la intención del usuario y los límites del espacio de trabajo. El sistema RAG precalcula los límites ambientales expandidos utilizando un margen de seguridad ( $\epsilon$ ) e inyecta estas restricciones en el contexto del LLM.
Generación y Discretización (El Analizador): El LLM sintetiza una secuencia de código G borrador. Un Analizador intermedio traduce estos comandos cinemáticos continuos (punto flotante $\mathbb{R}^3$ ) a lógica espacial discreta ( $\mathbb{Z}^3$ ). Este proceso aplica dilataciones de suma de Minkowski a la geometría de la herramienta para encapsular incertidumbres físicas (por ejemplo, retraso del servomotor), convirtiendo la trayectoria en un conjunto finito de solicitudes de recursos espaciales. La discretización produce un conjunto finito de solicitudes de recursos espaciales directamente desde el código G; el Probador SL luego verifica la separación contra el entorno sobre estas reclamaciones simbólicas. No se realiza ninguna simulación geométrica, renderizado de volumen barrido o reproducción cinemática en ninguna etapa.
Verificación Formal: El Probador SL evalúa la trayectoria discretizada utilizando Triples de Lógica de Separación $\{P\}C\{Q\}$ ${P} C {Q}$ . Verifica la Conjunción Separadora ( $*$ $*$ ), que afirma que el volumen barrido por la herramienta es estrictamente disjunto de los obstáculos ambientales.
- Éxito: Si la conjunción se mantiene, el movimiento está matemáticamente probado como seguro.
- Fallo (Carrera de Datos Espacial): Si el volumen de la herramienta interseca con el entorno, la conjunción separadora falla. Esta contradicción lógica se identifica específicamente como una Carrera de Datos Espacial (Spatial Data Race), que es la formalización matemática de una colisión física. El probador no verifica errores lógicos generales; su único objetivo es detectar colisiones físicas.
Retroalimentación y Refinamiento: Ante un fallo, el sistema no rechaza simplemente el código. En su lugar, condensa los vóxeles conflictivos en una caja delimitadora mínima y alineada con los ejes ( $B_{conflict}$ ). Este fallo matemático se traduce en una señal de error estructurada en lenguaje natural que contiene las coordenadas específicas de la colisión y una directiva para evitar el volumen restringido.
Autocorrección: La señal de error se adjunta a la ventana de contexto del LLM, guiando al modelo para refinar el segmento específico de la trayectoria de la herramienta. El bucle se repite hasta lograr una prueba formal de disyunción espacial.

Contribuciones Clave

El artículo describe tres contribuciones principales al campo de la IA neuro-simbólica y la fabricación:

Arquitectura Neuro-Simbólica Generador-Verificador: Un marco bipartito que desacopla la cinemática física continua de la evaluación lógica espacial. El LLM actúa como un generador creativo, mientras que el Probador SL actúa como un verificador implacable y determinista, asegurando que la salida sea correcta por construcción.
Traducción Simbólica a Neural mediante Carreras de Datos Espaciales: Un mecanismo formal para comunicar contradicciones lógicas al motor neuronal. Al redefinir las colisiones físicas como violaciones de la conjunción separadora (denominadas formalmente Carreras de Datos Espaciales), el sistema traduce intersecciones geométricas en directivas estructuradas y legibles por máquina (cajas delimitadoras) que restringen el proceso generativo del LLM.
Autocorrección Determinista y Automatizada: A diferencia de los enfoques empíricos que dependen de la validación humana en el bucle o de métricas de similitud de trayectorias, este marco introduce un bucle de retroalimentación totalmente automatizado. El Probador SL proporciona una retroalimentación espacial precisa, con cero falsos positivos, permitiendo que el LLM refine autónomamente las trayectorias hasta establecer una prueba formal de seguridad.

Resultados y Afirmaciones

El artículo establece la viabilidad teórica y el diseño arquitectónico de este enfoque neuro-simbólico. Afirma que al integrar el marco GLLM con el modelo de Montón Espacial:

El sistema traduce con éxito las colisiones físicas en contradicciones lógicas (Carreras de Datos Espaciales) que pueden ser verificadas formalmente.
El uso de sumas de Minkowski en la fase de discretización permite al sistema garantizar matemáticamente los márgenes de seguridad frente a incertidumbres mecánicas sin complicar la lógica discreta del probador.
El mecanismo de retroalimentación restringe efectivamente el espacio de búsqueda probabilístico del LLM, evitando alucinaciones repetidas y guiando al modelo hacia trayectorias libres de colisiones verificadas matemáticamente.

Los autores señalan que, aunque la arquitectura está establecida, la validación experimental exhaustiva (por ejemplo, comparación con herramientas CAM tradicionales como VERICUT en secuencias industriales a gran escala) sigue siendo un esfuerzo en curso para trabajos futuros.

Significancia

La significancia de este trabajo radica en su cambio de seguridad empírica a seguridad formal en la fabricación impulsada por IA. Al conceptualizar el espacio de trabajo físico como un recurso lógico gestionado, el marco permite la aplicación de pruebas matemáticas rigurosas a sistemas ciberfísicos. Este enfoque aborda la brecha crítica de "intención" entre las instrucciones humanas y la ejecución de la máquina, ofreciendo un camino escalable hacia la fabricación CNC totalmente autónoma y libre de colisiones. Demuestra que la IA generativa puede implementarse de forma segura en entornos físicos de alto riesgo cuando se combina con una capa de verificación simbólica determinista que trata la seguridad como una necesidad lógica en lugar de una probabilidad estadística. Es importante notar que la garantía de seguridad formal aplica al espacio de trabajo tal como se modela en el Montón Espacial en el momento de la generación del código, y no se extiende a cambios ambientales posteriores a la generación.

Correct-by-Construction G-Code Generation: A Neuro-Symbolic Approach via Separation Logic