기술 요약: PROVE-RT

문제 정의

안전 필수 실시간 시스템(RTS)은 타이밍 정확성을 보장하기 위해 엄격한 스케줄링 가능성 분석을 필요로 한다. PROSA/ROCQ 프레임워크를 사용한 기계화된 검증은 전통적인 종이와 펜 기반의 증명보다 더 신뢰할 수 있는 대안을 제공하지만, 이러한 증명을 수동으로 구축하는 것은 비용이 매우 많이 든다. 이는 상당한 도메인 전문 지식과 증명 엔지니어링 노력을 요구하며, 사소한 모델 변경만으로도 기존 증명이 무효화되어 광범위한 유지보수가 필요할 수 있다.

대규모 언어 모델(LLM)이 일반 수학 및 소프트웨어 검증을 위한 형식적 증명 생성에서 유망한 성과를 보여주었음에도 불구하고, 실시간 스케줄링 가능성 분석에 대한 적용은 세 가지 뚜렷한 과제에 직면해 있다:

1. 데이터 부족: PROSA 특유의 추상화, 용어 및 증명 패턴을 학습할 수 있는 대규모의 기계화된 학습 코퍼스가 부족하여, LLM의 학습 능력이 제한된다.
2. 정형화 격차 (Formalization Gap): 문헌의 스케줄링 가능성 분석은 비기계화된 형태(산문, 방정식, 스케치)로 표현되어 있으며, 이는 ROCQ 정리 증명기가 요구하는 명시적인 구조적 요구사항(변수, 가설, 타입 클래스 인스턴스, 의존성 순서)이 결여되어 있다.
3. 구조적 복잡성: 스케줄링 가능성 레마(lemma)는 태스크 모델, 워크로드 정의, 간섭 경계의 깊은 계층 구조를 포함한다. 유효한 증명을 생성하려면 단순히 택틱(tactic)을 선택하는 것을 넘어, 올바른 의존성 순서로 구성된 컨텍스트를 구축해야 하며, 이는 표준적인 정리 증명보다 훨씬 더 복잡하다.

방법론: PROVE-RT 프레임워크

PROVE-RT는 비형식적 스케줄링 가능성 분석으로부터 의존성 순서가 지정된 PROSA/ROCQ 스크립트 생성을 자동화하기 위해 설계된 LLM 지원 프레임워크이다. 이 프레임워크는 5단계 파이프라인을 통해 작동한다:

1. 시스템 불변량 추출 (System Invariant Extraction):
   입력된 스케줄링 가능성 분석은 LLM에 의해 처리되어 일련의 시스템 불변량(정의, 레마, 정리)과 그에 대응하는 **비형식적 스케치(informal sketches)**를 추출한다. 이 스케치는 각 불변량의 진술, 직관 및 증명 개요를 설명한다. 결정적으로, 시스템은 불변량들이 반드시 도입되어야 하는 순서를 결정하기 위해 **의존성 그래프(DAG)**를 구축하여, 선행 조건이 종속된 구조보다 먼저 도입되도록 보장한다.

2. PROSA 문서 처리:
   도메인 특화된 컨텍스트의 부재를 해결하기 위해, PROSA 라이브러리 문서는 검색 가능한 코퍼스로 처리된다. 여기에는 **구조 인식 청킹(structure-aware chunking)**이 포함된다:

   • 증명 지향적 청킹 (Proof-Oriented Chunking): Analysis 및 Results와 같은 모듈의 경우, 코드 블록을 기술적 텍스트와 쌍으로 묶어 증명과 그 동기 사이의 연결을 보존한다.
   • 섹션 단위 청킹 (Section-Level Chunking): 다른 모듈의 경우, 더 작고 독립적인 섹션을 사용한다.
   • 의존성 복구 (Dependency Recovery): 증명 지향적 모듈의 경우, 시스템은 검색된 파편이 유효하기 위해 필요한 선행 정의 및 타입 클래스 컨텍스트를 식별하고 포함하도록 구문 인식 복구를 수행한다.

3. 검색 증강 생성 (RAG):
   각 불변량에 대해, 프레임워크는 비형식적 스케치(진술, 직관, 결론)를 기반으로 검색 쿼리를 구성한다. 시스템은 라이브러리 특유의 정의, 가정 및 증명 패턴을 LLM에 제공하기 위해 처리된 코퍼스에서 관련 문서 파편과 증명 예시를 검색한다.

4. 단계별 스켈레톤 생성 (Staged Skeleton Generation):
   프레임워크는 구조 생성과 증명 생성을 분리한다. LLM은 먼저 각 불변량에 대한 구조적으로 유효한 스켈레톤을 생성한다.

   • 규칙: 모든 증명을 포함하는 구성 요소(레마/정리)는 지연된 의무(Admitted.)와 함께 생성되며, 증명을 포함하지 않는 구성 요소(정의)는 완전히 명시된다.
   • 무결성: 시스템은 모델이 주장을 뒷받ền되지 않은 가정으로 바꾸는 것을 방지하기 위한 규칙을 강제한다.
   • 검증: 스켈레톤은 다음 단계로 넘어가기 전, 타입 정확성과 구조적 유효성을 검증하기 위해 coqc로 컴파일된다.

5. 반복 수정을 통한 증명 완성 (Proof Completion with Iterative Repair):
   유효한 스켈레톤이 확립되면, LLM은 지연된 Admitted. 의무를 해소하도록 유도된다. 이 단계에서는 **반복 수정(iterative repair)**을 활용한다. 만약 생성된 증명이 컴파일에 실패하면, 컴파일러 에러 메시지가 LLM에 피드백되어 수정을 유도한다. **증명 무결성 검사기(proof-integrity checker)**는 모델이 지원되지 않은 공리(axiom)를 도입하거나 새로운 전역 정의로 책임을 전가함으로써 증명 의무를 우회하지 않도록 보장한다.

주요 기여

1. PROVE-RT 프레임워크: PROSA/ROCQ에서 RTS 스케줄링 가능성 분석의 기계화를 구체적으로 겨냥한 최초의 LLM 지원 프레임워크이다. 이는 스케칭, 스켈레톤 생성, 증명 완성을 결합한 단계적 접근 방식과 의존성 인식 검색을 도입한다.
2. 시스템 불변량 데이터셋: 1,191개의 실시간 시스템 논문에서 추출된, 명시적인 의존성 정보를 포함한 13,134개의 비형식적 스케치로 구성된 대규모 코퍼스를 구축하였다. 이 데이터셋은 기계화 도구의 학습 및 평가를 위한 도메인 특화 데이터의 심각한 부족 문제를 해결한다.
3. 실험적 분석을 통한 과제 규명: LLM 기반 기계화의 실패 모드를 상세히 연구하여, 직접적인 프롬프팅의 불충분함과 검색 가이드 및 의존성 순서의 필요성을 강조하였다.

실험 결과

프레임워크는 다양한 스케줄링 가능성 분석 카테고리(예: 응답 시간 분석, EDF, FIFO)를 나타내는 300개의 선별된 비형식적 스케치에 대해 평가되었다.

• 베이스라인 성능: 최첨단 LLM(GPT-5, Claude-Opus-4.6)의 직접적인 프롬프팅은 유효한 PROSA 스크립트를 안정적으로 생성하는 데 실패했다. GPT-5는 **0.0%**의 성공률을 기록했고, Claude-Opus-4.6은 단 **0.33%**만을 달성했다. 주목할 점은, 베이스라인의 많은 "성공적인" 컴파일 사례들이 PROSA 라이브러리를 활용하지 않고 일반적인 ROCQ 코드만을 생성했다는 것이다.
• PROVE-RT 성능: 밀집 검색(dense retrieval, semantic embeddings)을 사용했을 때, PROVE-RT는 **44.7%**의 성공률(300개 스케치 중 134개 완전 기계화)을 달성했다.
  • BM25 검색은 42.0%를 달성했다.
  • 하이브리드 검색은 41.0%를 달성했다.
• 복잡도의 영향: 스케치 내의 섹션 수(의존성 깊이)가 증가함에 따라 성공률이 감소하였으며, 이는 긴 의존성 체인이 여전히 중요한 과제임을 나타낸다. 그러나 PROVE-RT는 여러 개의 다중 섹션 스케치를 성공적으로 기계화함으로써 비사소한 의존성 구조를 처리할 수 있음을 입증했다.
• 검색 효용성: 밀집 검색은 특히 정의(definitions)에 대해 엔드 투 엔드 성공에 가장 효과적이었던 반면, 희소(BM25) 및 하이브리드 방식은 증명 대상 구성 요소에 대한 정확한 레마 이름 및 식별자를 검색하는 데 강점을 보였다.

의의 및 주장

본 논문은 검색 가이드 및 단계적 LLM 지원이 직접적인 프롬프팅에 비해 스케줄링 가능성 분석의 자동 기계화를 크게 향상시킬 수 있음을 PROVE-RT를 통해 입증한다고 주장한다. 의존성 인식 스케칭, 스켈레톤 생성, 반복적 증명 수정을 통해 작업을 분해함으로써, 프레임워크는 비형식적 문헌과 엄격한 정리 증명 사이의 정형화 격차를 극복한다.

저자들은 PROVE-RT를 인간의 노력을 완전히 제거하는 완전한 솔루션이 아니라, 실시간 시스템의 기계화된 검증에 대한 진입 장로를 낮추는 중요한 단계로 정의한다. 구축된 데이터셋은 LLM 지원 정형화를 위한 이 분야의 향후 연구를 촉진할 핵심 자원으로 강조된다. 또한, 본 연구는 생성형 AI가 생성한 스케줄링 가능성 분석을 검증하기 위해 이러한 프레임워크를 사용할 수 있는 잠재력을 제시하며, 이를 통해 안전 필수 도메인에서의 생성형 AI에 대한 신뢰 계층을 추가한다.