본 논문은 현대 소프트웨어 시스템의 신뢰성과 보안을 확보하는 데 중요한 소프트웨어 테스트 및 검증에 대해 다룬다. 기존의 형식적 검증 기법(모델 검증 및 정리 증명)의 확장성 문제점을 지적하며, 최근 등장한 대규모 언어 모델(LLM) 기반 소프트웨어 분석의 새로운 패러다임을 제시한다. LLM은 버그 예측 및 불변식 생성과 같은 작업에서 유망한 성능을 보이지만, 기존 기법의 형식적 보장은 제공하지 못한다. 본 논문에서는 기존의 형식적 방법, LLM 기반 분석, 그리고 두 기법의 장점을 결합한 하이브리드 기법 등 세 가지 주요 접근 방식에 초점을 맞춰 최첨단 소프트웨어 테스트 및 검증에 대한 종합적인 연구를 제시한다. 각 접근 방식의 강점, 한계 및 실제 응용 프로그램을 탐구하고, 독립적인 방법의 약점을 해결하기 위한 하이브리드 시스템의 잠재력을 강조한다. 형식적 엄격성과 LLM 기반 통찰력을 통합하는 것이 소프트웨어 검증의 효율성과 확장성을 향상시킬 수 있는지 분석하고, 더욱 강력하고 적응력 있는 테스트 프레임워크를 위한 경로로서의 실행 가능성을 탐구한다.
