▲

AI가 형식 검증을 주류로 만들 것이다

 (martin.kleppmann.com)
11P by GN⁺ 3일전 | ★ favorite | 댓글 1개
  • 형식 검증(formal verification) 은 코드가 명세를 항상 만족함을 수학적으로 증명하는 방법으로, 오랫동안 연구 중심의 한정된 영역에 머물러 있었음
  • seL4 마이크로커널 등 일부 대형 시스템이 형식 검증으로 개발되었지만, 높은 난이도와 비용 때문에 산업 현장에서는 거의 사용되지 않았음
  • 최근 LLM 기반 코딩 보조 도구가 구현 코드뿐 아니라 여러 언어의 증명 스크립트 작성에서도 성과를 내며, 검증 비용 구조를 크게 바꿀 가능성이 제시됨
  • AI가 코드 생성과 함께 정확성 증명까지 자동화할 수 있다면, 인간의 코드 리뷰보다 신뢰할 수 있는 개발 방식으로 전환될 수 있음
  • 형식 검증의 자동화는 AI 시대의 소프트웨어 신뢰성 확보 핵심 기술로, 기술적 한계보다 문화적 전환이 주류 확산의 관건이 될 전망임

형식 검증의 현재와 한계

  • Rocq, Isabelle, Lean, F*, Agda 등 증명 지향 언어와 도구는 코드가 명세를 만족함을 수학적으로 증명할 수 있게 함
    • seL4 운영체제 커널, CompCert C 컴파일러, Project Everest 암호 프로토콜 스택 등이 대표 사례
  • 그러나 산업 현장에서는 형식 검증이 거의 사용되지 않음
    • seL4의 경우 8,700줄의 C 코드 검증에 20인년과 20만 줄의 Isabelle 코드가 필요
    • 한 줄의 구현당 23줄의 증명과 반나절의 인력이 요구됨
  • 전 세계적으로 이러한 증명을 작성할 수 있는 전문가는 수백 명 수준으로 추정됨
  • 경제적으로도 대부분의 시스템에서 버그로 인한 손실보다 검증 비용이 더 큼, 따라서 실용성이 낮았음

AI가 바꾸는 형식 검증의 경제성

  • 최근 LLM 기반 코딩 어시스턴트가 구현 코드뿐 아니라 증명 스크립트 작성에서도 성과를 보임
    • Nature, Galois, arXiv 등에서 LLM이 여러 언어로 증명을 생성한 사례가 보고됨
  • 현재는 전문가의 지도가 필요하지만, 완전 자동화가 수년 내 가능할 것으로 예상됨
  • 검증 비용이 급감하면 더 많은 소프트웨어에 형식 검증을 적용할 수 있음
  • 동시에 AI가 생성한 코드는 인간 검토 대신 형식 검증으로 신뢰성 확보가 필요
    • AI가 코드의 정확성을 스스로 증명할 수 있다면, 수작업 코드보다 선호될 가능성 있음

LLM과 증명 검증의 상호 보완성

  • LLM이 증명 스크립트를 작성할 때 허위 내용(환각) 을 생성해도, 증명 검사기(proof checker) 가 이를 거부함
    • 검사기는 자체적으로 검증된 소규모 코드로 구성되어 있어 잘못된 증명을 통과시키기 어려움
  • 따라서 LLM의 불확실성을 형식 검증의 엄밀성이 보완함
  • 이 조합은 AI가 생성한 코드의 신뢰성을 확보하는 안전한 자동화 경로로 작동

새로운 과제: 명세 정의의 정확성

  • 자동화된 검증 환경에서도 명세(specification) 를 올바르게 정의하는 것이 핵심 과제로 남음
    • 증명된 속성이 실제로 개발자가 의도한 속성과 일치하는지 확인해야 함
  • 명세 작성은 여전히 전문성과 신중한 사고가 필요하지만, 수작업 증명보다 훨씬 간단하고 빠름
  • AI가 자연어와 형식 언어 간 명세 번역을 지원할 수도 있음
    • 다만 의미 손실 위험이 존재하며, 이는 관리 가능한 수준으로 평가됨

소프트웨어 개발 방식의 변화 전망

  • 개발자는 원하는 코드의 속성을 선언적 명세로 기술하고, AI가 구현과 증명을 함께 생성하는 형태로 전환 가능
  • 이 경우 개발자는 AI가 생성한 코드를 직접 검토할 필요가 없으며, 컴파일러의 기계어처럼 신뢰 기반으로 사용 가능
  • 요약하면 다음 세 가지 변화가 예상됨
    1. 형식 검증 비용의 급격한 하락
    2. AI 생성 코드의 신뢰 확보를 위한 검증 수요 증가
    3. 형식 검증의 정밀성이 LLM의 확률적 특성을 보완
  • 이러한 요인들이 결합되면 형식 검증은 소프트웨어 공학의 주류 기술로 자리 잡을 가능성이 높음
  • 향후 한계 요인은 기술보다 개발 문화의 변화 수용 속도가 될 것으로 전망됨
▲
GN⁺ 3일전  [-]
Hacker News 의견들

  • 나는 형식 검증(formal verification) 이 명세보다 구현이 훨씬 복잡한 영역에서 진가를 발휘한다고 생각함
    예를 들어 암호화 구현의 비트 단위 최적화나 컴파일러 최적화 단계 같은 곳임
    하지만 대부분의 개발자(혹은 AI)가 작성하는 코드는 이미 고수준 언어 덕분에 명세에 가깝기 때문에, 형식 검증의 이점이 크지 않다고 봄
    명세를 따로 작성하는 게 더 읽기 쉬울지도 의문임
    지금도 다양한 프레임워크와 라이브러리가 구현 세부를 추상화해주기 때문임
    형식 검증이 더 강력한 보장을 줄 수는 있겠지만, 대부분의 사람은 그런 수준의 보장을 원하지 않으며 AI가 새로 그 필요를 만들지도 않을 것 같음

  • 어떤 사람들은 AI가 형식 검증을 완전히 자동화할 것이라 예측하지만, 나는 그 논리에 문제가 있다고 봄
    AI가 소프트웨어를 자동으로 증명할 수 있다면, 굳이 인간이 작성한 소프트웨어를 검증할 필요도 없을 것임
    AI가 스스로 아이디어를 구상하고 구현하며 검증 수준을 결정할 수 있을 테니까
    결국 인간이 하는 프로그래밍이나 검증은 사라질 가능성이 큼
    실제로 인간이 증명 보조기를 설계하는 건 가능하지만, 그걸로 대규모 프로그램을 검증하는 건 훨씬 어려움
    따라서 그런 AI가 등장한다면, 스스로 새로운 증명 보조기를 만들어낼 수 있을 것임
    물론 이런 상상은 SF 영역에 가깝고, AI가 어떤 일을 더 쉽게 혹은 어렵게 할지 명확히 알지 못하는 상태에서의 예측은 의미가 없음
    관련 논의 링크

    • 인간과 로봇의 첫 전쟁은 우리가 “안 돼”라고 말할 때, AI가 “이 기술이 인류에게 좋다”고 주장하는 순간일지도 모름
      그게 인류가 완전히 다른 국면으로 넘어가는 전환점이 될 것 같음

  • 코딩 에이전트(Claude Code, Codex CLI 등)에서 유용한 결과를 얻으려면, 그들이 작성한 코드를 실행하고 검증할 수 있는 환경을 잘 갖추는 게 핵심임
    Python처럼 실행이 쉬운 언어가 가장 적합하고, HTML+JS라면 Playwright 같은 도구를 써야 함
    그다음 단계는 자동화된 테스트 스위트, 그리고 코드 포매터, 린터, 퍼저 같은 품질 도구임
    디버거도 좋지만, 상호작용적이라 에이전트가 다루기 어렵다는 점이 있음
    형식 검증 도구도 이 스펙트럼에 포함된다고 봄 — 요즘 모델들은 특수한 프로그래밍 언어도 잘 다루기 때문임
    만약 코딩 에이전트가 별로 쓸모없다고 느껴진다면, 실행 및 테스트 환경이 부족해서일 가능성이 큼

    • 강력한 타입 시스템을 가진 언어를 쓰는 것도 큰 도움이 될 것 같음
      Haskell을 예로 들면, 컴파일만 되면 거의 항상 제대로 동작함
      이런 특성이 인간에게 유용하다면 LLM에게도 마찬가지일 것임
      특히 property test는 LLM과 궁합이 좋음 — 적은 테스트로 넓은 오류 영역을 커버할 수 있기 때문임
      수학 커뮤니티에서 Lean 코드 개선에 LLM을 쓰는 시도가 있는 걸 보면, 더 강력한 타입 시스템을 활용한 소프트웨어 개발도 충분히 가능할 것 같음
    • LLM이 디버깅을 학습하기는 쉽지 않을 것 같음
      디버깅은 순차적이지 않고, 원인과 결과의 시점이 뒤섞이기 때문임
      예전에 gdb로 멀티스레드 버그를 잡을 때 ChatGPT를 시도해봤지만, 단순한 프린트 추가 제안만 반복했음
      결국 경험과 직관이 필요한 영역임을 다시 느꼈음
    • 결국 이런 도구들이 인간 개발자에게도 똑같이 중요하다는 게 흥미로움
      주니어 엔지니어에게 디버거나 테스트 러너 없이 일하라고 하는 건 말이 안 됨
    • 모델이 세미콜론 하나 때문에 “생각”하며 컴파일을 반복할 걸 기다리는 건 꽤 웃길 듯함
      결국 컴퓨팅 자원이 더 필요해질 것 같음
    • 나는 Claude Code와 Codex, Gemini를 멀티 에이전트 구조로 함께 사용함
      Claude가 구현하고, Codex와 Gemini가 리뷰함
      이 방식은 비용이 많이 들지만, 자기 편향(self-bias) 을 줄이고 코드 품질을 높이는 가장 확실한 방법이었음
      정적 분석 도구가 추가로 도움이 되겠지만, 단순히 툴을 늘리는 것만으로는 충분하지 않다고 느낌

  • 검증 과정이 자동화되면, 진짜 어려운 부분은 명세(specification)를 정확히 정의하는 일로 옮겨감
    증명 자체보다 명세 작성이 훨씬 빠르고 쉽지만, 여전히 전문성과 신중함이 필요함
    과거에 형식 증명이 확산되지 못한 이유는 어려움 때문만이 아니라, 워터폴 방식이 사라지고 애자일 개발이 대세가 되었기 때문임
    긴 명세를 쓰는 대신, 사용자 요구에 맞춰 빠르게 반복하는 방식으로 진화했음

  • 이제 OCaml을 배워야 할 때인 것 같음
    많은 증명 보조기와 검증 시스템이 OCaml 코드를 생성할 수 있고, ADA/Spark도 고려할 만함
    어떤 식으로든 AI 시대의 소프트웨어 공학이 바뀌겠지만, 우리는 지금보다 더 높은 품질의 소프트웨어를 만들어야 함
    형식 검증은 그 목표에 분명 도움이 될 것임

  • 아직 미완성이지만, 내 실험 프로젝트를 공유함
    코드 중심의 글이 부족한 세상에서 누군가 재미있는 해커톤 아이디어를 찾고 있다면 참고할 만함
    py-mcmas 프로젝트 링크

  • LLM은 검증이 쉬운 문제를 잘 푸는 경향이 있음
    그래서 나는 문제 해결을 세 단계로 나눔
    1️⃣ 성공 조건 프로그램을 먼저 작성하고
    2️⃣ 그 프로그램으로 원래 문제를 검증하게 하고
    3️⃣ 마지막으로 내가 직접 확인함
    이런 방식은 예전부터 써온 접근이지만, 이제는 Opus나 GPT-5.2 같은 모델이 무인 모드로도 잘 수행함
    관련 블로그 글

    • 하지만 많은 문제는 검증이 어렵고, LLM은 겉보기엔 맞지만 실제론 틀린 결과를 잘 만들어냄
      검증이 오래 걸리는 분야에서는 오히려 인간의 검증 부담만 늘어날 수 있음

  • “검증 프로그램은 누가 검증하나?”라는 질문이 나올 수 있음
    LLM이 그것도 작성한다면 끝없는 거북이의 탑(turtles all the way down) 처럼 보일 수 있음

    • 하지만 증명은 기계적으로 검증되기 때문에, 올바른지 확인하는 건 쉽고
      어려운 건 증명을 만드는 과정임
      물론 복잡한 명제에서는 예외가 있지만, 버그를 줄이는 데 큰 도움이 됨

  • 형식 검증이 대중화된다고 해서 모두가 Lean이나 Isabelle을 쓰게 되진 않을 것 같음
    오히려 AI가 기존 워크플로우에 자연스럽게 녹아드는 형태로 확산될 것임
    예를 들어 CI에서 속성 검증, IDE에서 “이 모듈의 불변식 증명하기” 버튼 같은 식임
    대부분의 엔지니어는 증명 스크립트를 직접 볼 필요도 없을 것임
    진짜 어려운 건 LLM이 증명을 만드는 게 아니라, 조직이 명세와 모델을 작성하도록 투자하게 만드는 일임
    AI가 명세를 제안하고 수정하는 걸 쉽게 만들어준다면, 검증은 테스트나 린터처럼 자연스러운 리팩터링 도구로 자리 잡을 것임

  • GPT‑5.2가 “garlic에 r이 몇 개인지”도 제대로 못 세더라며 불평하는 사람도 있음

    • 하지만 그건 드라이버로 무게를 재려는 것과 같음
      정말 필요하다면 LLM에게 파이썬 스크립트를 작성해 실행하게 하면 됨
    • 이런 비판은 솔직히 지루함
      맞는 말이긴 하지만, 토크나이징 구현 세부일 뿐 실제 유용성과는 거의 무관함
      단어 속 글자 수 세는 일에 LLM을 쓸 일은 거의 없음
답변달기