Designing FSMs Specifications from Requirements with GPT 4.0

논문 요약: GPT-4 를 활용한 요구사항 기반 유한 상태 기계 (FSM) 명세 설계

1. 문제 정의 (Problem)

• 배경: 반응형 시스템의 실행 가능한 형식 명세 (Formal Specification) 인 유한 상태 기계 (FSM) 는 모델 기반 시스템 공학 (MBSE) 및 자동화된 테스트에서 핵심적인 역할을 합니다.
• 현재의 한계: FSM 은 주로 자연어 (텍스트) 로 작성된 요구사항 문서에서 설계됩니다. 이 과정은 수동으로 수행될 경우 시간 소모가 크고, 생성된 FSM 의 품질이 낮을 경우 테스트 단계에서 결함이 누락되어 시스템 고장이나 치명적인 사고로 이어질 수 있습니다.
• 연구 목표: 대규모 언어 모델 (LLM, 특히 GPT-4) 의 능력을 활용하여 자연어 요구사항에서 FSM 을 자동으로 생성하고, 생성된 명세에 결함이 있을 경우 이를 자동으로 또는 반자동으로 수정 (Repair) 하는 프레임워크를 제안하는 것입니다.

2. 방법론 (Methodology)

연구팀은 GPT-4 를 사용하여 텍스트 설명에서 결정적 유한 상태 기계 (DFSM) 를 생성하고, 생성된 FSM 의 정확성을 평가하며 결함을 수정하는 4 가지 접근법을 고안했습니다.

• 데이터 생성 및 실험 환경:

  • 실제 데이터를 대신할 수 있는 시뮬레이션 데이터를 생성했습니다. 이는 무작위로 생성된 '오라클 (Oracle, 기준이 되는 올바른 FSM)'과 이를 기반으로 생성된 자연어 설명으로 구성됩니다.
  • GPT-4o 를 사용하여 텍스트 설명을 CSV 형식의 FSM 명세로 변환하는 프롬프트 엔지니어링을 수행했습니다.

• 정확성 평가 (Evaluation):

  • 구문 기반 비교 (Syntax-based): 생성된 FSM 과 오라클 FSM 의 상태 및 전이 (Transition) 구조를 비교하여 추가/결손 전이, 출력 오류, 전이 오류 등을 식별합니다.
  • 의미 기반 비교 (Semantics-based): 두 FSM 이 동일한 입력 시퀀스에 대해 다른 출력 시퀀스를 생성하는지 확인합니다. 이를 위해 구별 시퀀스 (Distinguishing Sequences) 와 검사 시퀀스 (Checking Sequences) 를 활용합니다.

• 수정 (Repair) 접근법 4 가지:

  1. 구문 오류 기반 수정: 생성된 FSM 과 오라클 간의 구문적 차이 (잘못된 전이, 누락된 전이 등) 를 식별하여, 이를 프롬프트에 명시적으로 추가/삭제 요청 형태로 포함시켜 LLM 에게 재생성을 요청합니다.
  2. 구별 시퀀스 (Distinguishing Sequences) 기반 수정: 두 FSM 을 구별하는 입력 시퀀스와 기대되는 출력 시퀀스를 프롬프트에 포함시켜 LLM 에게 수정을 유도합니다.
  3. 검사 시퀀스 (Checking Sequence) 기반 수정 (반자동): 실제 전문가 (Human Expert) 가 시스템의 동작을 알지 못하더라도, 특정 입력 시퀀스 (검사 시퀀스) 에 대한 기대 출력을 전문가에게 문의하여 프롬프트를 수정하는 방식입니다.
  4. 결함 모델 (Fault Model) 기반 수정: LLM 이 주로 범하는 오류 유형 (출력 오류, 결손 전이 등) 을 기반으로 '변이 기계 (Mutation Machine)'를 구축합니다. 이는 가능한 수정 후보들의 영역 (Repair Domain) 을 정의하며, SAT 기반 마이닝 알고리즘과 전문가의 출력을 통해 올바른 FSM 을 자동으로 찾아냅니다.

3. 주요 기여 (Key Contributions)

1. 시뮬레이션 데이터셋 및 평가 프레임워크: FSM 생성 및 평가에 사용할 수 있는 무작위 오라클 FSM 과 자연어 설명 생성 모듈을 개발했습니다.
2. 프롬프트 엔지니어링: 자연어 설명을 CSV 형식의 FSM 명세로 변환하기 위한 최적화된 GPT-4 프롬프트를 설계했습니다.
3. 4 가지 수정 전략 제안: 생성된 FSM 의 결함을 수정하기 위해 구문 오류, 구별 시퀀스, 검사 시퀀스, 그리고 결함 모델 (변이 기계) 을 기반으로 한 4 가지 수정 방법을 제안하고 실험적으로 검증했습니다.
4. LLM 성능에 대한 실증적 분석: FSM 크기가 커질수록 LLM 의 오류 발생률이 증가하며, 복잡한 의미 분석 (다수의 입력 - 출력 시퀀스 처리) 에는 한계가 있음을 규명했습니다.

4. 실험 결과 (Results)

• 생성 정확도: GPT-4 는 작은 규모의 FSM (5 상태) 에서는 높은 정확도를 보였으나, 상태 수가 10 개 이상으로 증가함에 따라 오류 (특히 출력 오류와 전이 결손) 가 빈번하게 발생했습니다.
• 수정 방법별 성과:
  • 구문 기반 수정: 가장 높은 성공률 (100%) 을 보였습니다. 구체적인 구조적 오류를 프롬프트에 명시하면 LLM 이 이를 잘 수정하는 것으로 나타났습니다.
  • 구별 시퀀스 기반 수정: 성공률이 낮았습니다 (5 상태 100%, 10 상태 0%). LLM 이 긴 시퀀스와 복잡한 분기 구조를 동시에 처리하는 데 어려움을 겪는 것으로 분석되었습니다.
  • 검사 시퀀스 기반 수정: 전문가의 개입이 필요하며, 계산 비용이 높고 성공률이 낮았습니다 (5 상태 기준 40%).
  • 결함 모델 기반 수정: 가장 유망한 방법으로, 5 상태와 10 상태 모두에서 100% 의 수정 성공률을 기록했습니다. LLM 의 일반적인 오류 패턴을 사전에 정의된 수정 영역 (Repair Domain) 으로 제한하고, 전문가의 출력을 통해 정답을 탐색하는 방식이 효과적이었습니다.

5. 의의 및 결론 (Significance & Conclusion)

• LLM 의 한계와 가능성: LLM 은 자연어에서 FSM 을 생성하는 데 유용하지만, 상태 수가 증가하거나 복잡한 논리적 연결을 처리할 때 정밀도가 떨어집니다. 특히 긴 시퀀스 기반의 의미 분석보다는 구체적인 구조적 지시나 제한된 수정 영역 내에서의 탐색이 더 효과적입니다.
• 실용적 제안: 완전 자동화보다는 전문가 중심의 반자동 수정 (Semi-automated repair) 접근, 특히 결함 모델 (Fault Model) 기반의 수정이 실제 시스템 공학에 적용 가능한 현실적인 해결책임을 시사합니다.
• 미래 전망: 산업 수준의 복잡한 요구사항 문서로 확장 시, 도메인 특화 정보가 LLM 의 정확도를 높이는 데 기여할 것으로 예상됩니다. 또한, 생성된 명세의 품질을 보장하기 위해 모델 기반 테스트 기법과의 결합이 필요합니다.

이 논문은 LLM 을 소프트웨어 명세 생성에 활용하는 초기 단계에서, 생성된 모델의 품질을 보장하기 위한 체계적인 검증 및 수정 프레임워크를 제시했다는 점에서 의의가 있습니다.