본 논문은 대규모 언어 모델(LLM)의 프로그램 의미론 추론 능력을 평가하기 위한 포괄적인 벤치마크인 FormalBench를 제안합니다. FormalBench는 프로그램의 정확성 검증을 돕기 위해 공식적인 프로그램 명세를 생성하는 작업을 통해 LLM의 추론 능력을 평가합니다. 이 작업은 모든 가능한 프로그램 실행에 대한 포괄적인 추론(완전성)과 형식 구문 및 의미론을 준수하는 정확하고 구문적으로 올바른 표현 생성(일관성)을 필요로 합니다. 실험 결과, LLM은 단순한 제어 흐름에서는 잘 수행하지만, 특히 고급 프롬프팅을 사용하더라도 루프와 같은 더 복잡한 구조에서는 어려움을 겪는 것으로 나타났습니다. 또한, 의미를 보존하는 변환에 대한 견고성이 제한적이며, 자가 복구 프롬프트를 설계하여 성공률을 25% 향상시켰습니다.
