LLM이 코드의 정당성을 증명할 수는 없지만, 그것을 위한 상용구는 작성할 수 있다
클린룸 검증은 검증 조건을 생성하고 해소하는 것을 요구한다. 여기서 LLM이 주석과 VC 생성을 자동화하여 실제 어려운 증명에 집중할 수 있게 하는 방법을 소개한다.
클린룸 소프트웨어 공학은 코드를 컴파일하기 전에 그 정당성을 증명할 것을 요구한다. 그것은 고귀하게 들리지만, 열 개의 정수를 정렬하는 함수를 위해 루프 불변식을 세 시간 동안 작성하다 본다면 상황이 달라진다. 병목 지점은 증명 자체가 아니다. 상용구이다. 검증 조건을 생성하고,…