The ZigZag Loops
The Convergence Loop
- LLM-N normalises the English
- LLM-L+ATP encodes in logic what was said in English
- LLM-NL says in English what it encoded in logic
- LLM-S judges if the last English and the new English mean the same thing
- Repeats until LLM-S says they mean the same
- LLM-S judges if the final English and the normalised English mean the same thing
- Repeats until LLM-S says they mean the same thing
- ATP system is run on the final logic
The Logic Loop
- LLM-L+ATP encodes in logic what it thinks was meant by the English
- ATP checks the syntax and types
- LLM-NL says in English what it encoded in logic
- LLM-S judges if the English and the original English mean the same
- Repeats until ATP success and LLM-S says they mean the same
LLM Verification
- LLM-N replies to the natural language in English
- LLM-NL converts the ATP proof to English
- LLM-S compares the two results
- This is a step towards
ATP using LLM solutions
