AI 퍼스트 개발, 코딩 가드레일, 그리고 폐기 가능한 아키텍처를 탐구합니다.
대규모 언어 모델은 놀랄 만큼 훌륭한 Rust 코드를 작성하지만, 형식적 증명을 요청하면 불변 조건을 환각으로 만들어내고 어떤 검증기도 받아들이지 않는 문법을 지어낸다. 이들이 실제로 제대로 하는 것, 실패하는 부분, 그럼에도 불구하고 활용하는 방법을 소개한다.
LLM은 컴파일되고 까지 통과하는 Rust 코드를 작성할 수 있다. 하지만 모든 가능한 입력에 대해 코드가 올바르다는 형식적 증명을 믿을 수 있게 작성하는 것은 아직 불가능하다. 문제는 Rust 문법이 아니다. 형식적 검증에서는 무엇을 증명할지 명시하고, 증명을 성립시키는 불변 조건을…
model checking이 며칠간의 프로덕션 런타임을 능가해 concurrency 버그를 찾는 이유, 그리고 자신의 코드에 적용하는 방법.
프로덕션에서 race condition이 떠오르기를 기다리는 건 테스트가 아니다. 성실함으로 위장한 희망이다. 앱을 몇 주씩 돌리고 metrics 대시보드를 지켜봐도, 두 개의 request가 정확히 동일한 cache eviction window에 걸릴 때만 발동하는…
Kani 같은 경계 model checker과 Alloy 같은 관계 모델 탐색기는 일반적인 어서션과 제약 조건으로 속성을 검증할 수 있게 한다. 활성 증명을 포기하는 대신, 학습 곡선은 주가 아닌 시간 단위로 측정된다.
model checker을 사용하기 위해 선형 시간 논리를 배울 필요는 없다. Kani, CBMC, Alloy 같은 도구는 일반적인 어서션과 관계 제약으로 속성을 검증할 수 있게 한다. 활성 속성을 증명하는 능력을 포기하는 대신, 학습 곡선은 주 대신 시간 단위로 측정되며, 대부분의…
Kani 같은 model checking 도구를 사용하면 형식적 증명 대신 단언으로 Rust 속성을 검증할 수 있다. 문제는 루프의 경계가 작지 않을 때 무슨 일이 일어나는지다.
한 줄의 증명도 쓰지 않고 Rust 코드의 정확성을 증명할 수 있다. 이 일을 하는 도구를 model checker라 부르며, 현재 Rust 에 가장 실용적인 것은 AWS 가 개발한 Kani 다. 평범한 Rust 단언을 작성하면 된다. Kani 는 이를 수학적 명제로 변환하고 가능한…
분산 버그는 배포 후 수정 비용이 많이 든다. 모델 검증을 사용하면 구현 코드를 한 줄도 작성하지 않은 상태에서 그 버그를 찾을 수 있다. 다음은 TLA+를 이용한 방법이다.
분산 프로토콜은 단위 테스트할 수 없다. 단위 테스트는 한 대의 머신에서 한 개의 프로세스를 정해진 순서로 실행한다. 당신의 프로토콜은 다섯 대의 머신에서 열 개의 프로세스를 통제할 수 없는 순서로 실행한다. 이 두 현실 사이의 간극이 바로 버그가 서식하는 곳이다. 모델 검증은 그…
인프라팀이 환경 간 차이를 명시적이고 타입 안전하게 만드는 컨텍스트별 DSL을 사용하여 dev, staging, production 간 설정을 관리하는 방법.
staging 환경은 작동한다. production 환경은 작동하지 않는다. 두 환경의 파일 간 diff는 400줄이며, 그 중 절반은 아무도 더 이상 믿지 않는 주석이다. 누군가 지난달 staging에 를 추가했다. production에는 아무도 추가하지 않았다. 애플리케이션은…
LLM은 토큰을 확률적으로 샘플링하기 때문에 구문을 환각한다. 문법 제약 디코딩은 각 단계에서 어휘를 필터링하여 구문적 유효성을 유지하는 토큰만 출력되도록 한다.
LLM에게 JSON 객체를 생성하라고 요청하면, 결국 뒤에 쉼표를 붙이거나 문자열 안에 이스케이프되지 않은 줄바꿈을 넣거나, 따옴표로 묶인 키가 있어야 할 자리에 bare word를 출력한다. 이 오류는 모델의 버그가 아니다. autoregressive sampling이 작동하는…
간단한 영어 설명에서 디자인 토큰을 생성할 수 있지만, 해당 설명을 스키마 계약과 스냅샷 테스트가 있는 한정된 컨텍스트 DSL로 다루는 경우에만 가능하다.
네, 영어로 테마를 설명하고 작동하는 디자인 시스템을 얻을 수 있다. 다만 영어 설명은 프롬프트가 아니다. 소스 파일이다. 그리고 모든 소스 파일처럼 컴파일러, 타입 시스템, 테스트가 필요하다. 챗봇 쿼리처럼 다루면 화요일에는 월요일과 다른 색상 팔레트를 얻게 된다. 한정된 컨텍스트와…
대부분의 bounded-context DSL에 parser generator은 과하다. 파서 콤비네이터를 사용하면 애플리케이션과 동일한 언어로 작동하는 파서를 생성 코드 없이, 빌드 단계 없이 구축할 수 있다.
Yacc grammar 파일을 열어 보면서 언어를 만드는 데 왜 두 번째 언어를 배워야 하는지 의문을 품어본 적이 있다면, 당신만 그런 것이 아니다. parser generator은 강력하지만, bounded context 안에서 자연스럽게 등장하는 작은 DSL에는 거의 항상 과하다.…
스키마 검증과 빌드 타임 검사를 사용해 애플리케이션이 트래픽을 처리하기 전에 설정 오류를 잡는 방법.
금요일 저녁, 3시간이 지난 시점에 애플리케이션이 를 던진다. 스택 트레이스는 설정 객체의 깊게 중첩된 속성을 가리킨다. 값은 다. 누군가 검증 로직을 갱신하지 않은 채 변경 사항을 프로덕션에 푸시했다. 이것은 런타임 버그가 아니다. 정책 실패다. 신뢰할 수 없는 데이터를 사전 검사…