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