6 posts
차등 테스트는 정답을 몰라도 버그를 찾아준다. 문제는 상관관계 있는 실수가 '일치'로 보인다는 점이다. 여기서 사각지대를 찾는 법을 알아본다.
형식적 증명 없이도 차등 테스트는 믿을 수 있다. 하지만 그 한계가 어디인지 정확히 알아야 한다. 약점은 공통 모드 오류(common-mode failure)다. 하나의 명세에 대한 모든 구현이 같은 잘못된 가정을 할 때, 모두 같은 결과를 낸다. 그러면 테스트 하네스는 이를 통과로…
N-version programming은 구현체들이 서로 일치한다고 가정한다. 테스트가 왜 부족한지, SMT solver가 어떻게 실제로 동등성을 증명할 수 있는지, 그리고 '충분히 좋음'과 '형식적으로 검증됨' 사이의 경계를 어디에 그어야 하는지 살펴본다.
n-version 시스템을 구축했다. 동일한 중요 함수를 독립적으로 구현한 세 가지 구현체, 다수결 결과를 선택하는 voter, 그리고 단일 장애점을 뛰어넘었다는 따뜻한 만족감까지. 하지만 함수들이 동등하다는 것을 증명한 게 아니다. 컴파일된다는 것만 증명했을 뿐이다.…
여러 LLM을 병렬로 실행하면 단일 모델이 자신 있게 납품할 오류를 잡아낼 수 있다. 실제로 작동하는 불일치 해결 시스템을 구축하는 방법은 다음과 같다.
프롬프트를 GPT-4o에 보낸다. 신뢰도 0.97의 JSON blob이 돌아온다. 똑같은 프롬프트를 Claude 3.5 Sonnet에 보낸다. 다른 JSON blob이 돌아오는데, 신뢰도 역시 0.97이다. 두 모델 모두 확신에 찬다. 두 모델 모두 각기 다른 방식으로 틀렸다. 이것은…
N-version programming은 간단해 보인다: 여러 구현체를 실행하고 가장 좋은 답을 고른다. 하지만 실제로 '최선'은 '가장 흔한'보다 정의하기 훨씬 어렵다.
같은 함수의 다섯 가지 구현체가 있다. 세 개는 같은 결과를 반환한다. 하나는 조금 다르다. 하나는 예외를 던진다. 어느 것이 맞는가? 대부분의 팀은 다수결을 기본으로 삼는다. 출력이 동일하고 오류가 명백할 때는 잘 작동한다. 하지만 구현체들이 미묘하게 의견이 갈리거나, 모든…
LLM을 활용한 N-version programming은 여러 모델이 필요하지 않다. 프롬프트, 페르소나, 추론 제약을 달리하면 단일 모델에서도 다양하고 정확한 구현을 추출할 수 있다.
N-version programming은 다양성이 서로 다른 작성자에게서 나온다고 가정한다. LLM을 쓸 때는 다른 모델, 다른 제공자, 아마도 다른 학습 실행본을 의미한다. 하지만 그 가정은 틀렸다. 똑같은 모델에게서도 질문하는 방식을 바꾸면—질문 내용이 아니라—의미 있는 다양성을…
N-version programming은 독립적인 팀이 독립적인 실수를 할 것이라 약속했다. 1986년 Knight와 Leveson의 실험은 정반대임을 입증했고, NASA는 조용히 물러섰다.
1980년대 초, NASA는 오늘날까지 안전 필수 엔지니어링을 괴롭히는 질문에 직면했다: 아직 발견하지 못한 버그를 어떻게 견딜 수 있는가? 그들의 답은 N-version programming이었다. 같은 명세를 세 개의 독립적인 팀에 주고, 세 프로그램을 병렬로 실행한 뒤, 출력에…