LLM 생성 출력의 자동형식화를 통한 요구사항 검증

기본 정보

• 논문 ID: 2511.11829
• 제목: Towards Autoformalization of LLM-generated Outputs for Requirement Verification
• 저자: Mihir Gupte, Ramesh S. (General Motors)
• 분류: cs.CL, cs.AI, cs.FL, cs.LO
• 발표 시간: 2025년 11월 18일 (arXiv 프리프린트)
• 논문 링크: https://arxiv.org/abs/2511.11829

초록

본 논문은 자동형식화(Autoformalization) 기술을 사용하여 대규모 언어모델(LLM) 생성 출력을 검증하는 가능성을 탐색합니다. LLM이 자연언어 요구사항을 구조화된 출력(예: Gherkin 시나리오)으로 변환하는 데 잠재력을 보이면서, 이러한 출력의 정확성을 형식적으로 검증하는 방법이 핵심 문제가 되었습니다. 연구팀은 두 가지 실험 그룹을 수행했습니다: 첫 번째 그룹은 서로 다른 표현의 두 자연언어 요구사항이 논리적으로 동등함을 성공적으로 식별했으며, 두 번째 그룹은 LLM 생성 출력과 원본 요구사항 간의 논리적 불일치를 식별했습니다. 연구 범위는 제한적이지만, 결과는 자동형식화가 LLM 생성 출력의 충실성과 논리적 일관성을 보장하는 데 상당한 잠재력을 가지고 있음을 시사합니다.

연구 배경 및 동기

1. 핵심 문제

LLM 응용이 확산되면서, 특히 테스트 시나리오 자동 생성 등 공학 작업에서 다음과 같은 핵심 과제가 발생합니다: LLM 생성 출력이 원본 자연언어 요구사항을 정확하게 반영하는지 검증하기 위한 형식적 방법의 부재. 예를 들어, "차속 ≥ 10이고 안전벨트가 미착용일 때 안전벨트 경고 시작"이라는 요구사항에서 Gherkin 시나리오를 생성한 후, 생성 내용의 논리적 정확성을 보장할 수 없습니다.

2. 문제의 중요성

자동차 공학 등 안전 관련 분야에서 요구사항 검증은 매우 중요합니다. 잘못된 요구사항 변환은 다음을 초래할 수 있습니다:

• 테스트 케이스의 불완전성 또는 오류
• 시스템 동작과 예상의 불일치
• 잠재적 안전 위험

3. 기존 방법의 한계

• 전통적 형식화 방법: 주로 수학 정리 증명에 적용되며, 공학 요구사항 검증 응용이 부족함
• LLM 평가 방법: 인간 검사 또는 휴리스틱 방법에 의존하며, 엄격한 논리 검증이 부족함
• 자동형식화 연구: 주로 데이터셋 구축 및 모델 훈련에 중점을 두며, 실제 공학 응용에 대한 관심이 적음

4. 연구 동기

본 논문은 자동형식화 기술을 LLM 출력 검증이라는 새로운 시나리오에 적용할 것을 제안하며, 자연언어 요구사항과 LLM 생성 출력을 모두 형식 논리 표현(Lean 4)으로 변환하고 정리 증명기를 활용하여 논리적 동등성을 검증합니다.

핵심 기여

1. LLM 생성 출력 검증을 위한 첫 번째 자동형식화 파이프라인 제안: 자연언어 요구사항과 LLM 출력을 Lean 4 형식화 표현으로 변환하고, 쌍방향 조건 동등성 증명을 통해 논리적 일관성을 검증
2. 두 가지 구체적 응용 시나리오 검증:
   • 서로 다른 표현의 자연언어 요구사항의 논리적 동등성 식별
   • LLM 생성 출력과 원본 요구사항 간의 논리적 불일치 감지
3. 핵심 기술 과제 식별:
   • 변수 접지(variable grounding)의 필요성 및 자동화 어려움
   • LLM 비결정성이 형식화에 미치는 영향
   • 자연언어 모호성 처리
4. 향후 연구 방향 제시: 신뢰할 수 있는 LLM 출력 검증 프레임워크 구축의 기초 마련

방법론 상세 설명

작업 정의

입력:

• 논리적 관계 검증이 필요한 명제 쌍(S₁, S₂):
  • 두 개의 자연언어 요구사항
  • 하나의 자연언어 요구사항과 하나의 LLM 생성 Gherkin 시나리오

출력:

• 논리적 동등성 판단: 동등(S₁ ↔ S₂ 증명 가능) 또는 비동등(증명 실패)

제약 조건:

• 명제는 명제 논리로 형식화 가능해야 함
• 변수 접지를 위해 시스템 컨텍스트 정보 필요

모델 아키텍처

전체 파이프라인은 네 가지 핵심 단계로 구성됩니다(그림 9 참조):

단계 1: 자동형식화

**DeepSeek-Prover-v2(7B 모델)**을 사용하여 자연언어 명제를 Lean 4 명제로 변환:

-- 예시: 요구사항 R1의 형식화
variable (vehicle_speed_avg : ℝ)
variable (calibratable_speed : ℝ)
variable (seatbelt_active : Bool)
variable (initiate_chime : Bool)

def seatbelt_chime_condition : Prop :=
  (vehicle_speed_avg ≥ calibratable_speed ∨ ¬seatbelt_active) → initiate_chime

프롬프트 템플릿(부록 A.1 참조):

• Lean 4의 def 명령문 생성을 명시적으로 요구
• 명제 논리(Prop 타입) 사용 지정
• 조건을 함의 관계(A ∧ B → C)로 표현하도록 요구

단계 2: 변수 접지(Variable Grounding)

현재 구현: 서로 다른 형식화에서 동일한 개념을 가리키는 변수를 수동으로 식별 및 통합

문제 예시:

• R1의 vehicle_speed_avg와 R2의 mean_vehicle_speed는 동일한 물리량을 가리킴
• Lean 컴파일러에 이러한 동등성을 명시적으로 알려야 함

-- 수동 접지 예시
(h_speed : vehicle_speed_avg = mean_vehicle_speed)
(h_belt : seatbelt_active = seatbelt_plugged_in)

단계 3: 쌍방향 조건 동등성 정리 구성

논리적 동등성을 검증하기 위한 형식화 정리 구성:

theorem req1_eq_req2 
  (h_grounding : <변수 접지 가정>) :
  (Proposition_A) ↔ (Proposition_B) := by
  <증명 과정>

단계 4: 자동 정리 증명

DeepSeek-Prover-v2를 다시 사용하여 Lean 증명 코드 생성:

• 증명 성공 → 두 명제는 논리적으로 동등
• 증명 실패 → 논리적 불일치 존재

기술 혁신점

1. 학제 간 응용 혁신: 수학 정리 증명 분야의 자동형식화 기술을 소프트웨어 공학 요구사항 검증에 처음 적용
2. 이중 계층 LLM 사용:
   • 첫 번째 계층: 형식화 번역(자연언어 → Lean)
   • 두 번째 계층: 정리 증명(동등성 검증)
3. 실패 기반 검증 메커니즘: 정리 증명기의 실패를 논리적 불일치의 지표로 활용하는 혁신적인 부정 검증 방법
4. 변수 접지 식별: 변수 접지가 자동형식화 파이프라인에서 불가결한 단계임을 명시적으로 제시하며, 이는 이전 연구에서 충분히 강조되지 않았음

실험 설정

데이터셋

실험 1: 요구사항 동등성 검증

• R1: "If Vehicle Speed Average Driven ≥ CALIBRATABLE Seatbelt Reminder Speed OR Seatbelt is inactive then initiate SeatBelt Chime"
• R2: "If mean vehicle speed is greater than CALIBRATABLE Seatbelt Reminder Speed OR Seatbelt is not plugged in then initiate chime for seatbelt"

실험 2: LLM 출력 검증

• R3: "When Front Passenger Seat Belt Status changes to 'Fastened' then the Front Passenger Seat Belt Reminder Indication On shall be set to FALSE."
• G3: LLM 생성 Gherkin 시나리오(4개 예시 행 포함, seat_occupancy 같은 추가 변수 도입)

평가 지표

정성적 지표:

• Lean 4 컴파일 성공/실패
• 정리 증명 성공/실패

검증 기준:

• 논리적 동등성: 정리 PA ↔ PB 증명 가능
• 논리적 불일치: 정리 증명 실패 또는 Lean 코드 컴파일 불가

구현 세부사항

모델 선택:

• DeepSeek-Prover-v2 (7B)
• 선택 이유:
  1. Lean 4에서 훈련됨
  2. 자연언어 이해 능력 보유
  3. 부분목표 분해 전략 채택

형식화 언어: Lean 4

• 강력한 정리 증명 능력
• 정확한 논리 표현
• DeepSeek-Prover-v2와의 호환성

수동 개입:

• 변수 접지 단계는 완전히 수동
• 형식화 출력 검증은 Lean 컴파일러에 의존

실험 결과

주요 결과

실험 1: 요구사항 동등성 검증(성공 사례)

형식화 출력:

• R1과 R2가 Lean 명제로 성공적으로 변환됨(그림 3, 그림 4)
• 변수 매핑이 수동으로 구축됨:
  • vehicle_speed_avg ≡ mean_vehicle_speed
  • seatbelt_active ≡ seatbelt_plugged_in

검증 결과(그림 5):

• ✅ Lean 컴파일 성공
• ✅ 정리 req1_eq_req2 증명 성공
• 결론: R1과 R2는 논리적으로 동등

의의: 파이프라인이 의미상 동일하지만 표현이 다른 요구사항을 식별할 수 있음을 증명하며, 요구사항 일관성 검사에 도움이 됨.

실험 2: LLM 출력 검증(실패 사례)

형식화 출력:

• R3: 단순 명제, 안전벨트 상태 변화 조건만 포함(그림 6)
• G3: 복잡한 명제, 추가 변수 포함(seat_occupancy, initial_seatbelt_status)(그림 7)

핵심 발견:

• G3이 R3에서 언급되지 않은 변수 도입
• 논리 구조가 더 복잡함(4개 시나리오 예시 포함)

검증 결과(그림 8):

• ❌ Lean 코드 컴파일 실패 또는 증명 실패
• 결론: G3과 R3은 논리적으로 불일치

의의: LLM 생성 출력의 "과도 생성" 문제를 성공적으로 감지 — 원본 요구사항에 없는 추가 제약 조건 추가.

사례 분석

사례: 모호성 문제(R4)

요구사항:

"When the seatbelt is Unfastened and the vehicle is in motion then the Front Passenger Seat Belt Reminder Indication On shall be set to TRUE."

문제: "vehicle in motion"의 형식화에 모호성 존재

두 가지 가능한 형식화(그림 10):

1. pass@1: 부울 변수 vehicle_in_motion : Bool
2. pass@2: 수치 변수 vehicle_speed > 0

분석:

• 두 형식화 모두 시스템 의미론상 정확할 수 있음
• 그러나 형식 논리상 동등하지 않음(다른 타입)
• 형식화에 대한 자연언어 모호성의 영향을 강조

실험 발견

1. 형식화는 해석 가능성에 의존: LLM의 비결정성으로 인해 동일한 요구사항이 다르지만 모두 "합리적인" 형식화 표현을 생성할 수 있음
2. 변수 접지가 병목:
   • 가장 시간이 많이 소요되는 단계
   • 시스템 영역 지식 필요
   • 현재는 수동으로만 가능
3. 시스템 컨텍스트가 매우 중요: 명확한 시스템 정의(예: 데이터 사전) 부재는 형식화 불일치를 초래
4. 부정 검증이 효과적: 증명 실패가 논리적 불일치를 효과적으로 지시

관련 연구

자동형식화의 데이터셋 구축

• ProofNet: 학부 수준 수학 자동형식화
• MiniF2F: 올림피아드 수준 수학 벤치마크
• 다국어 데이터셋: Lean, Isabelle, Coq의 결합 훈련으로 성능 향상

LLM 훈련 전략

• "초안-스케치-증명" 방법(Jiang et al.): 증명 개요 생성으로 형식화 안내
• 부분목표 분해: DeepSeek-Prover가 채택한 재귀 검색 전략
• 강화학습: 정리 증명 성공률 향상

비결정성 대응

• 기호 동등성 프레임워크: pass@1과 pass@k의 차이 처리
• RAG 방법: 정확한 형식 정의 검색으로 컨텍스트 제공

응용 분야 확장

• 수학 문제 풀이: 고등학교에서 대학 수학까지
• 코드 검증: 프로그램 정확성 검증
• 생의학: 사실 검증

본 논문의 기여: 공학 요구사항 검증과 LLM 출력 검증에 자동형식화를 처음 적용하여 새로운 응용 방향을 개척.

결론 및 토론

주요 결론

1. 가능성 검증: 자동형식화 파이프라인이 LLM 생성 출력과 원본 요구사항 간의 논리적 일관성을 효과적으로 검증할 수 있음
2. 이중 응용 가치:
   • 요구사항 일관성 검사(동등 요구사항 식별)
   • LLM 출력 품질 제어(논리 오류 감지)
3. 개념 증명: 표본이 제한적이지만, 정리 증명 기술을 소프트웨어 공학에 적용할 가능성을 성공적으로 시연

한계

1. 규모 제한:
   • 3개 요구사항 쌍만 테스트
   • 대규모 평가 부재
   • 통계적 유의성 분석 없음
2. 수동 의존성:
   • 변수 접지는 완전히 수동
   • 시간이 많이 소요되고 오류 가능성 높음
   • 확장성 제한
3. 모델 제한:
   • 7B 모델 사용(자원 제약)
   • 더 큰 모델(671B)이 더 나은 성능을 보일 수 있음
   • 형식화 품질은 모델 능력에 의존
4. 모호성 미해결:
   • 자연언어의 고유한 모호성
   • 시스템 온톨로지 지원 부재
   • 여러 "정확한" 하지만 동등하지 않은 형식화 생성 가능
5. 영역 특정성:
   • 실험은 자동차 안전 요구사항으로만 제한
   • 일반화 능력 미지수

향후 방향

논문은 세 가지 핵심 연구 질문(RQ)을 제시합니다:

RQ1: 최적 형식화 방법

• k-pass 전략 탐색(여러 형식화 생성, 가장 가능성 높은 것 선택)
• 단일 변환과 다중 샘플링의 정확성 비교

RQ2: 변수 접지 자동화

• 방법 1: 컨텍스트 단일 형식화(단일 호출에서 모든 명제 처리)
• 방법 2: 유사도 기반 접지(임베딩을 사용한 시스템 온톨로지 매칭)
• 과제: LLM의 접지 가정 자체의 정확성 검증 방법

RQ3: 제약 시스템에서의 LLM 검증

• 시스템 동작의 지식 그래프 구축
• LLM 순회 메커니즘 개발
• 자동형식화를 사용한 출력 논리 일관성 보장
• 응용 시나리오: 스마트 홈, 차량 보조 등 제한된 동작 공간 시스템

기타 방향:

• 자동화된 변수 정규화 기술 개발
• 영역 특정 온톨로지 통합(예: 자동차 시스템 데이터 사전)
• 시간 논리 및 복잡한 제약으로 확장

심층 평가

장점

1. 문제 정의의 참신성:
   • 자동형식화를 LLM 출력 검증에 체계적으로 처음 적용
   • 공학 실무의 실제 문제점 해결
   • 새로운 연구 방향 개척
2. 방법론의 명확성:
   • 파이프라인 설계가 간결하고 명확함
   • 성숙한 도구 활용(Lean 4, DeepSeek-Prover)
   • 재현성이 강함
3. 문제 식별의 깊이:
   • 변수 접지의 핵심성 명시
   • 모호성 문제의 심층 분석
   • LLM 비결정성의 영향에 대한 솔직한 논의
4. 실용적 가치가 높음:
   • 안전 관련 분야(자동차 공학) 대상
   • 요구사항 공학 프로세스에 직접 적용 가능
   • LLM 응용의 신뢰성 향상에 도움
5. 우수한 작문 품질:
   • 구조가 명확하고 논리가 엄밀함
   • 상세한 프롬프트 템플릿 제공(부록)
   • 풍부한 그림, 이해하기 쉬움

부족한 점

1. 실험 규모가 심각하게 부족:
   • 단 3개 샘플: 통계학적 결론을 도출할 수 없음
   • 다양한 영역, 다양한 복잡도의 요구사항 테스트 부재
   • 더 큰 데이터셋에서의 성능 평가 미실시
   • 권장사항: 최소 50-100개 요구사항 쌍으로 충분한 평가 필요
2. 정량적 평가 부재:
   • 정확도, 재현율 등 지표 없음
   • 형식화 성공률 미보고
   • 인간 검증과의 비교 부재
   • 권장사항: 표지된 데이터셋 구축, 정밀도 지표 계산
3. 수동 개입이 과다:
   • 변수 접지가 완전히 수동으로 자동화 주장을 약화시킴
   • 자동화 방안의 구체적 구현 미제시
   • 확장성 의문
   • 권장사항: 최소한 원형 자동 접지 시스템 구현
4. 모델 선택이 제한적:
   • 자원 제약으로 7B 모델만 사용
   • 671B 모델이나 다른 대안 미탐색
   • 모델 크기가 결과에 미치는 영향 분석 부재
   • 권장사항: 최소한 소수 샘플에서 다양한 모델 비교
5. 실패 사례 분석 부재:
   • 정리 증명 실패 원인의 상세 분석 미실시
   • 형식화 오류 vs 실제 논리 불일치 구분 미실시
   • 거짓양성/거짓음성 분석 부재
   • 권장사항: 오류 분류 체계 구축
6. 평가 기준이 단일:
   • Lean 컴파일 성공/실패에만 의존
   • 부분적으로 정확한 경우 미고려
   • 세분화된 오류 유형 분석 부재
7. 일반화 능력 미지수:
   • 자동차 안전 요구사항만 테스트
   • 다른 영역(의료, 금융 등)에서의 적용성 미검증
   • Gherkin 시나리오의 특수성이 방법의 일반성을 제한할 수 있음

영향력

분야에 대한 기여:

• ⭐⭐⭐⭐ 개념 기여도 높음: 새로운 연구 방향 및 응용 시나리오 제시
• ⭐⭐ 기술 기여도 중간: 주로 기존 기술의 조합 응용
• ⭐⭐⭐ 실용적 가치 중상: 공학 실무의 실제 문제 해결

실용적 가치:

• 단기: 요구사항 공학자에게 검증 사고 제공
• 중기: 전문 요구사항 검증 도구 개발 촉발 가능
• 장기: LLM 응용 품질 보증의 표준 프로세스가 될 가능성

재현성:

• ✅ 오픈소스 도구 사용(Lean 4, DeepSeek-Prover)
• ✅ 상세한 프롬프트 템플릿 제공
• ❌ 코드 또는 데이터 미공개
• ❌ 수동 단계의 재현 어려움
• 평가: ⭐⭐⭐(중간)

예상 영향:

• LLM 출력 형식화 검증에 관한 더 많은 연구 촉발 가능
• 요구사항 공학과 형식화 방법의 결합 추진 가능
• 변수 접지 문제가 새로운 연구 핫스팟이 될 가능성

적용 시나리오

높은 적용성:

• ✅ 안전 관련 시스템의 요구사항 검증(자동차, 항공, 의료)
• ✅ 요구사항 일관성 검사 및 중복 제거
• ✅ LLM 생성 테스트 케이스의 품질 제어

중간 적용성:

• ⚠️ 복잡한 비즈니스 논리 검증(형식화 능력 확장 필요)
• ⚠️ 다중 모달 요구사항(그래프 포함 요구사항 등)
• ⚠️ 실시간 시스템(시간 논리 확장 필요)

부적용:

• ❌ 높은 모호성의 자연언어 텍스트
• ❌ 명확한 시스템 정의가 부족한 시나리오
• ❌ 실시간 응답이 필요한 시나리오(현재 수동 단계가 너무 느림)

개선 권장사항

1. 즉시 실행 가능:
   • 최소 50개 요구사항 쌍으로 확장
   • 기초 자동 변수 접지 원형 구현
   • 오류 분류 체계 구축
2. 단기 개선:
   • 다양한 규모 모델 비교
   • 정량적 평가 지표 도입
   • 다중 영역 테스트
3. 장기 목표:
   • 완전 자동화 파이프라인
   • 영역 지식 그래프 통합
   • 시간 논리 및 복잡한 제약 지원

참고문헌(핵심 문헌)

1. Weng et al. (2025): Autoformalization in the era of large language models: A survey - 종합 문헌
2. Wu et al. (2022): Autoformalization with large language models - 자동형식화 기초 연구
3. Ren et al. (2025): DeepSeek-Prover-v2 - 본 논문에서 사용한 핵심 모델
4. Jiang et al. (2022): Draft, sketch, and prove - 부분목표 분해 방법
5. de Moura & Ullrich (2021): The Lean 4 theorem prover - 형식화 언어

종합 평가: 이것은 개념 증명형 탐색 논문으로, 가치 있는 새로운 연구 방향을 제시하지만 실험 검증이 심각하게 부족합니다. 프리프린트 및 초기 연구로서, 이 논문은 핵심 문제를 성공적으로 식별하고 실행 가능한 기술 경로를 제공하지만, 성숙한 솔루션까지는 아직 거리가 멉니다. 논문의 주요 가치는 문제 정의 및 방향 제시에 있으며, 기술 혁신에 있지 않습니다. 후속 연구는 변수 접지 자동화 및 대규모 평가 문제 해결에 중점을 두기를 권장합니다.