검증 실패로부터 코딩 에이전트를 위한 재사용 가능한 가이드로

코딩 에이전트는 프로그램이 명세(specification)를 만족하고, 그 명세가 요청된 동작을 포착했는지 확립해야 합니다. 우리는 검증 실패에 대한 전문가 진단이 이 작업의 재사용 가능한 가이드가 될 수 있는 방법을 연구합니다. 우리의 접근 방식은 K 프레임워크 내 실행 가능한 언어 정의와 명세를 구성하고, 증명을 복구하며, 그 적절성을 감사(auditing)하기 위한 일련의 절차들을 결합합니다. 164개의 Python 프로그래밍 태스크로 구성된 벤치마크인 HumanEval에서 진행된 인간 주도 개발 캠페인은, 두 번의 목표화된 수리(repair) 이후 최종 AI 감사 통과 판결로 측정했을 때, 시맨틱스와 키트(kit)를 사용하여 164/164의 성공률을 달성했습니다. 감사가 성공적인 증명이 해결하지 못한 문제를 탐지하는지 확인하기 위해, 우리는 작성자 검토가 완료된 깨끗한 패키지와 결함이 있는 패키지 쌍 12개를 구성했습니다. 모든 패키지는 K 증명을 통과했으며, 완료된 감사들은 모든 결함을 식별하고 모든 깨끗한 패키지를 수용했습니다. 그런 다음 우리는 KleverBench를 사용하여 변경된 연산자 의미를 가진 31개 프로그램에 대한 명세 및 증명 구성을 테스트했습니다. 완전한 수용 규칙 및 동등하게 긴 일반적인 조언과의 비교는 두 가지 모델 및 예산 설정 전반에 걸쳐 혼합된 결과를 나타냈으며, 자원 한계 내에서 유용한 가이드를 선택하는 것에 대한 추가 연구를 촉진합니다. 인간 검토가 이루어진 Optimism 증명은 London 시맨틱스 하에서 무제한 가스로 주어진 입력 경계 내의 여섯 가지 연산에 대한 예상 일시 중단 복구(pause reverts)를 확립했습니다. 우리는 검증 가능한 정확성 주장을 가진 프로그램을 제공하는 에이전트를 향한 진척 상황, 어려움, 그리고 교훈들을 보고합니다.