Lean 증명 자동화, 연구를 넘어 실제 소프트웨어로 진입하다

Lean 증명 자동화는 7월 26일 실용적인 경계를 넘었다. 보안 엔지니어 Adam Langley가 AI 지원을 받아 형식 검증한 Zstandard 디코더를 소개한 것이다. Langley에 따르면 여러 대규모 언어 모델이 약 20분 만에 상당한 분량의 증명을 생성했다. 이후 Lean은 미완성 플레이스홀더를 허용하지 않은 채 해당 증명을 검사했다. 작은 실험이지만, 검증된 소프트웨어에 대한 고질적인 가정, 즉 증명 비용이 더 이상 프로그램 비용을 훨씬 웃돌지 않을 수 있다는 점에 도전한다.

그렇다고 AI 모델이 광범위하고 철학적인 의미에서 디코더의 정확성을 증명했다는 뜻은 아니다. Langley는 검증할 속성을 선택하고 구현의 상당 부분을 작성했으며, Lean이 생성된 증명 항을 받아들였는지 확인했다. 그의 디코더는 표준 zstd 명령보다 약 10배 느리기도 했다. 진정한 변화는 더 좁지만 더 유용하다. AI는 이제 어떤 엔지니어링 프로젝트가 경제적으로 타당해 보이는지를 바꿀 만큼의 형식 증명 작업을 수행할 수 있다.

이는 일반 테스트와 형식 검증을 새로운 경쟁 구도에 놓는다. 테스트는 선택된 실행을 표본으로 삼는 반면, 형식 증명은 정리로 표현된 모든 입력을 포괄할 수 있다. 역사적으로 이처럼 강한 보장은 막대한 인건비를 수반했다. 유명한 seL4 운영체제 프로젝트는 구현 작업을 크게 웃도는 증명 노력을 보고했다. AI가 신뢰할 수 있는 검증 경로에 진입하지 않은 채 이 노동을 압축한다면, 증명으로 뒷받침되는 소프트웨어는 더 이상 커널과 암호화 분야에만 허용되는 전문 영역으로 보이지 않게 된다.

Lean Zstandard 실험이 실제로 바꾼 것

중요한 결과는 AI가 코드를 작성했다는 사실이 아니다. AI가 생성한 증명 작업이 독립적인 기계적 검사기를 통과했다는 점이다.

Langley는 함수형 프로그래밍 언어이자 대화형 정리 증명기인 Lean으로 Zstandard 압축 해제기를 만들었다. 일반적으로 Zstd로 줄여 부르는 Zstandard는 빠른 무손실 압축을 위해 설계된 압축 형식이다. 이 디코더는 압축된 헤더, 엔트로피 부호화 심볼, 길이, 오프셋 및 반복 시퀀스를 정확히 해석해야 한다.

이러한 세부 사항은 일반적인 타입 시스템이 배제하기 어려운 버그를 정확히 만들어 낸다. 디코딩된 길이가 사용 가능한 입력과 맞지 않을 수 있다. 배열 인덱스가 경계를 넘을 수 있다. 손상된 테이블이 존재해서는 안 되는 상태를 만들 수 있다. 개발자는 보통 검증, 런타임 검사, 테스트, 퍼징 및 신중한 리뷰로 이런 가능성을 관리한다.

Lean은 또 다른 선택지를 제공한다. 의존 타입 시스템은 타입에 값에 관한 사실을 포함할 수 있게 한다. 함수는 바이트 배열과 함께, 그 배열이 요청된 길이를 가진다는 기계 검사 가능한 보장을 반환할 수 있다. 이후 코드는 요소에 접근할 때 그 보장을 사용할 수 있다.

Langley는 런렝스 인코딩을 처리하는 디코더 분기에서 이 패턴을 보여줬다. 이 분기는 블록에서 한 바이트를 읽어야 했다. Lean은 블록에 그 바이트가 포함되어 있다는 증명을 요구했다. 구현은 요청된 읽기 길이를, 이 블록 유형의 콘텐츠 크기가 항상 1임을 보여주는 정리와 연결했다.

이 국소 증명은 짧았다. 더 중요한 사례는 Zstandard가 심볼을 효율적으로 표현하기 위해 사용하는 유한 상태 엔트로피, 즉 FSE와 관련된다. Langley는 형식에 설명된 테이블 구축 알고리즘을 구현한 뒤, AI 시스템에 출력의 보편적 속성을 증명하도록 요청했다.

요청된 속성은 예제 기반 테스트를 넘어섰다. 테이블 크기, 각 심볼에 할당된 항목 수, 테이블 내 유효한 전이를 다뤘다. 다시 말해 이 증명은 명세가 제공한 세 개의 테스트 벡터뿐 아니라, 허용되는 모든 분포에서 성립해야 하는 구조적 규칙을 기술했다.

Langley는 여러 LLM이 이 증명을 약 20분 안에 완성했다고 보고한다. 또한 이 작업이 일반적인 월간 구독 할당량의 일부만 소비했다고 말한다. 모델들은 그의 명령형 구조가 Lean의 증명 도구와 잘 맞지 않았기 때문에 구현 일부를 수정했다. 이후 그는 최종 증명이 타입 검사에 통과했고, 미완성 증명을 명시하는 Lean의 표식인 sorry를 포함하지 않는다는 점을 확인했다.

코드 발췌와 한계를 포함한 그의 전체 설명은 원문 proof automation 게시물에서 확인할 수 있다. 그는 디코더 저장소를 공개하지 않았으므로, 외부 개발자는 아직 모든 주장을 재현할 수 없다. 이는 독립적으로 벤치마크된 결과가 아니라 경험 보고로 남아 있다.

그럼에도 이 실험은 신뢰할 만한 워크플로를 제시한다. 인간이 불변 조건을 명시한다. AI는 증명을 탐색하고 필요하면 코드를 재구성한다. Lean은 생성된 증명 항을 검사한다. 모델이 노동을 제공하지만, 검사기가 수용 여부를 결정한다.

이 분업이야말로 이 결과를 일상적인 AI 코딩 데모와 구분하는 요소다.

Lean 증명 자동화가 지식 노동자에게 중요한 이유

증명 자동화가 중요한 이유는 중요한 가정을 문서의 문장으로 남겨 두는 대신, 검사 가능하고 재사용 가능한 작업 산출물로 바꿀 수 있기 때문이다.

대부분의 지식 노동자는 압축 디코더를 작성하지 않는다. 그러나 이들 역시 문서화되지 않은 가정으로 구성된 시스템 안에서 일한다. 재무 모델은 특정 열에 고유 식별자가 들어 있다고 기대한다. 정책 워크플로는 모든 승인에 책임 있는 담당자가 있다고 가정한다. 연구 파이프라인은 모든 인용문이 출처를 유지한다고 기대한다.

팀은 이런 규칙을 문서, 주석, 온보딩 자료 또는 회의록으로 표현하는 경우가 많다. 그러나 작업이 도구와 부서를 넘나들수록 규칙은 약해진다. 필드 이름 변경, 예외적인 레코드 또는 변경된 프로세스는 즉각적인 경고 없이 규칙을 무효화할 수 있다.

형식 기법은 소프트웨어에서 유사한 문제를 다룬다. 선택된 가정을 기계가 검사할 만큼 정밀한 문장으로 바꾼다. Lean은 의존 타입을 사용한다. 즉 타입이 값에 의존할 수 있어 입력과 출력 간의 상세한 관계를 인코딩할 수 있다.

이 언어는 AI가 생성한 증명 스크립트를 실행하고 결론을 신뢰하는 데 그치지 않는다. Lean 전술은 논증을 독립적으로 검사할 수 있는 표현인 증명 항을 구성한다. 이후 작은 커널이 각 항이 시스템의 논리 규칙을 따르는지 검증한다. 공식 Lean kernel 문서는 편리한 자동화와 신뢰할 수 있는 검사의 이러한 분리를 설명한다.

이 구조는 AI를 둘러싼 위험 계산을 바꾼다. 언어 모델은 전술을 환각하거나, 정의를 오해하거나, 잘못된 목표를 추구할 수 있다. 그러나 이런 실패 대부분은 조용히 수용되는 정리가 아니라 거부되는 코드로 이어진다. 모델은 신뢰할 수 없을 수 있지만 최종 수용 관문은 엄격하게 유지된다.

그렇다고 전체 워크플로에 오류가 없다는 뜻은 아니다. 유효한 증명도 잘못된 문장을 확립할 수 있다. 정의는 현실 세계의 동작을 빠뜨릴 수 있다. 가져온 라이브러리는 가정을 도입할 수 있다. 검증된 소스 수준 함수도 여전히 검증되지 않은 컴파일러, 운영체제 또는 프로세서에 의존할 수 있다.

Lean의 자체 proof validation 지침은 이러한 경계를 강조한다. 커널 수용은 정리가 그 정의와 의존성으로부터 따라온다는 사실을 보여준다. 그것이 사람이 의도한 바를 정확히 포착했다는 사실까지 보여주지는 않는다.

지식 노동자에게 이 구분은 수식은 완벽하지만 비즈니스 정의가 잘못된 스프레드시트와 닮아 있다. 계산은 내부적으로 일관될 수 있지만, 잘못된 질문에 답할 수 있다. 형식화는 가장 어려운 검토를 명세 쪽으로 이동시킨다.

이러한 전환은 가치가 있다. 인간은 수천 개의 기계적 증명 단계보다 의도와 맥락을 더 잘 검토하는 경향이 있다. AI는 반복적인 탐색을 더 많이 흡수하고, 사람은 실제로 참이어야 하는 것이 무엇인지 면밀히 살필 수 있다.

같은 패턴은 이미 실무 정보 작업에 나타나고 있다. AI는 요약, 분류, 쿼리 및 변환을 초안으로 만든다. 책임 있는 워크플로는 이후 결과를 원자료, 스키마, 제약 조건 또는 결정론적 계산과 대조한다. 증명 자동화는 이 패턴을 훨씬 더 엄격한 수준에 적용한다.

이는 개인 맥락이 여전히 중요한 이유도 분명히 한다. 모델은 보지 못한 불변 조건을 보호할 수 없다. 팀에는 올바른 동작을 정의하는 의사결정 기록, 명세, 사례 및 예외에 대한 접근이 필요하다. 잘 관리된 personal knowledge base는 형식 증명이 여전히 전문 활동에 머무르더라도 입력 규율의 일부가 된다.

당면한 기회는 모든 메모를 형식화하는 데 있지 않다. 이미 숨겨진 명세처럼 작동하는 비용 큰 가정을 식별하는 데 있다. 그런 가정은 흔히 시스템, 팀 또는 규제 의무의 경계에 자리한다.

새로운 경쟁은 증명 비용과 검증 가치의 대결이다

AI가 형식 검증을 바꾸려면, 명세와 유지보수 작업을 늘리는 속도보다 증명 노동을 줄이는 속도가 더 빨라야 한다.

형식 검증은 설득력 있는 결과가 부족했던 적이 없다. seL4 마이크로커널은 대표적인 사례다. 기계 검사된 증명은 구현과 형식 명세를 연결하고, 테스트만으로는 확립할 수 없는 속성을 다룬다.

공식 seL4 verification 자료는 지원되는 구성에 코드 수준 기능 정확성 증명이 포함된다고 설명한다. 일부 구성은 이러한 보장을 바이너리 코드까지 확장한다. 이 프로젝트는 지속적인 전문 인력 투입을 정당화할 만큼 위험 부담이 클 때 형식 기법이 무엇을 제공할 수 있는지 보여준다.

동시에 도입이 좁은 범위에 머문 이유도 드러낸다. Langley는 seL4 회고 자료를 인용하며, 엔지니어들이 설계와 구현보다 증명에 약 10배 더 많은 노력을 쏟았다고 추정한다. 그는 또한 증명 코드가 C 구현보다 20배 이상 많았다고 언급한다.

이 비율을 보편적인 비용으로 받아들여서는 안 된다. seL4는 복잡한 운영체제 커널 전반에 걸쳐 유난히 강력한 보증을 추구했다. 속성, 언어 및 도구 체인이 달라지면 비용도 달라진다. 그럼에도 이 수치는 역사적 문제를 잘 포착한다. 증명 작업이 제공 비용을 지배할 수 있다는 점이다.

전통적인 증명 자동화는 이 부담의 일부를 줄인다. 단순화기, 결정 절차, SAT 솔버 및 SMT 솔버는 많은 목표를 해결할 수 있다. 그러나 개발자는 종종 각 솔버가 잘 처리하는 방식에 맞춰 코드와 보조정리를 구성해야 한다.

Langley는 이를 솔버를 만족시키는 데 필요한 육감을 기르는 일로 설명한다. 유리한 단편 밖에 있는 목표는 자동화된 탐색을 비생산적인 경로로 보낼 수 있다. 그러면 엔지니어는 도구가 풀 수 있는 형태로 문제를 번역하는 데 시간을 쓴다.

LLM은 다른 역량을 제공한다. 주변 정의를 읽고, 오류 메시지를 살피고, 전술을 시도하고, 중간 보조정리를 도입하며, 구현을 수정할 수 있다. 모든 문제가 하나의 고정된 결정 절차에 맞아야 하는 것은 아니다.

이 유연성은 기존 증명 도구 위에서 AI를 오케스트레이션 계층으로 유용하게 만든다. 모델은 적합한 곳에서 결정론적 전술을 호출하고, 다른 곳에서는 명시적 논증을 작성하며, Lean의 피드백을 활용해 실패를 수정할 수 있다. 모델이 증명 전략을 탐색하는 동안 커널은 엄격한 수용 검사를 제공한다.

Langley의 경험은 중요한 비용도 드러낸다. 그는 Id.run을 과도하게 사용했는데, 이는 Lean 내부에서 명령형 계산을 표현하는 방식이다. 그 때문에 AI 보조 도구가 테이블 구축 코드를 변경했다. 원래 코드는 읽기 쉽고 실행 가능했을 수 있지만, 증명에는 덜 친화적이었다.

이는 증명 공학, 즉 증명이 가능하고 유지보수 가능하도록 프로그램과 보조정리를 구성하는 작업이다. AI는 비용을 줄일 수 있지만 근본적인 긴장을 없애지는 못한다. 인간에게 익숙한 방식, 런타임 성능 및 증명의 단순성에 최적화된 코드는 언제나 같은 형태를 공유하지는 않을 것이다.

따라서 경제적 질문도 달라진다. 팀은 더 이상 “이것을 증명할 수 있는가?”만 묻지 않는다. 대신 “개발자가 제품을 변경하는 속도만큼 AI가 증명과 그 뒷받침 구조를 유지할 수 있는가?”를 묻는다.

이는 안정적이고 명시적인 경계를 지닌 소프트웨어에 유리하다. 파서, 인가 정책, 프로토콜 상태 머신, 금융 계산, 데이터 변환은 대체로 명확한 속성을 드러낸다. 또한 이들의 실패 모드는 더 높은 수준의 보증을 정당화한다.

AWS는 인가 정책 언어 Cedar를 통해 유용한 프로덕션 비교 사례를 제공한다. AWS는 Rust 구현과 나란히 실행 가능한 Lean 모델을 유지하고, 증명과 차분 테스트를 함께 사용한다. 공개된 verified development 설명에 따르면 Cedar 릴리스에는 최신 모델, 증명, 테스트가 필요하다.

Cedar가 모든 애플리케이션이 Lean으로 옮겨가야 한다는 것을 증명하는 것은 아니다. 다만 형식적 산출물이 실제 릴리스 프로세스 안에서 살아갈 수 있음을 보여준다. AI 지원 증명 탐색은 이러한 프로세스를 지속할 수 있는 팀의 범위를 넓힐 수 있다.

가장 강력한 단기 모델은 여전히 하이브리드 방식일 가능성이 높다. 엔지니어는 주류 언어로 프로덕션 코드를 구현한다. 고가치 동작은 Lean으로 형식화한다. 테스트는 두 구현을 비교하고, 증명은 모델의 속성을 확립한다.

Langley는 디코더 자체를 Lean으로 구현하는 더 직접적인 경로를 택했다. 이는 코드와 정리 사이의 강한 연결을 만들었지만, 큰 성능 저하를 수반했다. 검증된 모델과 검증된 프로덕션 코드 사이의 선택은 여전히 핵심 과제다.

증명이 증명하지 않는 것

커널이 검증한 증명은 한 종류의 불확실성을 제거할 수 있지만, 명세와 구현 경계, 운영 환경은 여전히 열어 둔다.

“이제 증명 자동화가 가능하다”라는 제목은 의도적으로 도발적이다. 이 실험은 실용적인 의미에서 이를 뒷받침하지만, 명시된 한계 안에서만 그렇다. LLM이 임의의 프로덕션 소프트웨어를 독립적으로 검증할 수 있음을 입증하는 것은 아니다.

첫째, 소스 코드를 사용할 수 없다. Langley는 증명이 타입 검사를 통과하고 미완성 플레이스홀더가 없음을 확인했다고 말한다. 독자는 그의 추론과 예시를 평가할 수 있지만, 전체 빌드를 재현할 수는 없다.

둘째, 이 작업은 장난감 수준의 디코더를 대상으로 했다. Zstandard는 본격적인 포맷이며, FSE 테이블 구성도 단순하지 않다. 하지만 이 프로젝트는 수년간의 기능 변경, 여러 팀, 하위 호환성, 적대적인 통합 환경, 프로덕션 사고 압박에 직면하지 않았다.

셋째, 이 디코더는 표준 명령줄 구현보다 약 10배 느렸다. 이 차이는 중요하다. 소프트웨어는 증명이 우아하다는 이유만으로 핵심 운영 요건을 포기할 수 없다.

Langley는 검증된 어셈블리가 성능 문제를 해결할 수 있는지 탐구했다. 그는 AWS의 LNSym 프레임워크를 사용해 최적화된 AArch64 어셈블리가 Lean 함수와 일치함을 증명하는 방안을 고려했다. 작은 예제에서는 작동했지만, 그의 테스트에서는 접근법이 확장되지 않았다. 유한 비트 벡터 명제용 전술인 bv_decide를 사용한 작은 예제 하나는 그의 컴퓨터가 감당할 수 있는 것보다 더 많은 메모리를 요구했다.

이는 검증에도 비용이 들지 않는 것은 아니라는 점을 상기시킨다. 증명 항은 커널이 처리하기에 비싸질 수 있다. 자동화된 탐색은 메모리나 시간을 소진할 수 있다. 이론적으로 유효한 워크플로도 빌드 예산을 초과할 수 있다.

넷째, 모델은 구현을 변경해야 했다. 이는 본질적으로 나쁜 일이 아니다. 증명은 프로그램 구조가 의존하는 관계를 숨기고 있음을 드러낼 수 있다. 명시적 불변식 중심으로 리팩터링하면 유지보수성이 개선될 수 있다.

하지만 AI가 생성한 리팩터링은 동작을 바꾸거나 성능을 떨어뜨릴 수도 있다. 최종 정리는 자신이 명시한 속성만 보호한다. 엔지니어는 그 속성 밖의 모든 것에 대해 여전히 테스트, 벤치마크, 코드 리뷰, 위협 모델링이 필요하다.

다섯째, 사람이 작성하는 명세는 여전히 가장 민감한 지점이다. 디코더 정리가 테이블의 올바른 형식을 증명하지만 다른 곳의 정수 오버플로를 빠뜨린다면, 검증된 속성은 여전히 참이지만 불완전하다. 형식화된 Zstandard 동작이 실제 포맷과 다르다면 Lean은 잘못된 모델을 충실하게 검증할 수 있다.

관련 압축 포맷은 RFC 8878에 문서화되어 있지만, 산문으로 된 표준을 정의로 옮기는 과정에는 해석이 개입된다. 모호성은 정리 증명기에 들어간다고 사라지지 않는다. 그것은 모델링 결정이 된다.

비전문가가 AI에 의존해 명제와 증명을 모두 생성할 때 이 위험은 커진다. 모델은 명제를 약화해 쉽게 증명 가능한 주장으로 만들 수 있다. 문제가 되는 입력을 제외하는 편리한 정의를 선택할 수 있다. 검증기를 통과하면서도 검토자의 의도를 놓칠 수 있다.

이는 증명 검토에 다른 인터페이스가 필요함을 의미한다. 검토자는 각 정리의 평이한 언어 설명, 가정, 가져온 공리, 다루는 코드 경로, 제외된 동작을 확인할 수 있어야 한다. 초록색 체크 표시만으로는 충분하지 않다.

조직은 또한 비즈니스 결정과 형식적 정의 사이의 추적 가능성이 필요하다. 정책이 바뀌면 누군가는 어느 정리가 이를 인코딩하는지 알아야 한다. 구현이 바뀌면 시스템은 어떤 보증을 다시 검토해야 하는지 식별해야 한다.

이 지점에서 AI 지원은 전술 작성 이상의 도움을 줄 수 있다. 에이전트는 관련 명세를 검색하고, 코드 변경을 영향을 받는 불변식에 매핑하며, 실패한 검증 의무를 요약할 수 있다. 검색 가능한 지식 기반은 설계 맥락과 형식적 산출물을 연결할 수 있다.

이러한 한계가 결과를 무효화하는 것은 아니다. 이는 흥미로운 실험을 신뢰할 수 있는 엔지니어링 관행으로 발전시키는 데 필요한 작업을 정의한다.

Lean 증명 자동화가 AI 코딩 도구에 가하는 압력

모델이 코드와 검증 가능한 증명을 함께 생성할 수 있게 되면, “테스트를 통과했다”는 말은 불완전한 품질 주장처럼 보이기 시작한다.

현재 AI 코딩 제품은 작업 완료, 리포지토리 이해, 도구 사용, 벤치마크 점수, 개발자 경험을 놓고 경쟁한다. 이들의 품질 게이트는 여전히 전통적인 개발 방식을 닮아 있다. 에이전트는 테스트, 린터, 타입 체커, 보안 스캐너, 사람 중심의 리뷰 워크플로를 실행한다.

이러한 검사는 중요하지만, 대부분 보편적 동작을 확립하지는 않는다. 단위 테스트는 선택된 하나의 입력이 한 번의 실행에서 기대한 결과를 냈음을 증명한다. 퍼징은 생성된 입력을 통해 커버리지를 넓히지만, 여전히 실행을 표본 추출한다. 정적 분석은 더 넓은 범주를 다룰 수 있지만, 각 분석기는 정의된 근사 범위 안에서 작동한다.

정리는 허용된 모든 입력이 선택된 속성을 만족한다고 명시할 수 있다. Lean이 증명을 검사한다면, 그 보증은 이를 생성한 모델을 신뢰하는 데 의존하지 않는다. 이는 에이전트형 코딩 시스템에 매력적인 제품 차별점이다.

압력은 먼저 좁은 작업에서 나타날 것이다. AI 에이전트는 성공한 파싱이 입력 경계를 절대 넘지 않는다는 증명과 함께 파서를 생성할 수 있다. 인가되지 않은 전이를 배제하는 정리를 갖춘 접근 제어 규칙을 구현할 수도 있다. 데이터베이스 마이그레이션을 만들고 형식 모델에서 스키마 불변식이 보존됨을 증명할 수도 있다.

주류 도구가 모든 사용자에게 Lean 문법을 노출할 필요는 없다. 형식 검증을 추가 검증 모드로 제공할 수 있다. 인터페이스는 개발자에게 평이한 언어로 속성을 승인하도록 요청하고, 그 형식적 번역을 보여 주며, 검증된 증명이나 구체적인 반례를 반환할 수 있다.

결정적인 기능은 순수한 정리 증명 점수가 아닐 것이다. 핵심은 통합이다. 증명 자동화는 리포지토리 맥락, 빌드 시스템, 명세, 성능 테스트, 코드 리뷰와 함께 작동해야 한다.

Langley의 실험은 유용한 제품 교훈을 제공한다. 모델은 대화형으로 작동했다. 증명하기 어려운 코드를 마주하고, 구조를 수정한 뒤 검증기가 결과를 받아들일 때까지 계속했다. 이는 자동완성 시스템보다 엔지니어링 에이전트에 더 가깝다.

이는 새로운 형태의 책임성도 시사한다. AI 코드 생성은 흔히 비대칭성을 낳는다. 모델은 사람이 검토할 수 있는 속도보다 더 빠르게 코드를 만들 수 있다. 증명을 생성하는 에이전트는 선택된 주장에 기계가 검증할 수 있는 증거를 첨부할 수 있다.

그 증거가 리뷰를 선택 사항으로 만들지는 않는다. 다만 검토자가 기계적 동작을 시뮬레이션하는 데 쓰는 시간을 줄이고, 주장 자체를 더 많이 검토할 수 있게 한다. 핵심 질문은 “모델이 어딘가의 인덱스 사례를 놓쳤는가?”가 아니라 “이것이 우리가 필요로 하는 속성인가?”가 된다.

경쟁사는 여러 경로로 대응할 수 있다. Lean을 직접 통합하거나, 모델을 다른 증명 보조 도구와 연결하거나, 특수화된 솔버용 인증서를 생성하거나, 형식 모델과 기존 코드를 결합할 수 있다. 승리하는 접근법은 도메인에 따라 달라질 수 있다.

Lean은 하나의 환경에서 프로그래밍, 정리 증명, 메타프로그래밍, 광범위한 자동화를 지원한다는 장점이 있다. 커널은 명확한 신뢰 경계도 제공한다. 그러나 Lean이 성능에 민감한 소프트웨어에 자동으로 적합한 배포 언어가 되는 것은 아니다.

따라서 증명을 생성하는 AI는 다른 LLM뿐 아니라 증명을 검사하는 개발 파이프라인과 경쟁하게 될 것이다. 신뢰할 수 있는 단위는 모델, 형식 명제, 증명 도구, 커널, 컴파일러 가정, 테스트, 검토자를 포함한 전체 시스템이다.

AI 제품을 구매하는 지식 노동자에게 이는 벤더 모델이 정확한지 묻는 것보다 더 나은 질문을 만든다. 어떤 출력이 결정론적 검증을 받는지, 어떤 주장에 검증 가능한 증거가 있는지, 어떤 부분이 여전히 확률적 판단에 의존하는지를 물어야 한다.

증명 자동화는 이 패턴의 가장 강력한 형태를 제공한다. 모든 작업에 적용되지는 않겠지만, 형식적으로 명세화할 수 있는 모든 출력에 대한 기대 수준을 높인다.

이것이 일반적인 엔지니어링이 될지 보여 줄 세 가지 신호

다음 단계는 재현성, 변화 속의 유지보수, 일상적 개발 도구 안의 증명 기반 기능에 달려 있다.

첫 번째 신호는 Langley의 실험에 견줄 수 있는 공개적이고 재현 가능한 소프트웨어 리포지토리다. 개발자는 정의, 프롬프트 또는 에이전트 추적 기록, 증명 항, 공리, 빌드 시간, 하드웨어 요구 사항을 검사할 수 있어야 한다. 독립된 팀은 이 과정을 다시 실행하고 대체 모델을 시험할 수 있어야 한다.

재현성은 현재 LLM이 상당한 수준의 증명 작업을 처리할 수 있다는 주장을 강화할 것이다. 재현에 실패한다면, 결과는 숙련된 한 엔지니어의 설정과 판단으로 범위가 좁아질 것이다. 어느 결과든 이용 가능한 증거를 개선한다.

두 번째 신호는 변화하는 코드 전반에서의 성능이다. 일회성 증명은 상당한 사람의 지침을 숨길 수 있다. 더 까다로운 시험은 에이전트가 정리를 약화하거나 프로그램을 왜곡하지 않고 현실적인 구현 변경 후 증명을 복구할 수 있는지다.

팀은 증명 복구 시간, 사람의 개입, 계산 비용, 정리 변경, 성능 회귀를 측정해야 한다. 또한 실패한 증명이 무해한 구조적 변경이 아니라 실제 버그를 드러내는 빈도도 추적해야 한다.

개발 수개월에 걸쳐 복구가 빠르게 유지된다면, AI는 증명 엔지니어링의 유지보수 부담을 줄인 것이다. 변경마다 광범위한 구조 조정이 필요하다면, 형식 검증은 안정적이고 고가치인 구성 요소에만 제한될 것이다.

세 번째 신호는 제품 통합이다. 특히 파서, 정책 엔진, 프로토콜 구현, 데이터 처리 코드에서 커널이 검증한 속성을 표준 출력으로 제공하는 코딩 에이전트를 주목해야 한다.

신뢰할 수 있는 제품은 정리 생성을 정리 검사와 분리해야 한다. 가정을 표시하고, 미완성 증명을 거부하며, 검증 로그를 보존하고, 코드 변경이 보증을 무효화할 때 경고해야 한다. 또한 테스트와 벤치마킹을 워크플로 안에 유지해야 한다.

이러한 기능이 주류 도구에 등장한다면 Lean 증명 자동화는 정리 증명 시연을 넘어선 것이다. 이들이 연구용 리포지토리에만 머문다면, 생산성 향상은 아직 통합 비용을 극복하지 못한 것이다.

지식 노동자에게 실질적인 대응은 더 나은 명세를 준비하는 일이다. 올바른 동작을 정의하는 결정을 기록하라. 원본 자료를 보존하라. 오해될 경우 막대한 실패 비용을 초래하는 불변 조건을 식별하라. 예외는 명시적으로 규정하라.

그런 다음 각 AI 워크플로에 더 날카로운 질문을 던져야 한다. 어떤 결과물이 신뢰할 수 있고 독립적인 검증을 받을 수 있는가?

Langley의 디코더가 모든 소프트웨어가 형식 검증될 수 있음을 증명하는 것은 아니다. 다만 AI가 비용 장벽을 공략하기 시작했고, Lean이 엄격한 최종 관문을 유지한다는 점을 보여준다. 그것만으로도 로드맵을 바꾸기에 충분하다.

가까운 미래는 오류 없는 모델이 작성한 소프트웨어가 아니다. 오류를 범할 수 있는 모델이 제안하고, 더 나은 명세로 제약되며, 모델이 얼마나 확신에 차 있든 개의치 않는 시스템이 검증하는 소프트웨어다.