자연어로 작성된 소프트웨어 요구사항에 대한 프로그램의 정확성 검증은 어렵고 미개척 분야입니다. 본 논문은 대규모 언어 모델(LLM)이 이 문제 해결에 유망하지만 단순한 버그조차 감지하지 못하는 경우가 많다는 점을 지적합니다. 이를 해결하기 위해 프로그램 분석 및 검증의 기본 개념을 자연어 문서에 적용한 새로운 접근 방식인 HoarePrompt를 제시합니다. HoarePrompt는 최강 후조건 미적분에서 영감을 얻어 LLM이 코드의 여러 지점에서 도달 가능한 프로그램 상태를 자연어로 설명하는 단계별 프로세스를 사용합니다. 루프를 관리하기 위해 모델 검증에서 널리 사용되는 k-induction 방법을 적용한 few-shot-driven k-induction을 제안합니다. 프로그램 상태가 설명되면 HoarePrompt는 LLM을 활용하여 이러한 상태 설명이 추가된 프로그램이 자연어 요구사항을 준수하는지 평가합니다. 프로그래밍 경진 대회 문제 해결책으로 구성된 CoCoClaNeL이라는 도전적인 데이터셋을 구축하여 프로그램 정확성 분류기의 품질을 평가했습니다. 실험 결과, HoarePrompt는 Zero-shot-CoT 프롬프트를 직접 사용하는 것보다 MCC를 62% 향상시켰고, LLM 기반 테스트 생성을 통해 정확성을 평가하는 분류기보다 MCC를 93% 향상시켰습니다. 유도적 추론 메커니즘은 MCC를 28% 향상시켜 루프 관리의 효과를 강조합니다.
