## Diagram: Our Proposed Apollo Pipeline
### Overview
This image is a system architecture diagram illustrating a closed-loop, iterative process for automated theorem proving or code verification. It details the interaction between a Large Language Model (LLM), a specialized "Apollo Proof Repair Agent," and a "Lean Server" environment. The system is designed to generate proofs, test them, extract errors, and iteratively repair them up to a specified number of attempts.
### Components and Spatial Grounding
The diagram is divided into three primary horizontal regions, enclosed within a global feedback loop.
**1. Global Loop (Outer Boundary)**
* **Position:** Surrounds the entire diagram.
* **Visuals:** A thick black line with directional arrows indicating a clockwise flow.
* **Label:** A grey box at the top center reads: `repeat up to r times`.
**2. Left Region: Generation**
* **Component:** `LLM`
* **Visuals:** A light blue box containing an icon of a brain superimposed on a computer microchip. A smaller blue tab at the top reads `LLM`.
**3. Center Region: Processing & Repair**
* **Component:** `Apollo Proof Repair Agent`
* **Visuals:** Enclosed in a dashed black bounding box. A yellow tab at the top reads `Apollo Proof Repair Agent`.
* **Sub-components (Inside the dashed box):**
* **Top (Main Agent):** A large yellow box containing two icons: a hand holding a wrench (symbolizing repair) and a computer monitor displaying lines of code `</>`.
* **Bottom Right:** A peach-colored box labeled `Subproof Extractor` containing an icon of a gear, a warning triangle, and a wrench.
* **Bottom Left:** A brown box labeled `Auto Solver` containing an icon of a tic-tac-toe board with a winning line drawn through the 'O's.
**4. Right Region: Verification & Control**
* **Component:** `Lean Server`
* **Visuals:** A white box with a grey tab at the top reading `Lean Server`. Inside the box is a stylized, geometric line-art spelling of the word `LEAN`.
* **Component:** Loop Control Interface
* **Position:** Bottom right, situated below the Lean Server.
* **Visuals:** A stylized dark computer window/terminal. It contains two prominent buttons:
* Left button: Green with a checkmark, labeled `exit loop`.
* Right button: Red with an 'X', labeled `continue`.
### Detailed Flow Analysis (Content Details)
The flow of information is denoted by colored arrows. Blue arrows generally indicate forward progression or outputs, while red arrows indicate feedback, errors, or return requests.
**Forward Flow (Blue Arrows):**
1. **LLM to Apollo Agent:** A blue arrow points right from the LLM to the yellow box of the Apollo Proof Repair Agent.
* **Label:** `proof attempt(s)`
2. **Apollo Agent to Lean Server:** A blue arrow points right from the yellow box of the Apollo Proof Repair Agent to the Lean Server. (No text label).
3. **Lean Server to Loop Control:** A blue arrow points down and left from the Lean Server to the Loop Control Interface.
**Feedback/Return Flow (Red Arrows):**
1. **Lean Server to Apollo Agent:** A red arrow points left from the Lean Server back to the yellow box of the Apollo Proof Repair Agent.
* **Label:** (Stacked text)
`proof state`
`compilation errors`
`syntax errors`
2. **Internal Apollo Agent Flow:**
* A red arrow points down from the yellow main box to the `Subproof Extractor`.
* A red arrow points left from the `Subproof Extractor` to the `Auto Solver`.
* A red arrow points up from the `Auto Solver` back to the yellow main box.
3. **Apollo Agent to LLM:** A red arrow points left from the yellow box of the Apollo Proof Repair Agent back to the LLM.
* **Label:** `sub-problem(s) to prove`
4. **Loop Control to Lean Server:** A red arrow points up and left from the Loop Control Interface back to the Lean Server.
### Key Observations
* **Color-Coded Semantics:** The diagram strictly adheres to a color-coding scheme for its data flow. Blue represents the generation and submission of attempts, while red represents the extraction of errors, breakdown of problems, and feedback loops.
* **Internal vs. External Loops:** There are multiple loops occurring. An internal loop exists within the Apollo Agent itself (Agent -> Extractor -> Solver -> Agent). A secondary loop exists between the Apollo Agent and the Lean Server. The primary global loop encompasses the LLM and is governed by the `repeat up to r times` constraint.
* **Termination Conditions:** The loop control interface at the bottom right dictates the end of the process. A successful proof (green check) triggers `exit loop`, while a failure (red X) triggers `continue`, pushing the process back through the global loop (provided the attempt count is less than *r*).
### Interpretation
This diagram outlines a sophisticated, AI-driven automated theorem proving or code synthesis pipeline, specifically tailored for the Lean theorem prover.
The process begins with an LLM generating initial `proof attempt(s)`. Instead of sending these directly to the Lean Server, they pass through the "Apollo Proof Repair Agent." This agent acts as an intermediary and refinement tool. It sends the proof to the Lean Server, which acts as the ground-truth verifier.
If the Lean Server rejects the proof, it returns highly specific feedback (`proof state`, `compilation errors`, `syntax errors`). The Apollo Agent receives this feedback. If the error is complex, the Apollo Agent utilizes its internal tools: the `Subproof Extractor` isolates the specific failing part of the proof, and the `Auto Solver` attempts to resolve it algorithmically.
If the Apollo Agent cannot fix the proof internally, it translates the specific failure into `sub-problem(s) to prove` and sends this refined prompt back to the LLM. This prevents the LLM from having to regenerate the entire proof from scratch, focusing its computational power only on the broken segments.
This entire cycle is bounded by a maximum retry limit (*r* times) to prevent infinite loops, ensuring computational efficiency. The system demonstrates a "neuro-symbolic" approach, combining the generative power of neural networks (LLM) with the strict, rule-based logic of symbolic solvers (Lean Server and Auto Solver).
