수학 연구의 AI 혁신 | "AI for Science/Engineering" Series | 리벨리온×모두의연구소

리벨리온과 모두의연구소가 함께하는 AI for Science/Engineering 연례 정기 세미나 2026의 강연으로, 인공지능과 수학 연구의 결합이 어디까지 왔는지 살펴봅니다. 세종대학교 수학통계학과 박예찬 교수가 사람이 쓴 수학 명제와 증명을 컴퓨터가 검증할 수 있는 형식 언어로 바꾸는 '자동 형식화(Autoformalization)'와, 컴퓨터가 증명 자체를 찾아내는 '자동 정리 증명(Automated Theorem Proving, ATP)'을 소개합니다.

이런 분께 추천해요

• AI가 수학 문장을 어떻게 이해하는지 궁금한 분
• 수학 정리의 증명 보조기와 LLM의 결합에 관심 있는 분
• 미래 수학 연구 방식의 변화를 먼저 확인하고 싶은 분
• AI와 수학의 융합, AI4Science에 관심 있는 엔지니어

다루는 내용

• 증명이 올바른지 컴퓨터로 확인하는 증명 보조기(Proof Assistant)와, 자연스러운 수학 문장을 형식 언어로 다시 써야 하는 어려움
• 대규모 언어 모델로 빠르게 발전하고 있는 자동 형식화 연구의 현재와 한계
• 언어 모델이 다양한 증명 방법을 제안·탐색하고 증명 보조기가 결과를 엄밀하게 검증하는 자동 정리 증명 연구
• 최신 AI 모델이 만든 수학적 성과를 Lean으로 형식화·검증하는 흐름과, AI와 증명 보조기가 바꿔 갈 수학 연구의 방식

참가 안내

• 참가비는 무료이며, 주차 공간이 협소하고 주차비는 지원되지 않아 대중교통 이용을 권장합니다.
• 같은 시리즈의 다음 세미나는 11월 12일(시스템 엔지니어링 — 생성형 AI, GNN, 강화학습의 산업 적용)과 12월 12일(모두콘2026 'AI4Science + NPU' 트랙)로 예정돼 있습니다.

행사 요약