Insights
AI가 자동으로 큐레이션·번역·정리하는 기술 동향 피드입니다.
본 글은 소프트웨어 개발이 명령형에서 형식 검증 가능한 선언적 언어로 전환될 것이라 예측합니다. LLM을 활용하여 복잡한 시스템의 설계와 컴파일을 시도하지만, 명세의 복잡성과 강력한 컴파일러 구현이라는 난제가 남아있음을 지적하며 현 단계에서는 실현 가능성에 회의적입니다.
AI 자동 생성 콘텐츠
본 콘텐츠는 RSS: GeekNews (한국어)의 원문을 AI가 자동으로 요약·번역·분석한 것입니다. 원 저작권은 원저작자에게 있으며, 정확한 내용은 반드시 원문을 확인해 주세요.
원문 바로가기오히려 LLM이 생성한 명령형 코드를 LLM으로 형식 검증하는 대신, 에이전트 개발까지 포함해 명령형 언어에서 함수형을 건너뛰고 결정론적 선언형 언어로 옮겨갈 것으로 봄.
SQL용 TypeScript처럼, 더 정교한 연산자로 명령형 코드와 같은 결과를 간결하게 표현하는 실험적 언어들이 등장할 듯함. 게임이나 Linux 커널에 쓸 만큼 빠른 코드로 컴파일하면서, 사실상 공유 메모리를 쓰는 분산 실행 엔진에서도 실행할 수 있을 것임.
산출물이 짧아지면 환각 가능성, 출력 토큰, 추론 반복이 줄고 사람이 검토하기도 쉬워짐. 여기에 정리 형태의 문법과 고수준 효과 시스템(effect system)을 넣어 함수의 동작을 제한하고, 암호 함수의 상수 시간 실행, 로컬 읽기·쓰기의 ACID 준수, 분산 함수의 정확히 한 번 전달 등을 검증할 수 있을 것임. 결국 모든 프로그램이 기본적으로 형식 검증되는 AdaErlangSQL+++ 같은 형태를 예상함.
설명한 것은 제한된 유사 영어 형식 언어로 작성한 고수준 설계 문서를 받아, 거의 임의의 복잡도를 가진 형식 검증 가능한 시스템으로 컴파일하는 언어임. 분산 시스템의 조율까지 포함하는 셈임.
정말 가능하다면 AGI의 강력한 증거이거나, 적어도 연봉 수십만~수백만 달러 소프트웨어 엔지니어 시대의 끝일 것임. 하지만 나는 실현 가능성이 낮다고 봄. 그토록 광범위하고 복잡한 동작을 잘 처리하는 컴파일러 자체가 터무니없이 복잡해질 것임.
일반 논리, 시간 논리, 요구사항 등을 통일된 관계형 언어로 표현하는 실험을 해봤는데, 작동은 하지만 예상 밖의 장애물이 있음.
명확한 선언적 사실에 LLM, 좋은 최적화기, 증명 인증 시스템을 붙이면 성능도 해결될 듯하지만, 관계형 명세는 너무 많은 동작을 자동으로 함축함. 그중 실제로 무엇을 계산할지 의식적으로 선택해야 하며, 결국 관계 사이에서 명령형과 비슷한 계산 경로를 찾게 됨. 같은 문제가 추상화 수준만 한 단계 올라가서 다시 나타나는 느낌임.
방향에는 공감하지만, 실제로 시도하는 곳이 있는지 궁금하고 직접 탐구해보고 싶음. 현재 AdaErlangSQL+++에 가장 가까운 답은 Rust 같지만, Rust의 의미 체계는 사람의 사용성을 중심으로 설계됨.
사람은 한 번에 유지할 수 있는 항목이 적은 반면 기억을 불러오는 범위는 모델의 문맥보다 넓은 듯함. LLM의 문맥 크기와 한계, 특성에 맞춰 언어와 도구를 새로 설계하면 어떤 모습일까? 짧은 연산자 대신 영어 단어처럼 더 풍부한 어휘를 활용할 수도 있겠지만, 모델 학습을 위해 먼저 엄청난 양의 소프트웨어를 작성하거나 변환해야 할 것임. 에이전트 전용 IDE도 필요함. Claude가 일주일 전에 직접 작성한 코드를 이해하려고 bash 반복문과 grep을 어설프게 엮는 모습을 보면 답답함. Anthropic은 여러 도구를 시험해도 grep이 낫다고 하지만, 매번 한두 차례 실패한 뒤에야 해결하는 것을 보면 납득하기 어려움. 코드 탐색과 검증에 특화된 도구가 있으면 더 빠르게 작업하고, 사소한 단계마다 확인하는 대신 코드 공간에서 더 많은 추론을 할 수 있을 것임.
LLM 열풍에는 회의적이지만, 그런 전환이 실제로 유용하게 작동한다면 큰 진전일 것임. 다만 먼저 명세의 복잡성과 충분히 똑똑한 컴파일러라는 오래된 난제를 해결해야 함.
원하는 동작을 정밀하게 명세하면서도 그 언어가 기존 프로그래밍 언어만큼 복잡해지지 않게 할 수 있을까? 선언적 명세에서 효율적이고 신뢰할 수 있는 구현을 안정적으로 생성할 수 있을까?
개발자가 여전히 세부 동작을 신중하게 명세해야 하고, 명세에서 좋은 구현을 생성하는 방법까지 확보했다면 LLM이 더할 가치는 얼마나 남을까? 구현 생성에는 LLM보다 결정론적 알고리즘이 더 나은 해법일 가능성이 커 보임.
자연어를 명세로 바꾸는 역할은 가능하겠지만, 정확히 작동해야 하는 시스템은 결국 개발자가 모든 세부 명세를 설계하고 검토해야 함. 기본 선택을 입력하면 초기 파일과 코드를 만들어주는 뼈대 생성 도구 정도의 역할은 현실적이고 유용하지만, 전체 개발 과정에서는 작은 부분일 수 있음. LLM이 더 나은 언어와 도구의 등장을 촉진하길 바라면서도, 그 도구가 생긴 뒤에도 LLM의 이점이 얼마나 남을지는 의문임.
부록에서는 에이전트가 작성한 증명도 동등성 정리를 증명한다는 점에서 다른 증명과 똑같이 유효하지만, 장황한 증명 방식의 확장성은 미지수라고 함. MachCSL 등에서는 복잡성의 벽에 부딪혔고, 확장하려면 더 나은 모듈식 추상화와 추론 원리가 필요했음. 적절한 추상화를 에이전트가 스스로 찾게 할 수 있는지, 전문 증명 엔지니어의 도움이 필요한지가 핵심임.
최근 LLM의 수학 증명에서도 비슷한 양상이 보여, 인간 수학의 볼록 껍질(convex hull) 바로 바깥에서 능력이 한계에 달할 것이라는 가설이 나옴. 형식 검증 대상 시스템은 학습 분포 안에 있다고 보장할 수 없어, 수많은 책에 반복 등장하는 수학 구조와 달리 사전학습의 방대한 지식이 큰 이점이 되지 않을 수 있음. Anthropic과 Theorem의 관찰은 이 가설에 힘을 실어준다고 봄.
[0] https://www-cdn.anthropic.com/files/4zrzovbb/website/6867ead....
예상 가능한 결과임. LLM은 사람이 모르는 방대한 지식을 조합하니 창의적으로 보이지만, 신경망은 보간에는 강하고 외삽에는 약함. 학습 데이터의 볼록 껍질을 정말 벗어나는 지식을 만드는 것은 외삽에 해당함.
나는 그 경계에 있는 코드와 아이디어를 자주 다루지만, 증명까지 시켜보며 밀어붙여도 LLM이 진정으로 혁신적인 해법을 제안하는 것은 보지 못함. 통찰을 주면 증명을 만들 수는 있지만, 새로운 아이디어는 직접 설명해줘야 쓰며 때로는 설명해도 익숙한 방법으로 되돌아감. 개인적인 관찰이지만, 이 문제를 해결한 논문을 아직 보지 못했고 신경망의 이론을 생각하면 저절로 외삽을 잘하게 되리라고 기대하지 않음.
커리–하워드 대응으로 보면 증명 작성은 특수한 언어로 코드를 작성하는 일임. 더 나은 추상화로 모듈식 증명을 만드는 것은 더 나은 모듈식 코드를 만드는 것과 같음.
에이전트는 전반적인 프로그래밍 실력을 높여야 함. 지금은 장황한 코드와 중복을 쉽게 허용하다가, 코드베이스가 커지면 제대로 처리하지 못함. 더 잘 모듈화된 증명을 학습시키면 일반적인 프로그래밍 능력, 적어도 Haskell 작성 능력은 좋아질 것으로 봄. 정리 증명기 상당수가 충분히 강력한 함수형 언어이기 때문이며, 그 능력은 Rust에도 일부 전이될 것임.
수학 학습이 Creusot, flux, Aeneas로 Rust 코드를 증명하는 능력으로 이어질 수 있고, 증명을 쓰지 않더라도 추론하기 쉬운 코드를 만들게 될 수 있음.
[0] https://creusot.rs/.
[1] https://flux-rs.github.io/.
[2] https://lean-lang.org/use-cases/aeneas/.
볼록 껍질 비유가 마음에 듦. LLM은 지식과 노하우를 사회 전반에 퍼뜨려 돈, 시간, 전문성 부족 때문에 막혀 있던 돌파구를 열어줄 수 있음. 개인적으로 인공지능 자체보다는 지식의 민주화 도구로서 더 가치 있다고 봄.
그 앞부분에서는 에이전트 증명이 CPU 레지스터 내용, 정수 변환, 주소 간 구별, 스택 주소의 정확한 내용, 모든 분기를 반복적으로 풀어 쓰는 반면, 인간 증명 엔지니어라면 즉시 추상화를 도입해 중복을 제거했을 것이라고 함.
이는 LLM이 자기 작업을 확인하려고 만드는 깨지기 쉬운 테스트와도 일치함. 거의 모든 것을 하드코딩해서, 소스의 본질과 무관한 변경에도 중요한 속성을 검사하지 않는 테스트들이 줄줄이 깨짐. LLM에 수정을 맡기면 다시 구체적 구현에 과도하게 묶인 테스트를 전부 새로 쓰며, 회귀 테스트 모음이라는 개념이 사실상 없음.
사람이든 LLM이든 구현자가 검증까지 맡으면 가정과 맹점, 오해를 그대로 옮길 수 있음. 요구를 충분히 구체화하지 않은 내 잘못이라고 할 수도 있지만, 원하는 결과를 얻기 위해 그렇게까지 설명해야 한다면 직접 구현하겠음.
관찰에는 동의하지만 그로부터 미래의 한계까지 단정하는 데에는 동의하지 않음. 충분히 어려운 문제로 강화학습을 하면 더 나은 증명 전략이 자연스럽게 나타날 수도 있음.
Postgres를 Rust로 다시 작성하면서 형식 검증을 꽤 성공적으로 활용하고 있음. Rust와 C를 모두 Lean으로 변환하는 컴파일러를 만들었고, 변환된 두 함수가 동일하게 동작한다는 Lean 증명을 LLM에 작성시킴.
지금까지 단일 스레드 실행 기준으로 코드의 약 12%, C 코드 약 7만 줄의 동등성을 증명함. 플랫폼별 부동소수점 연산 결과 같은 아주 미세한 동작 차이도 발견함. 확장 방법을 연구 중이며, 더 확장하지 못하게 할 근본적 한계는 보이지 않음.
그 컴파일러의 정확성은 어떻게 검증하나요? 최소한 Lean으로 정의한 C와 Rust의 형식 의미론이 필요할 듯한데, 둘 다 엄청난 작업으로 보임.
Rust와 C를 Lean으로 변환하는 컴파일러는 rustc나 clang을 포크한 것인가요, 아니면 다른 기반인가요? 12%면 상당히 고무적임. 핵심 동작을 정적 분석으로 저렴하고 실용적으로 증명할 수 있기를 바라며, LLM과 프로그래밍 언어 이론의 접점은 아직 탐구가 부족해 보임.
Lean 증명 작성에는 어떤 모델이 생산적인가요?
지난 몇 주 동안 직장에서 이런 작업을 하고 있음. 에이전트가 SIMD나 CUDA 최적화 실험을 담은 PR을 올리고, 원래 구현과 동작이 동등하다는 Rocq 증명까지 첨부하면 확신을 가지고 병합할 수 있다는 것이 매우 강력함.
증명한 정리가 실제 코드에 적용된다는 확신은 어떻게 얻나요?
작업 흐름이 궁금함. 기존 바이너리의 속성을 증명하는 실험을 하고 있는데 진행 속도가 극도로 느림.
집을 짓는 일에는 원하는 것을 정하는 의도, 그 의도를 명세로 옮긴 설계도, 실제 결과가 설계도와 맞는지 확인하는 검증이라는 세 층이 있음.
이 연구는 검증을 거의 완벽하게 만들지만, 검증은 설계도만 확인할 뿐 의도까지 확인하지는 않음. 잘못된 설계도로 지은 집도 완벽한 검사를 통과할 수 있음. 나머지 절반은 명세가 의도와 일치하고 에이전트가 작업하는 동안에도 그 일치가 유지되도록 하는 일임. 나는 그 부분을 개발하고 있어 상호 보완적이라고 봄. https://github.com/pullboard-dev/pullboard
대체 무엇을 기준으로 형식 검증한다는 것인가요? 의도한 입력과 의도하지 않은 입력, 모든 이해관계자와 사용자 행동까지 포괄하는 완전한 형식 명세가 바이브 코딩 시대에 존재한다는 것인가요? 본문도 그런 명세가 없다는 점은 인정함.
결국 일반적인 퍼저로 충돌을 찾고 수정한 다음, 그 충돌이 수정됐다는 형식 증명을 쓰는 것이라면 별 의미가 없어 보임. 내가 놓친 것이 있나요?
본문의 요지는 퍼즈 테스트가 더는 충돌을 찾을 수 없다는 증명이 생각보다 강력하다는 것임. 실제 퍼즈 테스트는 인코딩·디코딩 왕복, 멱등성, 대수 법칙, 차등 테스트, 자기 일관성, 참조 구현과의 동등성 같은 고수준 속성을 검사하기도 함.
예를 들어 LZO 테스트가 압축 후 해제한 결과와 원본의 일치를 검사하고 불일치 시 충돌한다면, 테스트가 절대 충돌하지 않는다는 증명은 그 속성 자체의 증명이 됨. 다만 프로그램의 의도를 완전히 담았다고 검증된 명세에 대한 정확성 증명은 아니라는 점은 맞음. 그래도 상당히 인상적임.
실제로 한 일은 일반적인 퍼저가 충돌을 찾지 못한다는 것을 증명하고, 반례가 발견되면 버그를 고친 뒤 다시 시도하는 것임.
퍼저는 가능한 입력 공간에서 무작위 표본을 뽑지만, 여기서는 그 입력 공간 어디에서도 충돌하지 않음을 증명함. 퍼저만으로 얻을 수 있는 것보다 엄밀히 더 강한 결과임.
주어진 입력 크기 범위의 모든 가능한 입력에 대해 기계어 수준에서 프로그램이 충돌하지 않음을 증명하는 것임. 퍼저가 실행한 사례만이 아니라 전체 입력 집합과 그 입력들이 거치는 모든 코드에 적용되므로, 어떤 퍼저보다도 검증 범위가 넓음.
버그가 있는 소프트웨어 A를 기능과 버그까지 그대로 유지한 소프트웨어 B로 바꾸는 데 유용함. 대규모 코드 구조 변경에서 버그를 추가하지도 제거하지도 않았는지 검증할 수 있음.
기술적으로 가능성은 높아 보이지만, 지금까지 소프트웨어에서 LLM을 도입하며 주로 모범 관행을 버려왔다는 점 때문에 검증 확대로 이어질지 회의적임. 직원들은 병에 소변을 보게 하면서 주 3일 근무 시대를 이야기하는 Bezos를 보는 느낌임.
자동 증명은 멋지지만, 암호학이나 항공우주처럼 이미 극도로 신중한 극소수 분야에만 머물 듯함. 나머지 분야는 얻은 여유를 검증하지 않은 코드를 더 빨리 출시하는 데 쓰며, 규율을 속도와 맞바꿀 것임.
병에 소변을 보는 상황은 지대로 설명할 수 있음. 생산성이 오르면 임대인이 임대료를 올리고, 희소한 토지 소유자들을 위해 더 많이 생산해야 함.
소프트웨어에는 이런 토지 희소성의 구조가 없음. Rust가 C보다 더 안전한 기반이듯, LLM으로 더 건전한 기반을 만들고 그쪽으로 이전하면서 코드 품질도 개선될 것임. Rust++ 라이선스 비용 때문에 병에 소변을 봐야 할 만큼 착취당하지는 않을 것임.
AI는 공학의 암흑 에너지처럼 서로를 더 빠르게 멀어지게 함. 일부는 저품질 결과물로, 다른 일부는 형식 명세 검증으로 향하며 시간이 갈수록 서로를 이해하기 어려워질 것임.
한때 지식인은 철학자였고 서로 대화할 수 있었지만, 이제는 서로 나눌 이야기가 거의 없는 분야별 박사들로 나뉨. 공학도, 소프트웨어 공학도 같은 분화를 거쳤고 지금 다시 그 일이 일어나는 중임.
인간의 지식과 경험을 특정 작업, 함수, 상황에 맞는 멱등적 지침과 코드로 정제하면, 거의 무한한 퍼징과 공격에 맞서 시험할 수 있음.
적절히 처리한 강철의 강도를 믿듯 코드도 다르지 않음. 언젠가는 등반가의 생명을 지탱하는 카라비너와 로프처럼 코드를 신뢰하는 단계에 도달할 것임.
코드는 물리적 장치에서 실행되며, 장치는 저전압, 비트 반전, 특정 생산분의 하드웨어 버그, 방사선, 노후화 등에 취약함. 밧줄에 매달린 채 AA 배터리로 작동하는 계산 장치에 목숨을 맡기고 싶지는 않음.
그 결론은 맞지 않음. 그 정도로 신뢰할 수 있는 코드는 이미 수십 년 전부터 존재함. Common Criteria와 EAL은 20세기 말에 자리 잡았고, 그전에는 1980년대부터 미국의 Rainbow Series가 있었음.
검증이 저렴하고 쉬워지는 것은 반갑지만, 아무도 신경 쓰지 않으면 의미가 없음. EAL1 인증은 고성능 서버 한 대 정도 비용으로도 가능하지만, 사실상 관심이 없어 널리 시행하지 않음. Microsoft가 Zune으로 배웠듯 저렴하거나 같은 가격에 더 좋다고 해서 사용되는 것은 아님. 문화적으로 코드 검증에 들이는 노력이 보상받게 해야 함.
[1]: https://en.wikipedia.org/wiki/Rainbow_Series.