paper-with-me

홈 › Papers

Robust Asynchronous Planning via Auto-Formalization

2026-05-31 · Jiayi Zhang, Jianing Yin, Ben Zhou, Li Zhang arxiv

LLMs can plan by either generating action sequences directly as a Planner or translating tasks into domain specific language for an external solver as a Formalizer. While most real-world tasks are asynchronous with non-uniform durations, concurrency, and execution-time constraints, existing benchmarks hardly cover them. We unify these asynchronous planning challenges under a single formulation and introduce the first three benchmarks that address each at scale. We conclude that the choice of formal representation primarily determines whether planning scales: as dependency graphs grow from 5 to 100 actions, Planner collapses from 96% to 5% plan accuracy and PDDL2.1 Formalizer from 13% to 0%, while CP-SAT Formalizer averages 94% and still achieves 83% at 100 actions. Faithfulness diagnostics show that PDDL2.1's predicate-based planning representation becomes brittle compared to general constraint satisfaction programs, when LLMs must keep predicates, effects, and goals consistent. Execution-time updates of planning constraints further degrade performance sharply (Planner 23.9%, PDDL2.1 0.7%, CP-SAT 46.1%), but a state-aware repair strategy that updates only event-induced constraints recovers CP-SAT Formalizer to 84.5%.

📄 PDF Abstract BibTeX arXiv:2606.00981

Code (0)

등록된 구현이 없습니다.

Similar Papers 제목 키워드 기반

Towards a Common Framework for Autoformalization

2025-09-11 · Agnieszka Mensfelt, David Tena Cucala, Santiago Franco, Angeliki Koutsoukou-Argyraki 외 arxiv

Autoformalization has emerged as a term referring to the automation of formalization - specifically, the formalization of mathematics using interactive theorem provers (proof assistants). Its rapid development has been d…

Theory-Scale Auto-Formalization of Logics for Computer Science

2026-06-25 · Yuming Feng, Frederick Pu, One An, Osbert Bastani 외 arxiv

Auto-formalization is critical for scalable formal verification, but existing progress largely focuses on isolated statements, while theory-scale auto-formalization, which coherently translates hundreds of interdependent…

Agent Hunt: Bounty Based Collaborative Autoformalization With LLM Agents

2026-03-06 · Chad E. Brown, Cezary Kaliszyk, Josef Urban arxiv

We describe an experiment in large-scale autoformalization of algebraic topology in an Interactive Theorem Proving (ITP) environment, where the workload is distributed among multiple LLM-based coding agents. Rather than …

Individual Planning in Infinite-Horizon Multiagent Settings: Inference, Structure and Scalability

2015-12-01 · NeurIPS 2015 12 · Xia Qu, Prashant Doshi

This paper provides the first formalization of self-interested planning in multiagent settings using expectation-maximization (EM). Our formalization in the context of infinite-horizon and finitely-nest…

Hypothesis-Disciplined Multi-Agent Automated Formalization of Asymptotic Statistical Theory

2026-06-03 · Tingzhou Wei, Zeyu Zheng, Ethan X. Fang, Junwei Lu arxiv

Asymptotic statistical theory is a challenging domain for AI-assisted formalization: its central results mix convergence statements, asymptotic expansions, functional analysis, and regularity conditions that have a large…