Fine-tune ChatGPT : Turn Conversations into Theorem Proving

I am talking about Enterprise AI. Although ChatGPT excelled in enlightening consumers to explore the “Wild West,” enterprises built “trans-continent railways” that will transform the landscape. The primary task - fine-tuning the landscape, and building structures that ship business values.?

To use minimal editorial/admin/ISV resources to carry the maximal fine-tuning impact, we need to configure minimally and see maximal throughput. What is needed? A foundational framework. Training data synthesis and random data generation start with a foundational framework that can specify business needs and turn that into data.?

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, using Modern Type Theory, a branch of Computational Linguistics that models Natural Language using Proof Assistants.?

Demo goal: to showcase a small dialog that can be automatically synthesized through question-answer pairs that can be independently specified. The process will demonstrate how a large-scale dataset can be built with a termination guarantee.?

• Step 1. Create a scratch pad in?https://coq.vercel.app/scratchpad.html
• Step 2. Copy and paste conversation logic

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
.


Parameter terminate_:Type.




Inductive response: MTT_Sentence->Prop:=
| qa1_
? ? (_: response bot_answer_yes_ * response bot_answer_not_yet_)
? : response customer_ask_whether_bus_arrive_stop_A_


| qa2_(_: response customer_said_great_I_will_get_down_)
? : response bot_answer_yes_
? ??
| qa3_
? ? (_: response bot_answer_great_I_think_I_solved_your_question_)
? : response customer_said_great_I_will_get_down_


| qa4_
? ? (_: terminate_)
? : response bot_answer_great_I_think_I_solved_your_question_


| qa5_
? ? (_: response customer_said_ok_then_I_will_wait_)
? : response bot_answer_not_yet_


| qa6_
? ? (_: response bot_answer_thank_you_for_patient_)
? : response customer_said_ok_then_I_will_wait_


| qa7_
? ? (_: terminate_)
? : response bot_answer_thank_you_for_patient_
.

?        

• Step 3. Theorem proving: prove that the termination is encountered by all possible responses to the initial utterance : customer_ask_whether_bus_arrive_stop_A_

Goal terminate_->response customer_ask_whether_bus_arrive_stop_A_
? intros.?
??
? constructor.?
? split.?
??
? constructor.?
? constructor.?
? constructor. trivial.?
? constructor.?
? constructor.?
? constructor. trivial.?
Defined.?

.        

Copy and paste the code in the left-hand side window, and use the DOWN ARROW in the right-hand side window to execute the code one by one. You will see the evolution of the interactive theorem proving that proved the goal.

Takeaway

GPT fine-tuning is a large rule set problem: the unique number of question-answer pairs may grow immensely and they need to work together towards a cohesive system.

Automated theorem proving is a powerful tool for managing large rule sets and this post shows the prospect of managing more complex question-answer sets from larger dialog systems.