기술 요약: 선언적 결정론적-확률적 구성을 통한 워크플로 오케스트레이션

1. 문제점: 파편화와 두 모드 간의 격차

현재의 LLM 기반 워크플로 시스템은 근본적인 파편화 문제를 겪고 있다. 실무자들은 단순한 자기 개선(self-refining) 작업을 수행하기 위해 80~150줄에 달하는 명령형 "글루 코드(glue code)"를 작성해야 하며, 이 과정에서 프롬프트 엔지니어링, Python 오케스트레이션, API 관리를 아우르는 이질적인 기술들을 숙달해야 한다. 기존 프레임워크(예: LangGraph, AutoGen, CrewAI)는 오직 **확률적 모드(probabilistic mode)**로만 작동하며, 근사치만을 생성할 뿐 재현 불가능한 출력을 내놓는다. 반면, 심볼릭 도구(SymPy, SageMath, Lean)는 **결정론적 모드(deterministic mode)**로 작동하여 정확하고 기계적으로 검증 가능한 결과를 생성한다.

본 논문은 "두 모드 간의 격차(two-mode gap)"를 식별한다. 즉, 기존의 어떤 워크플로 언어도 단일 명세 내에서 "이 단계를 근사적으로 계산하라"와 "이 단계를 정확하게 계산하라"를 동시에 선언할 수 없다. 실제 에이전트 작업(예: 숙제 도우미)은 확률적 계획 및 서사와 결정론적 대수 실행 및 검증이라는 두 가지 모두를 필요로 한다. 현재 이러한 모드들을 조정하려면 수동 상태 관리와 애플리케이션 특화 코드가 경계 영역을 연결해야 하며, 이는 표현력의 한계를 만들고 도메인 전문가의 진입 장벽을 높인다.

2. 방법론: SPL 언어 및 아키텍처

저자들은 이러한 계산 모드를 통합하기 위해 설계된 선언적 언어인 **SPL(Structured Prompt Language)**을 제시한다. SPL은 다섯 가지 설계 원칙을 따른다:

1. 선언적 구성 (Declarative Composition): 프로그래머는 각 단계가 무엇을 계산하는지와 그 모드를 지정할 뿐, 그것이 어떻게 실행되는지는 명시하지 않는다.
2. 동등한 기본 단위 (Co-equal Primitives): 이 언어는 확률적(System 1) 모드와 결정론적(System 2) 모드를 동등한 일급 시민(first-class citizens)으로 취급한다.
3. 공유 변수 공간 (Shared Variable Space): 통합된 @variable 네임스페이스를 통해 수동 마샬링 없이 모드 간의 원활한 데이터 흐름을 허용한다.
4. DODA (Design Once, Deploy Anywhere): .spl 명세는 불변하며, 모델 제공자(Ollama, Anthropic 등)와 검증기(SymPy, Sage, Lean)는 CLI 플래그를 통해 호출 시점에 선택된다.
5. 컴파일 대상 (Compilation Target): 이 언어는 최적화 가능한 중간 표현(IR)을 생성한다.

핵심 기본 단위 (Core Primitives)

• 확률적 (System 1):
  • GENERATE: 근사적 출력을 생성하기 위해 LLM을 호출한다.
  • EVALUATE: 의미론적 분기(예: 환각 또는 정의되지 않은 용어 체크)를 위해 LLM을 런타임 판사로 사용한다.
  • WHILE: LLM이 판단한 품질 게이트를 기준으로 반복한다.
  • EXCEPTION: LLM 특유의 실패 모드(환각, 컨텍스트 오버플로)를 처리한다.
• 결정론적 (System 2):
  • SOLVE: 정확한 계산을 위해 Python 표현식을 라이브 커널(IPython)로 전달한다.
  • ASSERT: 워크플로 지속 여부를 결정하기 위해 커널 내에서 불리언(Boolean) 표현식을 평가한다.
  • CALL PARALLEL: 병렬 브랜치(예: 솔버 암과 LLM 전용 암의 비교)를 실행한다.

검증기 사다리 (The Verifier Ladder)

SPL은 런타임에 선택 가능한 3단계 심볼릭 검증기 계층 구조를 구현한다:

• R1 (SymPy): 대수적 항등식 및 미적분용 (밀리초 단위, 외부 의존성 없음).
• R2 (SageMath): 정수론, 기하학, 조합론용 (별도 환경 필요).
• R3 (Lean 4): Mathlib에 대한 형식적 증명용 (수 분 소요, 높은 신뢰도).
  언어는 ASSERT 실패 시 R1에서 R2 또는 R3로 에스컬레이션(escalation)할 수 있도록 허용하며, 이는 Python 조건문 없이 선언적으로 표현된다.

3. 주요 기여

1. 선언적 두 모드 구성: SPL은 GENERATE 및 EVALUATE와 함께 커널로 계산을 라우팅하는 SOLVE 및 ASSERT 프리미티브를 도입한다. 변수 바인딩은 런타임에 의해 완전히 관리되는 공유 네임스페이스를 통해 이러한 모드 사이를 흐른다.
2. DODA 원칙: 단일 .spl 파일은 로컬 노드, 클라우드 API, 분산 그리드에서 변경 없이 실행된다. 모델 및 검증기 선택은 호출 시점으로 유예되어, 논리적 워크플로와 물리적 실행을 분리한다.
3. 검증기 사다리: ASSERT를 통해 접근 가능한 정답 보장(SymPy, SageMath, Lean 4)의 구성 가능한 계층 구조이다. 에스컬레이션 로직은 코드로 작성되는 것이 아니라 워크플로에 선언된다.
4. 통제된 경험적 평가: 6개의 난이도 티어에 걸쳐 1,200회 실험(10개 모델 × 20개 문제 × 2개 암 × 3회 반복)을 수행하여, "솔버 암(Solver Arm, LLM이 분해하고 커널이 실행/검증)"과 "LLM 전용 암"을 비교하였다.

4. 실험 결과

실험은 단일 단계 다항식(T0)부터 전문가 수준의 상미분방정식(ODE, T5)까지의 심볼릭 수학 문제를 대상으로 10개의 모델(gemma4:e2b, sonnet-4-6, qwen2.5 포함)을 평가했다.

• 검증된 정확성 vs 출력 생성: LLM 전용 암은 거의 100%의 통과율(비어 있지 않은 응답으로 정의됨)을 달성했으나, 이는 검증되지 않은 결과였다. 기계 검증된 정확성을 요구하는 솔버 암은 상당한 편차를 보였다:
  • gemma4:e2b는 **93%**의 검증된 정확도를 달성했다 (LLM 전용 97% 대비).
  • sonnet-4-6은 **85%**의 검증된 정확도를 달성했다 (LLM 전용 100% 대비).
  • 하위 티어 모델(예: phi3)은 **32%**의 검증된 정확도로 떨어졌다.
• 실패 모드: 주요 실패 모드는 포맷 미준수(예: 마크다운 펜스)가 아니라 solver_error(커널이 거부한 표현식)였다. 이는 추론 능력이 있는 모델이라도 결정론적 엔진이 요구하는 엄격한 expr|op 구문을 생성하는 데 실패할 수 있음을 나타낸다.
• 백엔드 난이도: SymPy 문제(T0–T2)는 78%의 총 합계 통과율을 보인 반면, SageMath 문제(T3–T5)는 54%로 떨어지는 그래디언트가 나타났다. 이는 수학적 난이도뿐만 아니라 API 표면의 생소함 때문인 것으로 분석되었다.
• 지연 시간(Latency): 많은 모델에서 솔버 암이 LLM 전용 암보다 빨랐는데, 이는 솔버 에러 발생 시 조기 종료(최종 서사 단계 건너뜀)가 발생하거나 커널이 사고의 연쇄(chain-of-thought)를 단축시키기 때문이다. 그러나 gemma4:e2b와 같은 고정밀 모델은 전체 체인을 완료함에 따라 25%의 지연 시간 증가를 겪었다.

5. 의의 및 주장

본 논문은 SPL이 수학 및 논리 워크플로에서 LLM의 역할을 **추론자(reasoner)**에서 **포맷 번역기(format translator)**로 근본적으로 전환한다고 주장한다.

• 인식론적 구분: 저자들은 System 1과 System 2의 구분이 시간적(빠름/느림)인 것이 아니라 인식론적(확률적/결정론적)인 것이라고 주장한다. SPL은 모드 경계를 소스 코드에 가시화함으로써 이를 공식화한다.
• 기술의 분리 가능성: 결과는 "포맷 준수"(구조화된 expr|op 계획 생성)가 "수학적 추론"과 분리 가능한 능력임을 입증한다. 작은 오픈 소스 모델(gemma4:e2b, 약 2B 파라미터)이 더 큰 모델보다 검증된 정확도에서 우수한 성능을 보였는데, 이는 해당 모델이 요구되는 구조적 포맷을 안정적으로 생성했고, 실제 유도는 커널이 처리했기 때문이다.
• 개인정보 보호 및 접근성: 명세를 실행 백엔드와 분리함으로써, SPL은 학생의 데이터가 기기를 떠나지 않으면서도(로컬 Ollala 및 SymPy 사용) 기계 검증된 정확성의 이점을 누릴 수 있는 개인정보 보호 중심의 오프라인 워크플로를 가능하게 한다.
• 표현력의 한계 극end: 논문은 현재의 명령형 "글루 코드" 방식이 표현력의 한계라고 상정한다. SPL의 선언적 구성은 의도가 IR에 명시되어 있기 때문에, 명령형 오케스트레이션 코드에서는 불가능한 미래의 최적화(배칭, 캐싱, 모델 라우팅)를 가능하게 한다.

저자들은 결론적으로 SPL이 확률적 생성과 결정론적 검증 사이의 간극을 메우며, 깊은 소프트웨어 엔지니어링 기술이나 독점적인 모델 접근 권한 없이도 고품질의 검증된 계산을 가능하게 한다고 밝히고 있다.