코딩 에이전트 컴파일러 개발에서의 신뢰할 수 있는 컴파일(Credible Compilation)과 검증(Verification)에 대한 정량적

형식 프로그램 검증 (Formal program verification)은 해당 분야의 오랜 목표입니다. 본 논문에서는 두 가지 주요 컴파일러 검증 접근 방식인 신뢰할 수 있는 컴파일/번역 검증 (credible compilation/translation validation)과 전체 검증 (full verification)에 대한 최초의 정량적 비교를 제시합니다. (인간의 감독 하에 작동하는) 코딩 에이전트가 개발한 최초의 검증된 컴파일러를 사용하여, 이 두 가지 접근 방식을 사용하여 여러 최적화 (optimizations)를 구현하는 코딩 에이전트의 정량적 결과를 제시합니다. 결과에 따르면 1) 검증 (verification)은 신뢰할 수 있는 컴파일 (credible compilation)보다 대략 한 자릿수(order of magnitude) 더 많은 개발 노력을 요구하며, 2) 증명 가능성 (provability)을 높이기 위해 코딩 에이전트는 검증된 최적화 (verified optimizations)를 위해 덜 효율적인 알고리즘과 데이터 구조를 선택하고, 3) 증명 노력 (proof effort)을 최소화하려는 시도로 코딩 에이전트는 검증된 최적화를 위해 최적화 범위 축소 (optimization scope reductions)를 반복적으로 구현하였으며, 4) 고려된 최적화들에 대해 인증서 확인 시간 (certificate checking time)이 최적화 및 인증서 생성 시간 (certificate generation time)을 압도합니다. 증가된 증명 오버헤드 (proof overhead)로 인해, 검증된 최적화는 신뢰할 수 있는 컴파일 최적화보다 실질적으로 더 많은 감독과 코딩 세션을 필요로 했습니다. 이러한 맥락에서 작동하는 현대적 코딩 에이전트의 역량을 고려할 때, 고려된 최적화들(도달 불가능 코드 제거 (unreachable code elimination), 데드 어사인먼트 제거 (dead assignment elimination), 상수 전파/폴딩 (constant propagation/folding))에 대해 신뢰할 수 있는 컴파일과 검증된 버전 모두 구현 노력이 실행 가능한 수준으로 유지되었습니다.