SWE-Proof가 주는 실무적 결론은 단순하다. 코드 생성 에이전트를 고를 때 “테스트를 통과했는가”만 보면 안 된다. 그렇다고 “형식 검증을 붙이면 신뢰성이 해결된다”고 볼 근거도 아직 부족하다. 이 벤치마크에서 확인되는 병목은 패치 생성 능력 자체보다, 자연어 이슈를 빠짐없는 형식 명세로 바꾸는 능력에 가깝다.

따라서 이 글의 독자는 코드 생성 모델을 평가하거나 사내 개발 에이전트 도입 기준을 정하는 팀이다. 의사결정 규칙은 이렇게 잡는 편이 안전하다. 기능 요구사항을 명세로 좁힐 수 있는 변경이라면 테스트 기반 평가에 형식 검증 평가를 추가하라. 반대로 명세 작성까지 모델에게 맡기는 제품이라면, 검증 통과율을 곧바로 신뢰성 지표로 쓰지 말고 “명세 충실성”을 별도 평가 항목으로 분리해야 한다.

SWE-Proof가 바꾸는 질문

기존 SWE 계열 벤치마크의 기본 질문은 “모델이 실제 저장소 이슈를 고쳐서 숨겨진 테스트를 통과하는가”에 가깝다. SWE-Proof는 질문을 한 단계 더 밀어붙인다. “그 패치가 기계가 확인할 수 있는 증명까지 동반하는가”다.

이 차이는 작지 않다. 테스트는 샘플이다. 통과했다고 해서 모든 관련 입력과 상태에서 맞는다는 뜻은 아니다. 또 널리 쓰이는 벤치마크일수록 데이터 암기 가능성 문제도 커진다. SWE-Proof 논문 초록은 바로 이 두 한계, 즉 테스트의 불완전성과 암기 취약성을 출발점으로 삼는다.

SWE-Proof의 구성도 기존 형식 검증 연구와 다르다. 기존 연구가 독립형 과제와 입력으로 주어진 명세를 다뤘다면, SWE-Proof는 실제 대형 저장소의 이슈를 대상으로 한다. SWE-Proof는 SWE-bench Verified의 500개 실제 이슈를 형식 검증 대상으로 전환하며, SWE-bench Pro에도 확장 적용된다. 대상 패치는 실제 저장소 패치와 동등한 Python 패치이며, 검증 구현은 백엔드별 언어로 작성된다. 백엔드는 Lean, Nagini, Velvet이다. Lean에서는 에이전트가 작성한 증명을 컴파일러가 확인하고, Nagini와 Velvet은 SMT 솔버로 의무 조건을 푼다.

즉 SWE-Proof의 가치는 “형식 검증 벤치마크”라는 말 자체보다, 실제 이슈 해결과 기계 검증을 같은 평가 안에 넣었다는 데 있다.

테스트 통과는 과대평가될 수 있다

실무적으로 중요한 신호는 이 부분이다. SWE-Proof 결과에 따르면 두 프런티어 모델에서 테스트를 통과한 패치 중 4분의 1에서 절반은 반례를 허용했다. 이는 테스트 기반 점수가 실제 정확도를 과대평가할 수 있다는 근거다.

이 수치를 모델 순위표처럼 읽으면 안 된다. 제공된 근거만으로는 SWE-Proof에서 기존 SWE-bench, SWE-bench Verified, SWE-bench Pro 대비 모델 간 전체 순위가 어떻게 바뀌는지 확인되지 않는다. 하지만 평가 방식의 위험은 뚜렷하다. 테스트 통과율은 “발견된 오류가 없다”는 신호이지 “명세 전체를 만족한다”는 증거가 아니다.

여기에 별도의 맥락도 있다. OpenAI가 공개한 SWE-bench Verified 관련 글은 모델이 자주 실패한 데이터셋의 27.6% 부분을 감사했더니, 감사 대상 문제 중 최소 59.4%에서 기능적으로 올바른 제출을 거부하는 결함 있는 테스트가 있었다고 보고했다. 한쪽에서는 테스트가 틀린 정답을 통과시킬 수 있고, 다른 한쪽에서는 맞는 정답을 떨어뜨릴 수도 있다. 방향은 다르지만 결론은 같다. 테스트 기반 벤치마크 하나로 모델의 코딩 능력을 안정적으로 재단하기 어렵다.

병목은 “증명”보다 “무엇을 증명할지”다

SWE-Proof에서 더 살펴볼 지점은 형식 검증을 붙였을 때 성능이 자동으로 좋아지지 않는다는 점이다. 올바른 형식 명세가 제공되면 Opus 4.8의 해결률은 85%에서 95%로 상승했다. 하지만 모델이 명세를 직접 작성하는 조건에서는 무보조 기준선 대비 이득이 없었다.

이 결과는 평가와 제품 설계 모두에 영향을 준다. 모델이 틀린 이유가 단순히 코드를 못 짜서가 아닐 수 있다. 요구사항의 일부만 형식화하거나, 이슈의 의도를 좁게 해석하거나, 저장소 상태와 상호작용하는 조건을 명세에서 빠뜨리면 검증은 오히려 착시를 만든다. 기계는 주어진 명세를 확인할 뿐, 그 명세가 사용자 의도를 충분히 담았는지는 자동으로 보장하지 않는다.

그래서 SWE-Proof가 드러낸 실패의 중심은 “패치를 생성하지 못함”에서 “명세가 요구사항을 충실히 담지 못함”으로 이동한다. 이 이동은 실무적으로 중요하다. 코드 에이전트 평가 항목을 패치 성공률 하나로 두면, 명세 작성 실패와 구현 실패를 구분하지 못한다. 개선해야 할 대상도 흐려진다.

의사결정 규칙

SWE-Proof를 평가 체계에 넣을지는 다음 기준으로 판단하는 것이 합리적이다.

첫째, 변경 요구가 기능적 정확성으로 표현될 수 있는가. 특정 함수 동작, 자료구조 불변식, 경계 조건처럼 명세화 가능한 부분이라면 형식 검증은 테스트가 놓치는 반례를 잡는 보완재가 된다. 이 경우 테스트 통과율만 보고 모델을 고르지 말고, 검증 가능한 하위 집합에서 반례 발생률과 증명 성공률을 함께 보아야 한다.

둘째, 명세를 누가 쓰는가. 사람이 검토한 올바른 형식 명세가 제공되는 워크플로라면 SWE-Proof식 평가는 모델의 구현·증명 능력을 더 선명하게 볼 수 있다. 반대로 모델이 이슈를 읽고 명세까지 스스로 써야 하는 제품이라면, “검증 통과”만으로는 부족하다. 명세가 원래 요구를 얼마나 포착했는지 별도 리뷰나 테스트가 필요하다.

셋째, 평가 범위를 과장하지 않는가. SWE-Proof는 실제 대형 저장소 이슈를 대상으로 한다는 점에서 독립형 형식 검증 과제보다 실무에 가깝다. 그러나 제공된 근거만으로는 운영 환경 상호작용, 권한 사용, 배포 절차, 장기 작업 같은 에이전트 전반의 안전성까지 평가한다고 보기 어렵다. 다른 언어, 산업 도메인, 비정형 작업으로의 일반화도 확인되지 않았다.

따라서 SWE-Proof는 코드 생성 에이전트 구매나 도입 판단에서 “테스트 통과율을 대체하는 단일 점수”가 아니라 “테스트가 과대평가하는 영역을 드러내는 2차 필터”로 쓰는 편이 낫다. 특히 내부 코드베이스에서 고위험 변경을 자동화하려는 팀이라면, 먼저 명세화 가능한 변경 유형을 골라 작은 평가 세트를 만들고, 테스트 통과 패치 중 반례가 나오는 비율을 측정해야 한다. 그 비율이 높다면 모델 교체보다 먼저 평가 체계가 부족하다는 신호로 봐야 한다.

다음으로 읽기

• AI 인프라 투자 전력 리스크
• STR-Agent와 LLM 라우팅의 경계
• Bypass Observation의 올바른 용도
• GoAnt와 품질-다양성 팩터 탐색
• BioSync 도입 판단의 핵심

참고 자료

• Why SWE-bench Verified no longer measures frontier coding capabilities - openai.com
• arxiv.org - arxiv.org