장봉준

8 minute read

학회장과 광화문이 가까워 밤에 뛰러 나가는 겸 구경갈 수 있었다

PLDI 2025는 태어나 처음으로 참가하는 국제학회였다. 그 중에서도 세계 최고 프로그래밍 언어 학회 PLDI가 우리나라 서울에서 열린 점이 아주 특별했다. 전세계 연구자들이 우리나라로 찾아오고, 거기다 내 연구를 우리나라에서 발표하기도 했으니 이보다 멋진 경험을 찾기는 힘들 것 같다.

전세계에서 모인 빼어난 학생들과 연구자들을 만나 이야기하며 연구 아이디어 이야기로 동기를 부여받기도 하고, 연구하며 어려웠던 점이나 사람 사는 이야기를 하면서 같은 커뮤니티의 일원으로 동질감을 느끼기도 하였다. 이 기행문을 통해 PLDI 2025 5일간 나의 경험을 공유해보고자 한다.

PLDI 워크샵

PLDI 첫 2일은 워크샵으로 시작했다. 그 중에서 첫날 오전에는 egglog 튜토리얼에, 오후에는 PLMW이 열려 참석하였다.

egglog 튜토리얼

egglog는 equality saturation 워크로드를 위해 구현된 egg와 Datalog를 통합한 프레임워크다. equality saturation은 나의 관심 분야인 컴파일러 최적화에서 최근 많은 관심을 끌고 있는 기술이다. 예를 들어, 최근 등장한 Cranelift 컴파일러 는 e-graph를 사용해 컴파일러 최적화기와 코드 생성기를 구현해 컴파일러 구현에 새로운 방향을 제시하고 있다. 튜토리얼에서는 egglog를 이용해 추론 규칙(Inference Rule, Deductive Reasoning)과 재작성 규칙(Rewrite Rule)을 선언하고 이를 통해 간단한 프로그램 분석기를 구현하는 방법, 코드 최적화기를 구현하는 법을 다뤘다. 튜토리얼의 자세한 내용은 egraphs-good/egglog-tutorial에서 확인할 수 있다.

튜토리얼을 통해 e-graph가 정말 흥미로운 연구대상임을 다시 느꼈다. 컴파일러 최적화기를 만들어낼 수도 있고, 프로그램 분석기를 만들어낼 수도 있다. e-graph의 적용 분야는 자동증명기, 프로그램 합성기, 그리고 새로운 재작성 규칙 발견까지도 나아가고 있다. 지금 내가 하고 있는 컴파일러 최적화 연구도 어떻게 e-graph의 지평을 넓힐 수 있을지 기대된다.

PLMW

첫날 오후에는 PLMW에 참석하였다. PLMW는 멘토링 워크샵으로 워크샵 양일 모두 열렸는데, 나는 그중에서도 첫날 서로 얼굴과 이름을 익히고 가까워질 수 있는 자리에 참석하였다.

특히 PL Card 프로그램에서 재밌는 기억이 많다. 이 프로그램은 카드 뭉치에서 카드를 뽑아 적혀있는 제시어를 설명하는 퀴즈 게임이다. 카드에 금지어도 적혀있었는데 금지어를 말하지 않고 제시어를 설명하는 게 꽤 고역이었다. 예를 들어, “C++” 제시어를 설명하려고 하는데 “C”나 “Programming”, “Language” 처럼 당연히 떠오르는 단어를 말하지 않고 “C++”을 제한시간 안에 설명하려고 하니 꽤 난이도가 있었다. Constrained Decoding이 걸려 토큰 확률 분포가 고장난 언어모델이 된 기분이었다. “C++”에 대한 나의 설명은 “Rust wants to get rid of it”이었는데, 같은 테이블에 있던 누군가 바로 맞췄던 기억이 난다.

또, “Garbage Collection”도 문제로 나와 나는 “C++은 이게 없는데 Java에는 있어”라고 설명했었다. 그런데 퀴즈가 끝나고 누군가 C++ standard에 Garbage Collection이 있지만 이를 따르는 C++ 구현체가 없다는 설명을 해줬다. 정말로 찾아보니 C++ 스탠다드에 Garbage Collection이 있었다. 도대체 C++에 없는 기능은 무엇이고, 그리고 이런 사실을 어떻게 아는 것일까. 프로그래밍 언어 고수들의 세계에 왔다는 생각이 들었다.

PLMW 세션을 통해 포르투갈에서 컴파일러를 연구하고 있는 Lucian과 친해졌는데 내가 매일같이 사용하는 Alive2를 개발한 Nuno Lopez 교수님에게 지도를 받는 학생이었다. Lucian은 마지막 날 내 발표에 찾아와 질문을 하기도 했고, PLDI 5일간 종종 만나 좋은 대화도 많이 나눴다.

PL 연구에 HCI의 원리를 적용하는 법에 대한 발표도 흥미로웠다. 연단이 아니라 무대 중간으로 나와 발표 내내 청중의 흥미를 끌어내는 발표 방식도 인상적이었다. HCI의 사용자 연구는 사용자가 겪는 문제를 이해하고, 문제에 대한 해결책을 디자인하고, 해결책의 효과를 입증하는 과정을 거친다. 사용자들이 겪는 문제를 사용자들이 원하는 해결책으로 해결가능한 경우가 많지 않기 때문에 문제를 제대로 이해하는 것이 중요하다는 것에 공감하며 강연을 들었다. PL과 HCI는 서로 거리가 먼 분야로 여겨지는데, 이 두 분야를 결합하는 아이디어가 있다는 것이 놀라웠다.

RPLS (Real-World Programming Language Specification)

둘째날 열린 RPLS에서 오전 세션이 특히 재미있었다. 그 중에서도 인터프리터, 컴파일러, 번역검산기 등 PL 도구를 자동으로 생성해내는 K-Framework 연구가 기억에 남는다.

K-Framework (이하 K) 발표는 제목부터 강력했다. “Programming Languages Must Have Formal Semantics. Period.”. 발표가 끝나고 연사인 Xiaohong Chen과 커피를 마시며 K에 대해 심도 있는 설명을 들을 수 있었다. 그 중에서 K의 설계 철학 그리고 올바름(Correctness)에 대한 설명이 기억에 남는다.

먼저, K는 연구 프로젝트로 시작했지만 이론보다 사용성에 더 무게를 두고 설계했다는 점이 흥미로웠다. 아무리 강력한 이론도 실제 세계에서 외면 받는다면 큰 족적을 남길 수 없는 게 사실이다. 그래서 K는 프로그래밍 언어 개발자들이 사용할 수 있는 도구들 즉 인터프리터, 컴파일러, 번역검산기 등을 자동으로 생성하고 바로 사용할 수 있도록 기능적인 측면을 강조하며 개발되었다고 한다.

또한, 올바름은 우리가 “무엇을 믿어야하는가”를 잘 따져봐야 논의할 수 있는 것이기 때문에 조심스럽게 접근해야한다는 설명도 들었다. 만약에 Z3 기반의 번역검산기를 사용한다고 해보자. 이 번역검산기의 결과를 그대로 사용한다면 우리는 Z3가 사용하는 논리 기반을 그대로 믿는 것이 된다. 하지만 정말로 그 논리 기반을 믿을 수 있는가? 게다가 Z3의 구현이나 번역검산기의 구현에 헛점은 없는가? 이는 수학에서 어떤 공리계를 믿어야 하는지를 의심하는 것과 비슷해 보였다. (참고: 수학의 선택공리 논쟁)

이런 점으로 미루어 볼 때, 거대한 K를 어떻게 그대로 믿을 수 있을까? 만약 K에 버그가 있다면 K가 만들어내는 모든 도구들도 신뢰할 수 없게 된다. 그래서 K는 K가 하는 모든 것에 자동으로 증명을 생성한다. 모든 것을 신뢰하지 않고 증명한다. 증명에 사용되는 공리도 매우 적어서 신뢰 문제에서 더 자유로울 수 있다는 설명이었다. 신뢰해야 하는 것이 적어서 더 신뢰할 수 있는 시스템이라는 설명이 재미있었다.

기억에 남는 발표들

Program Synthesis from Partial Traces

PLDI 본행사 첫째날 프로그램 합성(Program Synthesis) 세션에서 발표된 논문이었다. 발표 흐름에 맞춰 자연스럽게 진행되는 슬라이드 흐름과, 잘 정리된 내용이 독보적인 발표였다. AWS 연구 인턴으로 진행된 프로젝트였는데, 클라우드 서비스를 사용할 때 남는 API 로그(Partial Traces)를 통해 사용자가 자주 반복하는 일들을 원클릭으로 한번에 실행할 수 있는 프로그램으로 만들어주는 것이 아이디어다. 예를 들어, 가상머신 인스턴스를 종료하고, 종료되지 않았다면, 강제로 종료하는 것을 사용자가 반복해 이것이 로그로 남는다면 이 전체 과정을 사용자가 원클릭으로 다시 사용할 수 있는 프로그램으로 만들어주는 것이다.

질문 시간에 정보보호개론 조교를 하며 가상머신 150개를 세팅하던 경험이 떠올라 내 경우에도 사용할 수 있는지 물어봤다. (“This is exactly the tool I need!”) 프로그램 로그만 잘남고, 내가 하는 일들이 API 단위로 잘 정리되어 있다면 안될 이유는 없다는 답을 들었다. 발표가 끝나고 나서 복도에서 만나 더 얘기를 했는데, 가상 머신이 모종의 이유로 작동을 멈추는 경우, 모든 가상머신을 한번에 세팅하면 안되는 이유 등 여러 엣지 케이스들에 대해 같이 생각을 해봤는데 재미있는 결론이 났다. 만약 조교 업무를 1년마다 반복하게 된다면, 해가 갈수록 엣지 케이스를 더 잘 해결하는 프로그램을 합성하게 될 것이다. 그런데 이전에 합성해둔 프로그램을 이용해 새로운 케이스에 대해 더 잘하는 프로그램은 어떻게 만들 것인지 잘 알려진 방법이 없는 것이다. 이 방법을 찾으면 아마 박사학위를 하나 더 받을 수 있겠다고 농담하며 이야기는 일단락되었다.

Lean

둘째날 기조연설과 Industry 세션에서 모두 Lean에 관한 이야기가 나왔다. 예전 NYU 부전공 프로그램에서 프로그램 검증 수업을 청강했던 경험이 내용을 이해하는 데 많은 도움이 되었다. NYU에서는 Rocq(그 당시에는 Coq이라 불렀다)를 사용했었는데, 비슷한 시스템인 Lean이 최근 이렇게까지 성장했다는 사실이 놀라웠다.

아침 기조연설에서는 Lean의 창시자, Leonardo de Moura가 Lean의 여러 면모를 설명했다. 최근 테렌스 타오가 Lean을 적극적으로 사용하는 모습을 보여주면서 많은 관심을 끌고 있다는 것은 알았지만 기조연설을 통해 몰랐던 사실을 더 많이 배울 수 있었다. 특히나 Lean을 증명보조기 종류 중 하나로만 생각했었는데 자동증명기와 일반적인 프로그래밍 환경까지 통합되어 여러 분야에 사용될 가능성이 많아보였다. 최근 내가 하고있는 컴파일러 최적화 검증을 자동화하는 데에도 도움이 되지 않을까 생각했다.

오후 Industry 세션에서는 AWS 공순호 박사님이 Lean을 이용해 AI를 훈련시키는 연구 방향에 대해 이야기해주셨다. 잘 해결되지 않는 어려운 문제에 대해 LLM이 사실상 동전던지기보다 나은 점이 없다는 위트있는 시작과 함께 강연이 시작되었다. 강연은 AI를 훈련시킬 데이터가 고갈되어가는 세상에서 Lean과 같이 엄밀한 시스템이 새로운 데이터를 합성시키는 역할을 할 수 있다는 것이 핵심이었다. 또한 AI가 Lean과 상호작용하며 강화학습을 통해 성능을 향상시킬 수 있다는 점도 재미있는 연구방향이었다.

PLDI가 끝나고 Lean을 더 공부해보기 위해 Lean의 기반인 Dependent Type Theory도 간략하게 공부해보고, 테렌스 타오가 공개한 Lean으로 작성된 해석학 교재를 따라가보며 증명도 작성해보았다. 아직 내가 이걸 사용해서 어떤 일을 할 수 있을지 감은 안오지만 Lean이 저변을 계속 넓혀가고 있는 만큼 언젠가 다시 Lean을 만날 날이 오지 않을까 생각이 들었다.

연구 발표

나는 PLDI 본행사 마지막날 오전 컴파일러 세션에서 발표하게 되었다. 태어나 처음으로 하는 학회 연구발표가 PLDI라니 정말 뜻깊고 신기한 경험을 했다. 첫 발표, 그리고 PLDI 발표이니 만큼 15분안에 연구 결과의 핵심을 뚜렷하게 전달하기 위해 많은 노력을 했다. 설명은 최대한 단순명료하게 다듬고, 연구의 배경이나 개념이 생소할 경우를 대비해 오해가 없도록 내용을 준비했다. 그리고 관중이 압도되지 않도록 애니메이션을 통해 한번에 하나씩만 설명하도록 발표 내용을 준비했다. 연구실 리허설에서 교수님과 다른 분들이 슬라이드의 작은 점 하나하나, 그리고 발표 흐름의 오류까지 꼼꼼하게 찾아주신 덕분에 가능했다.

발표 전날에 마지막 점검을 했다. 호텔에서 치맥을 시켜놓고 태은님, 수진님, 그리고 동재님이 발표를 다시 한번 점검해주셨다. 마지막 점검이었는데 내 입, 슬라이드 애니메이션 그리고 몸짓이 동기화된 것을 확인하니 기분좋은 자신감이 솟아났다. 긴장한탓에 말을 빨리 해서 주어진 15분보다 시간을 덜 쓰긴 했지만 다음날 무대에서는 이것만 조심하면 되겠다고 다짐하며 치맥과 함께 마지막 발표 준비를 마쳤다.

PLDI 본행사 마지막날 11:50에 발표를 시작했다. 슬라이드 애니메이션을 모두 머리에 외우고 무대 가운대로 와서 설명할 생각이었는데 (스티브 잡스처럼 하고 싶었다), 생각과 다르게 프로젝터 빔이 내 눈에 닿는 바람에 옆으로 비켜 설명해야했다. 무대 구조가 예상과 달라 조금 당황하긴 했지만 전날 밤 리허설을 상기시키며 15분을 최대한 모두 사용하려고 주의하며 발표를 진행했다. 발표 도중 연구에 관심을 가져주신 분들이 슬라이드 내용을 사진으로 찍어가는 경우도 볼 수 있었고, 발표를 마치고 남은 시간에 질문도 여러번 받았다. 세션을 모두 마치고 추가적인 질문도 받아서 준비한 내용을 성공적으로 전달한 것 같아 많은 보람을 느낄 수 있었다. 연구실 내부 리허설, 전날 점검 그리고 발표 당일까지 격려과 많은 관심을 보내주신 연구실 분들께 감사하다는 말을 전하고 싶다.

네트워킹 경험
컴파일러 세션에서 발표중인 Chris Fallin

이번 PLDI 2025에서 다른 연구자들과 네트워킹한 경험도 빼놓을 수 없다.

최근 연구하고 있는 Cranelift 컴파일러의 리드 개발자인 Chris Fallin, Cranelift 컴파일러의 최적화 규칙과 코드 생성 규칙의 검증 도구 Crocus를 작성한 Alexa VanHattum도 만나 얘기할 수 있었다. 최근 Cranelift에 최적화 규칙을 추가하는 PR을 4개 보냈었는데 Chris Fallin이 나를 알아보는 신기한 경험도 하고, 내 연구 방향에 대해 설명하는 기회도 가졌다. 내 연구를 알아보는 사람들이 있다는 걸 느끼고, 사람들에게 도움을 줄 수 있는 연구를 더 열심히 해야겠다는 다짐을 했다.

우연히 Lean의 창시자 Leonardo de Moura와 옆자리에 서게 되어 Lean 개발 이야기도 생생하게 들을 수 있었다. 또한, 내가 자주 사용하는 Alive2의 창시자인 Nuno Lopez도 만나 얘기해볼 수 있었는데, 스마트폰없이 피처폰만으로 서울을 돌아다니는 무용담을 들을 수 있었다. (생각해보니 같이 사진이라도 찍을 걸 그랬다!)

또한 우리나라에서 PL을 연구하시는 다른 분들도 만나는 기회도 가졌다. 연세대학교 정기웅 박사과정님의 소개로 고려대학교 전민석 박사님, 우리학교 강지훈 교수님 연구실의 안해찬님, 이정인님을 만나 같이 식사자리를 가졌다. 이와 더불어 서울대학교 연구실에 계시는 대학원생분들은 어떤 분야에 관심을 가지고 계시는지도 알 수 있었다. 우리나라에서 정형검증에 관심을 가진 분들이 많이 있다는 것을 느꼈고, 시간이 날 때마다 나도 전산논리를 다시 공부하고 Lean을 익혀야겠다는 생각을 했다.

마치며

이번 PLDI 2025는 다른 연구자들과 만나 내 시야를 넓히고 재미있는 아이디어들을 배울 수 있었던 최고의 학회였다. 최대한 많이 배워가고자 모든 세션에 적극적으로 참여하고자 했고 들은 모든 연구발표에 대해 최대한 질문을 하려고 노력했다. 이런 학회에서 직접 발표까지 하다니, 정말로 영광스러운 기회였다. 컴퓨터 과학자로서 한발짝 성장한 느낌이다. 5일 모두 참여를 지원해주신 허기홍 교수님께 깊은 감사를 드린다.

You May Also Enjoy