Goedel-Code-Prover: 오픈 소스 최첨단 코드 검증을 위한 계층적 증명 탐색 (기술 요약)

이 논문은 Lean 4 환경에서 자동화된 코드 검증을 수행하기 위한 새로운 프레임워크인 Goedel-Code-Prover를 제안합니다. 대형 언어 모델 (LLM) 은 코드를 생성할 수 있지만, 그 정확성을 보장하는 데는 한계가 있으며, 형식적 검증 (Formal Verification) 을 위한 기계 검증 가능 증명의 구성은 여전히 자동화의 난제였습니다. 이 연구는 복잡한 검증 목표를 구조적으로 단순한 하위 목표 (subgoals) 로 분해한 후, 전술 (tactic) 수준에서 증명을 수행하는 계층적 증명 탐색 (Hierarchical Proof Search) 프레임워크를 제시합니다.

1. 문제 정의 및 배경

• 코드 검증의 난제: LLM 기반 코딩 에이전트는 단위 테스트 등을 생성하지만, 미묘한 논리적 오류나 명세 불일치를 완전히 배제하지는 못합니다. 형식적 검증은 이를 해결할 수 있으나, 수동으로 증명을 작성하는 것은 매우 노동 집약적이고 전문성이 요구됩니다.
• 기존 방법의 한계: 기존 LLM 기반 증명 시스템 (수학 증명 등) 은 코드 검증에 직접 적용하기 어렵습니다. 그 이유는 다음과 같습니다.
  1. 근거 없는 분해 (Ungrounded Decomposition): 수학 분야에는 풍부한 증명 텍스트 코퍼스가 존재하지만, 프로그램 정확성에 대한 자연어 추론 코퍼스는 부재합니다. 이로 인해 LLM 이 제안하는 하위 목표가 종종 부정확하거나 원래 목표보다 단순하지 않은 경우가 많습니다.
  2. 개념의 팽창 (Concept Proliferation): 수학은 공유된 라이브러리 (Mathlib 등) 를 통해 재사용 가능한 정리를 활용하지만, 프로그램 검증은 각 함수 정의마다 새로운 계산 행동, 제어 흐름, 데이터 구조 불변식을 다루어야 하므로 매번 새로운 개념을 배워야 합니다.
  3. 전술 분포의 이동 (Tactic Distribution Shift): 수학 증명은 대수적 정규화 전술에 의존하는 반면, 코드 검증은 이산적/재귀적 도메인을 다루기 위해 SMT 기반 전술이나 계산적 반영 (computational reflection) 등 프로그램 특화 도구가 필요합니다.

2. 방법론 (Methodology)

2.1 계층적 증명 탐색 프레임워크

프레임워크는 두 단계로 구성됩니다 (그림 2 참조):

1. 재귀적 정리 분해 (Recursive Lemma Decomposition): 상위 검증 목표를 구조적으로 단순한 보조 정리 (lemmas) 로 분해합니다.
2. 정리 완성 (Lemma Completion): 분해된 리프 (leaf) 정리를 반복적인 전술 생성 및 Lean 4 컴파일러 피드백을 통해 증명합니다.

2.2 분해 점수 (Decomposition Score)

이 프레임워크의 핵심은 **원칙적인 분해 점수 (Principled Decomposition Score)**입니다. 이 점수는 학습 보상 (training reward) 과 추론 시 순위 기준 (inference-time ranking criterion) 으로 모두 사용되어 최적화와 배포 간의 정렬을 보장합니다.

• 구성적 정당성 (Constructive Justification): 제안된 하위 목표들이 부모 정리를 논리적으로 함축하는지 확인합니다.
  • Proof Reconstruction: LLM 이 생성한 증명 재구성을 통해 논리적 함축을 검증합니다.
  • Quickcheck: 자동화된 반례 탐색을 통해 제안된 정리가 반례가 없는지 (유효한지) 검증합니다.
• 구조적 효과성 (Structural Effectiveness): 분해가 원래 작업의 난이도를 줄이는지 측정합니다.
  • 연산자 발자국 (Operator Footprint): Lean 의 추상 구문 트리 (AST) 에서 논리 연산자와 프로그램 연산자의 총 출현 수를 계산하여 목표의 복잡도 $d(G)$를 정의합니다. 분해된 하위 목표들의 복잡도가 원래 목표보다 감소하는 정도를 점수화합니다.

2.3 학습 파이프라인 (Hybrid Reinforcement Learning)

분해 (계획) 과 완성 (증명) 을 하나의 통합 정책 (Unified Policy) 으로 학습합니다.

• 초기화: GPT-5.2, Gemini-3-Flash 등 최첨단 모델을 사용하여 분해 및 완성 트래젝토리를 생성하고, Qwen-3-8B 기반 모델을 지도 학습 (SFT) 합니다.
• 하이브리드 강화 학습 (Hybrid RL):
  • 분해: 연속적인 분해 점수 (S) 를 밀도 보상 (dense reward) 으로 사용하여 GRPO(Group Relative Policy Optimization) 를 통해 탐색을 유도합니다.
  • 완성: 희소 이진 신호 (성공/실패) 의 문제를 해결하기 위해 고품질 증명 트래젝토리의 지도 학습 재연 (Supervised Replay) 을 병행하여 안정성을 확보합니다.

2.4 추론 파이프라인

• 계획 단계: 현재 열린 목표 중 가장 복잡한 (연산자 발자국이 큰) 목표를 선택하여 분해하고, 분해 점수에 따라 후보를 순위 매겨 탐색합니다.
• 증명 단계: 분해된 리프 정리에 대해 반복적으로 전술을 생성하고 Lean 컴파일러의 오류 피드백을 받아 증명을 수정합니다.

3. 주요 기여 (Key Contributions)

1. 계층적 증명 탐색 프레임워크: Lean 4 코드 검증을 위해 복잡한 목표를 구조적으로 단순한 하위 목표로 분해한 후 전술 수준 증명을 수행하는 새로운 아키텍처 제안.
2. 원칙적인 분해 점수: 구성적 정당성과 구조적 단순성을 결합한 점수 체계로, 학습 보상과 추론 시 검색 기준을 일관되게 적용하여 최적화 효율성을 극대화.
3. 하이브리드 RL 파이프라인: 분해와 완성을 통합된 정책으로 학습하며, 연속 보상과 지도 학습 재연을 결합하여 구조적 탐색과 안정적인 증명 생성을 균형 있게 달성.
4. 성능 입증: 8B 파라미터 모델이 84 배 이상 큰 기존 신경 증명기 (Neural Provers) 보다 뛰어난 성능을 보임.

4. 실험 결과 (Results)

세 가지 Lean 4 코드 검증 벤치마크 (Verina, Clever, AlgoVeri, 총 427 개 작업) 에서 평가되었습니다.

• 성공률: Goedel-Code-Prover-8B 는 **62.0%**의 전체 증명 성공률을 기록했습니다.
  • Verina: 68.8%, Clever: 54.0%, AlgoVeri: 62.3%.
  • 이는 가장 강력한 베이스라인 (최첨단 LLM 및 기존 신경 증명기) 대비 2.6 배의 향상입니다.
  • 32B~671B 크기의 기존 모델 (DeepSeek-Prover-V2 등) 을 능가하는 성능을 보였습니다.
• 추론 시 확장성 (Inference-Time Scaling): 검색 반복 횟수와 샘플링 예산 (pass@k) 이 증가함에 따라 성공률이 단조 증가하는 것을 확인했습니다. 이는 모델이 아직 확장 잠재력을 완전히 활용하지 못했음을 시사합니다.
• 증명 복잡도: 검증된 증명들은 평균 8~17 개의 분해된 정리와 130 줄 이상의 증명 코드를 포함하며, 가장 복잡한 경우 680 줄을 초과하여 복잡한 추론 능력을 입증했습니다.
• 점수의 예측력: 분해 점수 (S) 와 증명 성공률 간의 상관관계가 매우 높았으며 (AUROC = 0.903), 이 점수가 추론 시 탐색 방향을 올바르게 안내함을 확인했습니다.

5. 의의 및 결론

이 연구는 **LLM 기반 코드 검증의 격차 (Math-Code Gap)**를 해소하기 위한 효과적인 접근법을 제시합니다. 수학 증명과 달리 프로그램 검증은 고유한 개념과 도구가 필요하므로, 단순한 전술 생성이 아닌 계획 (분해) 과 실행 (완성) 의 통합이 필수적입니다.

Goedel-Code-Prover 는 상대적으로 작은 모델 (8B) 이지만, 계층적 분해 전략과 원칙적인 점수 기반 학습을 통해 최첨단 대형 모델들을 압도하는 성능을 달성했습니다. 이는 형식적 검증 분야에서 목적에 맞게 훈련된 전용 모델의 중요성과, 분해 전략이 복잡한 검증 작업 해결의 핵심 열쇠임을 보여줍니다. 향후 비공식 명세 처리 및 더 큰 코드베이스 확장 등을 통해 연구가 이어질 것으로 기대됩니다.