Towards Formalizing a Fragment of ChatGPT Prompts

We are working on the "Representation Capability" in our ChatGPT Organization Maturity Model.

Using formalization techniques, we can express the semantic structure of the ChatGPT prompts. Once the prompts got a formal structure, they can help analytics or can trigger logic.

The example prompts are from Daren Cox's medium post "ChatGPT prompt engineering, let's think step-by-step and other magic phrases," because his post, in my opinion, has good in-depth literature support (I think represents a community standard.)

Some example prompts I used in that post:

• Using these examples:?
• Classify the following film description:?
• “Let’s think step-by-step”
• “Thinking aloud”

The formalism methodology I chose was Formal Semantics in Modern Type Theories, because it is both modal-theoretic and proof-theoretic, meaning it is both powerful and practical: we can use Proof Assistant Coq to implement the semantic structure, and then convert to Functional Programming languages.

The keys to a successful formalization

• Do not bother with the completeness (that MTT formalism is for use, rather than for modeling).
• Utilizing the type system to encode semantic constraints (such as dependencies between parts)
• The final representation should resemble English (should minimize extra symbolic notations.)

In the attached code snippets, the final representation is

(Step_by_Step Think) (Using_these_examples?Classify (Following Film_Description))

ChatGPT can directly react to the above prompt segment.

Next Step

* Work on the coverage (covering more diversified prompt structures)

Takeaway

* Using Modern Type Theories, we can effectively model the natural language prompt structure.

* That formalism, compared to other ones, such as Montague Semantics, is a more practical one, and more computer-friendly.

Appendix

Definition CN:= Set.


Definition Prompt:=Set.


Parameters Agent : CN.
Parameter Entity: CN.
Parameter ChatGPT : Agent.


Parameter Examples: CN.




Parameter these_examples: Examples.
Parameter Using_something: Examples->(Entity->Prompt)->(Entity->Prompt).


Definition Using_these_examples:= Using_something these_examples.


Parameter Classify
? ?: Entity->Prompt.


Parameter This_One: Entity.


Parameter What_About_something: Entity->Prompt.


Definition What_About_This_One:= What_About_something This_One.




Parameter Film_Description: Entity.
Parameter Following: Entity->Entity.


Check (Following Film_Description).


Check Using_these_examples.


Check (Using_these_examples
?Classify (Following Film_Description)).


Parameter Think: Prompt->Prompt.


Parameter Step_by_Step: ( Prompt->Prompt)->( Prompt->Prompt).
Parameter Aloud:? ( Prompt->Prompt)->( Prompt->Prompt).


Check (Step_by_Step Think).


Check (Aloud Think).


Check (Step_by_Step Think) (Using_these_examples
?Classify (Following Film_Description)).