논리적 명세(logical specification)로부터 하드웨어 회로를 자동으로 구축하는 문제인 Reactive synthesis는 형식 검증(formal verification) 분야의 오래된 과제입니다. 이는 두 가지 이유로 해결하기 어렵습니다. 하나는 알고리즘적으로 어렵다는 점이며, 다른 하나는 수동으로 형식 명세(formal specifications)를 작성하는 것이 매우 어렵다는 점입니다. 본 논문에서는 이 문제의 양면을 모두 다룹니다. 알고리즘 측면에서는, 대규모 추론 모델(large reasoning models)을 모델 체커(model checkers)와 결합하여 타당한 심볼릭 피드백(sound symbolic feedback)을 통해 합성된 Verilog 구현을 반복적으로 수정하는 Reactive synthesis를 위한 신경-심볼릭(neuro-symbolic) 접근 방식을 제시합니다. 우리의 접근 방식은 연례 합성 경진대회(annual synthesis competition)의 최고 전용 도구들보다 더 많은 벤치마크를 해결하며, 결정 불가능(undecidable)한 것으로 알려진 문제인 매개변수화된 시스템(parameterized systems) 구축으로까지 확장됩니다. 명세 측면에서는, 평가를 위한 자연어 명세(natural-language specifications) 수동 작성 데이터셋을 도입함으로써 명세 작업을 시계열 논리(temporal logic)에서 자연어(natural language)로 전환하는 자동 형식화(autoformalization) 단계를 소개합니다. 우리는 형식 명세로부터 시작하는 것과 대등한 성능을 입증함으로써, Natural synthesis를 실행 가능한 엔드 투 엔드(end-to-end) 워크플로우로 확립합니다.