paper-with-me

홈 › Papers

Language Model as Planner and Formalizer under Constraints

2025-10-07 · Cassie Huang, Stuti Mohan, Ziyi Yang, Stefanie Tellex, Li Zhang arxiv

LLMs have been widely used in planning, either as planners to generate action sequences end-to-end, or as formalizers to represent the planning domain and problem in a formal language that can derive plans deterministically. However, both lines of work rely on standard benchmarks that include only generic and simplistic environmental specifications, leading to potential overestimation of the planning ability of LLMs and safety concerns in downstream tasks. We bridge this gap by augmenting widely used planning benchmarks with manually annotated, fine-grained, and rich natural language constraints spanning four formally defined categories. Over 4 state-of-the-art reasoning LLMs, 4 formal languages, and 4 datasets, we show that the introduction of one-sentence constraints consistently halves performance, indicating current LLMs' lack of robustness and an avenue for future research.

📄 PDF Abstract BibTeX arXiv:2510.05486

Code (0)

등록된 구현이 없습니다.

Similar 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-u…

MMFormalizer: Multimodal Autoformalization in the Wild

2026-01-06 · Jing Xiong, Qi Han, Yunta Hsieh, Hui Shen 외 arxiv

Autoformalization, which translates natural language mathematics into formal statements to enable machine reasoning, faces fundamental challenges in the wild due to the multimodal nature of the physical world, where phys…

CktFormalizer: Autoformalization of Natural Language into Circuit Representations

2026-05-08 · Jing Xiong, Qi Han, Chenchen Ding, He Xiao 외 arxiv

LLMs can generate hardware descriptions from natural language specifications, but the resulting Verilog often contains width mismatches, combinational loops, and incomplete case logic that pass syntax checks yet fail in …

Risk-Controlled Lean-as-Judge for Natural-Language Mathematical Reasoning

2026-05-27 · Pauline Bourigault, Xiaotong Ji, Matthieu Zimmer, Rasul Tutunov 외 arxiv

Lean is increasingly used to judge natural-language mathematical answers, but its signal is partial: many answers never formalize, and a failed proof may reflect an ill-typed statement or a missing library fact, not a wr…

Mathematical Reasoning

Language Models as Higher-Order Planning Formalizers

2026-03-25 · Owen Jiang, Cassie Huang, Ashish Sabharwal, Li Zhang arxiv

Recent work provides overwhelming evidence that LLMs, even those trained to scale their reasoning trace, quickly deteriorate at planning as problems become more complex. LLM-as-Formalizers aim to address this by employin…