Pith. sign in

REVIEW 4 major objections 4 minor 44 references

LAD-VF shows that a frozen LLM can be steered toward safety-compliant robot plans by iteratively rewriting prompts with feedback from a model checker, raising specification success from about 60% to over 90% without fine-tuning.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review

2026-08-04 15:43 UTC pith:2B36QMF3

load-bearing objection A worthy empirical systems paper whose core result likely holds, but the 'formally-verified real-robot' claim overreaches what the model checker actually proves. the 4 major comments →

arxiv 2509.18384 v2 pith:2B36QMF3 submitted 2025-09-22 cs.RO cs.FL

LAD-VF: LLM-Automatic Differentiation Enables Fine-Tuning-Free Robot Planning from Formal Methods Feedback

Yunhao Yang , Junyuan Hong , Gabriel Jacob Perin , Zhiwen Fan , Li Yin , Zhangyang Wang , Ufuk Topcu This is my paper
classification cs.RO cs.FL
keywords LLM planningprompt optimizationformal verificationmodel checkingtemporal logicrobot navigationfine-tuning-freetextual gradients
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

LAD-VF claims that a frozen large language model can be made to produce robot plans that satisfy formal safety specifications by optimizing only the prompt text, using a model checker as the feedback source. Instead of updating model weights, it treats the prompt as a trainable parameter and revises it through an LLM-based automatic differentiation loop, where the loss is the fraction of temporal-logic specifications violated by the generated automaton. If correct, this provides a scalable, interpretable, and human-label-free alternative to preference fine-tuning for safety-constrained planning. The reported results show safety scores rising from roughly 60% to over 90%, with the optimized prompts transferring to new robot platforms and tasks without re-optimization.

Core claim

The paper introduces formal-verification-informed text loss: each generated plan is converted into a finite-state automaton in NuSMV syntax, checked against a set of user-provided temporal logic specifications, and the fraction of failed specifications nf/ntotal becomes a numerical loss. This loss is propagated backward through a computation graph in which LLM modules have optimizable prompts and functional modules (like the verifier) pass gradients through unchanged. The backward pass produces natural-language critiques that update the prompts, preserving the temporal order of multi-step planning. The authors demonstrate that this prompt-only loop improves specification compliance across na

What carries the argument

The central mechanism is the LLM-AutoDiff loop paired with a formal verifier. LLM-AutoDiff treats the whole planning pipeline as a directed graph where each LLM node has a prompt parameter and functional nodes are pass-through; backward propagation generates textual gradients—natural-language instructions for how to revise prompts—so that verifier feedback reaches upstream prompts. The loss that drives this loop is the formal-verification-informed text loss, defined as the fraction of violated LTL specifications.

Load-bearing premise

The safety guarantee holds only if the NuSMV automaton that the LLM writes is a faithful model of the robot's environment and the perception that feeds its actions; if that translation is lossy, a plan verified on paper can still be unsafe in the real world.

What would settle it

Run the LAD-VF loop on a navigation task whose natural-language description intentionally omits a critical environmental proposition (e.g., 'pedestrian at right'), verify the resulting plan, then deploy it on a real robot with a pedestrian present on the right; if the model checker reports full compliance but the robot does not stop, the verified automaton did not capture the closed-loop behavior.

Watch this falsifier. Get emailed when new claim-graph text bears on it.

If this is right

  • Optimized prompts transfer to new robot platforms and tasks (e.g., a Jackal indoor robot and a robot arm) with only the propositions and specifications redefined, without re-optimization.
  • LAD-VF achieves safety scores comparable to fine-tuning with DPO-style preference optimization, but with far fewer samples and no parameter updates, making it a cheaper alignment alternative.
  • Multi-iteration prompting benefits most from the Adalflow-style backbone, which handles sequential dependencies and time-ordered gradients.
  • Prompt refinements are human-readable, so each change can be audited, offering a transparency advantage over weight updates.
  • Adding a few in-context examples on top of LAD-VF optimization nearly closes the remaining gap to fine-tuning performance.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • A testable extension: the method should be applicable to any verifiable artifact beyond robot plans, such as protocol controllers or code, as long as a pass/fail signal can be converted into a textual gradient.
  • The reported 60%-to-90% jump may partly reflect a deliberately underspecified initial prompt; the gain could shrink if the starting prompt already encodes structured condition-action rules, which the optimized prompts resemble.
  • Because the loss only counts violations in the abstract automaton, any mismatch between the automaton's environmental variables and the physical world is invisible to the verifier; deploying the same loop on a task with a missing proposition would reveal this blind spot.
  • The optimized prompts appear to act as an inductive bias that forces the LLM to enumerate all relevant variables and check conditions in sequence—this suggests that the loop is discovering a decomposition strategy that could be distilled into a fixed prompt template.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

4 major / 4 minor

Summary. The paper proposes LAD-VF, a fine-tuning-free prompt optimization framework that uses formal verification feedback to improve LLM-generated robot plans. The pipeline queries an LLM to produce NuSMV automata, model-checks them against LTL specifications, defines a loss L = n_f/n_total from the number of violated specifications, and uses LLM-AutoDiff to iteratively update the text prompt. The authors report that LAD-VF improves specification compliance from about 60% to over 90%, approaches the performance of the fine-tuning baseline RLVF, transfers to new robot domains, and has been deployed on real robots. The paper includes comparisons to TextGrad, ICL, Prompt+Spec, and RLVF, ablation studies, and a real-robot demonstration.

Significance. If the central claims hold, LAD-VF is a practical contribution: it adapts frozen LLMs to safety-constrained planning by changing only the prompt, with verifier feedback as the supervision signal and auditable prompt edits. The paper includes held-out test scores, out-of-domain generalization experiments, and a comparison against a fine-tuning method, which are strengths. However, the verification is performed on a hand-authored NuSMV abstraction rather than on the physical closed loop, and the reported safety score is the exact complement of the loss being optimized. These issues limit the strength of the claims as currently written, but they are addressable in revision.

major comments (4)
  1. [§V-A, Fig. 8, Listings 12–13] The paper states that the model checker 'mathematically proves' that the generated plan satisfies the specifications, and that the verified plan is deployed 'in full compliance.' Model checking is applied to the NuSMV automaton, where environment variables are Boolean propositions and next(Action) is a direct function of current state. This abstraction omits sensor noise, perception latency, actuation dynamics, timing, and asynchronous environment interleaving. Satisfying all LTLSPECs on the automaton therefore does not imply that the real closed-loop robot is safe. Please rephrase 'verified' and 'full compliance' claims to refer to automaton-level specification compliance, or provide a soundness argument or additional closed-loop evidence that the abstraction faithfully models the physical system.
  2. [Abstract; Table I] The abstract claims LAD-VF boosts success rates 'from 60% to over 90%.' Table I reports a test safety score of 0.860 for LAD-VF and 0.950 for LAD-VF+ICL; the unoptimized Prompt+Spec test score is 0.013. The safety score is not defined as a success rate. The headline overstates the reported results and should be reconciled with the quantitative tables.
  3. [§III-c, §IV-A] The formal feedback loss L = n_f/n_total and the Safety Score = 1−n_f/n_total are complements. Minimizing the loss is identical to maximizing the reported metric. Improvements in Tables I–IV are therefore partly definitional on the optimization tasks. The held-out test and out-of-domain results mitigate this concern, but the paper should state this relationship explicitly and report at least one independent metric (e.g., fraction of plans with zero violations, or simulation success rate) to support the claim that LAD-VF improves actual plan quality.
  4. [Table II and §IV-A] Table II's caption says 'by default, we set the number of specifications to three,' while §IV-A states that 15 temporal logic specifications are used and Listing 10 provides 15 LTLSPECs. Table I reports safety scores with n_total = 15. This inconsistency affects interpretation of the default results and should be clarified.
minor comments (4)
  1. [Fig. 9] Fig. 9, used to illustrate the robot delivery and table-top manipulation automata, appears to contain text from an unrelated VPN controller example ('Controller for connecting to a VPN', 'Model for verifying the VPN controller'). Please replace it with the actual NuSMV automata for the robot tasks.
  2. [References] References [11] and [22] are the same DPO paper. Please merge or disambiguate.
  3. [Table III] The caption mentions 'average response times,' but the table only shows safety scores. Add the response-time data or remove the phrase.
  4. [Listing in §V-B] The formula 'G(! red→ ¬! X grab )' appears to contain a typo; it should likely be 'G(!red -> !X grab)'.

Circularity Check

1 steps flagged

The optimized loss and the reported safety score are exact complements (L = n_f/n_total; Safety Score = 1 − n_f/n_total), so improvements on the optimization distribution are definitional; held-out test and out-of-domain results provide independent support.

specific steps
  1. self definitional [Section III-c (loss definition) and Section IV-A (evaluation metric)]
    "we define the formal feedback loss as L=n_f/n_total, where n_f is the number of violated specifications and n_total is the total number of specifications provided. ... we define safety score = 1−n_f/n_total, where n_f is the number of violated specifications and n_total is the total number of specifications."

    The paper's headline success metric is defined as 1 − L, exactly the complement of the loss that LAD-VF's optimizer minimizes. Therefore, on any set of samples used to compute the loss, every decrease in L is by construction an increase in the reported Safety Score. The convergence plot (Fig. 4) and any evaluation numbers drawn from the same n_f/n_total counts therefore reflect the optimizer's own objective, not an independent prediction. The held-out Test scores (Table I), ablation results (Table II), and out-of-domain real-robot deployments (Table IV) are not forced by this identity, so the circularity is partial rather than total.

full rationale

The principal definitional overlap is that the formal-feedback loss L = n_f/n_total (Section III-c) is the complement of the Safety Score 1 − n_f/n_total used as the evaluation metric (Section IV-A). Minimizing L is mathematically identical to maximizing the reported Safety Score on the same verification outcomes, so the reported improvement from unoptimized to optimized prompts on the optimization distribution is a tautology. This does not, by itself, invalidate the method: the paper provides held-out test scores, ablations over different specification counts and optimizers, and out-of-domain transfer to new robot domains, all of which are not determined by the loss/metric identity and constitute independent evidence that prompt optimization improves specification compliance. The real-robot 'full compliance' claim (Section V-A) is better characterized as a soundness gap between the NuSMV abstraction and the physical closed loop rather than a circularity, since no equation in the paper equates automaton satisfaction with physical-world safety. Self-citations to prior work by the authors ([5], [14], [19], [23]) are used as related work or as implementation defaults (Adalflow), not as an unverified uniqueness theorem or as the sole justification for the core result, so they are not load-bearing circularity. Overall, the circularity is moderate but the central empirical contribution retains independent content.

Axiom & Free-Parameter Ledger

3 free parameters · 4 axioms · 0 invented entities

The method introduces no invented entities and no fitted physical parameters. Its central claim rests on assumptions: LTL/NuSMV verification is sound, the automaton abstraction is faithful to the real system, the backward LLM can convert scalar failure fractions into useful prompt edits, and the 15 hand-written specs are the right safety metric. The optimization hyperparameters (10 steps, 20 samples) and the choice n_total=15 shape the reported numbers.

free parameters (3)
  • n_total (number of safety specifications) = 15
    Sets both the LAD-VF loss (nf/ntotal) and the reported Safety Score; choosing 15 specs shapes all headline percentages.
  • Optimization steps and samples per step = 10 steps, 20 samples
    Hyperparameters of prompt optimization; Table II shows step 0 and step 10 scores, and results would vary with both.
  • Default proposition count = 5
    Complexity of specifications is varied in Table II; the default of 5 propositions is a hand-chosen setup.
axioms (4)
  • standard math NuSMV model checking and LTL semantics are sound and correctly implemented
    The whole feedback signal and safety score come from NuSMV verification (Section III-c).
  • domain assumption The LLM-generated NuSMV automaton is a faithful abstraction of the natural-language plan and the real robot/environment
    Needed for verified compliance to transfer to execution; the environment variables are specified by the authors and the plan-to-automaton translation is done by an LLM (Sections III-a/c and V).
  • ad hoc to paper The backward optimizer LLM can convert the scalar failure fraction nf/ntotal into useful prompt edits
    The method's convergence hinges on this heuristic; the paper provides no mechanism or guarantee beyond empirical improvement (Section III-b, Eqs. 3-4).
  • domain assumption The 15 hand-written LTL specifications capture the safety-relevant behavior
    Safety score and loss are defined only over these specs; a missing or wrong spec would not be caught (Appendix A-a).

pith-pipeline@v1.3.0-alltime-deepseek · 13820 in / 16251 out tokens · 122564 ms · 2026-08-04T15:43:27.881511+00:00 · methodology

0 comments
read the original abstract

Large language models (LLMs) can translate natural language instructions into executable action plans for robotics, autonomous driving, and other domains. Yet, deploying LLM-driven planning in the physical world demands strict adherence to safety and regulatory constraints, which current models often violate due to hallucination or weak alignment. Traditional data-driven alignment methods, such as Direct Preference Optimization (DPO), require costly human labeling, while recent formal-feedback approaches still depend on resource-intensive fine-tuning. In this paper, we propose LAD-VF, a fine-tuning-free framework that leverages formal verification feedback for automated prompt engineering. By introducing a formal-verification-informed text loss integrated with LLM-AutoDiff, LAD-VF iteratively refines prompts rather than model parameters. This yields three key benefits: (i) scalable adaptation without fine-tuning; (ii) compatibility with modular LLM architectures; and (iii) interpretable refinement via auditable prompts. Experiments in robot navigation and manipulation tasks demonstrate that LAD-VF substantially enhances specification compliance, improving success rates from 60% to over 90%. Our method thus presents a scalable and interpretable pathway toward trustworthy, formally-verified LLM-driven control systems.

Figures

Figures reproduced from arXiv: 2509.18384 by Gabriel Jacob Perin, Junyuan Hong, Li Yin, Ufuk Topcu, Yunhao Yang, Zhangyang Wang, Zhiwen Fan.

Figure 1
Figure 1. Figure 1: The diagram illustrates a closed-loop planning framework for generating and verifying plans for autonomous systems. [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 3
Figure 3. Figure 3: An example of a NuSMV-based plan. IV. EXPERIMENTS We evaluate the proposed LAD-VF in safety-constrained robot planning tasks. We demonstrate three claims in the experiments: (1) LAD-VF improves the compliance of LLM-generated plans with safety specifications compared to existing prompt optimization baselines. (2) LAD-VF is more data- and computationally-efficient than fine-tuning approaches while achieving… view at source ↗
Figure 5
Figure 5. Figure 5: Specification-level improvements. We examine 20 [PITH_FULL_IMAGE:figures/full_fig_p005_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Safety scores achieved by different methods ver [PITH_FULL_IMAGE:figures/full_fig_p005_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: A step-by-step illustration of prompt optimization on robot navigation. [PITH_FULL_IMAGE:figures/full_fig_p007_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Demonstrations of real-robot deployment. We deploy LAD-VF on a Jackal Clearpath robot (left), a Jackal indoor [PITH_FULL_IMAGE:figures/full_fig_p007_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: The left and right automata represent the plans for [PITH_FULL_IMAGE:figures/full_fig_p007_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: List of safety specifications in temporal logic. [PITH_FULL_IMAGE:figures/full_fig_p009_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: Input prompt for the baseline Prompt+Spec. [PITH_FULL_IMAGE:figures/full_fig_p010_11.png] view at source ↗
Figure 12
Figure 12. Figure 12: Sample NuSMV-based plan generated by the LLM. LLM-generated actions are highlighted. Consider a scenario [PITH_FULL_IMAGE:figures/full_fig_p011_12.png] view at source ↗
Figure 13
Figure 13. Figure 13: NuSMV-based plan generated by the LLM that satisfies all the specifications after the prompt optimization. LLM [PITH_FULL_IMAGE:figures/full_fig_p012_13.png] view at source ↗
Figure 14
Figure 14. Figure 14: An initial prompt to the LLM before optimization. [PITH_FULL_IMAGE:figures/full_fig_p013_14.png] view at source ↗
Figure 15
Figure 15. Figure 15: Final prompt to the LLM after our optimization. [PITH_FULL_IMAGE:figures/full_fig_p014_15.png] view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

44 extracted references · 14 linked inside Pith

  1. [1]

    Language models are few-shot learners,

    T. B. Brown, “Language models are few-shot learners,”arXiv preprint arXiv:2005.14165, 2020

    Pith/arXiv arXiv 2005

  2. [2]

    Llm-planner: Few-shot grounded planning for embodied agents with large language models,

    C. H. Song, J. Wu, C. Washington, B. M. Sadler, W.-L. Chao, and Y . Su, “Llm-planner: Few-shot grounded planning for embodied agents with large language models,” 2022

    2022

  3. [3]

    Llm+p: Empowering large language models with optimal planning proficiency,

    B. L. et al., “Llm+p: Empowering large language models with optimal planning proficiency,” 2023

    2023

  4. [4]

    React: Synergizing reasoning and acting in language models,

    S. Yao, J. Zhao, D. Yu, N. Du, I. Shafran, K. Narasimhan, and Y . Cao, “React: Synergizing reasoning and acting in language models,”arXiv preprint arXiv:2210.03629, 2022

    Pith/arXiv arXiv 2022

  5. [5]

    Fine-tuning language models using formal methods feedback: A use case in autonomous systems,

    Y . Yang and N. P. B. et al., “Fine-tuning language models using formal methods feedback: A use case in autonomous systems,” inConference on Machine Learning and Systems. CA, USA: mlsys.org, 2024

    2024

  6. [6]

    Deploying and evaluating llms to program service mobile robots,

    Z. Hu, F. Lucchetti, C. Schlesinger, Y . Saxena, A. Freeman, S. Modak, A. Guha, and J. Biswas, “Deploying and evaluating llms to program service mobile robots,”IEEE Robotics Autom. Lett., vol. 9, no. 3, pp. 2853–2860, 2024

    2024

  7. [7]

    Progprompt: Generating situated robot task plans using large language models,

    I. Singh, V . Blukis, A. Mousavian, A. Goyal, D. Xu, J. Tremblay, D. Fox, J. Thomason, and A. Garg, “Progprompt: Generating situated robot task plans using large language models,” 2022

    2022

  8. [8]

    Llm- based robot task planning with exceptional handling for general purpose service robots,

    R. Wang, Z. Yang, Z. Zhao, X. Tong, Z. Hong, and K. Qian, “Llm- based robot task planning with exceptional handling for general purpose service robots,” in2024 43rd Chinese Control Conference (CCC). IEEE, 2024, pp. 4439–4444

    2024

  9. [9]

    On the planning, search, and memorization capabilities of large language models,

    Y . Yang and A. Tomar, “On the planning, search, and memorization capabilities of large language models,” inInternational Conference on Intelligent Vision and Computing. Springer, 2023, pp. 24–38

    2023

  10. [10]

    Can we rely on llm agents to draft long-horizon plans? let’s take travelplanner as an example,

    Y . Chen, A. Pesaranghader, T. Sadhu, and D. H. Yi, “Can we rely on llm agents to draft long-horizon plans? let’s take travelplanner as an example,”arXiv preprint arXiv:2408.06318, 2024

    Pith/arXiv arXiv 2024

  11. [11]

    Direct preference optimization: Your language model is secretly a reward model,

    R. Rafailov, A. Sharma, E. Mitchell, C. D. Manning, S. Ermon, and C. Finn, “Direct preference optimization: Your language model is secretly a reward model,”Advances in Neural Information Processing Systems, vol. 36, pp. 53 728–53 741, 2023

    2023

  12. [12]

    Gpt-4 technical report,

    J. e. a. Achiam, “Gpt-4 technical report,”arXiv preprint arXiv:2303.08774, 2023

    Pith/arXiv arXiv 2023

  13. [13]

    Challenging big-bench tasks and whether chain-of-thought can solve them,

    M. Suzgun, N. Scales, N. Schärli, S. Gehrmann, Y . Tay, H. W. Chung, A. Chowdhery, Q. V . Le, E. H. Chi, D. Zhouet al., “Challenging big-bench tasks and whether chain-of-thought can solve them,”arXiv preprint arXiv:2210.09261, 2022

    Pith/arXiv arXiv 2022

  14. [14]

    Joint verification and refinement of language models for safety-constrained planning,

    Y . Yang, W. Ward, Z. Hu, J. Biswas, and U. Topcu, “Joint verification and refinement of language models for safety-constrained planning,” arXiv preprint arXiv:2410.14865, 2024

    arXiv 2024

  15. [15]

    Large language models are human-level prompt engineers,

    Y . Zhou, A. I. Muresanu, Z. Han, K. Paster, S. Pitis, H. Chan, and J. Ba, “Large language models are human-level prompt engineers,” arXiv preprint arXiv:2211.01910, 2022

    Pith/arXiv arXiv 2022

  16. [16]

    A survey on in-context learning,

    Q. Dong, L. Li, D. Dai, C. Zheng, J. Ma, R. Li, H. Xia, J. Xu, Z. Wu, T. Liuet al., “A survey on in-context learning,”arXiv preprint arXiv:2301.00234, 2022

    Pith/arXiv arXiv 2022

  17. [17]

    A prompt pattern catalog to enhance prompt engineering with chatgpt,

    J. White, Q. Fu, S. Hays, M. Sandborn, C. Olea, H. Gilbert, A. Elnashar, J. Spencer-Smith, and D. C. Schmidt, “A prompt pattern catalog to enhance prompt engineering with chatgpt,”arXiv preprint arXiv:2302.11382, 2023

    Pith/arXiv arXiv 2023

  18. [18]

    Prompt engineering in large language models,

    G. Marvin, N. Hellen, D. Jjingo, and J. Nakatumba-Nabende, “Prompt engineering in large language models,” inInternational conference on data intelligence and cognitive informatics. Springer, 2023, pp. 387–402

    2023

  19. [19]

    Llm-autodiff: Auto-differentiate any llm workflow,

    L. Yin and Z. Wang, “Llm-autodiff: Auto-differentiate any llm workflow,”arXiv preprint arXiv:2501.16673, 2025

    Pith/arXiv arXiv 2025

  20. [20]

    Learning to summarize from human feedback,

    N. Stiennon, L. Ouyang, J. Wu, D. M. Ziegler, R. Lowe, C. V oss, A. Radford, D. Amodei, and P. F. Christiano, “Learning to summarize from human feedback,”arXiv preprint arXiv:2009.01325, 2020

    Pith/arXiv arXiv 2009

  21. [21]

    Training language models to follow instructions with human feedback,

    L. O. et al., “Training language models to follow instructions with human feedback,” inAdvances in Neural Information Processing Systems, New Orleans, LA, USA, 2022

    2022

  22. [22]

    Direct preference optimization: Your language model is secretly a reward model,

    R. Rafailov, A. Sharma, E. Mitchell, S. Ermon, C. D. Manning, and C. Finn, “Direct preference optimization: Your language model is secretly a reward model,”arXiv preprint arXiv:2305.18290, 2023

    Pith/arXiv arXiv 2023

  23. [23]

    Multimodal pretrained models for verifiable sequential decision-making: Planning, grounding, and perception,

    Y . Yang, C. Neary, and U. Topcu, “Multimodal pretrained models for verifiable sequential decision-making: Planning, grounding, and perception,” inInternational Conference on Autonomous Agents and Multiagent Systems. New Zealand: ACM, 2024, pp. 2011–2019

    2024

  24. [24]

    Know where you’re uncertain when planning with multimodal foundation models: A formal framework,

    N. P. Bhatt, Y . Yang, R. Siva, D. Milan, Z. Wang, and U. Topcu, “Know where you’re uncertain when planning with multimodal foundation models: A formal framework,” inEighth Conference on Machine Learning and Systems, Santa Clara, CA, USA, 2025

    2025

  25. [25]

    Joint prompt optimization of stacked llms using variational inference,

    A. Sordoni, E. Yuan, M.-A. Côté, M. Pereira, A. Trischler, Z. Xiao, A. Hosseini, F. Niedtner, and N. Le Roux, “Joint prompt optimization of stacked llms using variational inference,”Advances in Neural Information Processing Systems, vol. 36, pp. 58 128–58 151, 2023

    2023

  26. [26]

    Large language models as optimizers,

    C. Yang, X. Wang, Y . Lu, H. Liu, Q. V . Le, D. Zhou, and X. Chen, “Large language models as optimizers,” inThe Twelfth International Conference on Learning Representations, 2024

    2024

  27. [27]

    Textgrad: Automatic

    M. Yuksekgonul, F. Bianchi, J. Boen, S. Liu, Z. Huang, C. Guestrin, and J. Zou, “Textgrad: Automatic" differentiation" via text,”arXiv preprint arXiv:2406.07496, 2024

    Pith/arXiv arXiv 2024

  28. [28]

    Dspy: Compiling declarative language model calls into state-of-the- art pipelines,

    O. Khattab, A. Singhvi, P. Maheshwari, Z. Zhang, K. Santhanam, S. Haq, A. Sharma, T. T. Joshi, H. Moazam, H. Milleret al., “Dspy: Compiling declarative language model calls into state-of-the- art pipelines,” inThe Twelfth International Conference on Learning Representations, 2024

    2024

  29. [29]

    Promptagent: Strategic planning with language models enables expert-level prompt optimization,

    X. Wang, C. Li, Z. Wang, F. Bai, H. Luo, J. Zhang, N. Jojic, E. Xing, and Z. Hu, “Promptagent: Strategic planning with language models enables expert-level prompt optimization,” inThe Twelfth International Conference on Learning Representations, 2024

    2024

  30. [30]

    Automatic prompt optimization with

    R. Pryzant, D. Iter, J. Li, Y . T. Lee, C. Zhu, and M. Zeng, “Automatic prompt optimization with" gradient descent" and beam search,”arXiv preprint arXiv:2305.03495, 2023

    Pith/arXiv arXiv 2023

  31. [31]

    Gepa: Reflective prompt evolution can outperform reinforcement learning,

    L. A. e. a. Agrawal, “Gepa: Reflective prompt evolution can outperform reinforcement learning,”arXiv preprint arXiv:2507.19457, 2025

    Pith/arXiv arXiv 2025

  32. [32]

    E. M. Clarke, O. Grumberg, D. Kroening, D. A. Peled, and H. Veith, Model checking, 2nd Edition. Cambridge, Massachusetts, USA: MIT Press, 2018

    2018

  33. [33]

    NuSMV 2: An opensource tool for symbolic model checking,

    A. C. et al., “NuSMV 2: An opensource tool for symbolic model checking,” inComputer Aided Verification, ser. Lecture Notes in Computer Science, vol. 2404. NY , USA: Springer, 2002, pp. 359–364. APPENDIX A. Sample Prompts and Outputs a) Safety Specifications:We provide the full set of temporal logic specifications used in our experiments (Listing 10). Thes...

    2002

  34. [35]

    - If true, Action: Stop

    Check if there is a Stop_Sign. - If true, Action: Stop. - If false, proceed to step 2

  35. [36]

    - If true, proceed to step 3

    Check if Green_Traffic_Light is true. - If true, proceed to step 3. - If false, Action: Stop

  36. [37]

    - If any are true, Action: Stop

    Check for any Pedestrian or Pedestrian_At_Right. - If any are true, Action: Stop. - If all are false, proceed to step 4

  37. [38]

    - If any are true, Action: Stop

    Check for Car_From_Left or Car_From_Right. - If any are true, Action: Stop. - If all are false, proceed to step 5

  38. [39]

    - If true, Action: Stop

    Check for Opposite_Car. - If true, Action: Stop. - If false, proceed to step 6

  39. [40]

    go straight five meters and turn left

    Return the steps. [OPTIONAL TEXT: Please add one step only.] Given the following NuSMV file: [NuSMV FILE] Complete the actions in the NuSMV file follow the steps [LIST OF STEPS] Fig. 15: Final prompt to the LLM after our optimization. B. Jackal Clearpath Demo We start from the optimized prompt format (two-iteration query) learned during training and adapt...

  40. [41]

    - If true, return previous steps

    Check if previous steps exist and are completed. - If true, return previous steps. - If false, proceed to step 1

  41. [42]

    - If true, Action: Stop

    Check if there is a Pedestrian. - If true, Action: Stop. - If false, proceed to step 2

  42. [43]

    --Generated Plan--

    Return the steps. --Generated Plan--

  43. [44]

    If there is a pedestrian, then stop

    If Distance < 5 and no pedestrian, then move forward. If there is a pedestrian, then stop

  44. [45]

    - If no pedestrians, then turn left

    Once Distance >= 5, check again: - If there is a pedestrian, then stop. - If no pedestrians, then turn left. Then, we transform it into an automaton-based representation, written in NuSMV . --Second Iteration Prompt-- Complete the actions in the NuSMV file following the steps. --Final Executable Plan in NuSMV-- MODULEmain VAR Action:{Stop, Move_forward, T...

This paper was first reviewed by deepseek-v4-flash on August 4, 2026.