고치려다 지운 증거, Verus에서 완전성을 되묻는 법

정확도 피드백이 명세의 구멍을 가리는 현상을 Verus와 Rust 실험으로 추적하고, 증거 수집과 수리를 나눈 단계 분리 감사가 왜 수율과 수리 성공률을 끌어올리는지 읽는다.

원문 논문 보기
'고치려다 지운 증거, Verus에서 완전성을 되묻는 법' 기사 커버 이미지

When Correctness Feedback Erases Evidence: Phase-Separated Completeness Auditing in Verus는 arXiv에 공개된 Verus 연구로 arXiv 번호 2610.20676으로 등록되어 있다. 원문 링크는 제목 아래에 걸어두었다.

이 연구가 내세우는 주장은 하나의 문장으로 정리되는데, 명세를 고치는 정확도 피드백이 오히려 명세의 빈틈을 드러내는 증거를 지우기 때문에 증거 수집과 수리를 단계로 나누어야 완전성 감사와 계약서 수리가 함께 살아난다는 것이다. 이 글에서는 그 문제의식에서 출발해 Verus와 Rust 과제에서 벌어진 일, 피드백이 증거를 지우는 과정, 독립 탐색이 수율을 끌어올린 이유, 형식 통제 실험의 뜻, 모델과 파서 조건에서의 일관성, 단계 분리 실행의 확인, 증인을 이용한 계약서 수리, 그리고 Dafny와 Lean에서 재현되지 않은 경계까지 차례로 따라간다.

왜 고치는 일이 증거를 지우게 될까

제가 이 논문에서 가장 흥미롭게 본 부분은 출발점의 불편함이었다. 보통은 틀린 것을 빨리 고치는 편이 좋은 일이라고 믿는데, 여기서는 그 선의가 오히려 일을 그르친다는 관찰에서 시작하기 때문이다. 검증 세계에서는 맞는 답을 만드는 일과 구멍을 찾는 일이 서로 다른 방향을 바라보는데, 두 일을 한 고리에 묶으면 고치는 쪽이 찾는 쪽을 계속 방해한다는 것이다. 그렇다면 왜 이런 충돌이 생길까. 답은 생각보다 단순한데, 완전성 감사라는 작업이 실패를 살려두어야 성립하기 때문이다.

완전성 감사는 계약서가 너무 헐거워서 엉뚱한 구현까지 통과시키는지를 묻는다. 그래서 감사자는 일부러 계약서의 허점을 찌르는 입력, 즉 통과해서는 안 되는데 통과해버리는 증인을 찾아내야 한다. 그런데 같은 고리 안에서 정확도 피드백이 계속 돌아가면 이야기가 달라지는데, 모델이 증인을 내놓을 때마다 검증자가 틀렸다고 고쳐주면서 다음 시도에서는 더 얌전한 답만 내놓게 만들기 때문이다. 마치 오답 노트를 쓰기도 전에 선생님이 답안지를 걷어가는 모습과 비슷한데, 무엇이 틀렸는지를 기록으로 남기지 못하면 다음 공부로 이어지지 않는 것이죠.

생각해보면 사람 조직에서도 비슷한 장면을 본 적이 있다. 불량이 나오면 현장에서는 일단 라인을 멈추고 불량품을 따로 모아두는데, 그 물건이 있어야 원인이 보이기 때문이다. 그런데 누군가 빨리 치우겠다고 불량품을 그 자리에서 고쳐버리면 기록은 사라지고 같은 불량이 다시 나오죠. 저는 그래서 이 논문의 첫 문장을 일종의 운영 원칙으로 읽었다. 인정된 실패를 먼저 보존하고 확정하라는 말인데, 수리보다 기록이 먼저라는 뜻이기 때문이다. 이 순서를 바꾸면 점수는 빨리 좋아질 수 있지만, 우리가 무엇을 놓쳤는지는 영원히 모르게 된다.

통과했는데도 찜찜한 계약서는 어디서 올까

Verus는 Rust 프로그램에 명세를 붙이고 기계적으로 증명하는 도구인데, 통과 표시가 나왔다고 해서 계약서가 좋다는 뜻은 아니다. 계약서가 너무 약하면 엉터리 구현도 버젓이 통과하기 때문인데, 예를 들어 정렬 함수를 만들었다고 해보자. 계약서가 결과 길이가 입력 길이와 같다고만 적혀 있으면, 아무렇게나 섞인 배열도 검증을 통과한다. 검증자는 거짓말을 하지 않았는데, 묻는 질문 자체가 헐거웠던 것이죠. 그렇다면 진짜 문제는 어디에 있을까. 코드가 아니라 질문에 있다는 점이 이 분야를 처음 접하면 헷갈리는 대목이다.

저는 여기서 조금 멈칫했는데, 우리가平时 모델 평가에서 정확도만 보는 습관과 똑같은 착각이 있기 때문이다. 저희가 새로운 AI 아키텍처를 볼 때도 benchmark 숫자만 보지는 않습니다. 실제로 무엇이 바뀌었고, 그 변화가 시스템에서 어떤 비용 구조를 만드는지를 함께 봅니다. 검증에서도 통과율이라는 숫자는 기초 체력에 가깝고, 계약서가 무엇을 묻고 무엇을 묻지 않는지가 더 깊은 구조인데, 이 구조를 보지 않으면 통과라는 말이 주는 안심에 속게 된다. 그래서 감사라는 말이 필요한데, 잘 돌아가는지를 묻는 게 아니라 무엇을 못 묻고 있는지를 묻는 일이기 때문이다.

이번 연구는 이 질문을 Verus와 Rust 과제 12개로 좁혀서 다룬다. 네 가지 모델 계열을 같은 호출 예산 아래에 놓고 비교하는데, 예산을 맞춘다는 말이 생각보다 중요한데, 시도 횟수가 다르면 운이 실력처럼 보이기 때문이다. 같은 돈을 쓰고 누가 더 많은 증인을 건져 올리는지를 재는 셈이죠. (참고로 Verus는 Rust에 특화된 검증기인데, 평소에 쓰는 테스트와는 결이 조금 다른 도구라고 보면 됩니다.) 이렇게 판을 깔아두면 남는 차이는 순전히 탐색 방식에서 오는데, 피드백을 주며 고칠 것인지, 아니면 피드백 없이 넓게 찾을 것인지가 갈림길이 된다.

고쳐진 코드 옆에서 사라지는 실패 사례와 유리 상자에 보관된 실패 사례를 나란히 보여주는 그림
고쳐진 코드 옆에서 사라지는 실패 사례와 유리 상자에 보관된 실패 사례를 나란히 보여주는 그림

피드백을 끄자 수율이 두 배로 뛴 이유

숫자부터 꺼내면 이야기가 빨라지는데, 피드백 없이 독립적으로 증인을 찾은 쪽은 확정된 증인 수율이 59.0퍼센트였고, IntentShield라는 교정 피드백 고리는 27.1퍼센트에 머물렀다. 두 배를 훌쩍 넘는 차이인데, 같은 예산을 쓰고도 결과가 이렇게 갈렸다는 점이 먼저 눈에 들어온다. 표면적으로 보면 단순합니다. 실제로는 그렇지 않습니다. 피드백이 있으면 더 똑똑해져야 할 것 같은데 오히려 증거를 덜 찾았기 때문인데, 우리의 직관과 정반대 방향이기 때문이다.

왜 이런 일이 생길까. 저는 이 숫자보다 그 뒤의 구조가 더 중요하다고 봅니다. 피드백 고리는 틀린 답이 나오면 곧바로 어디가 틀렸는지를 알려주고 고치게 하는데, 이 과정이 반복되면 모델의 다음 답은 점점 검증자를 통과하는 쪽으로 기울기 때문이다. 통과하는 답은 보기에는 깔끔한데, 문제는 그 깔끔함이 계약서의 허점을 찌르는 모서리를 뭉갠다는 데 있다. 모서리를 찾아야 하는 감사자에게는 재앙에 가까운데, 자꾸 둥글게 다듬어진 답만 나오면 구멍은 그대로 남기 때문이다. 그래서 피드백을 끈 쪽이 더 많은 구멍을 찾았는데, 못생긴 실패를 그대로 두었기 때문이다.

여기서 재미있는 질문이 생깁니다. 그렇다면 피드백은 원래 나쁜 것일까. 저는 그렇게 읽지 않았는데, 목적이 다르면 약도 독이 되기 때문이다. 정확도를 올리는 일에서는 피드백이 약이지만, 구멍을 찾는 일에서는 같은 피드백이 독이 되죠. 병원으로 치면 치료와 진단이 다른 것처럼요. 열이 나면 해열제를 먹는 것이 치료에는 맞지만, 원인을 찾는 단계에서 함부로 열을 내려버리면 단서가 사라진다. 이 논문은 바로 그 구분을 하자는 것인데, 감사 단계에서는 환자를 고치지 말고 증상을 기록하라는 뜻이다. 저는 이 비유가 논문의 태도를 가장 잘 보여준다고 봤다.

다시 시작해서가 아니라 다른 말을 들어서 달라졌다

물론 여기서 곧바로 반론이 나온다. 피드백 없는 쪽이 잘 나온 이유가 단순히 여러 번 다시 시작해서 운이 좋았던 것 아니냐는 의심인데, 연구진은 이 의심을 그대로 두지 않고 형식 통제 실험을 하나 더 얹는다. 주고받는 말의 형식은 피드백 고리와 똑같이 맞추되 내용은 비워둔 반복 대조군을 돌린 것인데, 다시 시작한다는 조건은 같게 두고 피드백 말의 유무만 다르게 만든 것이다. 그랬더니 차이의 더 큰 몫은 다시 시작이 아니라 피드백 내용에서 왔다. 다시 말해 말을 어떻게 하느냐가 결과를 갈랐다는 뜻이죠.

이 대목은 얼핏 작아 보이지만 실제로는 논문의 허리를 받치는 부분인데, 운과 개입을 가르는 장치이기 때문이다. 만약 차이가 단순히 시도 횟수에서 왔다면 누구든 많이 뽑으면 될 일인데, 실험은 말이 문제라고 말해주기 때문이다. 피드백 문장 안에 들어 있는 고치라는 압력이 모델의 다음 분포를 좁혔고, 그 좁아짐이 증인의 다양성을 갉아먹었다는 해석이 가능해진다. 저는 이 해석이 설득력 있다고 봤는데, 언어 모델이 사람의 말에 생각보다 민감하게 기울기 때문이다. 고치라는 말을 들으면 고치는 쪽으로만 상상하고, 찾으라는 말을 안 들으면 엉뚱한 곳까지 상상하죠.

실제 시스템 관점에서 보면 다음 질문이 바로 생깁니다. 그렇다면 에이전트에게 일을 시킬 때도 피드백 문구를 함부로 쓰면 안 되는 것 아닐까. 맞는 말인데, 다만 절반만 맞는 말이라서 조심해야 한다. 고치는 단계에서는 구체적인 피드백이 여전히 필요하기 때문인데, 문제는 단계를 섞을 때 생긴다. 찾을 때는 입을 다물고 넓게 보게 하고, 고칠 때는 입을 열어 정확히 짚어주는 식으로 역할을 나누면 되는 것이죠. 저는 그래서 이 실험을 단순한 대조군이 아니라 운영 지침으로 읽었다. 언제 말을 아끼고 언제 말을 보탤지를 정해주는 장치이기 때문이다.

Rust 코드와 명세 계약과 검증 통과 표시가 완전성 감사 고리로 이어지는 개념도
Rust 코드와 명세 계약과 검증 통과 표시가 완전성 감사 고리로 이어지는 개념도

어떤 모델에서도 같은 방향으로 기울면 무엇을 믿어야 할까

다음으로 눈여겨볼 점은 일관성인데, 피드백 없는 쪽의 우세가 네 가지 모델 계열 모두에서 같은 방향으로 나타났다는 것이다. 한두 모델에서만 튀는 현상이라면 우연이나 궁합 문제로 볼 수 있는데, 계열을 바꿔도 화살표가 같은 쪽을 가리키면 이야기가 달라진다. 구조적인 문제일 가능성이 커지기 때문인데, 모델의 성격보다 작업의 성격에서 온 신호라는 뜻이죠. 저는 이런 패턴을 보면 마음이 조금 놓이는데, 한 집안의 버릇이 아니라 동네 전체의 지형처럼 보이기 때문이다.

여기서는 조금 조심해서 읽을 필요가 있습니다. 모든 모델에서 통했다고 해서 모든 상황에서 통한다는 뜻은 아니기 때문이다. 뒤에 다루겠지만 Dafny와 Lean에서는 같은 효과가 재현되지 않았는데, 그래서 이 일관성은 Verus와 Rust라는 울타리 안에서 읽어야 한다. 울타리를 넓히면 깨질 수 있는 결과인데, 그 점을 미리 말해두는 편이 정직하죠. 그럼에도 울타리 안에서의 일관성은 가볍지 않은데, 적어도 이 작업 묶음에서는 피드백이 증거를 지운다는 말이 모델을 가리지 않았기 때문이다.

개인적으로 인상 깊었던 점은, 강한 모델일수록 피드백의 유혹이 더 클 수 있다는 상상이 가능하다는 것이다. 강한 모델은 고치는 말을 더 잘 알아듣기 때문에 더 빨리 얌전해지는데, 빨리 얌전해진다는 말이 곧 빨리 모서리를 잃는다는 뜻이 될 수 있기 때문이다. 물론 이 부분은 논문이 직접 측정한 것은 아니고 제 해석인데, 그래도 실무에서는 비슷한 장면을 자주 본다. 말을 잘 듣는 직원이 지시를 곧이곧대로 따르느라 엉뚱한 발견을 덜 가져오는 경우처럼요. 잘 듣는 것이 늘 좋은 것은 아니고, 언제 잘 들어야 하는지가 더 중요하다는 교훈이죠.

파서를 고쳐도 순위가 바뀌지 않았다는 말의 뜻

또 하나 짚고 넘어갈 것은 파서 수리에 대한 확인인데, 출력 형식이 깨져서 버려진 답을 고쳐주고 다시 재도 순위가 바뀌지 않았다는 것이다. 이 말이 왜 중요할까. 자칫하면 피드백 없는 쪽이 형식을 더 잘 맞춰서 이긴 것 아니냐는 의심이 나올 수 있기 때문인데, 그 의심을 형식 고치기라는 별도 손질로 걷어낸 것이다. 형식을 고쳐줘도 승패가 그대로면 승패의 원인은 형식이 아니라 내용이라는 뜻이죠. 저는 이 장치를 논문의 양심이라고 봤다. 이기기 위해 유리한 조건을 숨기지 않고, 질 수 있는 반론을 먼저 꺼내 검증했기 때문이다.

생각해보면 평가에서는 이런 사소한 손질이 전체 신뢰를 좌우한다. 출력에 쉼표 하나가 빠져서 버려진 답이 수십 개씩 쌓이면, 그 버려짐이 실력 차이로 둔갑할 수 있는데, 연구진이 그 통로를 미리 막아둔 것이다. 파서라는 말은 어렵게 들리지만, 내용으로 치면 받아쓰기 점수를 깎기 전에 글씨를 먼저 알아봐 준 셈인데, 글씨를 알아봐 줘도 등수가 그대로면 진짜 글솜씨 차이로 읽을 수 있죠. 이런 확인이 쌓여야 숫자를 믿게 되는데, 저는 그래서 이 한 줄을 가볍게 넘기지 않았다.

그렇다면 이제 남은 질문은 하나인데, 피드백 없이 따로 돌린 결과가 정말 믿을 만한 증인인지, 그리고 그 증인이 실제로 계약서를 고치는 데 쓸모가 있는지이다. 수율이 높다는 말만으로는 부족한데, 건져 올린 것이 진짜 구멍인지, 그 구멍으로 다음 단계가 열리는지를 봐야 하기 때문이다. 다음 장면부터는 바로 그 질문을 다룬다.

같은 호출 예산 저울 위에서 59퍼센트와 27퍼센트 수율을 비교하는 막대 그림
같은 호출 예산 저울 위에서 59퍼센트와 27퍼센트 수율을 비교하는 막대 그림

모아서 한 번에 돌려도 잃지 않는다는 확인

연구진은 여기서 한 걸음 더 나아가 단계 분리 실행이라는 별도 묶음을 돌린다. 앞선 독립 탐색의 답을 재활용하지 않고, 증거를 모으는 단계와 수리하는 단계를 아예 나눠서 새로 실행하는 방식인데, 그래도 전체 수율은 앞서와 같은 수준으로 나왔다. 답을 베껴서 잘 나온 것이 아니라, 단계를 나눈다는 설계 자체가 수율을 만든다는 뜻이죠. 저는 이 확인을 보고 고개를 끄덕였는데, 한 번의 요행이 아니라 다시 세워도 서는 구조라는 말이 되기 때문이다.

더 흥미로운 대목은 따로 있는데, 확정된 증인 대부분이 따로 떼어둔 held-out 사례에서도 실패한다는 점이다. 쉽게 말해 한 번 찾은 구멍이 특정 문제에만 붙어 있는 우연이 아니라, 다른 문제에서도 통하는 구멍이라는 뜻인데, 이 점이 증인의 품질을 말해준다. 그냥 운 좋게 걸린 엉뚱한 입력이 아니라 계약서의 허점을 찌르는 입력이라는 것이죠. 테스트로 치면 한 문제만 맞히는 요령이 아니라 여러 문제에 통하는 원리 같은 것인데, 그래서 이 증인들은 버릴 것이 아니라 모아둘 가치가 있다.

여기서 다시 오답 노트 비유가 돌아온다. 오답 노트가 쓸모 있으려면 틀린 문제가 다음 시험에도 나와야 하는데, held-out 실패라는 말은 바로 그 조건을 확인해준 것이다. 모아둔 오답이 다른 시험지에서도 적중한다는 뜻이기 때문인데, 그렇다면 다음 단계는 정해져 있다. 이 오답들을 들고 계약서를 고치러 가는 것이다. 그런데 고치는 방법에도 갈래가 있어서, 어떻게 고치느냐에 따라 결과가 크게 달라진다. 그 이야기는 다음 장면에서 이어진다.

증거 수집 단계와 수리 단계를 벽으로 나눈 뒤 증인을 앞으로 넘기는 시간표
증거 수집 단계와 수리 단계를 벽으로 나눈 뒤 증인을 앞으로 넘기는 시간표

실패를 남겨야 계약서를 제대로 고칠 수 있다

계약서를 고친 뒤에는 구현 성공률로 성적을 매기는데, 단계 분리 증인으로 다듬은 Phase-Revised 계약서는 81.3퍼센트의 구현 성공률을 냈고, IntentShield 고리로 다듬은 IS-Revised 계약서는 62.5퍼센트에 머물렀다. 피드백 없이 직접 고친 Direct-Revised 계약서도 Phase-Revised 바로 뒤에 붙었는데, 두 무피드백 증인 경로가 나란히 앞섰다는 점이 눈에 띈다. 숫자를 나란히 놓으면 차이가 분명한데, 81.3과 62.5 사이에는 거의 20퍼센트포인트에 가까운 간격이 있기 때문이다. 같은 수리 엔진을 썼다고 가정하면, 들어간 재료가 결과를 갈랐다는 뜻이죠.

왜 이런 차이가 생길까. 이유는 재료의 선명도에 있는데, 좋은 증인은 계약서의 어디가 헐거운지를 콕 집어주기 때문이다. 예를 들어 길이가 같다는 말만 있던 계약서에 순서까지 묻도록 고치려면, 순서가 뒤섞인 채로 통과해버린 입력이 있어야 한다. 그 입력이 눈앞에 있으면 고치는 방향이 분명해지는데, 반대로 증인이 없으면 고치는 사람은 어둠 속에서 손을 더듬게 된다. 저는 이 숫자보다 그 뒤의 구조가 더 중요하다고 봅니다. 증인이 있다는 것은 질문이 있다는 뜻이고, 질문이 분명하면 답도 분명해지기 때문이다.

실제 시스템 관점에서 보면 다음 질문이 바로 생깁니다. 그렇다면 실무에서도 실패 사례를 먼저 모아두는 창고를 만들어야 하는 것 아닐까. 저는 그렇다고 보는 편인데, 다만 창고가 있다고 다 되는 것은 아니라서 조건이 붙는다. 모아둔 실패가 확정된 것이어야 하고, held-out에서도 통하는 수준이어야 하기 때문인데, 그냥 많이 모은다고 되는 일이 아니다. 적중하는 실패를 골라서 남기는 일인데, 이 논문이 말하는 certify라는 말이 바로 그 고르는 일을 뜻한다. 도장을 찍어 보관한 실패만이 다음 수리의 재료가 된다는 것이죠.

약하게 고치는 길과 증인으로 고치는 길은 어떻게 갈릴까

연구진은 무피드백 증인 경로를 약화된 계약서와도 비교하는데, 결과는 두 무피드백 증인 경로가 완화된 계약서보다 분명히 앞섰다는 것이다. 약화라는 말은 계약서를 넓게 풀어서 일단 통과시키는 쪽인데, 당장은 편하지만 구멍은 그대로 남는다. 반면 증인으로 고치는 길은 구멍을 메우면서 계약서를 단단하게 만드는 쪽인데, 당장은 손이 가지만 다음 구현이 덜 흔들린다. 그래서 저는 이 비교를 땜질과 수리의 차이로 읽었다. 땜질은 오늘을 넘기게 해주고, 수리는 내일을 바꾸죠.

여기서 잠깐 정직한 반론을 꺼내야 하는데, 강한 계약서가 늘 좋은 것은 아니기 때문이다. 계약서가 너무 빡빡하면 좋은 구현까지 막아버릴 수 있는데, 증인에만 매달리다 보면 과도하게 좁은 계약서가 나올 위험이 있다. 연구진이 구현 성공률까지 함께 본 이유도 여기에 있는데, 계약서만 단단해지고 구현이 막히면 소용이 없기 때문이다. 그런데 이번에는 단단해진 계약서에서 구현 성공률이 오히려 올라갔는데, 이는 고친 방향이 엉뚱하지 않았다는 뜻이죠. 빡빡해진 것이 아니라 정확해진 것인데, 이 차이는 결과로만 알 수 있다.

그렇다면 이 흐름은 어디까지 일반화할 수 있을까. 좋은 소식과 조심스러운 소식이 함께 있는데, 좋은 소식은 단계 분리가 재활용 없이도 통했다는 점이고, 조심스러운 소식은 이 효과가 특정 울타리 안에서만 확인됐다는 점이다. 다음 장면에서는 바로 그 울타리 이야기를 다룬다. 어디까지 믿고 어디부터 의심해야 하는지를 가르는 선이기 때문이다.

구체적인 실패 사례로 느슨한 계약서를 단단하게 고치는 과정을 보여주는 그림
구체적인 실패 사례로 느슨한 계약서를 단단하게 고치는 과정을 보여주는 그림

왜 Verus에서만 보이고 옆 동네에서는 안 보일까

연구진은 같은 질문을 들고 Dafny와 Lean 평가로 가보는데, 거기서는 이 효과가 재현되지 않았다고 분명히 말한다. 저는 이 고백이 논문을 더 믿게 만든다고 봅니다. 되면 된다고만 말하는 논문보다, 어디서는 안 된다고 말하는 논문이 더 정직하기 때문인데, 경계를 그어준 덕분에 독자는 믿음의 범위를 정할 수 있다. Verus와 Rust 작업 묶음에서 본 현상이라는 말인데, 옆 동네 도구에 그대로 옮겨 붙일 수는 없다는 뜻이죠.

왜 이런 경계가 생길까. 논문이 원인을 단정하지는 않지만, 몇 가지 짐작은 가능한데, 언어와 검증기의 결이 다르고, 계약서를 쓰는 방식과 피드백이 들어오는 지점도 다르기 때문이다. Verus에서는 모델이 증인을 내놓기 쉬운 틈이 있었고, 피드백이 그 틈을 메우는 방향으로 작동했을 수 있다. 반면 다른 도구에서는 틈의 모양이 다르거나 피드백의 압력이 약해서 같은 기울기가 안 생겼을 수 있죠. (참고로 Dafny와 Lean은 각각 다른 검증 생태계를 가진 도구인데, 같은 감사라는 말을 써도 실제 손 움직임은 꽤 다르다고 보면 됩니다.) 저는 여기서 성급한 일반화를 멈췄다. 지형이 다르면 같은 씨앗도 다르게 자라기 때문이다.

그렇다면 사람의 역할은 무엇일까. 저는 앞으로 보고 싶은 것이 분명한데, 각 도구에서 피드백이 증거를 지우는 정도를 재는 눈금부터 만드는 일이다. Verus에서 통하는 처방을 다른 곳에 그대로 쓰기 전에, 그곳의 피드백이 얼마나 증거를 뭉개는지를 먼저 재야 하기 때문이다. 저희 팀이 새로운 검증 파이프라인을 본다면 먼저 물을 것도 같은 질문이다. 감사와 수리를 한 고리에 묶을 것인지, 나눌 것인지를 정하기 전에, 피드백의 압력이 어디로 흐르는지를 보자는 것이죠. 이 질문이 있어야 다음 도구가 나와도 같은 실수를 반복하지 않는다.

그래서 무엇을 먼저 하고 무엇을 나중에 할까

앞에서 미뤄둔 질문으로 돌아올 차례인데, 결국 순서는 어떻게 세워야 할까. 논문이 주는 답은 짧은데, 인정된 실패를 먼저 보존하고 확정하라는 것이다. 모으고, 도장을 찍고, 그다음에 고치라는 뜻인데, 이 순서를 지키면 감사와 수리라는 서로 다른 목적이 서로를 갉아먹지 않는다. 59.0과 27.1이라는 수율 차이, 81.3과 62.5라는 수리 성적 차이, held-out에서의 실패, 형식 통제와 파서 확인, 그리고 Dafny와 Lean에서의 불발까지 모두 같은 방향을 가리키는데, 순서를 나누는 쪽이 증거를 살리고 결과도 낫다는 것이다.

이 논문이 흥미로운 이유는 단순히 피드백이 나쁘다는 데 있지 않다. 일을 두 종류로 나눠보고, 각 일에 맞는 태도를 정해준 데 있다. 찾을 때는 고치지 말고, 고칠 때는 찾은 것을 들고 가라는 말인데, 말로만 들으면 당연하지만 막상 파이프라인을 짜면 자꾸 한 고리에 다 넣게 된다. 한 번에 돌리면 편해 보이는데, 편한 구조가 증거를 지운다는 것이 이번 결과의 뼈아픈 대목이죠. 앞으로 에이전트로 검증 일을 시킬수록, 한 고리에 무엇을 몇 개나 넣을지를 먼저 따져봐야 할 것 같다. 고치는 말을 언제 꺼낼지를 정하는 일이, 어쩌면 모델을 바꾸는 일만큼 중요해질 테니까요.

효과가 또렷한 Verus 섬과 평평한 Dafny와 Lean 섬을 담은 경계 지도
효과가 또렷한 Verus 섬과 평평한 Dafny와 Lean 섬을 담은 경계 지도

참고 자료

  1. When Correctness Feedback Erases Evidence: Phase-Separated Completeness Auditing in Verus · arxiv.org

    리뷰 원문