LLM을 통한 자연어의 전략적 시계열 명세(Strategic Temporal Specifications) 번역

시스템 요구사항에 대한 엄격한 정식화(formalization)는 멀티 에이전트 시스템 (Multi-Agent Systems, MAS) 검증을 위한 근본적인 전제 조건입니다. 그러나 정확한 정식 명세(formal specifications)를 작성하는 것은 오류가 발생하기 쉽고, 시간이 많이 소요되며, 전문 지식이 집중적으로 요구되는 작업으로 잘 알려져 있습니다. 이러한 어려움은 요구사항이 전략적 능력과 시계열적 목표를 포착해야 하는 MAS에서 더욱 두드러집니다. 현재 자연어로부터 MAS 명세를 도출하기 위한 확립된 방법론은 존재하지 않습니다. 우리는 대규모 언어 모델 (Large Language Models, LLMs)을 사용하여 전략적 요구사항에 대한 자연어 설명을 잘 형성된 ATL/ATL* 공식으로 번역하는 프레임워크를 제시합니다. NL-to-ATL/ATL* 번역 작업을 위한 지도 학습 (supervised learning)을 지원하는 가용 데이터셋이 없기 때문에, 우리는 미세 조정 (fine-tuned)된 모델의 학습 및 평가에 사용될 전문가 검증을 거친 새로운 데이터셋을 생성하고 큐레이션합니다. 전문가 주석과 가장 잘 일치하는 LLM 심사위원 (LLM judge) 하에 평가된 홀드아웃 테스트 세트 (held-out test set)에서, 소규모 오픈 웨이트 (open-weight) 모델 (3 - 7B 파라미터)의 도메인 내 미세 조정은 강력한 퓨샷 (few-shot) 독점 API 베이스라인과 대등한 성능을 보입니다. 우리의 최적 미세 조정 시스템은 0.84의 의미론적 정확도 (semantic accuracy)에 도달하며, 이는 가장 강력한 퓨샷 독점 베이스라인의 0.86과 통계적으로 대등한 수준인 동시에 요구사항을 온프레미스 (on-premises) 환경에서 유지할 수 있게 합니다. 우리는 더 나아가 심사위원의 신뢰도가 생성기 (generator)의 성능과 반비례한다는 것을 발견했습니다. 오픈 웨이트 모델인 Llama-3.3-70B가 인간의 판결과 가장 밀접하게 일치하는 반면, 가장 강력한 독점 모델들은 참조 문구의 충실한 의역을 과도하게 거부하여 가장 신뢰할 수 없는 심사위원이 되었습니다. 생성된 명세의 실질적인 적용 가능성을 평가하기 위해, 우리는 우리의 도구를 기존의 전략적 논리 모델 체커 (strategic logics model checker)에 임베딩하여, 비전문가 사용자가 자연어로 전략적 속성을 명시할 수 있도록 했습니다.