Proof Strategy Extraction from LLMs for Enhancing Symbolic Provers

이 논문은 대형 언어 모델 (LLM) 의 증명 전략을 추출하여 Rocq(구 Coq) 의 기호적 증명기 (CoqHammer) 에 적용하는 'Strat2Rocq'를 제안함으로써, 자동 증명 성공률을 13.41% 향상시키고 추출된 레마가 LLM 증명 에이전트의 성능도 개선한다는 것을 보여줍니다.

핵심

🎬 영화 한 편으로 이해하기: "명탐정 vs. 천재 작가"

이 문제를 해결하기 위해 두 명의 캐릭터를 상상해 보세요.

1. 전통적인 증명 프로그램 (CoqHammer):

   • 성격: 아주 꼼꼼하고 논리적이지만, **계산 속도가 느리고 규칙만 따르는 '명탐정'**입니다.
   • 약점: 복잡한 문제를 풀 때, 아주 작은 단계부터 하나하나 차근차근 추리해야 합니다. 때로는 "이런, 이걸 증명하려면 induction(수학적 귀납법) 이 필요한데 나는 그걸 못 해!"라고 포기해 버리기도 합니다.
   • 장점: 보안이 완벽하고, 인터넷 없이도 내 컴퓨터에서 무료로, 빠르게 작동합니다.

2. 대형 언어 모델 (LLM):

   • 성격: 수만 권의 책을 읽은 천재 작가입니다.
   • 약점: 아주 똑똑해서 "아, 이 문제는 이렇게 풀면 되겠네!" 하고 직관적으로 답을 말해줍니다. 하지만, 그 답을 증명하는 과정을 하나하나 논리적으로 보여주기엔 실수가 많고, 컴퓨터 리소스를 많이 먹으며, 기밀 정보가 유출될 위험이 있습니다.

🚀 이 연구의 핵심 아이디어: "명탐정에게 천재 작가의 '비법 노트'를 주자!"

기존에는 천재 작가 (LLM) 가 직접 문제를 풀게 하거나, 명탐정 (전통 프로그램) 이 혼자 끙끙 앓게 했습니다. 하지만 이 연구는 **"천재 작가의 머릿속에 있는 '직관적인 해법'을 추출해서, 명탐정이 사용할 수 있는 '비법 노트 (Lemma)'로 만들어주자"**고 제안합니다.

🛠️ Strat2Rocq(스트랫 -2- 로크) 의 작동 원리

이 시스템은 크게 두 단계로 나뉩니다.

1 단계: 오프라인 학습 (비법 노트 만들기)

• 천재 작가 (LLM) 에게 수천 개의 수학 문제를 보여줍니다.
• 작가가 "이 문제는 A, B, C 순서로 풀면 돼!"라고 자연어 (말) 로 설명하게 합니다.
• 연구진은 이 설명을 분석해서, "A+B=C 라는 공식을 쓰면 바로 해결된다!" 같은 **핵심 공식 (Lemma)**을 찾아냅니다.
• 이 공식들을 명탐정이 이해할 수 있는 **공식 언어 (Rocq)**로 번역하여 '비법 노트'에 적어둡니다.
  • 비유: 천재 작가가 "이 문제는 '삼각형의 내각의 합은 180 도'라는 법칙만 알면 1 초 만에 풀린다"고 말하면, 우리는 그 법칙을 명탐정에게 주는 '비법 카드'로 만듭니다.

2 단계: 온라인 증명 (실전 적용)

• 이제 새로운 문제가 생겼을 때, **명탐정 (CoqHammer)**만 사용합니다. (천재 작가는 필요 없습니다!)
• 명탐정은 문제 풀이를 시작하기 전에, 우리가 미리 만들어둔 **'비법 노트'**를 펼쳐봅니다.
• "아! 이 문제는 'power_1'이라는 공식을 쓰면 바로 해결되네!"라고 생각하며, 복잡한 추리 없이 순식간에 문제를 해결합니다.

📊 결과는 어땠나요?

• 성공률 상승: 명탐정 (CoqHammer) 이 혼자 풀 때보다 약 13.4% 더 많은 문제를 성공적으로 풀었습니다.
• 보안과 비용: 천재 작가 (LLM) 를 실시간으로 부르지 않아도 되므로, 비용이 절감되고 보안 위험도 사라집니다.
• 부수적 효과: 이 '비법 노트'를 다시 천재 작가에게 주면, 작가의 실력도 4% 정도 더 좋아졌습니다. 서로의 장점을 공유한 셈입니다.

💡 왜 이것이 중요한가요?

지금까지 "AI 가 모든 걸 다 할 거야"라고 생각했지만, 이 연구는 **"AI 의 지혜를 뽑아내어, 우리가 믿고 쓸 수 있는 전통적인 도구 (보안, 비용 효율성) 를 더 강력하게 만들 수 있다"**는 것을 보여줍니다.

마치 천재 요리사 (LLM) 가 알려준 '비밀 레시피'를 받아, 일반 주방장 (전통 프로그램) 이도 고급 요리를 완벽하게 만들어내는 상황과 같습니다.

📝 한 줄 요약

"AI 의 직관적인 해법을 '공식'으로 변환해 전통적인 증명 프로그램에게 주면, 보안과 비용을 지키면서도 훨씬 더 똑똑하게 문제를 풀 수 있다!"

기술 요약

논문 요약: 증강된 심볼릭 증명기를 위한 LLM 증명 전략 추출 (Proof Strategy Extraction from LLMs for Enhancing Symbolic Provers)

이 논문은 대형 언어 모델 (LLM) 의 내부 증명 전략을 추출하여 심볼릭 증명기 (Symbolic Prover) 의 성능을 향상시키는 새로운 연구 방향을 제시합니다. 저자들은 Strat2Rocq이라는 프레임워크를 제안하여, LLM 이 생성한 자연어 증명 과정을 분석하고 이를 Rocq(구 Coq) 형식의 재사용 가능한 보조 정리 (Lemma) 로 변환하는 방법을 고안했습니다.

1. 문제 제기 (Problem)

소프트웨어 검증 분야에서 상호작용 정리 증명 (Interactive Theorem Proving, ITP) 은 중요하지만, 형식적 증명을 작성하는 데에는 막대한 인력이 필요합니다.

• LLM 의 한계: 최근 LLM 은 증명 자동화에서 뛰어난 성능을 보이지만, 고비용, 보안 위험 (비밀 코드베이스 유출), 그리고 하드웨어 제약 (소규모 안전 필수 기업 등) 으로 인해 순수 심볼릭 접근법을 완전히 대체할 수 없습니다.
• 심볼릭 증명기의 한계: 전통적인 심볼릭 증명기는 비용 효율적이고 안전하지만, 복잡한 증명 전략이나 휴리스틱이 부족하여 증명 실패율이 높습니다.
• 연구 질문: "LLM 의 내부 증명 능력을 추출하여 심볼릭 증명기의 능력을 향상시킬 수 있는가?"

2. 방법론 (Methodology: Strat2Rocq)

저자들은 LLM 의 증명 능력을 심볼릭 증명기 (CoqHammer) 가 직접 활용할 수 있도록 **오프라인 (Offline)**과 온라인 (Online) 두 단계로 나누어 접근합니다.

1 단계: 오프라인 보조 정리 마이닝 (Offline Lemma Mining)

훈련 데이터셋 (기존의 증명된 정리들) 을 기반으로 LLM 의 증명 전략을 추출합니다.

1. 자연어 증명 생성 (NL Proof Generation): 각 정리에 대해 LLM 에게 단계별 자연어 증명을 요청합니다. 이때 타입 정의, 함수 정의, 파일 컨텍스트 등을 프롬프트에 포함시켜 LLM 의 추론 과정을 명확히 유도합니다.
2. 일반화 및 형식화 (Generalization & Formalization): 생성된 자연어 증명에서 핵심 추론 단계를 추출하여 일반적인 보조 정리 (Lemma) 로 일반화합니다. 이를 Rocq 언어로 형식화하고, 자동 증명 에이전트 (Proof Agent) 를 통해 해당 보조 정리의 증명을 검증합니다.
   • 핵심 아이디어: LLM 이 특정 단계에서 직접 결론을 도출하는 방식 (예: a+b+c를 c+b+a로 즉시 변환) 을 심볼릭 증명기가 사용할 수 있는 명시적인 정리로 변환합니다.

2 단계: 온라인 정리 증명 (Online Theorem Proving)

새로운 증명 대상 정리가 주어지면, 오프라인 단계에서 추출된 보조 정리들을 증명 컨텍스트에 주입합니다.

• CoqHammer 활용: 추출된 보조 정리들을 컨텍스트에 추가함으로써, CoqHammer 가 LLM 의 내부 지식을 활용하여 더 효과적으로 증명을 시도합니다.
• 효율성 유지: CoqHammer 는 KNN 기반의 보조 정리 선택 메커니즘을 사용하여, 컨텍스트에 추가된 보조 정리의 수가 많아져도 증명 효율성이 떨어지지 않도록 설계되었습니다.

3. 주요 기여 (Key Contributions)

1. 새로운 연구 문제 제안: LLM 의 증명 능력을 오프라인으로 추출하여 심볼릭 증명기를 강화하는 새로운 패러다임을 제시했습니다.
2. Strat2Rocq 프레임워크 개발: LLM 이 생성한 자연어 증명을 분석하여 재사용 가능한 보조 정리를 추출하고, 이를 심볼릭 증명기에 통합하는 구체적인 방법을 구현했습니다.
3. 실증적 검증: 오픈소스 Rocq 프로젝트 (Coq-Art, Ext-Lib, Vfa, CompCert) 를 대상으로 실험하여 방법론의 유효성을 입증했습니다.

4. 실험 결과 (Results)

총 2,394 개의 Rocq 정리를 대상으로 3-폴드 교차 검증을 수행한 결과는 다음과 같습니다.

• 심볼릭 증명기 성능 향상: Strat2Rocq 를 적용한 CoqHammer 는 기존 대비 평균 13.41% 더 많은 정리를 성공적으로 증명했습니다. 특히 CompCert(인증된 C 컴파일러) 에서 17.75% 의 향상 효과를 보였습니다.
  • 성공 요인: 유도 (Induction) 가 필요한 증명에서 LLM 이 추출한 보조 정리를 통해 유도 없이 증명을 완료하거나, 기존에 선택되지 않던 유용한 보조 정리를 효과적으로 선별하는 능력을 향상시켰습니다.
• 다른 LLM 모델 적용성: Claude 3.7 Sonnet 뿐만 아니라 OpenAI o3-mini 와 같은 다른 LLM 에서도 유사한 전략 추출이 가능하며, 서로 다른 LLM 에서 추출한 보조 정리를 결합하면 성능이 더욱 향상됨을 확인했습니다.
• LLM 에이전트 성능 향상: 추출된 보조 정리는 LLM 증명 에이전트 (RAG 모듈 적용) 의 성능도 4.00% 향상시켰으며, 불필요한 LLM 호출을 줄여 토큰 사용량을 감소시켰습니다.
• 추출 방법의 중요성: 자연어 증명 생성 단계를 생략하고 바로 형식화를 시도할 경우, 추출된 보조 정리의 수가 63% 이상 감소하고 성능이 저하되어, 자연어 중간 단계가 필수적임을 입증했습니다.

5. 의의 및 결론 (Significance)

이 연구는 LLM 과 심볼릭 시스템의 상호 보완적 관계를 극대화하는 새로운 길을 제시합니다.

• 보안 및 비용 효율성: LLM 을 실시간으로 호출할 필요 없이, 오프라인에서 추출된 지식만으로 개인 컴퓨터에서도 안전하고 비용 효율적으로 고성능 증명이 가능해집니다.
• LLM 이해의 확장: LLM 의 내부 작동 원리를 심볼릭 모델 (보조 정리) 로 근사화함으로써, LLM 이 어떻게 형식적 증명을 수행하는지에 대한 해석 가능한 통찰을 제공합니다.
• 실용적 가치: 소프트웨어 검증, 특히 보안이 중요한 환경에서 LLM 의 능력을 안전하게 활용하여 증명 자동화 수준을 높이는 데 기여합니다.

요약하자면, Strat2Rocq 는 LLM 의 '직관'을 심볼릭 증명기가 이해할 수 있는 '규칙'으로 변환하여, 두 기술의 장점을 결합한 차세대 증명 자동화 솔루션을 제시합니다.