매우 창의적이고 상상력이 풍부한 예술가 (AI) 가 로봇 팔을 사용하여 대리석 덩어리에서 조각상을 새기는 방법을 가르치려 한다고 상상해 보세요. 이 예술가는 당신의 설명 ("새를 새겨라") 을 이해하는 데 뛰어나고 로봇을 위한 지시 사항을 작성할 수 있습니다. 하지만 이 예술가는 실제로 작업장을 본 적이 없습니다. 대리석을 고정하는 무거운 클램프가 어디에 있는지, 또는 로봇 팔의 크기가 얼마나 되는지 알지 못합니다. 결과적으로 종이에 보면 완벽해 보이지만 로봇이 클램프에 정면으로 충돌하여 기계를 파손시키는 지시 사항을 작성할 수도 있습니다.

이 논문은 바로 그 문제를 해결하기 위해 창의적인 예술가와 엄격하며 수학적으로 완벽한 안전 검사관을 팀으로 구성하는 방안을 제안합니다.

다음은 그들의 파트너십이 작동하는 방식을 간단한 단계로 나눈 것입니다:

1. 두 명의 파트너

예술가 (AI): 이는 기존 연구에서 개발된 대규모 언어 모델 (GLLM) 입니다. GLLM 은 자연어 요청 ("새를 새겨라") 을 로봇 지시 사항 (G 코드) 목록으로 변환하는 데 탁월합니다. 작업과 기계에 대한 맥락을 끌어오는 RAG(검색 증강 생성) 기술과 문법적·의미적 검사를 처리합니다. 하지만 GLLM 은 로봇이 물리적으로 무엇에 부딪히지 않도록 하는 '충돌 회피' 기능은 전혀 포함하지 않았으며, 처음부터 그런 목적으로 설계된 것도 아닙니다.
검사관 (안전 증명기): 이는 저자들이 이전 논문 (arXiv:2605.10437, "Separation Logic for Verifying Physical Collisions of CNC Programs") 에서 소개한 '분리 논리 (Separation Logic)' 기반의 증명기입니다. 여기서 '공간적 힙 (Spatial Heap)' 모델과 증명기가 처음 등장했습니다. 검사관의 유일한 임무는 물리적 충돌, 즉 공구와 장애물이 동시에 같은 공간을 차지하려 할 때 발생하는 '충돌'을 감지하는 것입니다. 이는 일반적인 코드 품질을 검토하는 것이 아니라, 오직 '충돌 (Crash)'만 탐지하는 전문 감지기입니다.

이 논문이 실제로 기여하는 바는 이 두 가지 기존 도구를 연결하는 것입니다. 즉, 검사관이 발견한 충돌 정보를 구조화된 가이드로 변환하여 예술가에게 되돌려주는 신경 - 심볼릭 (neuro-symbolic) 피드백 루프를 구축한 것입니다.

2. "디지털 모래상자" (공간 힙, Spatial Heap)

수학이 작동하도록 하기 위해 시스템은 물리적 작업장을 작은 정육면체들의 거대한 3D 격자 (마인크래프트의 3D 버전과 유사) 로 변환합니다.

일부 정육면체는 잘려야 할 재료인 **"대리석"**으로 표시됩니다.
일부는 장애물인 **"클램프"**로 표시됩니다.
일부는 안전한 공간인 **"빈 공기"**로 표시됩니다.
로봇의 공구 또한 특정 모양의 정육면체로 표현됩니다.

중요한 점은 검사관이 로봇이 움직이는 것을 실제로 지켜보거나 기하학적 시뮬레이션을 실행하지 않는다는 것입니다. 대신 검사관은 G 코드 스크립트를 직접 한 줄씩 읽어갑니다. 각 이동 지시가 어떤 정육면체들을 점유해야 하는지 계산하여, 공구가 점유하려는 정육면체가 이미 클램프나 다른 장애물에 의해 점유되어 있는지 확인합니다. 규칙은 간단합니다: 공구가 주장하는 정육면체는 클램프가 주장하는 정육면체와 겹쳐서는 안 됩니다.

3. 안전 버퍼 ("푹신한 코트")

로봇은 완벽하지 않습니다. 약간 흔들리거나 공구가 아주 조금 구부러질 수도 있습니다. 이를 고려하기 위해 시스템은 공구의 정확한 크기만 확인하지 않습니다. 공구 주변에 "푹신한 코트" (수학적 안전 마진) 를 입힙니다.

공구의 폭이 5mm 라면, 안전을 위해 시스템은 이를 7mm 폭인 것처럼 취급합니다.
검사관은 이 "푹신한 공구"가 무엇에 닿는지 확인합니다. 닿는다면 그 이동은 금지됩니다.

4. "데이터 레이스" (충돌 경보)

컴퓨터 과학에서 "데이터 레이스"는 두 개의 프로그램이 동시에 같은 메모리를 사용하려 할 때 발생합니다. 저자들은 물리적 충돌을 **"공간적 데이터 레이스 (Spatial Data Race)"**라고 부릅니다.

예술가가 충돌을 일으킬 이동 지시를 작성할 때:

검사관은 G 코드를 분석하여 3D 격자를 살펴봅니다.
"공구 정육면체"가 "클램프 정육면체"와 겹치는 것을 발견합니다.
수학 증명이 실패합니다. 검사관이 "STOP! 같은 공간을 차지하려 하고 있습니다!"라고 외칩니다.

5. 피드백 루프 ("거기 가지 마" 메모)

과거에 AI 가 실수를 하면, 단순히 "다시 시도해 보라"고 말하고 운을 기대했을 것입니다. 이는 비효율적입니다.

이 시스템은 더 똑똑합니다. 검사관이 충돌을 발견했을 때 단순히 "아니오"라고 말하지 않습니다. 충돌의 정확한 위치를 파악하고 그 주위에 작고 정밀한 상자를 그립니다.

메시지: "당신은 X, Y, Z 좌표로 이동하려 했습니다. 이 특정 상자 안에 클램프가 있습니다. 이 상자 안으로 들어가지 마십시오."
수정: 이 메모는 예술가에게 다시 전송됩니다. 예술가는 메모를 읽고 실수를 깨닫고, 그 상자를 우회하도록 지시 사항을 다시 작성합니다.

6. 결과: "구현 시 정합성 (Correct-by-Construction)"

예술가가 작성하고, 검사관이 확인하고, 검사관이 충돌을 지적하며, 예술가가 수정하는 이 루프를 검사관이 현재 작업 공간과 프로버에게 제공된 장애물 설명에 따라 공구가 충돌할 가능성이 매우 낮음을 수학적으로 증명할 때까지 계속 반복합니다.

시스템은 수학 증명이 통과될 때까지 멈추지 않기 때문에, 최종 지시 사항 세트는 해당 작업 공간과 장애물 묘사에 대해 **"구현 시 정합성 (Correct-by-Construction)"**을 갖게 됩니다. 이는 코드가 단순히 테스트를 통과했기 때문이 아니라, 그 설계 자체가 주어진 공간 모델 내에서 안전함을 의미합니다.

이 보장은 **작업 공간 조건부 (workspace-conditional)**입니다. 즉, 코드 생성 후 작업 공간이 변경되지 않는 한 (예: 고정 장치 이동, 새로운 원료 추가, 작업자가 공구실을 방치하는 등) 충돌이 발생하지 않음을 보장합니다. 코드 생성 이후 작업 공간이 변하면 이 보장은 무효화될 수 있으므로, 이는 무조건적인 보장이 아니라 주어진 공간 모델에 대한 검증된 보장입니다.

요약

이 논문은 창의적인 AI 와 엄격한 수학 기반 안전 검사관을 짝지어 AI 가 생성한 로봇 지시 사항을 안전하게 만드는 방법을 설명합니다. 검사관은 물리적 세계를 격자로 변환하고 겹침 (충돌) 을 확인한 뒤, 지시 사항이 현재 작업 공간 모델에 대해 수학적으로 충돌이 없음을 보장될 때까지 AI 에게 정밀한 "진입 금지" 경고를 반복적으로 전송합니다.

기술 요약: 분리 논리를 통한 Correct-by-Construction G-코드 생성

문제 제기

대형 언어 모델 (LLM) 을 컴퓨터 수치 제어 (CNC) 가공에 통합하면 자연어에서 저수준 기계 지시어 (G-코드) 합성을 자동화할 수 있는 잠재력이 있습니다. 그러나 생성 모델을 사이버 - 물리 시스템에 직접 배포하는 것은 치명적인 안전 문제를 야기합니다. GLLM 프레임워크와 같은 LLM 은 목표 기하학적 형상과 의미론적으로 일치하는 문법적으로 올바른 코드를 생성할 수 있지만, 고유한 공간 인식과 결정론적 안전 보장이 부족합니다.

주요 한계점은 무한하고 장애물이 없는 작업 공간을 전제로 하는 도구 경로의 "할루시네이션"입니다. 논리적으로 타당한 도구 경로조차도 동적 환경 변수 (예: 업데이트된 고정구, 재고 치수) 와 기계적 현실 (예: 서보 지연, 스핀들 런아웃) 로 인해 물리적 충돌을 초래할 수 있습니다. 기하학적 시뮬레이션이나 최악의 경우 마진 테스트와 같은 전통적인 안전 메커니즘은 시각화에는 효과적이지만, 연속적인 물리적 이동과 극단적인 경우의 충돌에 대한 안전을 보장하는 데 필요한 기호적, 수학적 증명이 부족합니다. 따라서 코드 실행 전에 공간적 불교합성을 수학적으로 보장할 수 있는 독립적이고 결정론적인 검증 메커니즘이 필요합니다.

방법론

본 논문은 확률적 AI 생성과 결정론적 형식 검증을 연결하는 뉴로 - 심볼릭 프레임워크를 제안합니다. 이 아키텍처는 생성기 (LLM) 와 검증기 (분리 논리 증명기) 라는 두 가지 주요 에이전트가 관여하는 단방향 반복 파이프라인으로 구성됩니다.

참고: 본 논문에서 사용되는 공간 힙 (Spatial Heap) 형식주의와 SL 증명기는 저자의 이전 연구 (Lee, arXiv:2605.10437) 에서 소개된 기존 작업입니다. 본 논문은 기존 증명기를 GLLM 과 통합하여 폐쇄 루프 뉴로 - 심볼릭 파이프라인을 구축하는 데 주된 기여를 합니다.

1. 생성기 - 검증기 아키텍처

생성기 (GLLM): 검색 증강 생성 (RAG) 으로 강화된 파인튜닝된 LLM(예: StarCoder-3B) 을 사용합니다. RAG 시스템은 프롬프트에 정적 컨텍스트 (기계 운동학적 한계, 작업 공간 지형, 도구 기하학) 와 동적 안전 마진을 주입합니다. GLLM 은 의미론적 및 구문론적 정확성을 담당하지만, 충돌 회피는 그 범위에 포함되지 않으며 본 논문 이전에도 수행된 바 없습니다.
검증기 (SL 증명기): 물리적 CNC 작업 공간을 이산적인 **"공간 힙 (Spatial Heap)"**으로 취급하는 도메인 특화 분리 논리 (SL) 증명기입니다. 이 모델에서 물리적 점유는 논리적 자원으로 관리되며, 이산 3 차원 정수 격자 ( $\mathbb{Z}^3$ ) 의 좌표는 Tool(도구), Environment(환경), Stock(재고), 또는 Empty(비어있음) 와 같은 상태로 매핑됩니다.

2. 뉴로 - 심볼릭 루프

이 프레임워크는 지속적인 반복 사이클을 통해 작동합니다:

초기화 및 RAG: 사용자 의도와 작업 공간 경계가 처리됩니다. RAG 시스템은 안전 마진 ( $\epsilon$ ) 을 사용하여 확장된 환경 경계를 사전 계산하고, 이러한 제약을 LLM 의 컨텍스트에 주입합니다.
생성 및 이산화 (파서): LLM 이 초안 G-코드 시퀀스를 합성합니다. 중간 파서가 연속적인 운동학 명령 (부동 소수점 $\mathbb{R}^3$ ) 을 이산 공간 논리 ( $\mathbb{Z}^3$ ) 로 변환합니다. 이 과정은 물리적 불확실성 (예: 서보 지연) 을 포괄하기 위해 도구 기하학에 **민코프스키 합 팽창 (Minkowski sum dilations)**을 적용하여 궤적을 유한한 공간 자원 요청 집합으로 변환합니다. 이 이산화 단계는 G-코드에서 직접 유한한 공간 자원 요청 집합을 생성하며, SL 증명기는 이러한 기호적 주장에 대해 환경과의 분리성을 검증합니다. 이 파이프라인에서는 기하학적 시뮬레이션, Swept-volume 렌더링, 또는 운동학 재생이 수행되지 않습니다.
형식 검증: SL 증명기는 분리 논리 삼항식 (Separation Logic Triples) $\{P\}C\{Q\}$ ${P} C {Q}$ 을 사용하여 이산화된 경로를 평가합니다. 도구의 쓸고 지나간 부피가 환경 장애물과 엄격하게 불교합임을 주장하는 분리 합 (Separating Conjunction)( $*$ $*$ ) 을 확인합니다.
- 성공: 만약 분리 합이 성립하면, 해당 이동은 수학적으로 안전함이 증명됩니다.
- 실패 (공간 데이터 레이스): 도구 부피가 환경과 교차하면 분리 합이 실패합니다. 이러한 논리적 모순은 물리적 충돌을 수학적으로 형식화한 **공간 데이터 레이스 (Spatial Data Race)**로 식별됩니다.
피드백 및 정제: 실패 시 시스템은 단순히 코드를 거부하지 않습니다. 대신 충돌하는 보크셀들을 최소의 축 정렬 바운딩 박스 (bounding box)( $B_{conflict}$ ) 로 압축합니다. 이 수학적 실패는 충돌의 특정 좌표와 제한된 부피를 우회하라는 지시를 포함한 구조화된 자연어 오류 신호로 변환됩니다.
자기 수정: 오류 신호가 LLM 의 컨텍스트 창에 추가되어 모델이 도구 경로의 특정 구간을 정제하도록 안내합니다. 공간적 불교합성에 대한 형식적 증명이 달성될 때까지 루프가 반복됩니다.

주요 기여

본 논문은 뉴로 - 심볼릭 AI 및 제조 분야에서 세 가지 주요 기여를 제시합니다:

생성기 - 검증기 뉴로 - 심볼릭 아키텍처: 연속적인 물리적 운동학을 논리적 공간 평가와 분리하는 이분적 프레임워크입니다. LLM 은 창의적 생성기로 작용하고, SL 증명기는 무너뜨릴 수 없는 결정론적 검증기로 작용하여 출력이 **구현 시 정오편 (correct-by-construction)**되도록 보장합니다.
공간 데이터 레이스를 통한 심볼릭 - 신경 변환: 논리적 모순을 신경 엔진에 전달하는 형식적 메커니즘입니다. 물리적 충돌을 분리 합 위반 (공간 데이터 레이스) 으로 재정의함으로써, 기하학적 교차점을 LLM 의 생성 과정을 제약하는 구조화된 기계 가독성 지시 (바운딩 박스) 로 변환합니다. 여기서 "공간 데이터 레이스"는 이 프레임워크 내 물리적 충돌의 공식적 명칭입니다.
결정론적 자동 자기 수정: 인간 - 루프 검증이나 경로 유사성 지표에 의존하는 경험적 접근과 달리, 이 프레임워크는 완전히 자동화된 피드백 루프를 도입합니다. SL 증명기는 정확한 거짓 양성 제로 (zero-false-positive) 공간 피드백을 제공하여, LLM 이 형식적 안전 증명이 수립될 때까지 궤적을 자율적으로 정제할 수 있게 합니다.

결과 및 주장

본 논문은 이 뉴로 - 심볼릭 접근법의 이론적 실현 가능성과 아키텍처 설계를 확립합니다. GLLM 프레임워크를 공간 힙 모델과 통합함으로써 다음과 같은 주장을 합니다:

시스템은 물리적 충돌을 형식적으로 검증 가능한 논리적 모순으로 성공적으로 변환합니다.
이산화 단계에서 민코프스키 합을 사용하면 증명기의 이산 논리를 복잡하게 하지 않으면서도 기계적 불확실성에 대한 안전 마진을 수학적으로 보장할 수 있습니다.
피드백 메커니즘은 LLM 의 확률적 검색 공간을 효과적으로 제한하여 반복적인 할루시네이션을 방지하고, 수학적으로 검증된 충돌 없는 도구 경로로 모델을 유도합니다.

저자들은 아키텍처가 확립되었지만, 대규모 산업 시퀀스에 대한 VERICUT 과 같은 전통적인 CAM 도구에 대한 벤치마킹과 같은 포괄적인 실험적 검증은 향후 작업으로 계속 진행 중임을 지적합니다.

의의

이 작업의 의의는 AI 주도 제조 분야에서 경험적 안전에서 형식적 안전으로의 전환에 있습니다. 물리적 작업 공간을 관리되는 논리적 자원으로 개념화함으로써, 이 프레임워크는 사이버 - 물리 시스템에 엄격한 수학적 증명을 적용할 수 있게 합니다. 이 형식적 안전 보장은 G-코드 생성 시점에 공간 힙 모델로 정의된 작업 공간 내에서 유효하며, 코드 생성 이후의 환경 변화에는 적용되지 않습니다. 이 접근법은 인간 지시와 기계 실행 사이의 중요한 "의도 격차"를 해결하여, 완전히 자율적이고 충돌이 없는 CNC 제조를 향한 확장 가능한 경로를 제공합니다. 이는 생성형 AI 가 안전을 통계적 확률이 아닌 논리적 필연성으로 취급하는 결정론적 심볼릭 검증 계층과 결합될 때 고위험 물리적 환경에 안전하게 배포될 수 있음을 보여줍니다.

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