The ZigZag Loops
The Convergence Loop
- LLM-L+ATP encodes in logic what it thinks was meant by the 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
- Repeats until LLM-S says they mean the same
- LLM-S judges if the final English and the original English mean the same
- Repeats until LLM-S says they mean the same
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
