LLM(Large Language Models)은 기존 솔루션을 능가하는 프로그램을 발견하며 프로그램 합성(Program Synthesis) 분야에서 인상적인 성공을 보여주었습니다. 그러나 이러한 접근 방식은 솔루션의 값이나 통과된 테스트의 수와 같이 프로그램의 품질을 나타내는 단순한 수치 점수에 의존합니다. 점수만으로는 프로그램이 왜 실패했는지에 대한 가이드를 제공하지 않기 때문에, 시스템은 일부가 성공하기를 바라며 많은 후보를 생성하고 평가해야 하며, 이는 LLM의 추론(Inference) 및 평가 비용을 증가시킵니다.
우리는 다른 접근 방식인 속성 가이드 기반 LLM 프로그램 합성(Property-guided LLM program synthesis)을 연구합니다. 프로그램을 평가한 후 점수를 매기는 대신, 후보가 형식적으로 정의된 속성(Property)을 만족하는지 확인합니다. 속성이 위반되면 평가를 조기에 중단하고, 프로그램이 정확히 어떻게 실패했는지를 보여주는 구체적인 반례(Counterexample)를 LLM에 제공합니다. 이러한 피드백은 프로그램 생성 횟수와 평가 비용을 모두 획기적으로 줄이며, LLM이 더 강력한 프로그램을 생성하도록 유도할 수 있습니다.
우리는 PDDL(Planning Domain Definition Language) 계획 도메인에서 이 접근 방식을 평가하며, LLM이 직접적인 휴리스틱 함수(Heuristic functions)를 합성하도록 요청합니다: 즉, 엄격하게 개선되는 전이(Strictly improving transitions)에 의해 도달 가능한 모든 상태는 엄격하게 개선되는 후속 상태를 가집니다. 이 속성을 가진 휴리스틱은 언덕 오르기(Hill-climbing) 알고리즘을 목표 상태로 직접 인도합니다. 반례 가이드 수정 루프(Counterexample-guided repair loop)는 하나의 후보 프로그램을 생성하고, 훈련 세트(Training set)에 대해 속성을 확인하며, 속성을 위반하는 첫 번째 사례를 반환합니다.
우리는 분포 외(Out-of-distribution) 테스트 세트를 포함한 10개의 계획 도메인에서 우리의 접근 방식을 평가합니다. 합성된 휴리스틱은 거의 모든 테스트 작업에서 효과적으로 직접적(Direct)이며, 기존의 가장 우수한 생성 방법과 비교했을 때 우리의 접근 방식은 도메인당 평균 7배 적은 프로그램을 생성하고, 탐색(Search)을 사용하지 않고도 더 많은 작업을 해결하며, 후보를 평가하는 데 수 자릿수(Several orders of magnitude) 적은 계산량을 요구합니다. 문제가 검증 가능한 속성을 허용하는 경우라면, 속성 가이드 LLM 합성은 비용을 절감하고 프로그램 품질을 향상시킬 수 있습니다.