션 웰렉

🏷️ 인물 LLM 머신러닝 추론 교수 NeurIPS논문 Star

개요

션 웰렉(Sean Welleck)은 카네기멜런대학교(Carnegie Mellon University, CMU) 언어기술연구소(Language Technologies Institute, LTI) 조교수이자 CMU L3 Lab의 리더입니다. LLM의 학습, 추론, 평가 알고리즘 전반을 연구하지만, 특히 수학적 추론과 자동 증명 생성 분야에서 가장 두드러진 성과를 내고 있습니다.

2022년부터 NaturalProver, Draft-Sketch-Prove 등 비공식 증명과 형식 증명기를 연결하는 연구들을 잇따라 발표하며 이 분야의 핵심 연구자로 자리매김했습니다. 2026년 3월에는 DARPA expMath 그랜트의 lead PI로 선정되어 AI와 수학의 접점에서 국가 차원의 연구를 이끌고 있습니다.

CMU 내 Hoskinson Center for Formal Mathematics에도 소속되어 있으며, 2025년 9월에는 NSF Institute for Computer-Aided Reasoning in Mathematics(ICARM)의 출범에도 합류했습니다. 수학의 자동화라는 장기 목표를 향해 학계와 정부 양쪽의 지원을 받는 독보적인 위치에 있으며, CMU L3 Lab은 2026년 가을 박사 과정 신입생을 모집하고 있습니다.

생애

션 웰렉은 수학과 컴퓨터과학의 접점에서 커리어를 구축해 왔습니다. 학부와 대학원 시절부터 자연어 생성과 추론에 관심을 가졌으며, 박사 과정 이후 LLM의 수학적 능력을 체계적으로 끌어올리는 연구에 집중했습니다.

CMU LTI에 조교수로 합류하기 전에는 워싱턴 대학교(University of Washington)의 Yejin Choi 교수 그룹 등에서 연구를 수행했습니다. 이 시기 NaturalProver와 같이 자연어로 표현된 수학 증명을 생성하는 연구가 시작되었습니다.

CMU 부임 이후에는 L3(Learning, Language, Logic) Lab을 꾸려 수학적 추론과 형식 증명을 동시에 다루는 연구 그룹을 운영하고 있습니다. DARPA expMath와 NSF ICARM, NSF MFAI, NSF AIMing 등 복수의 연방 연구비를 수주하며 미국 내 AI-수학 연구의 선두 그룹 중 하나로 자리매김했습니다.

업적

웰렉의 가장 널리 인용되는 작업은 NaturalProver(NeurIPS 2022)입니다. 정리 증명에 필요한 배경 지식(정의, 보조 정리 등)을 검색하거나 사람이 제공하는 방식으로 조건화해서 자연어 수학 증명을 생성하고, constrained decoding으로 배경 지식의 실제 사용을 강제하는 프레임워크입니다. 기존 생성 모델이 수학적으로 근거 없는 증명을 내놓는 "환각" 문제를 구조적으로 억제하는 방법을 제시했다는 점에서 주목받았습니다.

후속작인 Draft, Sketch, and Prove(ICLR 2023 oral)는 비공식 증명을 안내자로 활용해 형식 증명기(Lean, Isabelle 등)가 더 쉬운 하위 목표에 집중할 수 있도록 유도하는 방법입니다. 사람이 쓴 비공식 증명과 기계가 검증하는 형식 증명 사이의 간극을 줄이는 파이프라인으로, 형식 수학 자동화 연구에서 표준 기준선으로 자리 잡았습니다.

DARPA expMath 과제에서는 순수 수학 분야의 진보를 가속화할 AI 협력자 개발과 전문가 수준의 수학 벤치마크 구축을 목표로 삼고 있습니다. ImProver 2(arXiv 2025)에서는 Lean 증명의 품질을 반복적으로 개선하는 자기 개선 LM 방법을 제안해 형식 증명 최적화 연구로 영역을 확장했습니다.

여담

웰렉은 LLM이 수학을 진정으로 이해하는지, 아니면 패턴을 기억하는지를 구분하는 문제를 오랫동안 천착해 왔습니다. 이 질문에 답하기 위해 단순한 수식 풀이가 아닌 형식 증명 검증이라는 엄밀한 기준을 채택한 것이 그의 연구 방향을 결정하는 핵심 선택이었습니다.

Lean-STaR(arXiv 2024) 연구는 증명 생각과 증명 단계를 교차하며 형식 증명 능력을 향상시키는 방법으로, Chain-of-Thought 방식과 형식 수학을 연결하는 시도입니다. 이 연구 방향은 최근 추론 모델들의 부상과 맞물려 더욱 주목받고 있습니다.

expMath 그랜트의 lead PI로 선정된 것은 그의 연구가 단순한 학술 기여를 넘어 미국 연방 차원의 수학 AI 어젠다를 형성하는 위치에 올랐음을 의미합니다. CMU의 Hoskinson Center와 NSF ICARM, DARPA expMath라는 세 개의 제도적 기반을 동시에 갖춘 연구자는 드뭅니다.

주요 논문