Natural Synthesis: Large Reasoning Models을 통해 Reactive Synthesis 도구 능가하기

요약

본 논문은 하드웨어 회로 자동 구축의 어려운 과제인 Reactive synthesis에 대한 새로운 접근 방식을 제시합니다. 알고리즘적으로는 대규모 추론 모델을 모델 체커와 결합한 신경-심볼릭(neuro-symbolic) 방법을 통해 Verilog 구현을 반복 수정하며, 결정 불가능한 매개변수화된 시스템까지 확장 가능함을 보여줍니다. 또한, 명세 작성의 어려움을 해결하기 위해 자연어 명세를 형식화하는 자동 형식화(autoformalization) 단계를 도입하여, 이를 엔드 투 엔드 워크플로우로 완성했습니다.

핵심 포인트

• Reactive synthesis는 논리적 명세로부터 하드웨어 회로를 자동으로 구축하는 어려운 과제이다.
• 알고리즘 측면에서 대규모 추론 모델을 활용한 신경-심볼릭 접근 방식을 통해 Reactive synthesis를 수행한다.
• 이 방법은 기존 최고 전용 도구보다 많은 벤치마크를 해결하며, 매개변수화된 시스템 구축까지 확장 가능하다.
• 자연어 명세(natural-language specifications)를 형식 논리(temporal logic)로 자동 변환하는 자동 형식화 단계를 도입했다.
• 이 모든 요소를 결합하여 자연어 명세부터 실행 가능한 하드웨어 구현까지의 엔드 투 엔드 워크플로우를 확립했다.