English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Tools annual

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Presents the access of premium content as premium feature

Premium Content

Global: Zendy Plus annual

Global: Zendy Free Plan

Generative large language models (LLMs) with instruct training such as GPT-4can follow human-provided instruction prompts and generate human-like responsesto these prompts. Apart from natural language responses, they have also beenfound to be effective at generating formal artifacts such as code, plans, andlogical specifications from natural language prompts. Despite their remarkablyimproved accuracy, these models are still known to produce factually incorrector contextually inappropriate results despite their syntactic coherence - aphenomenon often referred to as hallucination. This limitation makes itdifficult to use these models to synthesize formal artifacts that are used insafety-critical applications. Unlike tasks such as text summarization andquestion-answering, bugs in code, plan, and other formal artifacts produced byLLMs can be catastrophic. We posit that we can use the satisfiability modulotheory (SMT) solvers as deductive reasoning engines to analyze the generatedsolutions from the LLMs, produce counterexamples when the solutions areincorrect, and provide that feedback to the LLMs exploiting the dialogcapability of instruct-trained LLMs. This interaction between inductive LLMsand deductive SMT solvers can iteratively steer the LLM to generate the correctresponse. In our experiments, we use planning over the domain of blocks as oursynthesis task for evaluating our approach. We use GPT-4, GPT3.5 Turbo,Davinci, Curie, Babbage, and Ada as the LLMs and Z3 as the SMT solver. Ourmethod allows the user to communicate the planning problem in natural language;even the formulation of queries to SMT solvers is automatically generated fromnatural language. Thus, the proposed technique can enable non-expert users todescribe their problems in natural language, and the combination of LLMs andSMT solvers can produce provably correct solutions.

Neuro Symbolic Reasoning for Planning: Counterexample Guided Inductive Synthesis using Large Language Models and Satisfiability Solving