PLDI 데뷔기

연구실의 지원을 받아 내 인생 첫 국제 학회를 PLDI로 장식할 수 있었다. 프로그래밍 언어 분야에서는 최고로 평가받는 학회 중 하나였기 때문에 큰 기대를 안고 서울로 떠났다.

아침 9시부터 일정이 있어 오전 4시 30분에 일어나 대전역으로 출발했다. 전날 밤 늦게 잠들어 늦잠을 잘까 걱정했는데, 다행히 제시간에 일어났다.

신라스테이 입구. 호텔 로비는 8층에 있다

이번 학회에서는 신라스테이에서 4박 5일간 머물렀다. 학회에서 지친 몸과 마음을 달래주는 안식처 역할을 톡톡히 해주었다. 학회가 진행되는 웨스틴 조선과는 도보로 20여분 떨어져 있었다. 다행히 오고 가는 길이 쉬워 첫 날 이후로는 지도 없이 다닐 수 있었다.

허충길 교수님에 따르면 12만원 상당의 도시락이라고 한다. 매우 맛있었다

맨 처음 참여한 세션은 egglog¹ 워크숍이었다. egglog는 E-graph를 위한 datalog 스타일의 언어로, datalog와 굉장히 유사하지만 E-graph를 위한 여러 기능과 설탕 문법 (Syntactic Sugar)을 제공한다. 튜토리얼은 정말 재밌었지만, datalog와 본질적으로 다른 게 무엇인지는 잘 와닿지 않았다.

첫 세션 이후에는 바로 점심 식사가 제공되었다. 연구실 분들을 통해 학회에서 제공하는 식사의 질이 천차만별이라는 이야기를 들었었는데, 역시 ‘밥심’을 중요시하는 한국답게 매우 훌륭한 식사가 나왔다.

네트워킹

이번 학회에서 가장 기대했던 것은 해외 연구자들과의 네트워킹이었다. 순수 국내파로서 외국 연구자들은 어떤 사람들일지 굉장히 궁금했다. 한편으로는 네트워킹 문화가 활발하지 않은 한국에서 나고 자란 내가 잘할 수 있을지 걱정되기도 했다.

그러나, 실패가 있어야 성장도 있는 법. 첫 학회지만 최대한 많은 사람과 대화해보기 위해 노력했다.

첫 번째 네트워킹

나의 첫 대화 상대는 코넬 대학교에서 유학 중인 일본인 연구자였다. egglog 워크숍을 시작하기 전 안면을 텄는데, 커피 브레이크 시간에 혼자 돌아다니는 것을 발견하고 나의 네트워킹 실습 먹잇감으로 삼았다. Prosys 네트워킹의 대가 태은님의 조언²에 따르면, 혼자 두리번거리며 돌아다니는 아시아계 사람이 최적의 후보였다.

자신감있게 첫 인사를 건네고 나의 연구 분야를 소개했다. 연구 소개는 태은님의 조언에 따라 미리 준비했기 때문에 막힘없이 이야기 할 수 있었다. 그러나, 따라오는 꼬리 질문에서 집중력을 잃어 일부 내용을 놓치고 말았다. 대화가 산으로 가던 중 2명이 더 참여하여 다시 대화는 정상 궤도로 돌아왔다.

이번 대화를 통해 말을 이해하지 못했을 때 대처하는 방법이 필요하다는 것을 깨달았다. 토종 한국인인 나의 영어 실력과 집중력으로는 30초 이상의 연속된 문장은 무리였다. 적절한 시점에 내가 이해한 것이 맞는지 확인하는 스킬이 필요하다는 것을 알게 되었다.

PLMW

신입 연구자들을 위해 학회 차원에서 네트워킹 특화 워크숍 (PLMW) 시간을 마련해 주었다. 대부분 석사 과정 혹은 박사 과정 학생이었기 때문에 좀 더 편하게 다가갈 수 있었다.

첫날 워크숍은 PL-Card 게임과 Skill-Exchange 두 가지 활동으로 구성되어 있었다. PL-Card는 일종의 금지어 게임으로, 주어진 단어를 연관 단어를 사용하지 않고 설명하는 게임이다. 한국에만 있는 게임인 줄 알았는데 글로벌한 게임이었다는 사실이 놀라웠다. 부족한 어휘력으로 금지어를 피해 설명하려니 식은땀이 줄줄 났다. 다행히 눈치 빠른 친구들의 도움으로 즐겁게 게임을 즐길 수 있었다.

Skill-Exchange는 비슷한 관심사를 가진 사람들 끼리 같은 테이블에 앉아 각자의 연구를 소개하는 시간이었다. 나는 확률적 프로그래밍과 코드를 위한 AI 테이블에 앉았는데 나와 비슷한 연구를 하는 사람은 딱 한 명 찾을 수 있었다. 앞선 네트워킹과는 달리 상대방과 나의 관심사가 비슷했기 때문에 좀 더 편하게 대화를 이어갈 수 있었다. AI 불모지인 PL 학회에서 나와 비슷한 일을 하는 사람이 있다는 것이 무척 반가웠다.

저녁과 함께하는 네트워킹

감동적인 코스 요리

저녁은 PLMW 참가자들을 대상으로 제공되었다. 5성급 호텔의 코스 요리가 나왔는데, 음식마다 서로 다른 식기를 사용해야 하는 코스요리였다. 유튜브를 통해 바깥쪽부터 사용하면 된다는 정보를 미리 습득했기 때문에 어려움 없이 음식을 즐길 수 있었다.

네트워킹은 저녁을 먹으면서도 계속되었다. 저녁은 원형 식탁에서 8명이 둘러 앉아 식사를 하는 형태였다. 이 방식에는 치명적인 단점이 있었는데, 맞은 편 사람이 하는 말이 전혀 들리지 않는다는 것이었다. 현장의 소음이 상당했고, 부족한 영어 듣기 실력과 오전 4시 30분부터 쌓인 피로가 맞물려 대화에 전혀 집중하지 못했다.

이 경험을 통해 원형 테이블에서 네트워킹을 하고 싶으면 그 사람의 옆에 앉아야 한다는 것을 깨달았다. 넷째 날 저녁 만찬도 비슷한 방식으로 진행되었는데, 나는 같은 실수를 반복하고 말았다. 이 글을 읽는 사람이 있다면 나와 같은 실수를 반복하지 않기를 바란다. 물론 숙련된 네트워킹 전문가라면 원형 테이블 전체의 분위기를 재미있게 이끌어갈 수 있을 것이다.

친구 만들기

첫 만남에 찍었던 명찰 사진. 개인 정보 보호를 위해 이름 부분은 잘랐다

이번 학회 목표 중 하나는 해외 연구자 친구를 한 명 만드는 것이었다. 결론부터 말하자면, 퍼듀 대학에서 유학중인 중국인 친구 한 명을 사귈 수 있었다 (인스타 맞팔까지 성공했다).

첫 만남은 둘째 날 커피 브레이크 시간이었다. 태은님의 조언에 따라 이번에도 혼자서 안절부절하며 차를 마시고 있는 친구를 네트워킹 먹잇감으로 삼았다. 한 번 안면을 트고 나니 이후에도 종종 마주쳤을 때 10분 정도의 짧은 대화를 나누게 되었다. 그 친구와는 유독 사적인 대화를 많이 주고 받았는데, 역시 친밀감을 올리기 위해서는 연구 이야기보다는 일상적인 이야기가 더 효과적인 것 같다.

기조연설

네트워킹에 대한 이야기는 이쯤 하고, 이번 학회의 전반적인 분위기를 기조연설을 통해 정리해보려고 한다. 기조연설은 말 그대로 앞으로 학회의 방향성을 엿볼 수 있는 발표다. 특히 AI가 세상을 뒤흔드는 이 시점에, 교수님이자 선배 연구자의 생각을 확인할 수 있는 소중한 기회였다.

이번 기조연설들은 모두 AI 시대에 PL 연구자들이 할 수 있는 것을 중점적으로 다루었다. 아무래도 AI가 전방위적인 영향력을 떨치다 보니 당연한 흐름이었다. 기조연설뿐만 아니라 기업 차원에서도 신경망에 논리를 접목하는 연구에 큰 관심을 보였다. 특히 최근 RLVR (Reinforcement Learning with Verifiable Rewards)에 대한 관심이 높아지다 보니 자연스러운 현상이라는 생각이 든다.

AWS의 공격적인 채용 홍보

공통적인 메시지는 신경망만으로는 모든 것을 할 수 없고, 특히 소프트웨어나 수학처럼 매우 복잡한 시스템의 경우 반드시 기호 기반 추론의 도움이 필요하다는 것이다. 신경망에는 환각(Hallucination)이 발생할 가능성이 항상 존재하기 때문이다. 기조연설 주제였던 LEAN⁴, 신경-기호 프로그램 합성⁵ (Neurosymbolic Program Synthesis) 모두 이와 일맥상통한다. 류석영 교수님의 언어 스펙³은 이 맥락에서 약간 벗어나지만, 기호 기반의 명세가 자연어 명세와 비교했을 때 압도적으로 활용도가 높다는 것을 보여주셨다는 점에서 어떤 지식을 기호로 표현하는

어떻게 연결할까?

각자가 확실한 장단점을 가지고 있으니 두 개를 합치는 것이 좋다는 것은 자명하다. 핵심은 신경망과 기호 기반 추론 시스템을 어떻게 연결할 것이냐다. LEAN과 언어 모델을 결합하는 방식의 경우, 언어 모델이 LEAN을 직접 사용하여 프로그램을 검증하고 수학 문제를 증명하면 된다는 식이었다. LEAN 자체가 증명에 성공했을 때 그 증명의 올바름을 보장하기 때문에, 모델은 증명을 완성하기 위한 탐색만 열심히 하면 된다.

신경-기호 프로그램의 예시

신경-기호 프로그램 합성은 기호로 풀어내기 어려운 현실 세계의 모호한 문제들을 신경망을 이용해서 해결하자는 아이디어였다. 예를 들어, 사진에 있는 물체를 인식해야 한다고 하면, 신경망이 물체를 인식하고 그 결과를 기호에 대응시킨다. 그다음부터는 전형적인 프로그램을 실행하는 것과 다를 바 없다. 다시 말하면, 어떤 도메인 특화 언어의 의미 (Semantics)를 정의할 때 신경망을 하나의 함수처럼 활용한 셈이다. 위 사례에서는 Is 함수가 그 예시가 되겠다.

두 방법의 기본적인 골자는 신경망과 기호 기반 추론 시스템 사이의 소통 수단으로 형식 언어 (Formal Language)를 사용한다는 것이다. 이러한 방식은 언뜻 보기에는 매우 간편하게 일반화하여 적용할 수 있을 것 같지만, 실제로는 그렇게 간단하지 않다. 다음 질문에 답을 할 수 있어야만 이 방식을 통해 문제를 해결할 수 있다.

어떻게 형식 언어로 변환할 것인가?

신경-기호 프로그램 합성 기조연설에서 소개한 사진 편집 문제에서는 사진 속 물체를 형식 언어 속 단어로 표현했다. 그 후, “X의 왼쪽”과 같은 상대적인 위치 관계를 하나의 식 (Expression)으로 표현한다. 사진 편집 작업에서는 이것이 자연스러운 선택이지만, 다른 종류의 문제에서도 올바른 선택일까?

Autoformalization!

LEAN의 사례에서도 비슷한 질문을 할 수 있다. LEAN으로 증명을 하는 것은 좋은데, 무엇을 증명해야 할까? 그리고, 그 증명 목표를 어떻게 작성해야 할까?

자연어로 어렴풋이 주어진 증명 목표를 자동으로 LEAN의 증명 목표로 변환하는 것은 대단히 어려운 문제다 (참고: Autoformalization). 수학이나 코딩 문제가 아니라 일반적인 추론에서 기호 기반의 추론을 적용하려면 문제는 더욱 어려워진다. 수능 국어, 윤리 문제를 LEAN에서의 증명 목표로 변환하는 것을 상상해보면 왜 이 방법이 일반적으로 적용하기 어려운지 알 수 있을 것이다. 매우 추상적인 가치를 표현하는 단어 (정의, 선악, 仁)를 수학적으로 정의하는 것도 마찬가지다.

기호 추론 시스템을 활용하기 위해서는 자연어, 사진, 영상 등 현실 세계의 온갖 모호한 요소들을 어떻게 기호에 대응시킬 것인지 미리 결정해야 한다. 이 작업을 수행하기 위해서는 풀고자 하는 문제에 대한 도메인 지식과 함께 이 도메인을 표현하기에 적합한 언어를 설계할 수 있어야 한다. 내가 최근에 작업한 VeriSafe Agent⁸ 논문은 이 문제를 “모바일 에이전트” 영역에서 해결한 것이다.

결국 해결하려는 문제마다 다음 2가지를 결정해야 한다: 1. 어떤 형식 언어를 사용할 것인가? 2. 실제 세상의 모호한 요소들을 어떻게 형식 언어로 변환할 것인가? 모든 문제에서 잘 동작하는 만능 솔루션은 없을 것이라고 감히 예상해본다.

인상적인 연구들

나는 주로 합성, 소프트웨어 공학, 머신 러닝, 검증 세션에 참여했다. 많은 연구들이 흥미로웠지만, 그 중에서도 가장 인상적이었던 연구를 2가지 소개해본다.

Program Synthesis from partial trace⁶

Program Synthesis from partial trace 발표 요약 슬라이드

프로그램 합성을 매우 실용적인 작업에 적용한 점이 인상 깊었다. AWS에서 자원을 관리하다 보면 여러 인스턴스에 대해 비슷한 작업을 반복적으로 하는 경우가 생기는데, 이를 사용자의 작업 내역(Trace)을 보고 자동으로 매크로를 만들어주는 연구였다. AWS뿐만 아니라 평소에도 반복적이지만 스크립트를 쓰기에는 귀찮은 작업들이 여럿 있는데, 적절한 시점에 내 동작을 그대로 매크로로 생성해주는 시스템이 있으면 정말 좋을 것 같다.

이 연구를 보면서 문제 정의의 중요성을 다시금 깨달을 수 있었다. 합성 방법론에서 혁신적인 것은 없었지만, 매우 현실적이고 실용적인 문제를 해결하기 위해 합성 기술을 사용했다는 점이 매우 긍정적으로 보였다.

Guided Tensor Lifting⁷

1저자의 구직 활동. LLM을 활용한 합성 가이드를 통해 여러 문제들을 해결한 것으로 보인다

처음에는 제목만 보고 그렇게 흥미로운 발표는 아닐 것이라 예상했으나, 발표의 질부터 그 내용까지 정말 인상적이었던 연구였다. 풀고자 한 문제는 C로 작성된 행렬 연산을 아인슈타인 표기법으로 변환하는 연구였다.

대상 문제 자체는 잘 알려진 문제였으나, 해결하는 데 쓰인 방법이 인상적이었다. 언어 모델로 정답 후보를 10개 정도 생성하고, 이 후보들을 가지고 확률 문법(Probabilistic Grammar)을 학습한다. 그리고 이 확률 문법을 가지고 프로그램 합성을 진행하여 정답 프로그램을 찾는다. 프로그램의 올바름은 bounded model checking으로 확인한다. 놀랍게도 벤치마크의 99%를 합성하는 데 성공했다고 한다.

이 연구는 문제보다도 방법론이 흥미로웠다. DSL의 경우 언어 모델이 사전에 학습한 적이 없기 때문에 잘 못하는 경우가 태반인데, 이런 경우엔 합성기가 오히려 더 잘할 수 있다. 여기에 단순 열거형 탐색을 하는 것이 아니라, 언어 모델의 대답을 참고서 삼아 탐색을 진행하겠다는 아이디어가 좋았다.

2025 PLDI가 내게 남긴 것

자신감

첫 국제 학회를 한국에서 참여했다는 것은 굉장히 큰 행운이었다. 이동, 시차에 대한 피로 없이 학회를 온전히 즐길 수 있었고, 관광지, 맛집 등으로 스몰토크를 이끌어 갈 주제도 많았다. 무엇보다도 익숙함이 주는 자신감 덕분에 사람들에게 쉽게 다가가고, 먼저 말을 걸 수 있었다.

또한, 해외 연구자들이라고 해서 우리와 크게 다르지 않다는 것을 느꼈다. 연구 내용뿐만 아니라 평소 고민하는 것, 연구 방향성, 발표를 준비하는 태도 등 여러 방면에서 비슷하다고 느꼈다. 역시 사람 사는 건 다 거기서 거기라는 생각과 함께 내가 더 잘할 수 있겠다는 자신감이 차올랐다.

소속감

같은 관심사를 가진 사람들과 교류하는 것만으로도 즐거운 경험이었다. 사실 프로그래밍 언어 분야는 굉장히 중요하지만 학생들의 관심도가 높은 분야는 아니다. 특히 최근 AI가 급부상하면서 사실상 절반 이상의 학생들이 AI 혹은 AI 관련 분야에 관심을 가지고 있는 것이 현실이다. 이번 학회를 통해 내 연구를 알리고 사람들과 논의하면서 내 연구를 어떻게 발전시켜야 할지 생각을 가다듬을 수 있었다. 평소 느꼈던 토론과 논의에 대한 갈증이 많이 해소된 값진 시간이었다.

2025 PLDI를 마치며

하루 일정을 마치고. 많이 힘들어 보인다

모든 일정을 마치고 집으로 돌아가는 기차에서 2026 PLDI에서 발표하는 나의 모습을 상상해보았다. 흐뭇하면서도 못할 이유가 없겠다는 생각이 들었다. 이번에는 내 연구에 대해서 말로만 설명해야 했지만, 다음 참석할 PLDI에서는 논문, 홈페이지, 발표까지 잘 준비해서 사람들에게 내 연구를 널리 알리고 깊이 있는 논의를 나눌 수 있으면 좋겠다. 나와 비슷한 관심사를 가진 사람과 공동 연구도 진행해보고 싶다.

힘든 일정이었지만 많은 것을 얻고 배워간다. 이번 학회에 참여할 수 있도록 지원해주신 허기홍 교수님께 깊이 감사드린다. 논문 작성부터 마지막 밤까지 발표 준비하느라 고생하신 봉준님께도 축하의 박수를 보낸다. 그리고 나와 대화를 나누고 내 연구에 대해서 함께 고민해준, 2025 PLDI에서 만난 모든 인연에게도 감사 인사를 전한다.

---

각주

[1] Haobin et al. “Unlocking advanced equality saturation–based optimizations with egglog” PLDI Workshops and Tutorials (2025)
[2] Taeeun Kim, “야 너두 네트워킹 할 수 있어”, https://prosys.kaist.ac.kr/networking-guide
[3] Sukyoung Ryu. “Programming Language Research for Technical and Social Good: What PL Can Do for Good?” PLDI Keynote (2025)
[4] Leonardo de Moura. “Lean: Machine-Checked Mathematics and Verified Programming, Past and Future” PLDI Keynote (2025)
[5] Işıl Dillig. “Neurosymbolic Program Synthesis: Bridging Perception and Reasoning in Real-World Applications” PLDI Keynote (2025)
[6] Ferreira et al. “Program Synthesis from Partial Traces” PLDI (2025)
[7] Yixuan et al. “Guided Tensor Lifting” PLDI (2025)
[8] Jungjae Lee et al. “Safeguarding Mobile GUI Agent via Logic-based Action Verification” MobiCom (2025)