Pith. sign in

REVIEW 4 major objections 4 minor 44 references

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

T0 review · 4 major / 4 minor · reviewed 2026-08-04 · deepseek-v4-flash

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

Pith's one-line read 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.

desk verdict A worthy empirical systems paper whose core result likely holds, but the 'formally-verified real-robot' claim overreaches what the model checker actually proves. read the letter →

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

Yunhao Yang , Junyuan Hong , Gabriel Jacob Perin , Zhiwen Fan , Li Yin , Zhangyang Wang , Ufuk Topcu This is my paper
classification cs.ROcs.FL
keywords LLMplanningpromptoptimizationformalverificationmodelcheckingtemporallogicrobotnavigationfine-tuning-freetextualgradients
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

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.

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.

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

Extended reading notes

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

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.

Editorial extensions

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.

Reading between the lines

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.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, 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 · score 3.0 of 10

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.

  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.

Assumptions & free parameters 3 free parameters · 4 assumptions · 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.
assumptions (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).

how reviews work

0 comments
Cite this review

Pith. "Pith review of LAD-VF: LLM-Automatic Differentiation Enables Fine-Tuning-Free Robot Planning from Formal Methods Feedback." pith.science (2026). https://pith.science/paper/2B36QMF3

@misc{pith2026250918384,
  author       = {Pith},
  title        = {Pith review of: LAD-VF: LLM-Automatic Differentiation Enables Fine-Tuning-Free Robot Planning from Formal Methods Feedback},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/2B36QMF3}},
  note         = {Machine review of arXiv:2509.18384}
}
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 the authors.

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. 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 the same … view at source ↗
Figure 5
Figure 5. Specification-level improvements. We examine 20 [PITH_FULL_IMAGE:figures/full_fig_p005_5.png] view at source ↗
Figures from the paper (10 more)
Figure 6
Figure 6. Figure 6: Safety scores achieved by different methods ver [PITH_FULL_IMAGE:figures/full_fig_p005_6.png]
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]
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]
Figure 9
Figure 9. Figure 9: The left and right automata represent the plans for [PITH_FULL_IMAGE:figures/full_fig_p007_9.png]
Figure 10
Figure 10. Figure 10: List of safety specifications in temporal logic. [PITH_FULL_IMAGE:figures/full_fig_p009_10.png]
Figure 11
Figure 11. Figure 11: Input prompt for the baseline Prompt+Spec. [PITH_FULL_IMAGE:figures/full_fig_p010_11.png]
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]
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]
Figure 14
Figure 14. Figure 14: An initial prompt to the LLM before optimization. [PITH_FULL_IMAGE:figures/full_fig_p013_14.png]
Figure 15
Figure 15. Figure 15: Final prompt to the LLM after our optimization. [PITH_FULL_IMAGE:figures/full_fig_p014_15.png]

Discussion (0). Sign in to comment.

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

    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

    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

Show all 44 references
  1. [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

  2. [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

    2024 arXiv

  3. [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

  4. [12]

    Gpt-4 technical report,

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

    2023 arXiv

  5. [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

    2022 arXiv

  6. [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

    2024

  7. [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

    2022 arXiv

  8. [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

    2022 arXiv

  9. [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

    2023 arXiv

  10. [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

  11. [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

    2025 arXiv

  12. [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

    2009 arXiv

  13. [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

  14. [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

    2023 arXiv

  15. [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

  16. [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

  17. [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

  18. [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

  19. [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

    2024 arXiv

  20. [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

  21. [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

  22. [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

    2023 arXiv

  23. [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

    2025 arXiv

  24. [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

  25. [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...

    2002

  26. [35]

    - If true, Action: Stop

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

  27. [36]

    - If true, proceed to step 3

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

  28. [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

  29. [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

  30. [39]

    - If true, Action: Stop

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

  31. [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...

  32. [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

  33. [42]

    - If true, Action: Stop

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

  34. [43]

    --Generated Plan--

    Return the steps. --Generated Plan--

  35. [44]

    If there is a pedestrian, then stop

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

  36. [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....

Pith tools

Reviewed August 4, 2026 · model on record in the stance chip above.