본 논문은 기존의 기호적 알고리즘과 대규모 언어 모델(LLM)을 결합하여 소프트웨어 검증기, 합성기 및 기타 자동 추론(AR) 도구를 구축하는 것에 대한 관심이 증가하고 있음을 배경으로 제시되었다. 현재의 신경 기호적 AR 시스템 구축 방식은 임시적인 프로그래밍 모델이며, 기존 기호적 알고리즘의 강력한 보장을 제공하지 못하고, 신경망과 기호적 추론의 깊은 동기화를 통해 LLM 기반 추론의 잠재력을 완전히 발휘하지 못한다는 한계점을 지적한다. 따라서 논문에서는 신경 기호적 전이 시스템(Neurosymbolic Transition Systems)을 원칙적인 계산 모델로 제안하며, 이 모델에서 기호적 상태는 직관과 짝을 이루고 상태 전이는 기호와 직관에 대해 병렬적으로 작동한다. 이 새로운 패러다임이 기존의 능력을 넘어 논리적 추론을 확장하는 동시에 기호적 알고리즘의 강력한 보장을 유지할 수 있는 이유를 논증하고, 제안된 계산 모델을 논리 프로그래밍 언어로 구현하는 방법을 개략적으로 설명한다.
