본 논문은 대규모 언어 모델(LLM)의 프로그램 의미론 추론 능력을 평가하기 위한 포괄적인 벤치마크인 FormalBench를 제시합니다. FormalBench는 프로그램의 정확성 검증을 돕기 위해 공식적인 프로그램 명세를 생성하는 작업을 통해 LLM의 추론 능력을 평가합니다. 연구 결과, LLM은 단순한 제어 흐름에서는 좋은 성능을 보이지만, 특히 루프와 같은 복잡한 구조에서는 어려움을 겪는다는 것을 보여줍니다. 또한, 의미를 보존하는 변환에 대한 견고성이 제한적임을 발견했습니다. 마지막으로, 일반적인 실패 패턴을 강조하고 성공률을 25% 향상시키는 자가 복구 프롬프트를 설계했습니다.
