Abstract
LLM은 빠른 코드를 사람이 소화하기 어려운 속도로 생산한다. 이처럼 막대한 양의 코드에는 발견하기 어려운 오류가 섞여 있어, 올바름(correctness)을 자동으로 검증하려는 시도가 이어지고 있다. 그러나 최근 실험에서 올바름과 성능을 함께 요구받은 LLM이 증명하기 쉬운 느린 코드를 선택하는 현상이 관찰되었다. 본 글은 LLM 생성 코드의 올바름과 성능을 함께 보장하는 자동 증명 및 최적화 파이프라인의 필요성을 논한다.
본문
LLM에게 빠른 코드 생성은 더 이상 어려운 일이 아니다. 인간은 오랫동안 알고리즘의 성능을 다듬어 왔다. LLM은 그 알고리즘들을 학습했고, 이제 최정상급 인간과 경쟁한다. 최근 국제정보올림피아드(IOI)에서는 금메달 수준에 올랐고, AtCoder에서는 세계 정상급 인간을 압도했다 12.
LLM은 효율적인 알고리즘을 잘 “알고"있다. 27개의 교과서 알고리즘을 구현하게 하자 GPT-5.6 Sol은 모든 문제에서 교과서 수준의 시간 복잡도를 달성했고, 하위 모델인 Luna도 25개(92.6%)에 성공했다. 빠른 코드 생성은 더 이상 문제가 아니다.
그렇다면 LLM이 작성한 코드를 신뢰할 수 있을까? 알고리즘 대회의 성적은 코드가 주어진 테스트를 통과했음을 보여줄 뿐, 모든 입력에서의 올바름을 보장하지는 않는다. LLM은 방대한 코드 더미를 생산하면서도 찾기 어려운 미묘한 오류를 함께 만들며 3, 이는 자동 증명에 대한 연구로 이어지고 있다 4. 결국 코드의 성능과 올바름 모두를 자동으로 증명해야 한다.
그러나 빠름과 올바름을 함께 요구하면, LLM은 “빠름"을 내려놓는다. 퀵 정렬(quicksort)을 요구했지만 $\mathcal{O}(n^2)$ 삽입 정렬(insertion sort)을 사용했고, 다항 시간에 풀리는 할당 문제(assignment problem)를 비현실적 $\mathcal{O}(n!)$의 전수 조사로 대체했다 5. 실험 결과, LLM이 생성한 구현 중 올바름과 성능을 모두 만족한 것은 27개 중 2개(7.4%)뿐이었다.
결국 코드의 올바름을 증명하는 것만으로는 충분하지 않다. 올바른 $\mathcal{O}(n!)$ 코드를 받아들일 개발자와 사용자는 존재하지 않는다. 올바름 증명과 복잡도 검증, 자동 최적화와 재증명을 반복하는 파이프라인이 필요한 시점이다.
-
BenchLM. Vals IOI (IOI). https://benchlm.ai/benchmarks/valsioi, ↩︎
-
MLQ.ai. OpenAI’s AI sweeps all five problems at AtCoder world tour finals, beating every human. https://mlq.ai/news/openais-ai-sweeps-all-five-problems-at-atcoder-world-tour-finals-beating-every-human/, 2026. ↩︎
-
Stack Overflow. AI — 2025 Stack Overflow developer survey. https://survey.stackoverflow.co/2025/ai, 2025. ↩︎
-
Miryung Kim. Happiness u-curve: Navigating the AI validation bottle- neck with conformance testing and proof-engineering. Keynote at the 47th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), June 2026. https://pldi26.sigplan.org/details/pldi-2026-papers/2/Happiness-U-Curve-Navigating-the-AI-Validation-Bottleneck-with-Conformance-Testing-a. ↩︎
-
Zhe Ye, Hantao Lou, Yuechun Sun, Peiyang Song, Zhengxu Yan, Tim- othe Kasriel, Qingyang Zhang, Kaiyu Yang, Soonho Kong, Jingxuan He, and Dawn Song. Vero: Can AI agents build formally verified software repositories? arXiv preprint arXiv:2608.13522, 2026. https://arxiv.org/abs/2608.13522. ↩︎