기술 요약: U-Define: LLM 기반 계획에서의 경직 및 유연 제약 조건을 위한 사용자 워크플로우 설계

1. 문제 제기

대규모 언어 모델 (LLM) 은 최종 사용자의 작업 계획 수립 장벽을 낮추었지만, 그 '블랙박스' 성격은 상당한 신뢰성 문제를 야기합니다. LLM 은 종종 일관성 없는 계획을 생성하거나 엄격한 요구사항을 준수하지 못하며, 확신에 차 있지만 오류가 있는 추론을 통해 출력을 생성합니다. 기존 검증 접근법 (예: 외부 비판가 또는 형식적 검증) 은 종종 유연성을 제한하는 경직된 사전 설계 템플릿이나 도메인별 명세에 의존합니다. 반면, 순수한 유연 제약 조건 접근법 (예: 수치 가중치 또는 유연한 선호도) 은 사용자가 해석하기 어렵고 중요한 안전 또는 논리 규칙을 보장하지 못하는 경우가 많습니다.

본 연구가 해결하는 핵심 과제는 사용자가 형식 명세 언어를 학습하거나 경직된 템플릿에 의존하지 않고도 LLM 기반 계획 내에서 경직 제약 조건(절대 위반되어서는 안 되는 규칙) 과 유연 제약 조건(유연성을 반영하는 선호도) 을 신뢰성 있게 표현하고 균형을 잡을 수 있는 상호작용 워크플로우를 설계하는 것입니다.

2. 방법론 및 시스템 설계

저자들은 사용자가 자연어로 제약 조건을 정의하고 엄격도에 따라 분류하며, 각 제약 조건 유형에 맞춘 검증 결과를 받도록 하는 워크플로우를 구현한 U-Define 시스템을 제안합니다. 이 시스템은 템플릿 의존성을 제거하고 하이브리드 검증 아키텍처를 도입함으로써 기존 연구 (VeriPlan) 를 확장합니다.

시스템 아키텍처

U-Define 은 계획 수립 과정을 세 단계로 구조화합니다:

1. 정의 단계:

   • 입력: 사용자가 자연어로 제약 조건을 입력하고 이를 경직 또는 유연으로 분류합니다.
   • 규칙 번역기: NL2LTL 데이터셋을 사용하여 LLaMA 7B 로 미세 조정된 전문 LLM 에이전트가 사용자가 정의한 경직 제약 조건을 선형 시간 논리 (LTL) 속성으로 번역합니다.
   • PRISM 변환: LTL 속성은 확률적 모델 체킹에 필요한 형식인 PRISM 모델링 언어로 추가 번역됩니다.
   • 검증: 시스템은 진행하기 전에 형식 규칙을 다시 자연어로 변환하여 사용자가 검증할 수 있도록 합니다.

2. 검증 단계:

   • 계획 생성: LLM 플래너가 사용자의 작업 프롬프트와 제약 조건을 기반으로 후보 계획을 생성합니다.
   • 경직 제약 조건 검증: 생성된 계획은 PRISM 형식으로 변환됩니다. 형식 모델 체커(PRISM 및 Stormpy 사용) 는 LTL 규칙 준수를 확인하기 위해 계획의 상태 공간을 철저히 탐색합니다. 이는 이진 유효성 결과와 위반된 특정 규칙 목록을 반환합니다.
   • 유연 제약 조건 검증: LLM-as-Judge 에이전트가 유연 제약 조건에 대해 계획을 평가합니다. 이는 사용자 선호도와의 일치 정도에 관한 1~5 점 별점 평가와 자연어 설명을 제공합니다.

3. 피드백 단계:

   • 사용자는 경직 제약 조건 위반을 기준으로 순위가 매겨진 계획과 검증 출력을 검토합니다.
   • 사용자는 제약 조건을 반복적으로 정교화하거나 규칙의 엄격도를 조정하거나 프롬프트를 수정할 수 있습니다. 시스템은 계획을 재생성하고 다시 검증하여 폐쇄형 피드백 루프를 생성합니다.

기술 구현

• LLM 에이전트: 대부분의 에이전트는 GPT-4 를 사용합니다. 규칙 번역기는 미세 조정된 LLaMA 7B 모델을 사용합니다.
• 형식적 검증: 모델 체킹을 위해 PRISM 및 Stormpy 를 활용합니다.
• 평가: 시스템은 구성 요소 수준의 기술 평가 (번역 정확도 측정) 와 두 가지 사용자 연구를 통해 평가되었습니다.

3. 주요 기여

기술적 기여

• 자동 번역 파이프라인: LLM 을 사용하여 자연어 경직 제약 조건을 형식 검증 산출물 (LTL 및 PRISM) 로 자동 번역하는 파이프라인으로, 사전 설계된 도메인 템플릿의 필요성을 제거합니다.
• 하이브리드 검증 메커니즘: 제약 조건 유형에 따라 서로 다른 검증 방법을 적용하는 시스템: 경직 제약 조건에 대한 형식 모델 체킹 (정확성 보장) 과 유연 제약 조건에 대한 LLM-as-Judge 평가 (선호도 일치성 평가).

시스템 기여

• U-Define 인터페이스: 경직 및 유연 제약 조건을 동시에 정의할 수 있으며, 마인드맵 레이아웃을 통해 시각화하고 차별화된 검증 피드백 (위반 목록 대 별점 평가) 을 제공하는 사용자 인터페이스.

경험적 기여

• 사용자 연구: 두 가지 연구가 수행되었습니다:
  1. 연구 1 (일반 사용자): 12 명의 참가자가 세 가지 시나리오 (휴가, 결혼식, 레시피 계획) 에서 수행한 피험자 내 절단 연구.
  2. 연구 2 (도메인 전문가): 교육, 건설, 금융 등 다양한 분야의 6 명의 전문가가 전문 계획 작업을 수행한 연구.
• 결과:
  • 지각된 가치: 전체 시스템 (C1) 은 지각된 유용성, 만족도 및 성능 측면에서 절단된 조건 (유연만, 경직만, 없음) 보다 현저히 우수했습니다.
  • 구별된 역할: 사용자는 경직 제약 조건이 불가피한 기반을 제공하고 유연 제약 조건이 맞춤화를 가능하게 한다는 상호 보완적인 역할을 수행한다고 인식했습니다.
  • 경직성 대 유연성: 경직만 조건은 반복 횟수가 적었지만 경직성과 지연으로 인해 만족도가 낮았습니다. 유연만 조건은 탐색을 장려했지만 신뢰할 수 없는 설명과 검증 격차로 고통받았습니다.
  • 전문가 과제: 전문가들은 엄격한 규칙 관리를 위해 시스템을 가치 있게 여겼지만, 수많은 제약 조건을 기억하고 입력하는 '문맥 오버헤드'에 직면했습니다. 또한 일부 전문 제약 조건 (수치적 한계, 캘린더 논리) 은 LTL 의 표현력을 초과한다고 지적했습니다.

4. 결과 및 의의

기술적 성능

• LTL 번역: 미세 조정된 LLM 은 인간이 생성한 기준 진실 (ground truth) 대비 평균 레벤슈타인 유사도 **83.12%**를 달성했습니다. 오류는 주로 논리 연산자 오류가 아닌 술어 수준 (예: 토큰 불일치) 에서 발생했습니다.
• PRISM 변환: PRISM 계획 변환은 **97.4%**의 유사도를 달성했으며, 오류 역시 술어 수준에서 발생했습니다.

사용자 경험 및 설계 시사점

본 논문은 U-Define 이 결정론적 검증의 신뢰성과 생성형 AI 의 유연성 사이의 간극을 성공적으로 메웠다고 주장합니다. 결과에서 도출된 주요 설계 시사점은 다음과 같습니다:

1. 혼합 제약 조건 지원: 시스템은 신뢰성과 개인화를 균형 있게 맞추기 위해 사용자가 경직 및 유연 제약 조건을 명시적으로 구분할 수 있어야 합니다.
2. 실행 가능한 설명: 경직 제약 조건에 대한 설명은 유연 제약 조건에서 사용자가 혼란을 느꼈던 일반적 스칼라 점수 대신 위반된 규칙을 명시적으로 나열해야 합니다.
3. 문맥 관리: 향후 시스템은 도메인 전문가가 식별한 중요한 필요 사항인 제약 조건 입력의 인지적 오버헤드를 줄이는 데 사용자를 지원해야 합니다 (예: 템플릿, 재사용 가능한 프로필, 외부 도구 통합을 통해).
4. 검증 범위: 시스템은 사용자의 제약 조건이 형식 엔진에 의해 완전히 검증될 수 없는 경우 (예: 수치 제약 조건) 를 투명하게 표시하고 해당 부분을 휴리스틱 검사로 처리해야 합니다.

의의

본 논문은 효과적인 계획 지원은 사용자가 제약 조건이 어떻게 표현되고 시행되는지에 대한 통제권을 갖도록 하는 것이 필요하다고 주장합니다. 제약 조건 엄격도를 정의할 권한을 사용자에게 부여하고 적절한 검증 메커니즘과 결합함으로써, U-Define 은 신뢰할 수 있는(중요 규칙의 형식적 검증을 통해) 이자 적응 가능한(유연한 선호도 처리를 통해) 계획 시스템을 구축할 수 있음을 보여줍니다. 이 접근법은 순수 템플릿 기반 검증과 순수 생성형 계획의 한계를 해결하여 복잡하고 실제적인 시나리오에서 더 신뢰할 수 있는 인간-AI 협업을 위한 길을 제시합니다.