9 posts
클린룸 검증은 검증 조건을 생성하고 해소하는 것을 요구한다. 여기서 LLM이 주석과 VC 생성을 자동화하여 실제 어려운 증명에 집중할 수 있게 하는 방법을 소개한다.
클린룸 소프트웨어 공학은 코드를 컴파일하기 전에 그 정당성을 증명할 것을 요구한다. 그것은 고귀하게 들리지만, 열 개의 정수를 정렬하는 함수를 위해 루프 불변식을 세 시간 동안 작성하다 본다면 상황이 달라진다. 병목 지점은 증명 자체가 아니다. 상용구이다. 검증 조건을 생성하고,…
30일 동안 LLM에 코드를 요청하기 전에 설계 설명을 작성했다. 그 결과는 내가 rubber-ducking을 바라보는 방식을 바꿔 놓았다.
대부분의 개발자는 LLM을 거꾸로 사용한다. 다섯 단어로 원하는 것을 설명하고, 200줄의 코드를 받은 뒤, 다음 한 시간은 모델이 내린 가정을 디버깅하는 데 쓴다. 나는 반대 workflow를 3개월간 실행했다. 한 줄의 코드도 요청하기 전에 완전한 설계 설명을 작성하는 것이다.…
LLM 대화에는 의도, 거부된 대안, 그리고 작동하는 코드가 담겨 있습니다. 이것이 바로 문서가 되어야 할 것입니다. 다음은 일회성 채팅을 내러티브를 잃지 않고 지속 가능하고 검색 가능한 문서로 전환하는 방법입니다.
당신은 Claude와 45분을 들여 재시도 회로를 설계했다. 실패 모드를 설명하고, 계단식 압력을 숨기기 때문에 지수 백오프를 거부한 뒤, jitter가 포함된 token-bucket rate limiting으로 결정하고 작동하는 구현을 생성했다. 설명은 명확했고, 추론은 타당했으며,…
파견 검사는 250줄을 검토하는 데 4~6명과 2시간이 필요하다. 대형 언어 모델은 준비 작업과 체크리스트 준수를 담당하여 비용을 줄일 수 있지만, 가장 비싼 결함을 찾아내는 인간의 역할을 대체할 수는 없다.
완전한 파견 검사에는 진행자, 낭독자, 2~4명의 검토자, 그리고 작성자가 필요하다. 팀은 한 시간에 125줄의 속도로 대략 250줄의 코드를 2시간 동안 검토한다. 작은 변경에도 8~12인시가 드는 셈이다. 대형 언어 모델은 250줄을 1초도 채 걸리지 않아 읽을 수 있다.…
대규모 언어 모델은 놀랄 만큼 훌륭한 Rust 코드를 작성하지만, 형식적 증명을 요청하면 불변 조건을 환각으로 만들어내고 어떤 검증기도 받아들이지 않는 문법을 지어낸다. 이들이 실제로 제대로 하는 것, 실패하는 부분, 그럼에도 불구하고 활용하는 방법을 소개한다.
LLM은 컴파일되고 까지 통과하는 Rust 코드를 작성할 수 있다. 하지만 모든 가능한 입력에 대해 코드가 올바르다는 형식적 증명을 믿을 수 있게 작성하는 것은 아직 불가능하다. 문제는 Rust 문법이 아니다. 형식적 검증에서는 무엇을 증명할지 명시하고, 증명을 성립시키는 불변 조건을…
LLM은 토큰을 확률적으로 샘플링하기 때문에 구문을 환각한다. 문법 제약 디코딩은 각 단계에서 어휘를 필터링하여 구문적 유효성을 유지하는 토큰만 출력되도록 한다.
LLM에게 JSON 객체를 생성하라고 요청하면, 결국 뒤에 쉼표를 붙이거나 문자열 안에 이스케이프되지 않은 줄바꿈을 넣거나, 따옴표로 묶인 키가 있어야 할 자리에 bare word를 출력한다. 이 오류는 모델의 버그가 아니다. autoregressive sampling이 작동하는…
간단한 영어 설명에서 디자인 토큰을 생성할 수 있지만, 해당 설명을 스키마 계약과 스냅샷 테스트가 있는 한정된 컨텍스트 DSL로 다루는 경우에만 가능하다.
네, 영어로 테마를 설명하고 작동하는 디자인 시스템을 얻을 수 있다. 다만 영어 설명은 프롬프트가 아니다. 소스 파일이다. 그리고 모든 소스 파일처럼 컴파일러, 타입 시스템, 테스트가 필요하다. 챗봇 쿼리처럼 다루면 화요일에는 월요일과 다른 색상 팔레트를 얻게 된다. 한정된 컨텍스트와…
여러 LLM을 병렬로 실행하면 단일 모델이 자신 있게 납품할 오류를 잡아낼 수 있다. 실제로 작동하는 불일치 해결 시스템을 구축하는 방법은 다음과 같다.
프롬프트를 GPT-4o에 보낸다. 신뢰도 0.97의 JSON blob이 돌아온다. 똑같은 프롬프트를 Claude 3.5 Sonnet에 보낸다. 다른 JSON blob이 돌아오는데, 신뢰도 역시 0.97이다. 두 모델 모두 확신에 찬다. 두 모델 모두 각기 다른 방식으로 틀렸다. 이것은…
LLM을 활용한 N-version programming은 여러 모델이 필요하지 않다. 프롬프트, 페르소나, 추론 제약을 달리하면 단일 모델에서도 다양하고 정확한 구현을 추출할 수 있다.
N-version programming은 다양성이 서로 다른 작성자에게서 나온다고 가정한다. LLM을 쓸 때는 다른 모델, 다른 제공자, 아마도 다른 학습 실행본을 의미한다. 하지만 그 가정은 틀렸다. 똑같은 모델에게서도 질문하는 방식을 바꾸면—질문 내용이 아니라—의미 있는 다양성을…