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