A method for the automated generation of proof exercises with comparable levels of proving complexity

이 논문은 첫 번째 논리 언어로 표현된 수학적 증명 연습문제의 난이도를 통제하여, 입력된 연습문제와 동등한 증명 복잡도를 가진 새로운 연습문제들을 자동으로 생성하는 방법을 제안합니다.

핵심

이 논문은 **"수학 증명 문제를 자동으로 만들되, 난이도를 똑같이 맞추는 방법"**을 소개합니다.

교사들이 시험 문제를 만들 때 가장 힘들어하는 부분이 바로 **"이 문제가 학생들에게 너무 쉬울까, 너무 어려울까?"**를 예측하는 일입니다. 보통은 문제를 만든 후 직접 풀어보거나 경험에 의존해서 난이도를 잡는데, 이 과정은 매우 시간이 걸리고 주관적입니다.

이 논문은 컴퓨터가 문제를 만들 때, **"이 문제와 똑같은 난이도 (증명 복잡도) 를 가진 다른 문제들"**을 자동으로 찾아내는 시스템을 제안합니다.

이 복잡한 아이디어를 쉽게 이해할 수 있도록 요리사와 레시피에 비유해 설명해 드리겠습니다.

---

1. 문제: "난이도 조절"이 어려운 이유

지금까지 자동 문제 생성 프로그램들은 주로 "문장 길이"나 "단어 개수" 같은 겉모습만 보고 난이도를 판단했습니다.

• 비유: 마치 "재료의 개수"만 보고 요리가 얼마나 어려운지 판단하는 것과 같습니다.
  • "감자 3 개, 양파 2 개"를 넣은 요리와 "감자 3 개, 양파 2 개"를 넣은 요리가 겉보기엔 똑같아 보일 수 있습니다.
  • 하지만 하나는 그냥 섞으면 되고, 다른 하나는 10 단계를 거쳐야 할 수도 있습니다.
  • 결과: 겉모습은 비슷해도, 학생이 풀 때 느끼는 '어려움'은 완전히 다를 수 있습니다.

2. 해결책: "증명의 뼈대"를 분석하다

이 논문은 문제를 풀 때 필요한 **논리적 단계 (증명 과정)**를 분석하여 난이도를 측정합니다.

• 핵심 아이디어: "문제를 푸는 데 필요한 최소한의 단계 수와 구조"가 바로 난이도입니다.
• 비유: 요리의 난이도를 '재료 개수'가 아니라 **'조리 단계의 복잡도'**로 봅니다.
  • "감자를 3 번 자르고, 2 번 볶는 요리"와 "양파를 3 번 자르고, 2 번 볶는 요리"는 조리 과정의 구조가 똑같다면 난이도도 똑같다고 봅니다.

3. 방법론: "논리 규칙"이라는 레시피 추출

이 시스템은 수학 (특히 집합론이나 정수론) 의 기본 법칙들을 컴퓨터가 이해할 수 있는 **'규칙 (레시피)'**으로 바꿉니다.

1. 입력: 교사가 하나의 증명 문제 (예: "A 집합이 B 집합의 부분집합임을 증명하라") 와 그 문제를 푸는 데 필요한 기본 법칙들을 줍니다.
2. 분석 (테이블루 증명): 컴퓨터는 이 문제를 풀기 위해 어떤 규칙들을 몇 번, 어떻게 적용해야 하는지 나무 모양의 증명 트리를 그립니다.
   • 이때 중요한 점은 논리 기호 (∧, ∨, ∀ 등) 를 모두 제거하고, 오직 수학 기호 (∈, ⊆ 등) 만 남긴다는 것입니다.
   • 비유: 요리의 '화학 성분'을 다 빼고, 오직 '손질, 볶기, 굽기' 같은 조리 동작만 남긴 것입니다.
3. 난이도 측정: 이 증명 트리의 **크기 (노드 수)**와 구조를 측정합니다. 이것이 바로 '증명 복잡도'입니다.

4. 결과: "난이도 twins" 문제 생성

이제 컴퓨터는 입력된 문제와 똑같은 증명 구조를 가진 다른 문제들을 찾아냅니다.

• 작동 원리:
  • 원래 문제: "A 와 B 의 교집합을 구하라" (증명 구조: 3 단계)
  • 생성된 문제: "A 와 B 의 차집합을 구하라" (증명 구조: 3 단계)
  • 비유: 원래 레시피가 "감자 3 번 자르고 볶기"였다면, 컴퓨터는 "양파 3 번 자르고 볶기"나 "당근 3 번 자르고 볶기"를 찾아냅니다. 조리 과정 (난이도) 은 똑같지만, 재료 (문제 내용) 는 다릅니다.

5. 왜 이것이 중요한가요? (실제 효과)

• 개인화된 학습: 학생 A 는 '교집합' 문제를 잘 풀지만 '차집합'은 어려워합니다. 이 시스템은 학생 A 가 '교집합' 문제를 풀었을 때, 난이도는 똑같지만 내용이 다른 '차집합' 문제를 자동으로 내줄 수 있습니다.
• 공정한 평가: 모든 학생에게 정말 똑같은 난이도의 문제를 주어, 실력 차이를 공정하게 측정할 수 있습니다.
• 교사 구원: 교사는 매일매일 새로운 문제를 만들지 않아도 되며, 컴퓨터가 "이 문제와 난이도 같은 문제 10 개"를 뚝딱 만들어줍니다.

요약

이 논문은 **"문제의 겉모습이 아니라, 문제를 푸는 '논리적 과정'의 구조를 분석해서 난이도를 재는 방법"**을 개발했습니다.

마치 요리사가 "이 요리는 3 단계로 만들 수 있으니, 재료만 바꿔서 3 단계로 만들 수 있는 다른 요리 10 가지를 찾아주세요"라고 주문하는 것과 같습니다. 이렇게 하면 학생들은 난이도가 일정하게 유지된 채로 다양한 연습 문제를 풀 수 있게 됩니다.

기술 요약

1. 문제 제기 (Problem)

• 자동 질문 생성 (AQG) 의 한계: 기존 AQG 시스템은 지식 소스에서 질문을 생성하지만, 생성된 문제의 난이도 (특히 논리적 증명 복잡도) 를 세밀하게 통제하는 메커니즘이 부족합니다.
• 난이도 평가의 모호성: 기존 연구들은 문제의 문법적 구조 (구문 수, 깊이 등) 나 머신러닝 기반의 인간 평가에 의존합니다. 그러나 문법적 구조가 유사해도 증명 전략이나 논리적 깊이가 다를 수 있으며, 머신러닝 모델은 인간 전문가 간의 의견 불일치로 인한 일관성 부족과 설명 가능성 (Explainability) 부재의 문제가 있습니다.
• 목표: 입력된 증명 문제와 동일한 수준의 증명 복잡도를 가진 새로운 증명 문제들을 자동 생성하는 방법론을 개발하는 것입니다.

2. 방법론 (Methodology)

논문의 핵심은 **이론 특화적 (Theory-specific) 절단 기반 표상 (Cut-based Tableaux)**을 사용하여 증명 복잡도를 정량화하고, 이를 기반으로 동형 (Isomorphic) 인 증명 구조를 가진 문제를 생성하는 것입니다.

A. 이론 특화적 증명 (Theory-specific Proofs)

• 정의: 논리 기호 ($\neg, \land, \lor, \to$ 등) 를 포함하지 않고, 오직 해당 이론 (예: 집합론) 의 정의적 공리 (Definitional Axioms) 에서 추출된 규칙만을 사용하여 증명하는 방식입니다.
• 규칙 추출 과정:
  1. 정의적 공리 (Definitional Axioms): 집합론 등 대학 수준의 이산수학 주제에 대한 공리들을 정의합니다.
  2. 규칙 임의형 (RINF) 변환: 공리들을 Prenex Normal Form (PNF), Skolemization, Conjunctive Normal Form (CNF) 을 거쳐 **Rule Implicational Normal Form (RINF)**으로 변환합니다.
  3. 규칙 추출: 변환된 식을 논리 기호 없는 선형 확장 규칙 (Linear Expansion Rules) 으로 추출합니다. 이 규칙들은 논리 기호를 포함하지 않으며, 전제와 결론 모두 '이론 특화적 공식 (Theory-specific formulas)'으로만 구성됩니다.
• 분석적 절단 (Analytic Cut): 증명 과정에서 절단 (Cut) 규칙을 적용할 때, 절단 공식이 이미 표상 (Tableau) 에 존재하는 공식의 부분식이어야 한다는 '분석적 (Analytic)' 제약을 둡니다. 이는 증명 확장을 통제하고 계산 효율성을 높입니다.

B. 증명 복잡도 (Proving Complexity) 의 정의

• 증명 동형 (Deductive Isomorphism): 두 증명의 복잡도가 비교 가능하려면, 두 증명의 **정당화 트리 (Justification Tree)**가 구조적으로 동형 (Isomorphic) 이어야 합니다.
  • 정당화 트리: 증명 트리의 폐쇄 (Closure) 노드에서 시작하여 각 노드가 어떻게 도출되었는지를 보여주는 트리 구조입니다.
  • 증명 크기 (Deductive Size): 정당화 트리의 노드 수로 정의됩니다.
• 비교 가능성 기준: 두 연습문제 (부정 가능한 공식 집합) 가 **최소 증명 (Minimal Proof)**을 가질 때, 그 증명들이 **증명 동형 (Proof-isomorphic)**이고, 공식들의 구문적 구조가 일치한다면 두 문제는 동일한 증명 복잡도를 가진 것으로 간주합니다.

C. 문제 생성 절차 (Generation Procedure)

1. 입력: 하나의 증명 문제 (부정 가능한 공식 집합) 와 이론 특화적 규칙 집합.
2. 최소 증명 탐색: 입력 문제에 대한 모든 가능한 증명을 탐색하여 **증명 크기 (Deductive Size) 가 최소인 증명 (Minimal Proof)**을 찾습니다.
3. 증명 동형 집합 탐색:
   • 최소 증명의 구조를 분석하여, 어떤 기호 (함수 기호, 술어 기호) 를 다른 기호로 치환할 수 있는지 결정합니다.
   • 증명 동형 후보 기호 (Proof-isomorphic Candidate Symbols): 특정 규칙의 전제와 결론 구조를 유지하면서 치환 가능한 기호들의 집합을 정의합니다.
   • 이 치환을 적용하여 새로운 공식 집합을 생성하고, 이것이 원래 증명과 동형인 최소 증명을 가지는지 확인합니다.
4. 출력: 입력 문제와 동일한 증명 복잡도를 가진 새로운 증명 문제들의 집합.

3. 주요 기여 (Key Contributions)

1. 증명 복잡도의 정량적 정의: 논리 기호를 배제하고 이론의 구조적 특성 (규칙 적용 횟수, 정당화 트리의 구조) 에 기반하여 증명 난이도를 객관적으로 정의했습니다.
2. 이론 특화적 표상 (Theory-specific Tableaux) 의 개발: 논리 기호 없이 공리에서 추출된 규칙만으로 증명을 수행하는 시스템을 구축하여, 증명 구조의 동형성을 명확하게 파악할 수 있게 했습니다.
3. 난이도 통제형 AQG 방법론: 머신러닝이나 문법적 복잡도 지표에 의존하지 않고, 증명 구조의 동형성을 기반으로 난이도가 통제된 문제를 자동 생성하는 알고리즘을 제시했습니다.
4. 구체적 구현: 집합론 (Set Theory) 을 예시로 하여, $\in, \subseteq, \cup, \cap, \setminus$ 등의 연산자를 포함한 증명 문제들을 생성하는 프로토타입을 개발했습니다.

4. 결과 및 실험 (Results)

• 집합론 예시: 집합론의 정의적 공리에서 추출된 규칙들을 사용하여, 입력된 증명 문제 (예: $x \in y \cap (w \cup z) \implies x \in (y \cap w) \cup z$) 와 동일한 증명 복잡도를 가진 다양한 변형 문제 (예: $x \in y \setminus (w \triangle z) \implies x \in (y \setminus w) \cup z$ 등) 를 성공적으로 생성했습니다.
• 효율성: 단순한 치환이 아닌 '증명 동형' 조건을 적용함으로써, 무작위 생성 시 발생할 수 있는 방대한 경우의 수를 줄이고 (예: 5625 건에서 144 건으로 축소), 의미 있는 난이도 조절이 가능한 문제들만 선별했습니다.
• 구현: 제안된 방법론의 전체 절차를 구현한 프로토타입이 GitHub 에 공개되었습니다.

5. 의의 및 향후 과제 (Significance & Future Work)

• 교육적 의의: 교육자가 학생의 수준에 맞춰 **개인화된 형성 평가 (Formative Assessment)**나 적응형 테스트를 설계할 때, 논리적으로 엄밀하게 난이도가 통제된 문제 풀이를 제공할 수 있습니다.
• 해석 가능성 (Explainability): 머신러닝의 '블랙박스'와 달리, 생성된 문제의 난이도가 왜 동일한지 그 근거 (증명 구조의 동형성) 를 명확히 설명할 수 있습니다.
• 한계 및 향후 연구:
  • 현재 방법은 논리 기호가 포함된 복잡한 명제 (STSNF 로 변환 불가능한 경우) 를 다루지 못합니다. 이를 해결하기 위한 변환 기법 연구가 필요합니다.
  • 정의적 공리 중 일부는 분석적 제약으로 인해 규칙 추출이 불가능한 경우가 있어, 이를 완화하는 방안이 필요합니다.
  • 실제 교육 현장에서 학생들의 인지적 부하 (Cognitive Load) 가 증명 구조의 어떤 특징 (예: 다전제 규칙 사용 여부) 에 의해 영향을 받는지 실증적 연구를 계획하고 있습니다.

결론적으로, 이 논문은 논리학 및 이산수학 교육에서 자동화된 문제 생성의 난제인 '난이도 통제'를 해결하기 위해, 증명의 구조적 동형성을 기반으로 한 엄밀한 계산적 방법론을 제시했다는 점에서 중요한 의의를 가집니다.