본 논문은 코드 생성, 완성, 수정과 같은 코딩 작업에서 강력한 성능을 보이는 대규모 언어 모델(LLM)이 코드에 대한 복잡한 심볼릭 추론을 처리하는 능력은 아직 충분히 탐구되지 않았다는 점을 지적합니다. 따라서 최악의 경우 프로그램 실행을 특징짓는 심볼릭 제약 조건을 추론하는 최악의 경우 심볼릭 제약 조건 분석 작업을 제시합니다. 이러한 제약 조건을 해결하여 소프트웨어 시스템의 성능 병목 현상이나 서비스 거부 공격 취약성을 노출하는 입력을 얻을 수 있습니다. 기존 최첨단 LLM(예: GPT-5)이 이 작업에 직접 적용될 경우 어려움을 겪는다는 것을 보여주고, 이 문제를 해결하기 위해 기존 프로그램 분석 도구를 사용하여 더 작은 구체적인 입력 크기에 대한 최악의 경우 제약 조건을 계산한 다음 LLM을 활용하여 이러한 제약 조건을 더 큰 입력 크기로 일반화하는 혁신적인 신경 기호 접근 방식인 WARP를 제안합니다. WARP는 LLM 기반 최악의 경우 추론을 위한 증분 전략, 강화 학습을 SMT(Satisfiability Modulo Theories) 솔빙과 통합하는 솔버 정렬 신경 기호 프레임워크, 그리고 엄선된 심볼릭 제약 조건 데이터 세트로 구성됩니다. 실험 결과, WARP가 최악의 경우 제약 조건 추론 성능을 지속적으로 향상시킨다는 것을 보여줍니다. 엄선된 제약 조건 데이터 세트를 활용하여 강화 학습을 통해 모델 WARP-1.0-3B를 미세 조정하여 크기가 같은 그리고 더 큰 기준 모델보다 성능이 크게 향상되었습니다. 이러한 결과는 증분 제약 조건 추론이 LLM의 심볼릭 추론 처리 능력을 향상시키고 엄격한 프로그램 분석에서 신경 학습과 형식적 방법 간의 더 깊은 통합 가능성을 강조합니다.
