Integrating ChatGPT with Proof Assistant — State of Affairs
Abstract
Integrating ChatGPT with Proof Assistant, a tool for constructing mathematical proofs, will increase the logic, accuracy, and transparency of ChatGPT responses. In this post, we will talk about state of affairs for ChatGPT and Proof Assistant respectively. Finally, I will highlight the thought process for the upcoming concrete design combining ChatGPT and Proof Assistant.
ChatGPT — State of Affairs
ChatGPT was trained by a large army of labelers, leveraging the Reinforcement Learning on Large Language Model with an internet scale. Unlike conventional “new things”, ChatGPT challenges the standard practice we rely upon to build human knowledge. Now let’s “listen” to our greatest philosophers of all times.
Socrates. He would reject ChatGPT, complaining that “this box thinks it knows everything.” Socrates would systematic examine an answer’s premises, sources, and reasonings. The “true insight” has a clearly defined boundary of knowledge.
Plato. He would reject ChatGPT, complaining that “this thing is too mutable.” Plato demands rigorous reasoning because that is the path towards Plato’s “world of ideas,” a reality containing eternal and immutable “patterns.” ChatGPT answers, to the contrary, are random and inconsistent.
Aristotle. He would be impressed by ChatGPT because he considers it resembles humans’ innate capability of organizing sensory impressions into categories (*). However, ChatGPT falls short of Aristotle’s next demand: a wholistic categorized knowledge base.
For thousands of years, we attribute our human knowledge growth to the above philosophers’ methodologies. The ChatGPT answers, although look “good,” cause frictions for serious knowledge creation.
Proof Assistant — State of Affairs
A computer could do math theorem proof, and Proof Assistant was built on top of Curry-Howard correspondence, as early as 1969. Being consistent, well-defined, and capable of building complex structures, Proof Assistant is a “good student” to our founding philosophers.
However, it has its problems on the opposite end. While ChatGPT produces too much knowledge without sources of truths, Proof Assistant delivers too little knowledge that are true but with a hard-to-understand format. Therefore, it only applies to narrowed domains such as math and software verification.
Let us dive deep into a specific pattern to see why conventional Proof Assistant is not productive in broader domains such as natural language knowledge. In the current Proof Assistant, the variable declaration is in the form of x : X, where x is a variable name and X is its type. And usually, there is surrounding text to explain that structure. Like Dr. Leemon Baird’s excellent lecture on Formal Methods in Hedera, the blue comments are accompanied by every Lemma (essentially a type declaration x: X). An example screenshot
It is a well explained easy to read block. But let us think of ways to generalize outside its domain, probably not so easy. The main issue is, the explanatory text (in a blue background) will not stay consistent with their target math structure unless with the help of human proofreading. And moreover, the explanation text is not visible in proof. Below is an example proof state(unrelated to the previous example), which contains hard-to-read symbols.
Without fixing the productivity, Proof Assistant will not become relevant in general domains where ChatGPT is operating on.
Combining Proof Assistant and ChatGPT
Opportunities
The arrival of ChatGPT made it possible to create a new hybrid system combining AI and reasoning, producing “self-evident” knowledge that stands up to human scrutiny. Some potential usage of that new hybrid system:
- With that, we could build question-answering systems with precise citations of answer origin and as intelligent as ChatGPT.
- With that, we could write our creative stories with solid reasoning and let ChatGPT fill in with “substance.” There will no longer be cheating — human adds value to ChatGPT raw answers.
We believe that the above vision is realistic because Generative AI is flexible on the output target: we have seen responses from ChatGPT that have the appearance of sound knowledge, and we could as well have it produces knowledge that is “self-evident,” containing necessary reasoning components to facilitate a rule-based knowledge refinery.
Descartes’ Dream
That idea is inspired by a great philosopher in 1600s named Descartes. He established the “mathematical method” for philosophizing. He insisted that our true knowledge cannot be acquired unless we can clearly and distinctly represent it using mathematics; and a truth is determined by proving a theorem. Consequently, our thoughts, represented by math structures, can form a reality, one that is as equally valid as the “extension” material world.
Using ChatGPT to help generate that “mind reality” with mathematic notations and then using Proof Assistant to prove those, we can produce good knowledge. Such knowledge is acceptable by Descartes’s standards. And we have that great philosopher’s life-long work to manifest that, this methodology is useful on philosophies — the highest level of knowledge, and therefore it necessarily useful to the rest of the human knowledge.
After 400 years, we have much more math disciplines available for practical knowledge representation, than the time Descartes wrote his “Discourse of Method.”
- Logics (various kinds, such as propositional, intensional, etc.)
- Montague Semantics (modeling the meaning of a language)
- Generative Grammar (modeling grammar with a deep insight of human innate faculty of language)
- Domain Models such as List, Map, Set, etc. (Useful for modeling business processes.)
Tighten the integration between Proof Assistant and ChatGPT
A foundational system design is being carved out by Pingping Consultation. To integrate with ChatGPT, we need to add several APIs to make transformations between math structures and natural language texts seamless.
- We need to have a utility so that x : X can be generated by a ChatGPT prompt.
- Furthermore, if x has associated definition (or in another word, be proven), then we should have another utility to query ChatGPT to obtain an explanatory text for that definition.
- If “x : X” is brought into a proof context, then we should furthermore brought its explanatory text into the same context.
With the above functionalities, the math symbols can be translated to texts and texts can generate math symbols, so that we can leverage language to generate new math structure for reliable knowledge generation.
What’s next
Pingping Consultation will have a new post sharing the design of the new system that integrates ChatGPT to Proof Assistant.
Pingping Consultation, founded by Pingping XIU in January, 2023, is a non-profit for developing responsible AI technologies through a multi-disciplinary approach.
(*) This paper also said LLM learned abstractions https://arxiv.org/pdf/2301.06627.pdf
Credit: sincerely thanks to my friend Frank Kane, Founder of Sundog Software LLC, for proofreading the script.