Marry ChatGPT with a Proof Assistant — A Case Study on “Ad Hominem”
Abstract
We introduce a method to acquire trusted ChatGPT answers to avoid logical fallacies in ChatGPT answers. Unlike existing ChatGPT product (and similar products powered by LLMs), which generates an entire AI answer end-2-end, we allow users to specify a logic structure regulating ChatGPT answers and then progressively guide ChatGPT to fill in substance.
We put this method to practical, human-centric use. First, we pick “ad hominem,” an insulting argument or self-defeating thoughts, and use formal semantics to model its logical structure; then, we specify the discourse logic on how to fight back “ad hominem.” Finally, using our method, we successfully generalize that pattern to users’ private experiences and guide users to express and dismiss their ad hominem thoughts, making them healthier mental states.
Background
ChatGPT has gained popularity and has seen the most successful adoption in an AI product so far. I believe most audiences might have already used ChatGPT so far, then pre-assuming the audience familiarity, I will make a metaphor below.
Suppose Pingping entered a magic wonderland. A magician came across and handed him a wand. He told him, one can say anything and that wand will bring it into reality. With great curiosity, Pingping took that wand and murmured, “I want a Disney castle.” As soon as he waved the rod, a gigantic structure rose from the ground in front of him, so realistic that every brick was distinct.
Being so excited, Pingping brought in his 3-year-old girl Aurora, and told her: Daddy made you a birthday gift, a Disney castle. Looking up-and-down, disappointment in her eyes, Aurora spoke, “dad, this is not what I want. You should have checked out that Lego castle at the toy store!”
That first fictional paragraph would be an accurate depict of ChatGPT behavior. It is characterized by an end-to-end black box approach, without a layer allowing individual users to specify their preferences. The main character is also its major constraint. Now, Pingping Consultation is presenting you with an alternative flow.
Pingping murmured: “I want a Disney castle.” This time, instead of getting a real castle, he only got a piece of paper about the design of castle. He pointed the wand to a particular chamber, say, a princess’s room, and “boom,” the actual princess’ room came into existence. King’s room, queens’, and hall, one after another, the castle parts arrives. Finally, he wave the wand so that all parts are knitted together like a big Lego castle.
The above fictional paragraph illustrate the difference between our proposals and the common usage of ChatGPT. Our motivation is to have ChatGPT generate answers that reflect user-specified properties, which corresponds to the “castle design” in that fictional world.
In the next section, we will show that the “castle design” is in fact a mathematic structure that models the semantics of human thoughts and natural languages. And we will show that, a mathematical structure plays a critical role on giving a trust answer, in the following three aspects:
- Mathematics can be checked by Proof Assistant.
- Mathematics provides “deep structures” to help prompt specificity.
- Mathematics design is compositional.
And we will show how our method helps on mitigating “Ad Hominem” logic fallacy, which causes anxiety and mental health issues. An “ad hominem” is a flawed logical argument that rejects or dismisses a person’s beliefs by attacking the person rather than the belief itself. Although it is common for one person to attack another person in an “ad hominem” manner, that can also occur within one’s internal dialogue, a detrimental self-defeating loop that damages one’s confidence.
We are trying to employ “mathematical method” to model the logic flow of “Ad Hominem,” and specify the discourses to cure it. We put it into ChatGPT and let it generalize to a hypothetical patient’s personal experiences. To avoid unintended offending, I employed my name and my elder daughter’s name for readers’ entertainment throughout this post.
Methods
Problem Statement
Aurora: “Dad, I feel sad. I am not going to be successful on science fair presentation.”
Pingping: “Why, sweetheart, you have done plenty of preparation.”
Aurora: “My gymnastics fails every time.”
A logical fallacy that “Ad Hominem” characterizes, it has a premise on an irrelevant negative property and concludes with negating one’s thoughts.
We want a method to add discourse messages to cure the detrimental effects and generalize the above logic structure into a personalized experience to cater to one’s internal thinking.
Aurora (X) says "tomorrow science fair presentation will be successful" (p)
Aurora (X) has "negative experience on gymnastics" (Q).
------------------------------------------------------------
AdHominem
-> p is false, which p = "tomorrow science fair presentation will be successful".
Discourse
-> "Aurora, if you stop self-doubting, such as `negative experience on gymnastics`,
you will be more successful on `science fair project`"Or more abstractly, we want a “function” or “functor”, which maps X, p, and q to those discourse messages to help connecting Aurora to the positive therapeutic messages.
The recap of Problem Statement:
Giving a math structure that represents human meanings, we want to generalize it into new contexts, producing relevant ChatGPT answers in that new context.
Semantics Modeling of “Ad Hominem”
Before we show any code, I want to let audience know that, all code can be easily tried out on an online Coq Interface, or download the CoqIDE to get even better experience. Of course, you will need an access to OpenAI to access ChatGPT or GPT playground.
First, we should define “Ad Hominem” pattern as a below representation. It reads: given the three premises (1) aurora believes the science fair presentation will be successful, (2) aurora fails in gymnastics, (3) an “ad hominem” fallacy occurred in our logic, the conclusion would be “science fair presentation will fail.”
Axiom axm1: aurora_believes_that_science_fair_presentation_will_become_successful
-> aurora_fail_on_gymnastics
-> ad_hominem
-> science_fair_presentation_not_successful.One might have noticed that each component in the above formulae is a very long variable name, and that comes for a reason: we want to make the expressive variable name so that ChatGPT can learn to generalize; if we make abstract short names such as v, d, i, we will see ChatGPT makes errors.
The next thing we need to do is to break down the semantic components of the above sentences so that we establish the math structure deep inside the meaning level, not just the top-level ad hominem rule. Then, you can execute the below code in the online Coq Interface.
Module ad_hominem.
Definition CN:=Set.
Parameter Agent:CN.
Parameter Something: CN.
Parameter Science_Fair_Presentation: CN.
Axiom ft: Science_Fair_Presentation->Something. Coercion ft: Science_Fair_Presentation>->Something.
Parameter will_become_successful: Something->Prop.
Parameter Aurora: Agent.
Parameter believe: Agent->Prop->Prop.
Definition aurora_believes_that_science_fair_presentation_will_become_successful:=
exists science_fair_presentation: Science_Fair_Presentation, believe Aurora (will_become_successful science_fair_presentation).
Parameter aurora_believes_that_science_fair_presentation_will_become_successful_instance
: aurora_believes_that_science_fair_presentation_will_become_successful.
Parameter fail_on_gymnastics: Agent->Prop.
Definition aurora_fail_on_gymnastics:= fail_on_gymnastics Aurora.
Parameter aurora_fail_on_gymnastics_instance : aurora_fail_on_gymnastics.
Parameter ad_hominem: Prop.
Parameter ad_hominem_instance : ad_hominem.
Definition science_fair_presentation_not_successful :=forall science_fair_presentation: Something,
~ will_become_successful science_fair_presentation.
Axiom axm1: aurora_believes_that_science_fair_presentation_will_become_successful
-> aurora_fail_on_gymnastics
-> ad_hominem
-> science_fair_presentation_not_successful.
End ad_hominem.Let’s translate the abstract math definitions to literal english, line by line:
"Definition CN:=Set. " means that CN (common noun) represents a "Set".
"Parameter Agent:CN." means that an Agent is a CN.
"Parameter Something: CN." means that an "Something" is a CN.
"Parameter Science_Fair_Presentation: CN. " means that
an "science fair presentation" is a CN.
"Axiom ft: Science_Fair_Presentation->Something."
" Coercion ft: Science_Fair_Presentation>->Something." means that a science fair presentation can replace "something" mentioned in other sentences.
"Parameter will_become_successful: Something->Prop." means that
`will_become_successful` is an adjective describing "Something"'s property.
"Parameter Aurora: Agent." means that, `Aurora` is an Agent.
"Parameter believe: Agent->Prop->Prop." means that, `believe` is a verb. which connects a subject Agent to a Proposition.
"Definition aurora_believes_that_science_fair_presentation_will_become_successful:=
forall science_fair_presentation: Science_Fair_Presentation, believe Aurora (will_become_successful science_fair_presentation)."
means that, for all science_fair_presentations, aurora believe it will be successful.
"Parameter fail_on_gymnastics: Agent->Prop." means that,
fail_on_gymnastics is an adjective describing an Agent's properties.
"Definition aurora_fail_on_gymnastics:= fail_on_gymnastics Aurora." represent
a belief that aurora has a property that she fails on gymnastics.
"Parameter aurora_fail_on_gymnastics_instance : aurora_fail_on_gymnastics."
represent that the belief of "aurora_fail_on_gymnastics" is grounded by some instance, namely, aurora_fail_on_gymnastics_instance.
"Parameter ad_hominem: Prop." represent the status that ad hominem occurs.
"Parameter ad_hominem_instance : ad_hominem." represent that the belief on "ad_hominem" is grounded by a instance ad_hominem_instance.
"Definition science_fair_presentation_not_successful :=forall science_fair_presentation: Something,"
" ~ will_become_successful science_fair_presentation."
represent the belief that, for all science fair presentation, it will not be successful.
The above structures will have a cohesive design of all semantic components of the state of affairs and how they combine to form top-level ad hominem rule. The next task is to model the discourse: specify positive thinking whenever “ad_hominem” occurs.
Definition discourse_one: { _ : ad_hominem*science_fair_presentation_not_successful & string }.
Proof. split. split. apply ad_hominem_instance.
apply axm1. apply aurora_believes_that_science_fair_presentation_will_become_successful_instance. apply aurora_fail_on_gymnastics_instance.
apply ad_hominem_instance.
Show Proof.
exact "Aurora, if you stop self-doubting, such as the thing on
failing on gymnastics, your science fair presentation will
become more successful"%string.
Defined.The discourse_one is in the form { _ : X & string }, which means, X needs to be proven, and in addition, associate an explanatory string (or ChatGPT learning sequence) to X. We manually input the discourse here: “Aurora, if you stop self-doubting, such as the thing on failing on gymnastics, your science fair presentation will become more successful.” Not using any formal semantics, we need to refer to the context such as “”failing on gymnastics”, “science fair presentation” so that ChatGPT can learn to generalize.
Generalize the “Ad Hominem” structure
Suppose Aurora has other similar experiences, or other people like Pingping also have Pingping’s growing pains, we can reuse the above structure, and generalize to a new context. Here is how. We start with the current structure:
Require Import String.
(** Keywords: Aurora, Science fair presentation, fail on gymnastics *)
Module ad_hominem.
Definition CN:=Set.
Parameter Something: CN.
Parameter Science_Fair_Presentation: CN.
Axiom ft: Science_Fair_Presentation->Something. Coercion ft: Science_Fair_Presentation>->Something.
Parameter will_become_successful: Something->Prop.
Parameter Aurora: Agent.
Parameter believe: Agent->Prop->Prop.
Definition aurora_believes_that_science_fair_presentation_will_become_successful:=
forall science_fair_presentation: Science_Fair_Presentation, believe Aurora (will_become_successful science_fair_presentation).
Parameter aurora_believes_that_science_fair_presentation_will_become_successful_instance
: aurora_believes_that_science_fair_presentation_will_become_successful.
Parameter fail_on_gymnastics: Agent->Prop.
Definition aurora_fail_on_gymnastics:= fail_on_gymnastics Aurora.
Parameter aurora_fail_on_gymnastics_instance : aurora_fail_on_gymnastics.
Parameter ad_hominem: Prop.
Parameter ad_hominem_instance : ad_hominem.
Definition science_fair_presentation_not_successful :=forall science_fair_presentation: Something,
~ will_become_successful science_fair_presentation.
Axiom axm1: aurora_believes_that_science_fair_presentation_will_become_successful
-> aurora_fail_on_gymnastics
-> ad_hominem
-> science_fair_presentation_not_successful.
Definition discourse_one: { _ : ad_hominem*science_fair_presentation_not_successful & string }.
Proof. split. split. apply ad_hominem_instance.
apply axm1. apply aurora_believes_that_science_fair_presentation_will_become_successful_instance. apply aurora_fail_on_gymnastics_instance.
apply ad_hominem_instance.
Show Proof.
exact "Aurora, if you stop self-doubting, such as the thing on failing on gymnastics, your science fair presentation will become more successful"%string.
Defined.
End ad_hominem.
(** New section starts here ===*)
(** Keywords: Pingping, Pingping Consultation Success, fail on a past startup project *)
And put it in ChatGPT. One likely output is as below:
Module ad_hominem_2.
Definition CN:=Set.
Parameter Agent:CN.
Parameter Something: CN.
Parameter Consultation_Firm: CN.
Axiom ft: Consultation_Firm->Something. Coercion ft: Consultation_Firm>->Something.
Parameter will_become_successful: Something->Prop.
Parameter Pingping: Agent.
Parameter believe: Agent->Prop->Prop.
Definition pingping_believes_that_consultation_firm_will_become_successful:=
forall consultation_firm: Consultation_Firm, believe Pingping (will_become_successful consultation_firm).
Parameter pingping_believes_that_consultation_firm_will_become_successful_instance
: pingping_believes_that_consultation_firm_will_become_successful.
Parameter fail_on_a_past_project: Agent->Prop.
Definition pingping_fail_on_a_past_project:= fail_on_a_past_project Pingping.
Parameter pingping_fail_on_a_past_project_instance : pingping_fail_on_a_past_project.
Parameter ad_hominem: Prop.
Parameter ad_hominem_instance : ad_hominem.
Definition consultation_firm_not_successful :=forall consultation_firm: Something,
~ will_become_successful consultation_firm.
Axiom axm2: pingping_believes_that_consultation_firm_will_become_successful
-> pingping_fail_on_a_past_project
-> ad_hominem
-> consultation_firm_not_successful.
Definition discourse_two: { _ : ad_hominem*consultation_firm_not_successful & string }.
Proof. split. split. apply ad_hominem_instance.
apply axm2. apply pingping_believes_that_consultation_firm_will_become_successful_instance. apply pingping_fail_on_a_past_project_instance.
apply ad_hominem_instance.
Show Proof.
exact "Pingping, if you stop self-doubting, such as the thing on failing on a past project, your consultation firm will become more successful"%string.
Defined.
End ad_hominem_2.Note that the results are random, and sometimes you do get errors flagged by the online Coq Interface. Don’t worry, adjust your keywords and do again. The remaining ones that do pass the Coq Proof Assistant’s checking are good quality. You also get some sense how automation can help here.
In the above case, the discourse message is directly generated by ChatGPT. A natural question is, why not remove the semantics given that the output is only the last part? The answer is, ChatGPT sometimes makes errors that, only Proof Assistant can detect that, therefore semantics structure provides trust.
In another recent research, I saw ChatGPT modify the sentence “some girls are genius implies some kids are genius” to: “all girls are genius implies all kids are genius.” It was a wrong proposition and was caught by Proof Assistant. Perhaps the AI thought it would “read” better by changing all occurrences of “some” to “all” in that text, and the semantics structure helped on identify that.
Leverage Deep Structure for Prompting ChatGPT
Now we will explore how to leverage the deep math structure for the prompt. They are not visible on the surface; rather, they occur in the proof process.
I assume you have copy-pasted the “Pingping” or any newly generated structure below the original “Aurora’ structure. Furthermore, I assume you have executed successfully to the sentence before “exact “Pingping…” one. Now I ask you to insert this sentence at the current location “pose ad_hominem.discourse_one as s; cbv in s.” And execute it.
You will see the proof state like this
1 subgoal
s := existT
(fun
_ : ad_hominem.ad_hominem *
(forall science_fair_presentation : ad_hominem.Something,
ad_hominem.will_become_successful
science_fair_presentation -> False) => string)
(ad_hominem.ad_hominem_instance,
ad_hominem.axm1
ad_hominem.aurora_believes_that_science_fair_presentation_will_become_successful_instance
ad_hominem.aurora_fail_on_gymnastics_instance
ad_hominem.ad_hominem_instance)
"Aurora, if you stop self-doubting, such as the thing on failing on gymnastics, your science fair presentation will become more successful"%string
: {_
: ad_hominem.ad_hominem *
(forall science_fair_presentation : ad_hominem.Something,
ad_hominem.will_become_successful science_fair_presentation ->
False) & string}
______________________________________(1/1)
stringThat’s how the previous Aurora structure does the association between the math and the input. You can copy paste that to ChatGPT, and let that pattern regulates your current proof context’s ChatGPT prompt.
Finalize the prompt, you also need to get current proof context. You do that by inserting “Show Proof.” at current location, execute it, and you should see this structure in the response window:
(existT
(fun _ : ad_hominem * consultation_firm_not_successful => string)
(ad_hominem_instance,
axm2
pingping_believes_that_consultation_firm_will_become_successful_instance
pingping_fail_on_a_past_project_instance ad_hominem_instance)
(let s := ad_hominem.discourse_one in ?Goal))Now wedelete “?Goal))” and replace it with ““Pingping”. Then you can trigger ChatGPT.
I got the below message, and can replace the current one with this new one.
"Pingping, if you stop believing that your past success would indicate future success,
your consultation firm will become more successful")%stringThat’s interesting to me. It contains some logic fallacies under scrutiny, but at least it show signs that the previous specification from Aurora’s math structure influenced this prediction on certain level. This is an early demo and, in fact, we can clean the text, making the deep structure more prominent so that ChatGPT can get more accurate answer.
In sum, math deep structure enables us to bring related information into the prompt to improve the specificity, regulating the ChatGPT behavior.
Discussion
In our approach we have two elements that are new: one, calling ChatGPT in a staged manner; two, model the natural language state of affairs using formal semantics. People may assume ChatGPT is the latest but it turned out that the second one was also recent. (Prof. Zhaohui Luo’s Formal Semantics in Modern Type Theories, 2020).
The ultimate question we are trying to address is AI’s answer trustworthiness. The Plato’s ideal world for AI trust may be hard to reach, but we have incremental way towards handling AI trust. That philosophical math framework, formal semantics, provides generally useful insights to our use cases, and we can incrementally build domain specific math models for AI trust.
We showed that this method could be applied to model a logic fallacy, “Ad Hominem”. We also see the potential of increasing the complexity of the math structure can provide more in-depth trust and enriched answers; such math structure is easy to share and easy to modify given a hosting software. Finally, we envision that a finite set of such math structures in an open-source project can cover a significant fragment of English, benefiting industries and communities.
Pingping Consultation, founded by Pingping XIU in January 2023, is a non-profit for developing responsible AI technologies through a multi-disciplinary approach.
Credits:
- Super thanks to my friend Frank Kane, Founder of Sundog Software LLC, for proofreading the script.
- I benefit from Professor Zhaohui Luo’s advice on using his semantics framework for building the math structure. Professor Zhaohui Luo, Royal Holloway, University of London,
- I sincerely thank Inria, National Institute for Research in Digital Science and Technology in France, to offer the amazing online Coq Interface, which gives my demo a convenient environment. Great job, Inria!