The ZigZag Loops
The Convergence Loop
- LLM-N normalises the natural language
- LLM-L+ATP encodes the natural language in logic
- LLM-NL says in natural language what si encoded in logic
- LLM-S judges if the previous and new natural language mean the same thing
- Repeats until LLM-S says they mean the same thing
- LLM-S judges if the final and original/normalised natural language mean the same thing
- Repeats until LLM-S says they mean the same thing
- Logic in between is accepted
The Logic Loop
- LLM-L+ATP encodes the natural language in logic
- ATP checks the syntax and types, repeats until passed
- LLM-NL says in natural language what is encoded in logic
- LLM-S judges if the provisional and original/normalized natural language mean the same thing
- Repeats until LLM-S says they mean the same thing