개설교과목
AI수학대학원 신규 교과목 취지 및 주요 내용(안)
개설교과목 (교과목 취지 및 주요 내용)
|
과목 구분 (강:실:학) |
교과목명 | 교과목 취지 및 주요 내용 |
|---|---|---|
|
전공선택 (기초) (3:0:3) |
형식화 수학 개론 | 의존형(type-theoretic) 논리와 Curry-Howard 동형을 통한 형식 논리, Lean 4 기본 문법, mathlib구조 등 수학의 형식화(formalization)를 위한 기초 개념을 다루며 학부 수준 정리(대수, 해석학) 형식화하여 증명을 재현함 |
| 상호작용형(대화형) 정리 증명론 | Lean의 메타프로그래밍 기법과 DSL 설계, 사용자 정의 tactic 및 문법 확장을 통해 증명 자동화의 구조와 원리를 이해하고 정수론, 위상수학 등 대학원 수준의 수학 내용을 형식화로 구현하여 고급 수준의 수학 형식화 개념과 기법을 이해함 | |
|
전공선택 (심화) (3:0:3) |
자동 추론과 증명 탐색 | SAT, SMT, DPLL 등 고정 논리 기반 자동 추론 기법과 1차 논리의 증명 구조, SMT 이론의 구조와 결정 절차를 이해, Lean 내장 tactic (simp, aesop, linarith 등)의 자동화 전략을 분석하고 mini prover 실습을 통해 증명 탐색 구조를 익힘 |
| 정리증명 인공지능 | GNN, Transformer를 활용한 증명 구조 임베딩, 강화학습 기반 tactic 탐색, LLM을 활용한 자동 문제 형식화 및 증명 생성 등 인공지능 기반 정리증명 기법을 다룸 | |
| 인공지능 기반 수학 발견 | 최신 인공지능 기법(GNN, Transformer, LLM, 심볼릭 연산 등)을 활용한 새로운 수학적 현상, 난제 발굴, 정리 증명 등 최신 연구 동향을 다룸. 주요 논문과 기술을 순번제로 발표하고 관련 기법을 적용한 소규모 프로젝트를 수행하여 향후 연구에 필요한 역량과 기술 개발 능력을 기름 |