Learning to Disprove: Formal Counterexample Generation with Large Language Models

이 논문은 Lean 4 에서 자동으로 검증 가능한 형식적 반례 생성을 목표로, 심볼릭 변이 전략과 다중 보상 전문가 반복 학습 프레임워크를 통해 대형 언어 모델을 미세 조정하여 수학 추론의 증명과 반례 발견 능력을 모두 향상시키는 방법을 제시합니다.

핵심

이 논문은 **"수학에서 '틀린 것'을 찾아내는 법을 AI 에게 가르치는 연구"**입니다.

기존의 AI 수학 연구는 대부분 "정답을 증명하는 것 (Proof)"에 집중했습니다. 마치 시험에서 "왜 이 답이 맞는지"를 설명하는 데만 열중했던 셈이죠. 하지만 수학에서 **'반례 (Counterexample)'**를 찾는 것, 즉 "이 명제는 틀렸습니다! 여기 틀린 예시가 있습니다!"라고 지적하는 능력은 그 못지않게 중요합니다.

이 논문은 AI 가 반례를 찾아내고, 그 반례가 진짜로 틀린 이유를 형식적인 언어 (Lean 4) 로 엄밀하게 증명하는 능력을 키우는 방법을 제안합니다.

핵심 내용을 일상적인 비유로 설명해 드릴게요.

---

1. 문제: AI 는 '맞는 것'은 잘 찾지만, '틀린 것'은 못 찾는다

지금까지의 수학 AI 는 마치 **"올바른 길만 찾아주는 내비게이션"**처럼 작동했습니다. 하지만 수학은 때로 "이 길은 가짜입니다!"라고 말해주는 **'가짜 길 탐지기'**가 필요합니다.

• 기존의 한계: 반례를 찾는 데이터가 너무 적고, AI 가 틀린 답을 내놓았을 때 "틀렸어"라고만 알려주는 신호 (보상) 가 너무 희박해서 AI 가 배우기 힘들었습니다.

2. 해결책 1: "가짜 문제"를 대량으로 만들어내는 마법 (Symbolic Mutation)

연구진은 AI 에게 반례를 가르칠 데이터를 직접 만들어냈습니다. 어떻게요? 수학의 '조작'을 이용했습니다.

• 비유: 레시피 변조하기
  • 원래 완벽한 요리 레시피 (정리, Theorem) 가 있다고 가정해 보세요. "소금 (가설 1) 과 설탕 (가설 2) 을 넣으면 맛있는 국 (결론) 이 나온다"는 명제입니다.
  • 연구진은 AI 에게 **"소금을 빼고 설탕만 넣으면 어떨까?"**라고 물어봤습니다.
  • 당연히 국이 맛이 없겠죠? (이게 바로 반례가 됩니다).
  • AI 는 원래 레시피에서 필요한 재료 (가설) 하나를 뺀 뒤, "아! 그럼 이 국은 맛이 없네!"라고 증명하는 연습을 합니다.
  • 이 과정을 통해 연구진은 57 만 개 이상의 '가짜 문제' 데이터를 만들어냈습니다. AI 가 반례를 찾는 훈련을 할 수 있는 거대한 운동장이 생긴 셈입니다.

3. 해결책 2: 두 번의 칭찬으로 학습시키는 '다중 보상 시스템' (Multi-Reward)

기존에는 AI 가 반례를 찾으면 "정답!"이라고 한 번만 칭찬했습니다. 하지만 반례 찾기는 어렵기 때문에, AI 가 실패하면 아무런 피드백도 못 받아서 학습이 멈췄습니다.

• 비유: 요리 대회 심사
  • 기존 방식: 요리사가 "소금 없이 국을 끓였는데 맛이 없다"고 증명하면 점수를 줍니다. 하지만 실패하면 0 점.
  • 새로운 방식 (이 논문의 방법):
    1. 첫 번째 점수: "소금 없이 국을 끓였을 때, 국이 맛이 없는지 (반례가 맞는지) 증명했니?"
    2. 두 번째 점수: "그리고 '소금이 꼭 필요하다'는 사실도 증명했니?"
  • AI 가 첫 번째 과제는 어렵지만, 두 번째 과제 (소금의 필요성 증명) 는 상대적으로 쉽습니다. AI 가 두 번째 과제를 성공하면 부분 점수를 줍니다.
  • 이렇게 작은 성공이라도 점수로 보상해주니, AI 는 포기하지 않고 계속 시도하며 더 잘하게 됩니다.

4. 결과: AI 가 "틀린 것"을 찾아내는 실력이 비약적으로 상승

이 방법으로 훈련된 AI 는 기존 최고의 수학 AI 들보다 훨씬 뛰어났습니다.

• 성과: 새로운 테스트에서 기존 AI 들보다 47%~74% 더 많은 반례를 찾아냈습니다.
• 의미: 이제 AI 는 단순히 "이게 맞다"고 말만 하는 게 아니라, **"이건 틀려요! 왜 틀린지 증명해 드릴게요"**라고 능동적으로 지적할 수 있게 되었습니다.

5. 결론: AI 의 '자기 성찰' 능력 향상

이 연구의 가장 큰 의의는 AI 가 **자신의 추론 과정을 스스로 검증 (Self-verification)**할 수 있게 되었다는 점입니다.

• 마치 학생이 시험 문제를 풀 때, "내 답이 맞을까? 아니면 반례가 있을까?"라고 스스로 의심하고 확인하는 능력을 키운 것과 같습니다.
• 이는 AI 가 단순히 계산을 잘하는 것을 넘어, 수학적 논리와 비판적 사고를 갖추는 중요한 첫걸음입니다.

한 줄 요약:

"이 논문은 AI 에게 '정답 찾기'뿐만 아니라 **'오답 찾기 (반례 생성)'**도 가르쳤으며, 이를 위해 가짜 문제를 대량으로 만들고, 작은 성공에도 점수를 주는 새로운 학습 방식을 개발하여 AI 의 수학 실력을 획기적으로 높였습니다."

기술 요약

이 논문은 "LEARNING TO DISPROVE: FORMAL COUNTEREXAMPLE GENERATION WITH LARGE LANGUAGE MODELS" (거부하기 학습: 대규모 언어 모델을 이용한 형식적 반례 생성) 으로, 수학 추론 분야에서 LLM 의 핵심적인 공백인 반례 (Counterexample) 생성에 초점을 맞춘 연구입니다.

주요 내용은 다음과 같습니다.

1. 문제 정의 (Problem)

기존의 AI 수학 연구는 주로 참인 명제에 대한 **증명 (Proof Construction)**에 집중되어 왔습니다. 그러나 수학에서 반례는 거짓인 명제를 기각하고, 추측을 정제하며, 교육적 가치를 높이는 데 필수적입니다.
현재 LLM 이 반례를 찾는 능력은 다음과 같은 두 가지 주요 한계에 직면해 있습니다.

• 데이터 부족: 반례 생성을 위한 전용 데이터셋이 극히 부족합니다 (기존 CounterMath 데이터셋은 1,216 개에 불과함).
• 희소 보상 (Sparse Reward): 복잡한 문제에서 LLM 이 올바른 반례를 찾지 못하면 훈련 중 보상이 0 이 되어 학습이 멈추거나 성능이 정체되는 문제가 발생합니다.

2. 제안된 방법론 (Methodology)

저자들은 **형식적 반례 생성 (Formal Counterexample Generation)**을 위한 통합 프레임워크를 제안하며, 이는 크게 두 단계로 구성됩니다.

A. 심볼릭 돌연변이 전략 (Symbolic Mutation Strategy) - 데이터 증강

훈련 데이터의 부족을 해결하기 위해, 증명 가능한 기존 정리의 필수 가정 (Hypothesis) 을 제거하여 새로운 반례 문제를 생성하는 방식을 도입했습니다.

1. 시드 정리 (Seed Theorem) 수집: Mathlib, Leanworkbook 등 다양한 소스에서 증명 가능한 보편적 형식 ($\forall x$) 의 정리를 수집합니다.
2. 가정 제거 (Hypothesis Dropping): 정리에서 하나의 필수 가정을 제거합니다. (예: $H_1(x) \land H_2(x) \to C(x)$ 에서 $H_1(x)$ 제거)
3. 반례 문제 생성: 제거된 가정이 필수적이므로, 새로운 명제 ($H_2(x) \to C(x)$) 는 거짓이 되며, 이에 대한 반례 ($\exists x, H_2(x) \land \neg C(x)$) 가 존재하게 됩니다.
4. 검증: Lean 4 정리 증명기를 사용하여 원본 정리의 증명에서 제거된 가정이 실제로 필수적인지 확인하고, 생성된 문제가 문법적으로 올바른지 검증합니다.
   • 이를 통해 약 575,000 개의 고품질 반례 훈련 데이터를 합성했습니다.

B. 다중 보상 유도 훈련 (Multi-Reward Guided Training) - 학습 효율성 향상

희소 보상 문제를 해결하기 위해 Expert Iteration 프레임워크에 다중 보상 (Multi-Reward) 메커니즘을 도입했습니다.

• 이중 검증 구조: 생성된 반례 $x^*$에 대해 두 가지 정리를 동시에 증명하도록 요구합니다.
  1. 변이 버전 (Mutated Version): 제거된 가정이 없는 원래 명제의 반례임을 증명 ($H_2(x^*) \to C(x^*)$).
  2. 제거된 가정 버전 (Dropped Hypothesis): 제거된 가정이 거짓임을 증명 ($\neg H_1(x^*)$).
• 보상 설계: 두 증명 중 하나라도 성공하면 보상을 받도록 설계하여, LLM 이 어려운 문제를 풀지 못하더라도 부분적인 성공 (예: 가정의 부정을 증명) 을 통해 학습 신호를 유지하게 합니다.
  • 최종 보상은 $r = \alpha \cdot I(\text{Mutated}) + (1-\alpha) \cdot I(\text{Dropped})$ 형태로 가중치를 부여합니다.
• 학습 파이프라인:
  1. 비공식 추론 (Informal Reasoning): LLM 이 구체적인 반례 예시 (Concrete Example) 를 제안.
  2. 형식 증명 (Formal Proof): 제안된 예시를 바탕으로 Lean 4 코드를 생성하여 증명.
  3. 피드백 및 미세 조정: 증명 성공 여부에 따라 가중치를 부여하여 모델을 미세 조정 (SFT).

3. 주요 기여 (Key Contributions)

1. 형식적 반례 생성 프레임워크: LLM 이 비공식적 추론으로 반례를 찾고, 이를 Lean 4 로 형식화하여 자동 검증받는 두 단계 프로세스를 정립했습니다.
2. 심볼릭 돌연변이 데이터 합성: 기존 데이터셋의 한계를 극복하고, 수학적 엄밀성을 유지하면서 대규모 반례 데이터 (575K 개) 를 자동 생성하는 방법을 제안했습니다.
3. 다중 보상 학습 전략: 증명 실패 시에도 학습이 가능하도록 하는 새로운 보상 설계로, 희소 보상 문제를 효과적으로 완화했습니다.

4. 실험 결과 (Results)

세 가지 새로운 벤치마크 (FOR-COUNTER, VERI-REASON, VERI-FORMALIZE) 에서 실험을 수행한 결과는 다음과 같습니다.

• 성능 향상: 제안된 프레임워크로 미세 조정된 모델은 기존 최첨단 LLM (Gemini-2.5, GPT-4.1, DeepSeek-R1 등) 과 오픈소스 정리 증명기 (Leanabell, Goedel 등) 보다 월등히 높은 성능을 보였습니다.
• 구체적 수치: Pass@1 성공률에서 가장 강력한 베이스라인 대비 47% ~ 74% 의 상대적 개선을 달성했습니다.
• 학습 효율성: 다중 보상 훈련은 단일 보상 훈련보다 수렴 속도가 빠르고 최종 성능이 더 높았습니다 (Pass@1 기준 약 49% vs 43%).

5. 의의 및 결론 (Significance)

이 연구는 수학 AI 가 단순히 "증명하는 것"을 넘어 "거짓임을 증명하는 (Disproving)" 능력을 갖추는 것이 중요함을 강조합니다.

• 자기 반성 능력 강화: LLM 이 자신의 추론 과정을 스스로 검증하고 오류를 수정할 수 있는 능력을 키워줍니다.
• 수학적 발견 지원: 새로운 추측의 타당성을 검증하거나 기존 추측을 반박하는 데 AI 를 활용할 수 있는 실질적인 도구를 제공합니다.
• 미래 방향: 형식적 반례 생성은 수학 연구의 자동화와 LLM 의 논리적 추론 능력 향상을 위한 중요한 새로운 방향성을 제시합니다.

요약하자면, 이 논문은 데이터 부족과 학습 보상 희소성이라는 두 가지 장벽을 심볼릭 돌연변이와 다중 보상 전략으로 극복하여, LLM 이 형식적 반례를 생성하는 데 있어 획기적인 성능 향상을 이루었음을 보여줍니다.