Bend 2와 바이브 코딩의 함정: 사전 조사를 건너뛰면 왜 중복된 형식 검증 노력이 발생하는가

핵심 요약

Bend 2는 인간이 *법칙(laws)*을 작성하고 LLM이 구현과 증명을 생성하도록 시도하지만, 이 접근 방식은 58줄의 법칙 명세와 442줄의 AI 생성 증명을 필요로 합니다. 반면, 동일한 정확성 속성을 SPARK에서는 12줄 미만으로 표현하고 자동으로 검증할 수 있습니다. 이는 사전 조사를 소홀히 할 경우 불필요하게 복잡한 솔루션이 만들어질 수 있음을 보여줍니다.

Bend 2가 제공한다고 주장하는 것

인간이 작성한 법칙: 개발자가 상위 수준의 불변성(예: “플레이어는 절대 깃발에 닿을 수 없다”)을 인코딩합니다.
LLM 생성 구현: AI가 게임 로직을 채웁니다.
LLM 생성 증명: AI가 구현이 법칙을 준수한다는 형식 증명을 작성합니다.
컴파일러 검증: Bend 컴파일러가 증명의 건전성을 확인합니다.

Bend 홈페이지의 데모에는 LAWS.bend 파일(58줄)과 이에 대응하는 PROOF.bend 파일(442줄)이 포함되어 있습니다. 블로그 게시물의 작성자는 이러한 장황함이 설계 결함을 나타낸다고 주장합니다.

바이브 코딩의 함정 설명

"바이브 코딩은 문제에 대해 충분히 학습하여 훨씬 더 나은 솔루션이 존재한다는 것을 인식하기 전에 상당한 수준의 솔루션을 구축할 수 있게 합니다." — @handle

*바이브 코딩(Vibe coding)*이란 기존 문헌을 조사하지 않고 막연한 아이디어를 바탕으로 LLM에게 완전한 시스템을 생성하도록 프롬프트를 입력하는 것을 의미합니다. 이 함정은 다음과 같은 경우에 나타납니다:

연구 생략 – 개발자가 문제가 이미 해결되었는지 확인하는 대신 LLM의 출력에 의존합니다.
중복 노력 발생 – 결과물인 시스템이 성숙한 도구들이 이미 제공하는 기능을 중복해서 구현합니다.
복잡성 팽창 – LLM이 기존의 자동화된 증명 도구로 피할 수 있었던 방대한 상용구(예: 442줄의 증명)를 생성해야 합니다.

구체적인 비교: Bend 2 vs. SPARK

블로그 작성자는 Bend의 데모를 형식 검증을 위해 설계된 Ada 기반 언어인 SPARK로 재현했습니다. SPARK 버전은 다음을 포함합니다:

열, 행, 게임 상태에 대한 타입 정의.
불변성을 표현하는 Safe 고스트 함수.
안전성 보존을 보장하는 사후 조건을 가진 Step 프로시저.
플레이어가 절대 이길 수 없다는 사후 조건을 가진 Replay 함수.
게임을 표시하기 위한 간단한 드라이버 프로그램.

이 코드에서 gnatprove를 실행하면 다음과 같은 결과가 나옵니다:

Success: all checks proved (12 checks).

단지 12개의 검증 조건만 생성되며, 수동 증명 스크립트는 필요하지 않습니다. 전체 정확성 논증은 기본 SMT 솔버에 의해 자동으로 처리됩니다.

주요 차이점

측면	Bend 2	SPARK
명세 크기	58줄의 법칙	~30줄의 Ada 타입 및 계약
증명 크기	442줄의 AI 생성 증명	0줄 (자동 SMT 증명)
도구 체인 성숙도	신규, AI 중심, 99% AI 작성 컴파일러	수십 년 된, 감사 완료, GNAT 도구 체인 통합
커뮤니티 지원	작음, 주로 실험적	확립된 Ada/SPARK 커뮤니티, 방대한 라이브러리

Hacker News의 커뮤니티 반응

@pu_pe는 Bend 작성자의 평판에 관한 논의를 언급하며, 논쟁이 기술적 실체보다는 인신공격에 더 집중되었다고 지적했습니다.
@z7은 작성자가 형식 검증에 대해 몰랐다는 주장을 바로잡으며, 해당 주제에 대한 작성자의 이전 게시물들을 지적했습니다.
@captainmuon은 기존 검증 언어들이 문법적으로 너무 무거운 경우가 많으며, 개발자들은 내장된 계약 기능을 갖춘 더 친숙한 언어(예: C# 또는 JavaScript)를 원한다고 주장했습니다.
@mentalgear는 모든 LLM 주도 프로젝트는 바퀴를 다시 발명하지 않기 위해 "먼저 기존 연구 조사 실행" 단계를 시작해야 한다고 강조했습니다.
@LightMachine은 명시적 증명이 성능을 위해 의도된 것이며 언어의 커널이 의도적으로 얇게 설계되었다고 말하며 설계 선택을 옹호했습니다.
@simonw는 프로젝트를 시작하기 전에 검색 기능이 있는 LLM에게 기존 기술을 찾아달라고 요청하여 시간을 절약했던 개인적인 워크플로우를 공유했습니다.
@thomasahle은 SPARK의 자동 증명이 SMT 솔버에 의존하며, 이는 무차별 대입 방식이라 Lean이나 Bend와 같은 대화형 증명기의 표현력까지 확장되지는 않는다고 설명했습니다.
@mccoyb는 Bend 2가 양적 타입 이론(QTT) 시스템이며, Ada/SPARK와는 검증 스펙트럼의 다른 부분에 위치한다고 강조했습니다.

이러한 댓글들은 분열된 시각을 보여줍니다. 어떤 이들은 Bend 2를 불필요한 재발명으로 보는 반면, 다른 이들은 이를 다른 검증 패러다임에 대한 목적 있는 탐구로 봅니다.

LLM을 사용하는 개발자를 위한 교훈

문헌 조사로 시작하기 – 코드를 작성하기 전에 LLM에게 문제와 관련된 기존 도구, 언어, 라이브러리를 나열하도록 요청하십시오.
검증 모델 식별하기 – 자동 SMT 기반 검증(예: SPARK, Dafny)이 필요한지, 아니면 대화형 정리 증명(예: Coq, Lean, Bend 2)이 필요한지 결정하십시오.
절약된 노력 측정하기 – 명세와 증명의 크기를 알려진 기준과 비교하십시오. 과도한 상용구는 기존 솔루션을 놓쳤다는 신호일 수 있습니다.
커뮤니티 자원 활용하기 – 확립된 생태계는 위험을 줄여주는 감사된 컴파일러, 표준 라이브러리, 도구를 제공합니다.
LLM 출력을 초안으로 취급하기 – 생성된 증명의 정확성과 대상 검증 프레임워크의 모범 사례 관용구와의 일치 여부를 검토하십시오.

결론

Bend 2는 AI로 증강된 형식 검증의 유망한 비전을 보여주지만, 장황한 증명 생성은 더 넓은 바이브 코딩의 위험을 강조합니다. 즉, 기술의 현주소를 먼저 이해하지 않고 정교한 시스템을 구축하는 것입니다. 짧은 사전 조사만 수행하더라도 개발자는 종종 수천 줄의 AI 생성 증명을 몇 개의 자동 검증 조건으로 대체하여 시간, 토큰, 잠재적 버그를 절약할 수 있습니다. Bend 2를 둘러싼 논의는 LLM이 생산성을 높이는 동시에 이미 잘 해결된 문제를 재발명할 위험도 증폭시킨다는 점을 상기시켜 줍니다.