## Code Comparison: LLM vs. LLM + APOLLO ### Overview The image presents a side-by-side comparison of code generated by two systems: "LLM" (left) and "LLM + APOLLO" (right). Both systems appear to be using a formal verification or theorem proving environment, likely Coq, based on the syntax. The code snippets define a theorem `imo_1983_p6` and a related nlinarith proof. ### Components/Axes There are no axes or traditional chart components. The image consists of two distinct code blocks, each with a header indicating the system that generated it ("LLM" and "LLM + APOLLO"). Each code block contains the following elements: * `import` statements: `Mathlib` and `Aesop` * `set_option` statement: `maxHeartbeats 0` * `open` statement: `BigOperators Real Nat Topology Rat` * `theorem` definition: `imo_1983_p6` * `nlinarith` proof block: containing a series of constraints and operations. ### Detailed Analysis or Content Details **LLM (Left)** * **Imports:** `import Mathlib`, `import Aesop` * **Option:** `set_option maxHeartbeats 0` * **Open:** `open BigOperators Real Nat Topology Rat` * **Theorem:** `theorem imo_1983_p6_llm (a b c : R) (h₀ : 0 < a ∧ 0 < b ∧ 0 < c) (h₁ : c < a + b) (h₂ : b < a + c) (h₃ : a < b + c) : 0 ≤ a ^ 2 + b ^ 2 + c ^ 2 - 2 * c * (b - c) + c ^ 2 * a * (c - a) := by` * **nlinarith:** * `nlinarith [sq_nonneg (a - b), sq_nonneg (b - c), sq_nonneg (c - a), mul_pos ho.left h₀.right, mul_pos ho.left h₁.right, mul_pos h₁.right.left h₀.right.right]` **LLM + APOLLO (Right)** * **Imports:** `import Mathlib`, `import Aesop` * **Option:** `set_option maxHeartbeats 0` * **Open:** `open BigOperators Real Nat Topology Rat` * **Theorem:** `theorem imo_1983_p6_apollo (a b c : R) (h₀ : 0 < a ∧ 0 < b ∧ 0 < c) (h₁ : c < a + b) (h₂ : b < a + c) (h₃ : a < b + c) : 0 ≤ a ^ 2 + b ^ 2 + c ^ 2 - 2 * c * (b - c) + c ^ 2 * a * (c - a) := by` * **nlinarith:** * `nlinarith [sq_nonneg (a - b), sq_nonneg (b - c), sq_nonneg (c - a), mul_pos (sub_pos.mpr h₁) (sub_pos.mpr h₂), mul_pos (sub_pos.mpr h₂) (sub_pos.mpr h₃), mul_pos (sub_pos.mpr h₃) (sub_pos.mpr h₁)]` **Differences in nlinarith:** The key difference lies within the `nlinarith` block. The "LLM" version uses `mul_pos ho.left h₀.right`, `mul_pos ho.left h₁.right`, and `mul_pos h₁.right.left h₀.right.right`. The "LLM + APOLLO" version uses `mul_pos (sub_pos.mpr h₁) (sub_pos.mpr h₂)` and similar constructions involving `sub_pos.mpr`. This suggests that APOLLO is introducing a step to explicitly prove the positivity of the differences before multiplying, potentially leading to a more robust or complete proof. ### Key Observations The code is nearly identical between the two systems, except for the `nlinarith` block. The "LLM + APOLLO" version appears to be more verbose and explicit in its reasoning, using `sub_pos.mpr` to demonstrate the positivity of terms before applying `mul_pos`. This could indicate that APOLLO is adding a layer of proof automation or simplification. ### Interpretation The image demonstrates a comparison between a baseline LLM and an LLM augmented with APOLLO for formal verification. The theorem `imo_1983_p6` likely represents a mathematical inequality. The difference in the `nlinarith` blocks suggests that APOLLO is enhancing the LLM's ability to generate proofs by adding more explicit reasoning steps. The use of `sub_pos.mpr` indicates that APOLLO is actively verifying the positivity of terms, which is crucial for the correctness of the proof. This suggests that APOLLO is not simply generating code, but also contributing to the proof strategy itself. The `maxHeartbeats 0` setting suggests that the systems are configured to avoid timeouts during proof search. The fact that both systems produce valid code (at least syntactically) indicates that the LLM has a good understanding of the Coq syntax and semantics. The addition of APOLLO appears to refine the proof process, potentially making it more reliable and complete.