A Neuro-Symbolic Approach for Reliable Proof Generation with LLMs: A Case Study in Euclidean Geometry

이 논문은 유사 문제 검색과 형식적 검증기를 결합한 신경-심볼릭 접근법을 통해 LLM 의 기하학적 증명 정확도를 크게 향상시키고 신뢰할 수 있는 추론을 가능하게 하는 방법을 제시합니다.

핵심

이 논문은 **"인공지능 (LLM) 이 수학 문제를 풀 때, 어떻게 하면 더 똑똑하고 신뢰할 수 있게 만들 수 있을까?"**라는 질문에 대한 답을 제시합니다.

기존의 인공지능은 방대한 책을 읽어서 언어 패턴을 학습했지만, 수학처럼 "100% 논리적으로 옳은" 답을 요구하는 분야에서는 종종 헛소리를 하거나 논리적 허점을 보입니다. 마치 재미있는 이야기를 잘 지어내는 작가가 있지만, 수학 시험에서는 실수를 자주 하는 학생과 비슷합니다.

저희 연구팀은 이 문제를 해결하기 위해 **"뇌 (AI) + 도구 (수학 검증기)"**를 결합한 새로운 방식을 제안했습니다. 이를 일상적인 비유로 설명해 드릴게요.

---

🧩 핵심 아이디어: "유명한 수학 선생님의 노트"와 "엄격한 감수자"

이 시스템은 두 가지 강력한 무기를 가지고 있습니다.

1. 비슷한 문제를 찾아주는 "유사 문제 검색기" (Analogical Guidance)

• 비유: 시험을 치르는데, "이번 시험 문제는 어제의 그 문제와 구조가 비슷해. 어제의 풀이법을 참고해 봐!"라고 알려주는 친구가 있다고 상상해 보세요.
• 작동 원리:
  • 인공지능에게 새로운 기하학 문제를 주면, 시스템은 먼저 문제의 핵심 구조 (점, 선, 각도의 관계) 만 추출합니다. (예: "A 가 B 와 평행하다"는 사실만 남기고 이름이나 숫자는 지웁니다.)
  • 그런 다음, 과거에 풀었던 수만 개의 문제 중에서 구조가 가장 비슷한 문제를 찾아냅니다.
  • 그 유사한 문제들의 정답과 풀이 과정을 인공지능에게 보여줍니다.
  • 효과: 인공지능은 "아, 이런 유형의 문제는 보통 이렇게 풀었구나!"라고 배우게 되어, 처음부터 막막해하지 않고 훨씬 정확한 답을 내놓을 확률이 높아집니다.

2. 틀린 점을 지적해주는 "엄격한 감수자" (Symbolic Verifier)

• 비유: 인공지능이 풀이를 쓰면, 옆에 앉은 **수학 선생님 (컴퓨터 프로그램)**이 "여기서 논리가 끊겼어", "이 정리는 조건이 안 맞는데 왜 썼지?"라고 즉시 지적합니다.
• 작동 원리:
  • 인공지능이 쓴 풀이를 컴퓨터가 논리적으로 하나하나 검증합니다. (사람이 눈으로 보는 게 아니라, 수학 공식으로 계산해 봅니다.)
  • 만약 틀린 점이 있으면, "어디가 왜 틀렸는지" 구체적으로 알려줍니다.
  • 인공지능은 이 피드백을 받고 다시 풀이를 고쳐서 제출합니다. 이 과정이 정답이 나올 때까지 반복됩니다.
  • 효과: 인공지능이 "아, 내가 실수했구나"라고 깨닫고 수정할 기회를 주어, 최종적으로 100% 논리적으로 옳은 증명을 완성하게 됩니다.

---

🚀 실제 성과: 얼마나 좋아졌을까요?

이 실험은 고등학교 수학 경시대회 (SAT 수준) 의 기하학 문제들로 테스트했습니다.

• 기존 AI (혼자서 풀 때): 10 문제 중 1 개 정도만 맞췄습니다. (10% 성공률)
• 새로운 방식 (유사 문제 + 감수자): 10 문제 중 8 개를 맞췄습니다. (80% 성공률)
  • 특히, OpenAI 의 o1 모델은 5870% 성능이 향상되었고, Gemini 모델도 5264% 나 좋아졌습니다.

재미있는 사실:
기존 AI 는 정답 (숫자) 을 맞출 수는 있어도, 그걸 증명하는 **과정 (논리)**을 엉망으로 쓰는 경우가 많았습니다. 하지만 이 새로운 방식을 쓰면, 정답도 맞고 증명 과정도 완벽해졌습니다.

---

💡 왜 이 방식이 중요할까요?

1. 신뢰성: "AI 가 말하니까 믿자"가 아니라, "논리적으로 검증했으니까 믿자"가 됩니다. 이는 의료, 법률, 공학처럼 실수가 치명적인 분야에서 AI 를 쓸 수 있는 문을 엽니다.
2. 비용 절감: 모든 수학 공식을 다 알려주는 게 아니라, 해당 문제와 관련된 공식만 골라서 알려주기 때문에 AI 가 처리해야 할 정보량이 줄어듭니다. (약 18,000 개의 공식을 2,500 개로 줄임)
3. 학습 효과: 학생들에게도 유용합니다. 비슷한 문제를 보여주면서 힌트를 주고, 틀린 부분을 정확히 지적해주는 개인 맞춤형 튜터 역할을 할 수 있습니다.

🎯 결론

이 연구는 **"AI 가 혼자서 모든 걸 다 할 필요는 없다"**는 것을 보여줍니다.
AI 가 가진 창의성과 언어 능력에, 논리적 구조를 찾아주는 도구와 엄격한 검증 시스템을 더하면, 우리는 훨씬 더 똑똑하고 신뢰할 수 있는 AI 를 만들 수 있습니다. 마치 재능 있는 학생에게 훌륭한 멘토와 엄격한 감수자가 붙어주면, 그 학생은 세계적인 수학자가 될 수 있는 것과 같습니다.

기술 요약

1. 연구 배경 및 문제 정의 (Problem)

• 문제의 본질: 대규모 언어 모델 (LLM) 은 자연어 처리에서는 탁월한 성능을 보이지만, 엄격한 논리적 추론과 기호적 추리가 요구되는 수학적 증명과 같은 형식적 영역 (Formal Domains) 에서는 어려움을 겪습니다. 이는 LLM 이 확률적 패턴 매칭에 기반하여 생성되므로, 모호함이 없고 절대적인 진리가 요구되는 수학 증명에는 적합하지 않기 때문입니다.
• 현재의 한계: 기존 LLM 은 증명의 긴 논리적 일관성을 유지하기 어렵고, 문제의 표면적 변화만으로도 성능이 급격히 떨어지는 등 진정한 수학적 추론보다는 패턴 매칭에 의존하는 경향이 있습니다.
• 목표: LLM 의 생성 능력을 활용하면서도, 신뢰할 수 있고 검증 가능한 형식적 증명을 생성할 수 있도록 돕는 신경 - 기호적 (Neuro-Symbolic) 시스템 개발.

2. 제안된 방법론 (Methodology)

저자들은 LLM 의 생성 능력과 두 가지 구조화된 구성 요소 (유추적 안내 및 기호적 검증) 를 결합한 2 단계 신경 - 기호적 접근법을 제안합니다.

A. 문제 추상화 및 유추 문제 검색 (Analogous Problems Retrieval)

• 추상화 (Abstraction): 대상 문제와 데이터셋 내 모든 문제를 추상화합니다. 구체적 엔티티 이름 (선, 각도 등) 을 <word>로, 숫자를 <num> 으로 치환하여 표면적 세부사항을 제거하고 구조적 유사성만 남깁니다.
• 유사성 측정: Jaccard 유사도를 기반으로 구성 (Construction), 조건 (Conditions), 목표 (Goal) 의 구조적 유사성을 계산합니다.
• 회귀 모델 학습: 두 문제 간의 구조적 유사성과 실제 증명 간의 유사성 (Proof Similarity) 을 예측하는 간단한 신경망 회귀 모델을 학습시킵니다.
• 검색: 대상 문제와 구조적으로 유사한 (유추) 문제들을 검색하여, 해당 문제들의 완전한 증명을 Few-shot 예시 (In-context examples) 로 제공합니다. 이는 LLM 이 올바른 증명 패턴을 학습하는 데 도움을 줍니다.

B. LLM 증명 생성 (LLM Proof Generation)

• 프롬프트 구성: 대상 문제, 검색된 유추 문제 및 그 증명, 그리고 **축소된 정리 사전 (Theorem Dictionary)**을 LLM 에게 제공합니다.
• 정리 사전 최적화: 전체 정리 사전 (약 196 개) 을 모두 제공하는 대신, 검색된 유추 문제의 증명에 사용된 정리들만 포함하도록 사전 크기를 줄입니다 (평균 2.5K 토큰으로 축소). 이는 비용 절감과 모델의 검색 공간 축소 (Focus) 에 기여합니다.

C. 기호적 검증 및 피드백 루프 (Symbolic Verifier & Iterative Feedback)

• 검증기 (Verifier): 생성된 증명을 기호적 논리 시스템 (Z3 SMT 솔버 등) 을 통해 검증합니다.
  • 작동 원리: 검증기는 정답을 미리 알지 못하며, 증명 단계가 주어진 조건과 논리적 제약으로부터 목표 값을 도출하는지 확인합니다.
• 피드백 루프:
  1. LLM 이 증명을 생성합니다.
  2. 검증기가 오류를 발견하면 자연어 피드백을 제공합니다.
  3. LLM 은 피드백을 컨텍스트에 포함시켜 증명을 수정하고 다시 시도합니다.
  4. 증명이 유효하거나 최대 재시도 횟수 (5 회) 에 도달할 때까지 반복합니다.
• 오류 분류:
  1. Tier 1: 정리 호출 문법 오류 (Syntax violation).
  2. Tier 2: 전제 조건 미충족 (Premise violation).
  3. Tier 3: 목표 달성 실패 (Goal not reached).

3. 주요 기여 (Key Contributions)

1. 신경 - 기호적 시스템 제안: 유추적 안내 (Analogical Guidance) 와 검증 피드백 (Verification Feedback) 을 통해 LLM 의 증명 생성 능력을 보조하는 새로운 아키텍처 제안.
2. 맞춤형 기호 검증기 설계: 단순한 정답 확인이 아닌, 증명 전체의 유효성을 평가하고 구조화된 피드백을 제공하는 검증기 개발.
3. 성능 향상 및 비용 절감:
   • O1 모델 기준 58%~70%, Gemini-2.5-Flash 기준 **52%~64%**의 증명 정확도 향상.
   • 유추 문제 기반의 정리 사전 축소로 입력 토큰 수를 18K 에서 평균 2.5K 로 대폭 감소시켜 비용 절감.
4. 오픈소스: 코드, 데이터, 평가 스크립트 공개 계획.

4. 실험 결과 (Results)

• 데이터셋: FormalGeo-7k (SAT 수준 유클리드 기하학 문제 6,981 개) 중 난이도 1~5 단계에 해당하는 50 개 문제 샘플 사용.
• 모델: OpenAI o1 및 Gemini-2.5-Flash 사용.
• 성능 비교:
  • Base Model (비교군): 유추 없이 무작위 예시와 전체 정리를 제공, 검증 없이 1 회 시도. 평균 정확도 10%.
  • 제안 방법 (Full Pipeline): 유추 + 검증 + 다중 실행 (Multiple runs) + 재시도 (Retries). 평균 정확도 80%.
  • 단일 실행 (Single run) 만으로도: 검증과 유추만 적용 시 **68%**의 정확도를 기록하여 베이스라인을 크게 상회.
• 구성 요소 기여도:
  • 유추 검색: 초기 증명 후보의 질을 높여 검증기의 수정 부담을 줄이고 성능을 향상시킴.
  • 검증 피드백: 오류 수정을 통해 정확도를 추가로 20~30% 향상시킴.
  • 다중 실행: 특히 난이도 높은 문제 (Level 4-5) 에서 성능 향상에 기여.
• 정답 vs 증명: 베이스 모델은 정답은 맞지만 증명이 틀린 경우가 많았으나, 제안 방법은 정답과 올바른 증명을 동시에 생성하는 비율이 높았습니다 (정답 100%, 증명 80%).

5. 의의 및 결론 (Significance)

• 신뢰성 있는 AI: LLM 이 수학적, 과학적, 교육적 분야에서 신뢰할 수 있는 도구로 활용될 수 있는 가능성을 입증했습니다.
• 확장성: 기하학이라는 구체적인 도메인에서 검증되었으나, SMT 기반 검증이 가능한 다른 형식적 영역 (수학, 논리, 보안 등) 으로 확장 가능한 프레임워크를 제시합니다.
• 교육적 활용: 유사한 해결된 문제를 제시하여 학습을 돕고, 기호적 검증기를 통해 맞춤형 피드백을 제공하는 교육용 시스템으로의 적용 가능성 제시.
• 미래 방향: 역삼각함수 지원 확대, 동적 시스템 분석을 위한 모델 체킹 (Model Checking) 도입, 더 정교한 유추 검색 메커니즘 연구 등을 계획 중입니다.

이 논문은 LLM 의 추론 한계를 기호적 도구와 유추 학습을 통해 극복함으로써, 고신뢰성 AI 시스템 구축을 위한 실용적인 신경 - 기호적 청사진을 제시했다는 점에서 중요한 의의를 가집니다.