형식 검증 가능한 AI 산출물 설계와 검사기 파이프라인

사람이 읽던 판정을 검사기로 옮기는 방식

OpenAI가 Astra의 해법 10건을 공개할 때 각 증명을 Lean 4로 형식화한 기계 검증 인증서를 저장소에 함께 올렸다. 모델이 낸 해법을 사람이 논증으로 읽어 판단하는 대신, 증명 검사기가 판정할 수 있게 한 사례다.

자연어 설명은 설득력과 정확성이 어긋날 수 있다. 반면 형식 증명은 검사기를 통과하거나 통과하지 못한다. 이 구조는 형식 증명에만 한정되지 않는다. 타입 검사, 스키마 검증, 실행 가능한 테스트, 린트처럼 기계가 판정할 수 있는 출력 형식을 요구하면 일반 개발 업무에도 옮길 수 있다.

이때 검토 부담은 산출물 건수에 비례하기보다 검증 규칙을 유지하는 비용으로 고정된다. 다만 검사기 통과가 정확성 전체를 보증하는 것은 아니다. 검사는 명세와 결과의 일치만 판정하며, 명세가 타당한지는 별도로 검토해야 한다.

출력 형식부터 검증 가능하게 만든다

모델에 자유 텍스트 대신 판정 가능한 형식을 요구한다. 구조화 데이터에는 JSON 스키마를, 코드에는 타입 시그니처와 테스트를, 논증에는 형식 증명을 적용할 수 있다. 프롬프트에 형식을 설명하는 것만으로는 이탈이 생기므로, 출력 계층에서도 구조를 강제해야 한다.

생성 직후에는 검사기 파이프라인을 실행하고 결과를 상태로 남긴다. 구문 검사, 스키마·타입 검사, 의미 검사를 차례로 배치하면 비용이 낮은 검사가 먼저 잘못된 결과를 걸러낸다. 통과·부분 통과·실패를 구분하고, 전체가 검증되지 않은 구간은 산출물에 분명히 표시한다. 그렇지 않으면 부분 검증을 전체 보증으로 오인하기 쉽다.

⤢✕

검사 실패 시에는 오류 메시지를 요약하거나 가공하지 않고 재생성 입력에 그대로 넣는다. 수정에 필요한 정보가 손실되면 재생성 정확도도 떨어진다. 반복에는 상한이 필요하다. 상한 없이 루프를 돌리면 같은 오류를 반복할 수 있으므로, 초과한 결과만 사람 개입 큐로 넘긴다.

검사기 실행 시간도 별도로 수집해야 한다. 형식 검증은 생성보다 느린 경우가 있어 병목이 검증 단계로 이동할 수 있다. 느린 검사는 비동기로 분리하거나 샘플링 적용을 검토할 수 있다.

규칙과 통과 이력도 산출물의 일부다

스키마, 타입 정의, 테스트는 형상관리 대상이다. 검증 규칙이 조용히 바뀌면 과거의 통과 이력은 의미를 잃는다. 산출물에는 통과 당시의 규칙 버전을 기록하고, 어떤 결과가 어떤 규칙으로 언제 통과했는지도 보존해야 한다.

이 기록은 사후 결함이 발견됐을 때 영향 범위를 계산하는 근거가 된다. 검사기 우회 권한은 제한하고, 우회가 발생하면 사유를 남긴다. 예외가 일상적인 경로가 되면 검증 구조 자체가 무력화된다.

기계 판정 범위와 사람 검토 범위를 나눈다

업무별로 기계 판정이 가능한 형식을 먼저 목록화한다. 구조화 데이터는 스키마, 코드는 타입·테스트, 설정은 유효성 검사에 연결할 수 있다. 자연어로만 다루던 산출물도 일부는 구조화 형식으로 옮길 수 있는지 검토한다.

검사기 도입 순서는 오류 발생 빈도와 구현 비용의 비율로 정한다. 비용이 낮고 자주 실패를 잡는 검사가 우선이다. 새 도구를 만들기 전에 기존 CI에 있는 린트와 테스트를 생성 파이프라인에 연결하는 편이 낫다.

재생성 반복 상한은 3회 내외에서 시작해 실측으로 조정한다. 반복 횟수 분포를 보면 상한의 적정값을 판단할 수 있고, 상한 도달 사례는 유형별로 분류해 명세 개선에 반영할 수 있다.

기계가 판정하지 못하는 항목은 목록으로 명시하고 담당을 정한다. 목록에 없는 항목은 검토 대상이 아니라는 규칙이 사람 검토의 범위를 고정한다. 특히 명세가 원래 요구를 제대로 반영하는지의 판단은 사람에게 남겨야 한다. 검사기는 명세 위반만 찾아낸다.

품질 지표로는 최초 시도 통과율, 평균 재생성 횟수, 사람 개입 비율, 통과 후 사후 결함 발생률을 둘 수 있다. 규칙 변경은 정기 배포에 포함하고, 변경 때는 회귀 확인을 거친다. 규칙을 강화하면 과거에 통과했던 산출물이 실패로 전환될 수 있다.

형식 검증과 사람 검토가 다루는 차이

구분	형식 검증 강제	자연어 출력 후 사람 검토
오류 유입률	명세 범위 내 0에 수렴	검토자 역량에 의존
건당 검토 비용	검사기 실행 비용	사람 시간
초기 구축	명세·검사기 필요	없음
적용 범위	형식화 가능 산출물	전체
확장성	건수 증가에 둔감	건수 비례 증가
명세 오류 대응	통과해도 틀릴 수 있음	검토자가 포착 가능

형식 검증은 명세 범위 안의 오류 유입을 사실상 차단하고, 결과 수가 늘어도 검토 비용이 함께 커지지 않는다. 판정 근거를 기록으로 남길 수 있다는 점도 다르다. 대신 명세와 검사기를 만드는 초기 비용이 필요하며, 잘못된 명세를 통과한 결과는 여전히 틀릴 수 있다.

사람 검토는 명세 밖의 문제와 맥락 오류를 포착할 수 있고 초기 구축 비용도 없다. 그러나 산출물 수에 따라 비용이 증가하며, 검토자의 피로와 역량에 따라 오류 유입률도 달라진다. 모델 산출량이 사람 검토 용량을 넘어서면 형식 검증이 확장 경로가 되고, 명세 타당성 검토만 사람에게 남기는 구성이 현실적이다.

자동 재생성은 사람을 기다리지 않고 루프를 돌릴 수 있어 단순 형식 오류가 많은 구간에서 개입 건수를 줄인다. 반대로 같은 오류를 반복하면 자원만 소모하고, 원인이 명세에 있을 때는 개선이 늦어진다. 즉시 사람 개입은 원인 진단과 명세 결함 발견이 빠르지만, 처리량은 사람 가용성에 묶이고 사소한 반복 오류에도 인력이 든다. 재생성 상한을 두고 초과 사례만 사람에게 넘기는 방식이 두 접근을 함께 쓰는 형태다.

모든 산출물을 형식화하면 보증 수준은 균일해지지만, 형식화가 어려운 영역에는 구현 부담과 표현력 제약이 생길 수 있다. 핵심 구간만 형식화하면 부담을 줄이고 효과가 큰 곳에 자원을 집중할 수 있지만, 미형식화 영역의 경계를 계속 관리해야 한다. 실패 비용이 높은 구간을 먼저 형식화하고 미검증 구간을 결과물에 표시하는 방식이 보증 수준과 구현 부담의 균형점이 된다.

검증과 확인은 서로 다른 활동이다

형식 증명은 정형 명세와 정형 검증이 결합된 사례다. 명세가 판정 기준이 되므로, 명세 품질이 보증 수준의 상한을 정한다. 명세와 구현의 일치를 기계가 판정한다는 점에서 리뷰 중심의 확인보다 결합이 강하다.

검사기 통과는 검증에 해당한다. 반면 명세가 원래 요구를 반영하는지 판단하는 일은 확인에 해당한다. 둘을 혼동하면 검사기를 통과했지만 쓸모없는 결과가 나올 수 있다. 미검증 구간을 표시하는 일은 확인 활동이 필요한 범위를 정의하는 장치이기도 하다.

우회 제한과 우회 사유 기록은 프로세스 준수 통제다. 통과 이력과 규칙 버전 기록은 결함 발생 뒤 영향 범위를 산정하기 위한 추적성 기반이 된다.

연구 발표와 애플리케이션 설계의 변화 방향

모델 산출물에 기계 검증 인증서를 함께 공개하는 방식은 연구 발표의 관행으로 굳어지는 흐름에 있다. 자연어 산출물을 구조화 형식으로 바꾸고 검사기를 연결하는 설계도 일반 애플리케이션 영역으로 확산되는 방향이다.

검사기 실행 시간은 파이프라인의 병목으로 부상할 수 있으며, 검증 인프라의 용량 산정은 별도 과제가 된다. 미검증 구간 표시는 AI 산출물의 표기 요건으로 요구되고, 보증 범위를 명시하는 일은 계약 항목으로 편입되는 방향이다.

Astra의 Lean 형식 증명 공개가 보여준 핵심은 판정 주체를 사람에서 검사기로 옮긴 데 있다. 타입 검사, 스키마 검증, 테스트 통과로 이 원리를 옮기면 결과물 수가 늘어도 검토 비용이 같이 늘지 않는 구조를 만들 수 있다. 단, 검사기 통과가 명세와의 일치만 보증한다는 한계를 인정하고, 명세의 타당성과 미검증 영역은 사람의 책임으로 남겨야 한다.