자동 형식화(Auto-Formalization)를 통한 강건한 비동기 계획 (Robust Asynchronous Planning)

LLM(Large Language Models)은 Planner(계획기)로서 행동 시퀀스를 직접 생성하거나, Formalizer(형식화기)로서 작업을 외부 솔버(solver)를 위한 도메인 특화 언어(domain specific language)로 변환함으로써 계획을 세울 수 있습니다. 대부분의 실제 작업은 비균일한 지속 시간, 동시성(concurrency), 실행 시간 제약 조건이 있는 비동기(asynchronous) 방식이지만, 기존의 벤치마크(benchmarks)는 이를 거의 다루지 못하고 있습니다. 우리는 이러한 비동기 계획 과제들을 단일 공식화(formulation) 아래 통합하고, 각각을 대규모로 다루는 최초의 세 가지 벤치마크를 소개합니다. 우리는 형식적 표현(formal representation)의 선택이 계획의 확장성(scaling)을 결정하는 주요 요인이라는 결론을 내렸습니다. 의존성 그래프(dependency graphs)가 5개에서 100개의 행동으로 증가함에 따라, Planner의 계획 정확도는 96%에서 5%로 급락하고, PDDL2.1 Formalizer는 13%에서 0%로 떨어지는 반면, CP-SAT Formalizer는 평균 94%를 유지하며 100개의 행동에서도 여전히 83%를 달성합니다. 충실도 진단(Faithfulness diagnostics) 결과, LLM이 술어(predicates), 효과(effects), 목표(goals)를 일관되게 유지해야 할 때, PDDL2.1의 술어 기반 계획 표현은 일반적인 제약 충족 프로그램(constraint satisfaction programs)에 비해 취약해지는 것으로 나타났습니다. 계획 제약 조건의 실행 시간 업데이트(Execution-time updates)는 성능을 더욱 급격히 저하시키지만(Planner 23.9%, PDDL2.1 0.7%, CP-SAT 46.1%), 이벤트로 유발된 제약 조건만 업데이트하는 상태 인식 복구 전략(state-aware repair strategy)을 사용하면 CP-SAT Formalizer의 성능을 84.5%까지 회복할 수 있습니다.