Can Large Language Models Model Programs Formally?
본 논문은 자동화된 프로그램 모델링의 어려움을 해결하기 위해 Python 프로그램을 모델 체킹 사양으로 변환하는 벤치마크 'Model-Bench'와 파이프라인을 제안하고, 이를 통해 대규모 언어 모델 (LLM) 의 프로그램 모델링 능력에 존재하는 한계를 실증적으로 규명합니다.
현재 상황: 우리가 쓰는 소프트웨어 (앱, 웹사이트 등) 에는 항상 '버그 (오류)'가 숨어 있을 수 있습니다. 기존에 개발자들이 하는 '테스트'는 "버그가 있는지 찾아내는 것"은 잘하지만, "이 프로그램에 절대 버그가 없다"는 것을 100% 증명하는 것은 불가능에 가깝습니다.
해결책 (형식적 검증): 이를 위해 '형식적 검증 (Formal Verification)'이라는 방법이 있습니다. 이는 프로그램을 수학적 논리로 변환하여 "이 프로그램이 어떤 상황에서도 절대 망가지지 않는다"는 것을 기계가 증명하는 방식입니다.
두 가지 방법:
정리 증명 (Theorem Proving): 수학 공리를 이용해 논리적으로 증명하는 것 (최근 AI 가 잘함).
모델 검사 (Model Checking): 프로그램의 모든 가능한 상황을 나열해서 하나하나 확인하는 것 (이게 더 어려움).
핵심 문제: 모델 검사를 하려면 먼저 복잡한 파이썬 코드를 **수학적으로 읽을 수 있는 '모델 (청사진)'**로 바꿔야 합니다. 하지만 이 '번역' 작업이 너무 어려워서 AI 가 잘 못 해냈습니다.
🧪 2. 연구 내용: '모델 벤치 (Model-Bench)'란 무엇인가요?
저희 연구팀은 이 난관을 해결하기 위해 **'모델 벤치 (Model-Bench)'**라는 새로운 시험지를 만들었습니다.
시험지 구성: 유명한 코딩 문제집 (HumanEval 등) 에서 가져온 400 개의 파이썬 프로그램을 준비했습니다.
과제: AI(대형 언어 모델) 에게 "이 파이썬 코드를 **TLA+**라는 특수한 수학 언어로 바꿔줘"라고 시켰습니다.
비유: AI 에게 "이 복잡한 한국 드라마 대본을, 모든 등장인물의 행동을 수학 공식으로 바꿔서 써봐"라고 시킨 것과 같습니다.
평가: 바뀐 수학 공식이 실제로 작동하는지, 그리고 원래 코드와 같은 행동을 하는지 TLC라는 검사 도구로 확인했습니다.
🔍 3. 실험 결과: AI 는 잘할까요?
결과는 아직은 부족하지만, 희망적인 방향을 보여줍니다.
📉 1) AI 의 한계 (현실)
AI 가 만든 수학 모델 중 약 66% 만이 실제로 작동했습니다. (나머지는 문법 오류나 논리 오류가 있었습니다.)
작동하더라도, 원래 프로그램과 행동이 100% 일치하는 경우는 50% 미만이었습니다.
비유: AI 가 만든 청사진은 "집이 무너지지 않을 것 같다"는 정도는 맞지만, "창문 위치가 원래 설계도와 1cm 도 틀렸다"는 식의 미세한 오류가 많았습니다.
🚀 2) 해결책: "코드 변환 (Code Transformation)"
AI 가 원본 코드를 직접 번역하는 것보다, 코드를 AI 가 이해하기 쉬운 형태로 미리 변형해 주면 훨씬 잘했습니다.
비유: AI 에게 "복잡한 고층 빌딩 설계도"를 바로 번역하게 하면 헷갈려 하지만, "단순한 블록 쌓기 놀이"로 변형된 설계도를 주면 훨씬 정확하게 번역합니다.
이 방법을 쓰면 AI 가 만든 모델의 정확도 (유사도) 가 18% 이상 향상되었습니다.
📊 3) 어떤 코드가 hardest?
코드가 어렵다고 해서 AI 가 못 하는 건 아니었습니다.
오히려 **중첩된 반복문 (for 문 안에 for 문)**이나 데이터 구조가 복잡한 코드일수록 AI 가 혼란을 겪었습니다.
비유: "100 번 반복해서 계단 오르기"는 AI 가 잘하지만, "계단 오르는 도중 갑자기 방향을 바꾸고, 계단 높이가 변하는 미로"를 그리게 하면 AI 는 길을 잃습니다.
💡 4. 결론 및 시사점
이 논문은 다음과 같은 중요한 메시지를 전달합니다.
AI 는 아직 완벽하지 않다: 현재 AI 는 복잡한 프로그램을 수학적으로 완벽하게 모델링하기엔 부족합니다.
도움이 되는 방법: AI 에게 코드를 번역하게 할 때, 코드를 단순화하거나 변형해 주는 전처리 과정이 필수적입니다.
미래 전망: 이 연구는 AI 가 소프트웨어의 안전성을 수학적으로 보장하는 '형식적 검증' 분야에서 중요한 첫걸음입니다. 앞으로 AI 가 더 똑똑해지면, 우리가 만든 앱이나 자율주행차, 의료 장비 등이 수학적으로 100% 안전하다는 것을 AI 가 자동으로 증명해 줄 날이 올 것입니다.
한 줄 요약:
"AI 가 복잡한 프로그램을 수학적으로 증명하는 건 아직 '어린 건축가'가 '고층 빌딩'을 설계하는 것과 비슷해 헛수고를 많이 하지만, 설계도를 단순화해 주면 훨씬 더 안전하고 정확한 청사진을 그려낼 수 있다는 것을 발견했습니다."
1. 문제 정의 (Problem)
소프트웨어의 정확성, 안전성, 신뢰성을 보장하기 위해 **형식적 검증 (Formal Verification)**이 필수적입니다. 형식적 검증은 주로 **정리 증명 (Theorem Proving)**과 **모델 체킹 (Model Checking)**으로 나뉩니다.
현재 상황: 최근 LLM 을 활용한 정리 증명 (자동 형식화, 증명 생성 등) 은 괄목할 만한 진전을 이루었습니다.
한계: 반면, 모델 체킹 분야는 자동화된 프로그램 모델링의 어려움으로 인해 상대적으로 소홀히 다루어졌습니다.
핵심 과제: Python 과 같은 동적 언어의 복잡한 런타임 동작 (가변 별칭, 고차 함수, 비동기 처리 등) 을 유한하지만 충실한 상태 공간 (State Space) 으로 추상화하여, 모델 체커가 검증 가능한 TLA+ (Temporal Logic of Actions) 명세로 변환하는 작업은 기술적으로 매우 어렵고 연구가 부족합니다.
2. 방법론 (Methodology)
저자들은 이 격차를 해결하기 위해 Model-Bench라는 벤치마크와 평가 파이프라인을 제안했습니다.
가. 벤치마크 구축 (Model-Bench Construction)
데이터 소스: HumanEval, MBPP, LiveCodeBench 등 3 개의 잘 알려진 Python 벤치마크에서 400 개의 프로그램을 선별했습니다.
데이터 전처리:
정제 및 단순화: TLA+ 로 표현하기 어려운 복잡한 라이브러리 (typing, math 제외), 클래스, 람다, 제너레이터 등을 제거하거나 LLM 을 통해 재작성했습니다.
타입 필터링: TLA+ 표현이 어려운 복잡한 타입을 가진 변수를 제외했습니다.
실행 검증: 필터링된 코드가 실제로 실행되고 테스트 케이스를 통과하는지 확인했습니다.
코드 변환 (Code Transformation):
Python 코드를 TLA+ 의 상태 머신 구조에 더 가깝게 변환하는 전처리 과정을 도입했습니다.
**제어 흐름 그래프 (CFG)**를 생성하고, 이를 pc(프로그램 카운터) 변수를 사용하는 while 루프 기반의 상태 전이 코드로 변환하여 LLM 이 패턴을 인식하기 쉽게 만들었습니다.
나. 평가 지표 (Evaluation Metrics)
생성된 TLA+ 모델의 품질을 평가하기 위해 두 가지 주요 지표를 사용했습니다.
Runnable@k: 생성된 k개의 모델 중 TLC 모델 체커를 통해 오류 없이 실행 가능한 모델의 비율.
State Similarity (상태 유사도): LLM 이 생성한 모델의 실행 궤적 (State Trace) 과 오라클 (참조) 모델의 실행 궤적이 얼마나 일치하는지를 측정합니다. 생성된 모델의 모든 상태 변수 값이 오라클 모델의 상태에 포함되어야만 매칭으로 간주합니다.
다. 실험 설정
다양한 LLM (DeepSeek-V3, Qwen3, Llama, Gemma 등) 을 대상으로 Few-shot 및 Zero-shot 프롬프트 설정에서 실험했습니다.
원본 Python 코드와 변환된 (Transformed) Python 코드를 입력으로 사용하여 성능을 비교했습니다.
3. 주요 기여 (Key Contributions)
Model-Bench 제안: Python 프로그램을 검증 준비가 된 TLA+ 명세로 변환하는 능력을 평가하기 위한 최초의 범용 벤치마크와 파이프라인을 구축했습니다.
코드 변환 기법 도입: LLM 의 모델링 능력을 향상시키기 위해 Python 코드를 TLA+ 스타일의 상태 머신 구조로 변환하는 전처리 기법을 제안하고 그 유효성을 입증했습니다.
포괄적인 평가 및 통찰: 다양한 LLM 에 대한 광범위한 실험을 통해 모델링의 한계를 규명하고, 향후 개선을 위한 구체적인 방향성을 제시했습니다.
4. 실험 결과 (Results)
전체 성능:
최상위 모델 (DeepSeek-V3) 이 Few-shot 설정에서 Runnable@1 약 51.75%, **상태 유사도 약 49.55%**를 기록했습니다.
Zero-shot 설정에서는 대부분의 모델이 0% 에 가까운 성능을 보였으며, Few-shot 학습이 성능 향상에 결정적인 역할을 했습니다 (Runnable@1 평균 17.57% 향상).
코드 변환의 효과:
변환된 코드를 입력으로 사용하면 Runnable@k 는 약간 감소했으나, 상태 유사도는 크게 향상되었습니다 (예: DeepSeek-V3 의 경우 유사도 18.99% 증가).
이는 변환된 코드가 LLM 이 TLA+ 의 논리적 구조를 더 잘 이해하도록 돕지만, 코드 길이 증가로 인한 '중간 정보 손실 (lost in the middle)' 현상이 발생할 수 있음을 시사합니다.
두 프롬프트 설정 (원본 + 변환) 을 결합하면 전체 실행 가능한 모델 수를 늘릴 수 있는 보완적 효과가 있음이 확인되었습니다.
복잡도와의 상관관계:
모델링 성공률은 알고리즘의 난이도보다는 구문적 복잡도 (순환 복잡도, 중첩 루프 깊이, 변수 수) 와 더 밀접하게 연관되어 있었습니다. 복잡도가 높을수록 성능이 급격히 저하되었습니다.
오류 분석 (Bad Case Analysis):
컴파일 오류: Python 의 내장 함수 (예: sort) 를 TLA+ 에 없는 연산자로 잘못 매핑하는 경우.
런타임 오류: TLA+ 의 1 기반 인덱싱과 Python 의 0 기반 인덱싱 차이로 인한 배열 접근 오류.
어설션 오류: 함수 호출 (lower()) 생략이나 상수 루프 횟수 사용 등 논리적 충실도 부족.
5. 의의 및 결론 (Significance)
형식적 검증의 자동화: LLM 이 소스 코드에서 직접 모델 체킹 명세를 생성할 수 있는지에 대한 체계적인 평가를 제공하여, 자동화된 형식적 검증 분야의 발전을 촉진합니다.
향후 방향: 현재 LLM 은 복잡한 프로그램의 추상화와 TLA+ 문법 준수에 여전히 한계가 있음을 보여주었습니다. 특히 중첩 루프와 데이터 구조가 복잡한 프로그램에 대한 모델링 능력 향상이 필요하며, 코드 변환 기법과 Few-shot 학습의 결합이 효과적인 전략임을 입증했습니다.
확장성: 제안된 벤치마크와 파이프라인은 다른 프로그래밍 언어와 형식 명세 언어로 확장 가능하여, 소프트웨어 공학 및 형식 방법 연구 커뮤니티에 중요한 기반을 제공합니다.
이 논문은 LLM 이 단순히 코드를 생성하는 것을 넘어, 형식적 검증이 가능한 고수준의 추상 모델을 구축할 수 있는 잠재력과 한계를 명확히 규명한 중요한 연구입니다.