FM-Agent: Scaling Formal Methods to Large Systems via LLM-Based Hoare-Style Reasoning

이 논문은 대규모 시스템의 정형 검증을 위해 LLM 을 활용해 상위 수준 의도를 자연어 명세로 자동 생성하고 이를 통해 컴포지셔널 추론을 수행하며 14 만 줄 이상의 코드에서 522 개의 새로운 버그를 발견한 'FM-Agent'프레임워크를 제안합니다.

핵심

FM-Agent: 거대 소프트웨어를 위한 'AI 감식관'의 등장

이 논문은 **"LLM(거대 언어 모델) 이 만든 거대한 소프트웨어 프로그램에 숨겨진 버그를 찾아내는 새로운 방법"**을 소개합니다. 제목인 FM-Agent는 'Formal Methods(형식적 방법론)'와 'Agent(에이전트)'의 합성어입니다.

이 복잡한 기술을 일상적인 비유로 쉽게 설명해 드리겠습니다.

---

1. 문제 상황: "AI 가 만든 거대한 도시"

최근 AI 가 코드를 작성해 주는 시대가 왔습니다. AI 는 수만 줄에 달하는 거대한 소프트웨어 (컴파일러, 운영체제 등) 를 단숨에 만들어냅니다. 하지만 AI 가 만든 코드는 때로 환각 (Hallucination) 현상이 일어나, 논리적으로 틀린 코드를 포함할 수 있습니다.

• 비유: AI 가 100 개 층짜리 거대한 빌딩을 단숨에 지어냈다고 상상해 보세요. 하지만 AI 는 건물의 내부 구조를 완벽히 이해하지 못해, 전선이 잘못 연결되거나 계단이 사라진 곳이 있을 수 있습니다.
• 과거의 한계: 기존에 이 빌딩의 안전을 검사하려면, 각 방마다 "이 방은 이렇게 만들어져야 한다"는 **엄격한 설계도 (명세)**를 사람이 직접 그려야 했습니다. 하지만 AI 가 만든 빌딩은 너무 크고 복잡해서, 사람이 모든 방의 설계도를 일일이 그릴 시간이 없습니다.

2. 해결책: FM-Agent 의 '상향식'이 아닌 '하향식' 접근

이 논문에서 제안하는 FM-Agent는 이 문제를 해결하기 위해 세 가지 핵심 아이디어를 사용합니다.

① "사용자의 눈으로 보기" (Top-Down Paradigm)

기존 방법은 "코드를 보고 이 코드가 무엇을 하는지 추측"하는 방식이었습니다. 하지만 코드가 버그가 있다면 추측도 틀립니다.

• FM-Agent 의 방법: "이 기능을 **사용하는 사람 (호출자)**은 이 기능이 어떻게 작동하기를 원할까?"를 먼저 생각합니다.
• 비유: 식당에 주문을 넣는 손님 (호출자) 은 "이 요리는 반드시 익혀져서 나와야 한다"고 기대합니다. 요리사 (함수) 가 실수로 생선을 반쯤 익혀서 내더라도, 손님의 기대 (설계도) 는 "완전히 익은 생선"입니다. FM-Agent 는 손님의 기대를 기준으로 요리사의 실수를 찾아냅니다. 코드가 잘못되어도 손님의 기대는 변하지 않기 때문에 버그를 정확히 찾을 수 있습니다.

② "자연어로 대화하는 검사관"

기존의 형식적 검증 도구는 복잡한 수학적 공식만 이해했습니다. 하지만 개발자의 의도는 보통 자연어로 표현됩니다.

• FM-Agent 의 방법: AI 가 코드를 읽으면서 "이 줄을 실행하면 결과가 어떻게 될까?"를 자연어로 추론합니다.
• 비유: 수학 공식만 아는 검사관 대신, 코딩을 잘하는 형사를 고용한 것입니다. 이 형사는 "이 코드를 실행하면 A 라는 결과가 나와야 하는데, 실제로는 B 가 나오네? 여기가 문제군!"이라고 자연스러운 언어로 버그를 지적합니다.

③ "실제 실험으로 증명하기"

이론상 버그가 있다고 해서 무조건 버그는 아닙니다. AI 가 착각했을 수도 있으니까요.

• FM-Agent 의 방법: "이 부분이 문제일 것 같아"라고 의심되면, 실제로 그 상황을 만들어내는 테스트 코드를 자동으로 작성하고 실행해 봅니다.
• 비유: 형사가 "여기서 폭발할 것 같다"고 의심하면, 실제로 폭탄을 설치해 보지는 않고 (위험하니까), 시뮬레이션을 돌려서 "아, 실제로 터지네!"라고 확인한 후에만 "여기가 문제다"라고 보고합니다.

3. 실제 성과: "이미 검사받았다고 생각했던 빌딩에서 522 개의 결함 발견"

연구진은 AI 가 만든 4 개의 거대 시스템 (컴파일러, 운영체제, 데이터베이스 등, 최대 14 만 줄의 코드) 에 FM-Agent 를 적용했습니다.

• 결과: 개발자들이 이미 다양한 방법으로 테스트를 끝냈다고 믿었던 시스템에서 새로운 버그 522 개를 찾아냈습니다.
• 위험성: 이 버그들은 시스템이 멈추거나 (Crash), 잘못된 결과를 내거나, 메모리를 손상시키는 심각한 문제들이었습니다.
• 속도: 이 모든 작업을 2 일 만에 완료했습니다.

4. 핵심 요약: 왜 이것이 중요한가?

이 논문은 **"AI 가 만든 거대한 소프트웨어를 사람이 일일이 검사할 수 없을 때, AI 가 스스로 '손님의 기대'를 기준으로 코드를 분석하고, 버그를 찾아내어 실제로 증명하는 시스템"**을 보여줍니다.

• 기존: 사람이 설계도를 그려야만 검사가 가능함 (너무 느리고 비쌈).
• FM-Agent: AI 가 "손님이 원하는 것"을 먼저 정의하고, 코드가 그 기대에 부합하는지 자연어로 추론하며, 의심되면 직접 테스트를 돌려 확인함.

이 기술은 AI 가 코드를 작성하는 시대에, 신뢰할 수 있는 소프트웨어를 만들기 위한 필수적인 안전장치가 될 것으로 기대됩니다. 마치 AI 가 지은 거대한 빌딩에, AI 가 스스로 안전 점검을 하고 "여기 벽이 약합니다"라고 알려주는 자동화된 안전 감시관과 같습니다.

기술 요약

1. 문제 정의 (Problem Statement)

대규모 시스템의 자동화된 소프트웨어 개발 (LLM 기반 코드 생성 포함) 이 보편화됨에 따라, 생성된 코드의 정확성을 보장하는 것이 중요해졌습니다. 그러나 기존 자동화 추론 기술은 다음과 같은 한계로 인해 대규모 시스템에 적용하기 어렵습니다.

• 코드 복잡성: 대규모 시스템은 복잡한 제어 흐름, 상태 조작, 깊은 절차 간 의존성을 포함하여 기존 기법들이 확장 (Scale) 되지 못합니다.
• 명세 작성의 부담: 호어 논리 (Hoare Logic) 와 같은 구성적 추론 (Compositional Reasoning) 은 함수별 정형 명세 (Formal Specification) 가 필요합니다. 하지만 대규모 시스템에서는 이를 수동으로 작성하는 데 막대한 노력이 듭니다.
• LLM 생성 코드의 특성: LLM 이 생성한 코드는 개발자가 직접 작성하지 않았기 때문에 개발자가 각 함수의 의도된 동작을 깊이 이해하기 어렵고, 구현체에 버그가 포함되어 있을 경우 구현체 기반 명세 생성은 오작동을 유발할 수 있습니다.
• 자연어 vs 정형 논리: 개발자의 의도는 자연어로 표현되지만, 기존 검증 도구는 정형 논리 (수식) 만 지원합니다.

2. 방법론 (Methodology)

이 논문은 대규모 시스템을 위한 자동화된 구성적 추론을 가능하게 하는 프레임워크 FM-Agent를 제안합니다. LLM 을 활용하여 함수 수준의 명세를 자동 생성하고, 이를 기반으로 호어 스타일 추론을 수행합니다.

핵심 통찰 (Key Insights)

1. 상향식 (Bottom-up) 이 아닌 하향식 (Top-down) 접근: 구현체 분석이 아닌, 호출자 (Caller) 가 기대하는 동작을 기반으로 명세를 생성합니다. 이를 통해 구현체의 버그에 영향을 받지 않고 개발자의 의도 (Design Intent) 를 반영할 수 있습니다.
2. 자연어 기반 추론: LLM 은 코드 의미론과 자연어를 모두 이해하므로, 정형 수식이 아닌 자연어 명세에 대해 호어 논리 추론을 확장하여 수행할 수 있습니다.
3. 시스템 진입점 기반 테스트 생성: LLM 은 시스템 전체의 입력과 내부 함수 동작 간의 상관관계를 파악하여, 버그를 유발하는 시스템 수준의 테스트 케이스를 생성할 수 있습니다.

FM-Agent 워크플로우

FM-Agent 는 크게 세 가지 구성 요소로 이루어져 있습니다.

1. 명세 생성기 (Specification Generator):

   • 하향식 패러다임: 시스템 진입 함수 (Entry Function) 부터 시작하여 호출 그래프를 따라 하향식으로 명세를 생성합니다.
   • 기대 명세 (Expected Specification): 호출자가 피호출 함수에 대해 기대하는 전조건 (Pre-condition) 과 후조건 (Post-condition) 을 분석하여 생성합니다.
   • 병렬 처리: 호출 그래프를 분석하여 독립적인 레이어 (Layer) 를 식별하고, 각 레이어 내 함수들의 명세를 동시에 생성하여 확장성을 확보합니다.
   • 소스: 구현체, 호출자의 기대 동작, 도메인 지식 (예: C 표준) 을 종합하여 명세를 작성합니다.

2. 코드 추론기 (Code Reasoner):

   • 자연어 호어 추론: 생성된 자연어 명세와 함수 구현체를 비교합니다.
   • 단계별 추론: 함수의 전조건에서 시작하여 각 문장 (Statement) 또는 코드 블록에 대해 LLM 을 이용해 후조건을 유추합니다.
   • 일치성 검증: 최종 실행 경로의 후조건이 명세의 후조건을 함의 (Entail) 하는지 확인합니다. 불일치가 발견되면 잠재적 버그로 보고합니다.

3. 버그 검증기 (Bug Validator):

   • 테스트 생성: 잠재적 버그가 발견되면, LLM 을 활용해 해당 버그를 유발하는 시스템 진입점 (System-entry) 테스트 케이스를 생성합니다.
   • 실행 및 확인: 생성된 테스트를 시스템에 실행하여 버그가 실제로 발생하는지 확인합니다. (허위 양성 (False Positive) 을 줄이기 위해 재시도 횟수 제한 등을 적용합니다.)

3. 주요 기여 (Key Contributions)

• 최초의 자동화된 구성적 추론 프레임워크: 대규모 시스템 (최대 143k LoC) 에 대해 자동화된 호어 스타일 추론을 수행하는 첫 번째 프레임워크를 제시했습니다.
• 하향식 명세 생성 패러다임: 구현체 분석이 아닌 호출자 관점에서의 기대 동작을 기반으로 명세를 생성하여, 구현체의 버그에 덜 민감하고 개발자의 의도를 정확히 반영하는 명세를 생성합니다.
• 자연어 기반 추론 확장: 기존 검증 도구가 정형 수식에만 의존하던 한계를 극복하고, LLM 을 활용하여 자연어 명세에 대한 호어 논리 추론을 가능하게 했습니다.
• 시스템 수준 테스트 생성: 내부 함수 버그를 유발하는 구체적인 시스템 입력을 자동 생성하여 버그의 근본 원인을 명확히 하고 수정을 돕습니다.

4. 평가 결과 (Evaluation Results)

FM-Agent 는 다양한 프로그래밍 언어 (C, Rust, Python 등) 로 작성된 4 개의 대규모 LLM 생성 시스템 (CCC, VibeTensor, VibeOS, Bespoke OLAP) 에 대해 평가되었습니다.

• 규모: 총 277k LoC, 8,549 개의 함수를 포함하는 시스템을 2 일 이내에 분석했습니다.
• 버그 발견: 기존 개발자가 다양한 테스트 (단위 테스트, 통합 테스트, 다중 에이전트 코드 리뷰 등) 를 거쳤음에도 불구하고, 총 522 개의 새로운 버그를 발견했습니다.
  • CCC (C 컴파일러): 339 개 발견 (IR 레벨 오류, 런타임 오류, 컴파일 충돌 등).
  • VibeTensor (ML 프레임워크): 141 개 발견 (메모리 누수, 잘못된 텐서 값 등).
  • VibeOS (운영체제): 23 개 발견 (메모리 손상, 무한 루프 등).
  • Bespoke OLAP (데이터베이스): 19 개 발견 (쿼리 결과 오류, 프로세스 충돌 등).
• 심각성: 발견된 버그 중에는 시스템 충돌, 잘못된 실행 결과, 메모리 손상 등 심각한 결과를 초래할 수 있는 것들이 다수 포함되어 있었습니다.
• 확장성: 기존 검증 도구 (Symbolic Execution, Verus 등) 는 이러한 대규모 시스템에 적용이 불가능했으나, FM-Agent 는 병렬 처리를 통해 확장 가능한 성능을 입증했습니다.

5. 의의 및 결론 (Significance)

• LLM 시대 소프트웨어 신뢰성: LLM 이 생성한 코드의 정확성을 검증할 수 있는 실용적인 방법을 제공하여, 대규모 자동화 개발의 신뢰성을 높이는 데 기여합니다.
• 형식 방법의 대중화: 수동 명세 작성이라는 큰 장벽을 LLM 이 자동화함으로써, 형식 방법 (Formal Methods) 을 대규모 시스템에 적용하는 새로운 길을 열었습니다.
• 검증과 테스트의 결합: 추론 (Reasoning) 을 통해 테스트가 놓칠 수 있는 심층적인 버그를 발견하고, 이를 검증 가능한 테스트 케이스로 변환하여 개발자가 수정할 수 있도록 돕습니다.
• 향후 방향: 현재 순차적 프로그램에 국한되어 있으나, 동시성 프로그램 (Concurrency) 지원 및 기존 정형 검증 도구와의 통합을 통해 시스템 신뢰성을 더욱 강화할 수 있는 잠재력을 가지고 있습니다.

요약하자면, FM-Agent는 LLM 의 능력을 활용하여 대규모 시스템의 복잡한 명세 작성과 추론 과정을 자동화함으로써, 기존에는 검증이 불가능했던 차원의 소프트웨어 버그를 발견하고 시스템의 신뢰성을 획기적으로 높인 획기적인 연구입니다.