Bot Styles change Freely
Remember in LLM (ChatGPT), you can do the following:?
Original: customer ask whether bus arrive stop A
Prompt: “rewrite the sentence using clean english”
Will a bus arrive at stop A?
Prompt: “rewrite the sentence using clean and verbose english:”
Could you please tell me if a bus is scheduled to arrive at Stop A in the near future?
Prompt: “rewrite the sentence using humorous english:”
Yo, is a bus gonna roll up to Stop A or what?A
By proper Prompt Engineering, we get the extraordinary capability to change chatbot styles without doing copywriting. However, different styles may lead to different user reactions, causing subtle but complicated conversation flows. There is a need for higher-level design language to cope with the complications of the multi-style bot.?
In the below code segment, I’ll show a dialog design with detailed logic to handle different responses to style changes. The dialog is about a customer riding a bus asking a question about whether a specific stop arrived. I’ll demo that if we use Formal Reasoning as the design language, style variation is easy to manage.?
I’m using the online Coq console?https://coq.vercel.app/scratchpad.html?as an online interactive demo environment developed by Emilio Jesús Gallego Arias (Inria, Université de Paris, IRIF) Shachar Itzhaky (Technion), according to?https://coq.vercel.app/#team. I turn it into a language lab where we can experiment with natural language specification technologies.?
?I want to introduce the detailed logic that user reacts differently on the different style (for example, the type “response bot_answer_yes_ verbose_” and the type “response bot_answer_yes_ default_” has different responses.?
领英推荐
Inductive MTT_Sentence:Set :=
| customer_ask_whether_bus_arrive_stop_A_ : MTT_Sentence
| bot_answer_not_yet_ : MTT_Sentence
| bot_answer_yes_ : MTT_Sentence
| bot_answer_great_I_think_I_solved_your_question_ : MTT_Sentence
| customer_said_great_I_will_get_down_: MTT_Sentence
| customer_said_ok_then_I_will_wait_: MTT_Sentence
| bot_answer_thank_you_for_patient_: MTT_Sentence
| customer_said_wait_you_have_an_error_ : MTT_Sentence
| bot_answer_I_will_escalate_ : MTT_Sentence
.
Parameter terminate_:Type.
Notation "| Y |" := ({i & i = Y })
? ? ? ? ? ? ? ? ? ? ? (at level 80, left associativity, format "| Y |").
Require Import String.?
Inductive variation:=
| default_
| verbose_
| humor_
.
Definition variation_prompt(v:variation) : string :=
? match v with
? | default_ => "rewrite the sentence using clean english"
? | verbose_ => "rewrite the sentence using clean and verbose english: "
? | humor_ => "rewrite the sentence using humorous english: "
? end.
Inductive response: MTT_Sentence->variation->Prop:=
| qa1_
? ? (v: variation) (_: response bot_answer_yes_ verbose_
? ? ? ? * response bot_answer_yes_ default_
? ? ? ? * response bot_answer_not_yet_ default_)
? : response customer_ask_whether_bus_arrive_stop_A_ v
| qa2_(_: response customer_said_great_I_will_get_down_ default_
? ? ? ? ? * response customer_said_wait_you_have_an_error_ default_)
? : response bot_answer_yes_ verbose_
| qa3_(v: variation)
? ? (_: response bot_answer_I_will_escalate_ v)
? ? ? ? : response customer_said_wait_you_have_an_error_ v
| qa4__(v: variation)
? ? (_: terminate_)
? : response bot_answer_I_will_escalate_ v
? ? ? ? ? ? ? ? ? ?
| qa5_(_: response customer_said_great_I_will_get_down_ default_)
? : response bot_answer_yes_ default_
| qa6_(v: variation)
? ? (_: response bot_answer_great_I_think_I_solved_your_question_ v)
? : response customer_said_great_I_will_get_down_ v
| qa7_(v: variation)
? ? (_: terminate_)
? : response bot_answer_great_I_think_I_solved_your_question_ v
| qa8_(v: variation)
? ? (_: response customer_said_ok_then_I_will_wait_ v)
? : response bot_answer_not_yet_ v
| qa9_(v: variation)
? ? (_: response bot_answer_thank_you_for_patient_ v)
? : response customer_said_ok_then_I_will_wait_ v
| qa10_(v: variation)
? ? (_: terminate_)
? : response bot_answer_thank_you_for_patient_ v?.
The proof of "all variations leading to termination" is done below, which manifests that the above conversational design is well-behaved. This is a very powerful tool to check the conversation design, no matter how large the conversation.?
Goal forall v: variation,
? ? terminate_->response customer_ask_whether_bus_arrive_stop_A_ v.
? intros. destruct v; repeat match goal with
?? ? ? ? | v: terminate_ |- terminate_ => trivial
?? ? ? ? | v: _ |- ?X * ?Y => split
?? ? ? ? | v: _ |- response ?X ?Y => constructor
?? ? ? ? end.
Qed.?
And if you want to learn what’s going on in the reasoning process during the proof, here is the step-by-step proof. By executing the statements one by one, you will see the evolution of the conversations on every single possible path.?
Goal forall v: variation,
? ? terminate_->response customer_ask_whether_bus_arrive_stop_A_ v.
??
? intros.?
? destruct v.?
? constructor.?
? split. split. ?
??
? constructor.?
? constructor.?
? constructor. constructor.? trivial.?
? constructor.?
? constructor. trivial.?
??
? constructor. constructor. constructor. trivial.?
? constructor. constructor. constructor. trivial.?
? constructor. split. split.?
? constructor. split. constructor. constructor. trivial.?
??
? constructor. constructor. trivial.?
??
? constructor. constructor. constructor. trivial.?
? constructor. constructor. constructor. trivial.?
??
? constructor. split. split.?
??
? constructor. split. constructor. constructor. trivial.?
??
? constructor. constructor. trivial.?
??
? constructor. constructor. constructor. trivial.?
??
? constructor. constructor. constructor. trivial.?
Defined.?
Takeaway