# Analysis plan (pre-registered before any run on `test`) Written 2026-11-03, during Phase 8 Part A, **before any configuration was run on the `test` split**. It fixes the metrics, tests and handling rules so that the analysis does not depend on the results. Any later change must be recorded at the end of this file with its date and reason, and reported in the paper as a deviation. Notation and equations refer to the report (`docs/report/Proyecto_Inteligencia.pdf`, Section IV-A). ## 1. Data and design - **Problems:** `data/eval.jsonl`, split `test`: 30 problems, stratified on the 3 × 3 grid (difficulty easy/medium/hard × area algebra/number theory/combinatorics, with the documented reallocation of Phase 7). The split was fixed with seed 2026 before any prompt tuning. - **Configurations:** C1–C5 (Section IV-A8), all on the same LangGraph graph, profile `experiment` (`deepseek-flash`, `config/models.yaml`), seed 2026, with the configuration frozen by the team's commit at the end of Part A (its hash is recorded in each `run_config.json`). - **Run order on `test`:** C5, C3, C4, C2, C1 (team decision 2026-10-31). - **One run per (configuration, problem).** No configuration is re-run on `test` to obtain a better result. The only exception is the `provider_error` rule of Section 5. - **Paired design:** every configuration sees the same 30 problems, so comparisons between configurations are paired by problem. - The LLM response cache stays on. Identical requests across configurations (e.g. the first attempt of C4 and C5) are answered from the cache; this keeps the paired comparison tighter and is stated in the paper. Costs are compared with the **nominal** cost (`cost_usd_nominal`: cache hits priced as fresh calls) so that run order does not favour later configurations. ## 2. Primary outcome - **Verified success** of configuration *m* on problem *x*: Acc(φ_x, c*_x) of Eq. 2 for the final assembled proof (status `solved` in `results.jsonl`). Only the Lean kernel decides (RNF-1). - **Success rate:** SR_m = (number solved) / 30, with a **Wilson 95 % interval**. - Since each problem is run once, pass@k of Eq. 15 is estimated only for k = 1 (= SR_m). This is stated as a limitation; no repeated sampling is run. ## 3. Planned comparisons (confirmatory) Three comparisons, decided now, each a **two-sided exact McNemar test** on the paired outcomes (binomial test on the discordant pairs b, c with p = 1/2), **Bonferroni-corrected** for 3 tests (reject at p < 0.05 / 3 ≈ 0.0167; adjusted p-values = min(1, 3p) are also reported): | ID | Comparison | Question | |---|---|---| | H1 | C5 vs C1 | Does the multi-agent pipeline beat direct proof prompting (at equal mean measured computation, `b_max` of C1 fixed in Part A)? | | H2 | C5 vs C3 | RAG contribution, Δ_RAG = SR_C5 − SR_C3 (Section IV-A9e). | | H3 | C5 vs C4 | Contribution of the Critic loop (retries and replanning). | For each one we report: b and c (discordant counts), ΔSR, a 95 % **paired bootstrap** interval for ΔSR (10 000 resamples of problems, seed 2026, percentile method), the exact p-value and the Bonferroni-adjusted p-value. With n = 30 the power is low; a non-significant result is reported as "no evidence of a difference", never as "no difference". **Exploratory only** (no correction, labelled exploratory, no claims): C3 vs C4, C1 vs C3, C1 vs C4, and any per-difficulty or per-area comparison. C2 is **not** compared with McNemar on verified success: its success is self-assessed, not verified. ## 4. Secondary outcomes 1. **Per cell of the 3 × 3 grid:** for each configuration, solved / n of each (difficulty, area) cell, with the cell's n shown. Descriptive only: no tests and no intervals per cell (n ≤ 5). Margins by difficulty and by area are reported with Wilson intervals. Empty cells (no easy combinatorics) are shown as "—". 2. **Baseline B (Eq. 16):** claimed rate |B⁺| / 30 (Wilson), and FPR_B = |{x ∈ B⁺ : ¬Acc}| / |B⁺| (Wilson), where every self-assessed proof is passed to the Autoformalizer–Verifier loop with the same budget (`run_baseline_b.py --check`, to be built before the C2 run on `test`). FPR_B is an upper bound on the true false-positive rate; a manual review of the B⁺ problems that fail formalization (all of them if ≤ 10, otherwise 10 drawn with seed 2026) separates wrong informal proofs from formalization failures. 3. **Efficiency (Section IV-A9c, RNF-3):** per configuration, C̄_solved = Σ_x C(x) / #solved (failed problems' calls included in the numerator), and the same ratio for tokens, nominal USD cost and wall-clock time; also the means per problem. 95 % bootstrap intervals (resampling problems). RNF-3 (C̄_solved ≤ 20) is checked for C5 and reported as met or not; it is not tuned. 4. **Refinement robustness (Eqs. 14, IV-A9d):** SR(k) for k = 1, 2, 3, where a C5 problem counts as solved at k if its accepted proof used at most k attempts on every subgoal (read from `trace.jsonl`); k = 1 is also reported from C4. Δ̂(k) = SR(k) − SR(k−1) is plotted against the independence curve of Eq. 14 with p_i estimated from first-attempt subgoal success in C5. The paper states that k = 1 from C4 has no retries or advice while k = 2, 3 come from C5. 5. **Error taxonomy (Section IV-A9f):** relative frequency of each κ class of Eq. 11 over **all failed attempts**, per configuration and per area; separately, the final failure reason per problem (`stage` and final status). C1 attempts are classified with the same κ. ## 5. Status handling | Status in `results.jsonl` | Meaning | Primary analysis | |---|---|---| | `solved` | Acc holds on the assembled proof | success | | `failed` (any `stage`) | the method did not find an accepted proof | failure | | `budget_exhausted` | `b_max` LLM calls reached | failure (the budget is part of the method) | | `timeout` / memory limit | Lean verification limits | failure | | `error` / `node_error` / `invalid_statement` | a bug in the system or the statement | failure; counted and listed | | `provider_error` | the API refused or failed after all transport retries | see below | | `budget_stop` | the project or run spend cap stopped the run | see below | | run status `lean_unavailable`; row with `lean_down: true` | Lean could not load Mathlib (start-up probes) | as `provider_error`: infrastructure; re-run once, see below | - **`provider_error`** is an infrastructure failure, not a decision of the model. After a run, the problems with `provider_error` are re-run **once**, in a new run folder with the same configuration and cache (the original run is kept untouched). The re-run's result replaces the provider error in the analysis. If it is again `provider_error`, it counts as a **failure** in the primary analysis, and a sensitivity analysis excludes those problems from that configuration (and, for McNemar, the pairs where either side is excluded). Counts are reported per configuration. - **`budget_stop`**: the problem and the rest of the run were not attempted. The team decides whether to raise the spend cap; if raised, only the problems not attempted are run with the same frozen configuration and merged. If not, that configuration is reported as **incomplete**: SR on the attempted problems (with n stated), a conservative SR counting not-attempted problems as failures, and McNemar only on the problems attempted by both configurations. - **Lean unavailable**: a run that stops with `lean_unavailable` made no LLM call for the problems not run; those problems, and a row marked `lean_down: true` (Lean was lost during it, so its failure may be Lean's), are re-run once with the same configuration, exactly like `provider_error`. A success in a `lean_down` row stands (the kernel accepted it). - Runs marked `degraded` (Lean file back-end used) are valid and are flagged in the tables. ## 6. Fidelity notes (manual check before reporting success) `data/curation/fidelity_review.yaml` lists, under `notes`, problems whose formal statement differs from the informal text in a way judged harmless at curation time. Every problem **solved on `test` by any configuration** that has a note is reviewed by hand before it is counted as a success in the paper (PLAN.md, Phase 9). The review records whether the accepted proof establishes what the informal problem asks. The verified SR (Section 2) is never changed by this review: the kernel's verdict is what it is. If a review concludes that the formal statement does not capture the informal problem, the paper reports it next to the table (problem, configuration, reason) and gives the SR both with and without that problem. ## 7. What is reported, in order 1. Table: SR with Wilson 95 % CI for C1, C3, C4, C5; claimed rate and FPR_B for C2. 2. Table: H1–H3 with b, c, ΔSR, bootstrap CI, exact p and Bonferroni-adjusted p. 3. Table: per-cell solved/n for each configuration, with difficulty and area margins. 4. Table: efficiency (calls, tokens, nominal cost, time per problem and per solved problem). 5. Figure: SR(k), k = 1…3, vs the independence curve of Eq. 14. 6. Figure or table: κ taxonomy per configuration and area. 7. Counts of `provider_error`, `budget_stop`, `error`, degraded runs and the fidelity reviews. Analysis code (`src/formal_mas/analysis/stats.py`, `scripts/compare.py`) is written in Phase 9 to implement exactly this plan; it is tested on `dev` runs before it reads any `test` result. ## Exploratory analysis (post hoc, decided 2026-11-08) Decided after all confirmatory `test` runs and their analysis were finished. It is exploratory and changes no result, test or conclusion of §2–§7. - **Motivation.** The hard problems look limited by the model rather than by the method: C1 and C5 solve the same 4 of the 10 hard `test` problems (`imo_1964_p1_2`, `imo_1965_p2`, `putnam_1964_b2`, `putnam_1965_b2`), so the agents add nothing on that stratum with DeepSeek-Flash. - **Run.** C5 exactly as frozen for the main runs (same graph, prompts, `pipeline.yaml` method settings, seed, `B_max`/`b_max`), with model profile `experiment_pro`: identical to `experiment` except that every role uses `deepseek-v4-pro` instead of `deepseek-flash` (`config/models.yaml`). Input: the 10 hard `test` problems, all of them (not only those C5-Flash failed), as a file with exactly those lines of `data/eval.jsonl` in dataset order; its sha256 and id list go in `run_config.json`. One run, `--run-usd 5.00`; if it ends in `budget_stop` it is not resumed and the problems without a complete row are reported as not attempted. - **Reported.** A descriptive paired table, problem by problem, C5-Flash (the kept rows of the main C5 `test` result, §Deviations) vs C5-Pro on the same 10 problems: solved, LLM calls, cost (real and nominal), wall time in minutes; plus totals. The 2×2 table of solved/not solved may be shown as counts. - **Not done.** No hypothesis test, CI or p-value; nothing is added to the Bonferroni family; no claim about Pro beyond these 10 problems. Pro's results never replace C5's in any main table. - **Fidelity.** Any new success gets the same manual fidelity check as §6 before it is reported. ## Deviations No deviation from the analysis itself. Infrastructure incidents during the `test` runs: - **2026-11-03, C5 on `test` interrupted by low memory.** Run `20261103T174646Z_C5_experiment` (commit `ad70ec2`, clean tree) was killed at about 19:16 UTC by the host (Claude Code stops background jobs when the machine runs critically low on memory; the Lean REPL, ~3.5 GB, was sharing RAM with an idle Lean language server, ~2.7 GB). It is an infrastructure failure, not a decision of the method. 23 of 30 problems had finished and are kept unchanged; the 24th (`imo_1987_p6`) was cut mid-problem and left no row in `results.jsonl`. No row was `lean_down`, and there was no `provider_error` or `budget_stop`. The 7 problems without a row were completed in two resume runs. Both used the same frozen configuration (the analysis is the same at either commit), the same seed and cache, and the language server was stopped first. The input of each is a file holding exactly the needed lines of `data/eval.jsonl`, unchanged and in the original order. Its sha256 and the id list are in that run's `run_config.json`, and a copy is kept as `test_remaining.jsonl` in that run's folder. 1. `20261103T212359Z_C5_experiment_resume` (commit `ad70ec2`, clean tree; input sha256 `53284f8f…086fc4`) ran all 7 from scratch: `imo_1987_p6`, `imo_1979_p1`, `imo_1984_p6`, `imo_1964_p1_2`, `putnam_1964_b2`, `putnam_1995_b1`, `putnam_1965_b2`. It reached its spend cap (`--run-usd 0.50`) during the third problem. `imo_1987_p6` and `imo_1979_p1` finished (both `failed`). `imo_1984_p6` got a `budget_stop` row after 19 calls, and the last 4 were not attempted. 2. `20261103T225140Z_C5_experiment_resume2` (commit `93bc701`, which changes only this file; clean tree; input sha256 `f3da0f6d…6d77f91`) ran `imo_1984_p6` from scratch, plus the 4 problems not attempted, with `--run-usd 1.00` (the cap raised by team decision, §5). The requests that `imo_1984_p6` repeats from step 1 are answered from the cache. **Merge:** the C5 result on `test` has one row per problem (30 in all), taken from the run where the problem finished: - 23 rows from the first run; - `imo_1987_p6` and `imo_1979_p1` from resume 1; - `imo_1984_p6` and the other 4 from resume 2. The `budget_stop` row of `imo_1984_p6` in resume 1 is discarded; only its complete row counts. The spend of the discarded attempts (`imo_1987_p6` in the first run and `imo_1984_p6` in resume 1) counts towards the project's real cost. It is not in any kept row, so each problem's efficiency figures come from its kept row only. Cache hits lower the real cost of the resume runs but not their nominal cost, and nominal cost is the figure compared (§1). - **2026-11-03, run order C4 before C3.** C4 was run right after C5, and C3 moved to the next off-peak morning, so the order is C5, C4, C3, C2, C1 instead of C5, C3, C4, C2, C1 (§1). The reason is schedule and cost only. C3 takes about 3 h and would have run into the provider's peak window (01:00 UTC), while C4 is short and is answered mostly from the cache of C5. This has no effect on the analysis. Each configuration is still run once on the same 30 problems with the same frozen configuration, and the comparisons are paired by problem. C4 shares its cached requests with C5, not with C3, so its cache hits are the same in either order. Costs are compared at nominal prices (§1), so run order does not favour either configuration. - **2026-11-04, per-run spend cap raised from 1.0 to 2.0 USD before C3 on `test`.** Team decision. Only `config/pipeline.yaml → spend.run_usd` changed (1.0 → 2.0); `run_eval.py --run-usd` can only lower that cap, so C3 (about 3 h, no cache shared with C5 because its prompts carry no lemmas; C5 on `test` cost 1.36 USD real in total) would otherwise very likely end in `budget_stop` before the 30th problem. This is a spend-control change, not a method change: the cap is checked before each paid request and only decides whether the request is sent, so it does not change any prompt, model, budget `B_max`/`b_max`, policy or result of a request that is sent. The project cap `spend.total_usd` stays at 9.0 USD. C5 and C4 ran under the 1.0 USD cap (or a lower `--run-usd`); C3 runs with `--run-usd 2.00`. The offline test that pins the configured caps (`tests/test_spend.py::test_real_pipeline_yaml_has_the_caps`) was updated to the new value. - **2026-11-05, per-run spend cap raised from 2.0 to 3.5 USD before C1 on `test`.** Team decision. Only `config/pipeline.yaml → spend.run_usd` changed (2.0 → 3.5). C1 costs more per call than C5 (the cost run `20261103T161957Z_C1_experiment_c1_cost` spent 0.21 USD real on 3 `dev` problems, about 0.07 USD per problem), so 30 problems would likely end in `budget_stop` under 2.0 USD. As before, this is a spend-control change, not a method change: the cap is checked before each paid request and only decides whether the request is sent, so it does not change any prompt, model, budget `B_max`/`b_max`, policy or result of a request that is sent. The project cap `spend.total_usd` stays at 9.0 USD. C1 runs with `--run-usd 3.50`. The offline test that pins the configured caps was updated to the new value. - **2026-11-05, C1 on `test` stopped by the team.** Run `20261105T131443Z_C1_experiment` (commit `5ed7507`, clean tree, `--run-usd 3.50`) was stopped on purpose at about 17:43 UTC, together with its whole process tree (REPL, `lake`), to free the machine for other work. It is an operational incident, not a decision of the method: no code, prompt, model or configuration changed. 23 of 30 problems had finished and are kept unchanged; the 24th (`imo_1987_p6`) was cut mid-problem (after 10 calls, 0.10 USD real) and left no row in `results.jsonl`. There was no `provider_error` or `budget_stop`. The 7 problems without a row will be completed in a resume run, following the same procedure as for C5 (same frozen configuration, seed and cache; input file with exactly the needed lines of `data/eval.jsonl`; `imo_1987_p6` run from scratch, its earlier spend counted in the project's real cost but in no kept row). The resume run is `20261107T200233Z_C1_experiment_resume` (commit `2c8eae5`, clean tree; input sha256 `009bece56dc0fdde3c814c9e81aeda6ee7bd8dd677d0fa29bab5dd723c907b8b`, the 7 problems in dataset order; `--run-usd 1.65` = 3.50 minus the 1.8407 USD C1 had spent, rounded down, so that C1 as a whole stays under 3.50). - **2026-11-07, `dirty: true` in four `run_config.json` files (recording artefact, found in the analysis).** `run_eval.py` rewrites `run_config.json` when a run ends, and the git state (and `created_utc`) were read again at that moment instead of at launch. In `20261103T212359Z_C5_experiment_resume`, `20261103T225140Z_C5_experiment_resume2`, `20261103T235556Z_C4_experiment` and `20261107T200233Z_C1_experiment_resume` the only changed file is `docs/analysis_plan.md`, edited while the run was going to log these very incidents; every tree was clean at launch (checked before each run, as the Phase 8 rules require). No code, prompt, configuration or data file changed, so the method is not affected. In those files `created_utc` is also the end time; the start is the timestamp in the run name and the `run_start` event of `trace.jsonl`. The two interrupted runs (`20261103T174646Z_C5_experiment`, `20261105T131443Z_C1_experiment`) never reached the final rewrite and show their launch state. Fixed after all `test` runs (`run_config.run_start_info`): `git` and `created_utc` now describe the launch, and the state when the file is written goes to `git_end` and `written_utc`. Runs already made are not rewritten. - **2026-11-08, spend caps raised for the exploratory C5-Pro run (spend control).** Team decision, after all confirmatory `test` runs. Only `config/pipeline.yaml → spend` changed: `total_usd` 9.0 → 12.5 and `run_usd` 3.5 → 5.0. The ledger stood at 7.36 USD; re-pricing C5-Flash's tokens on the 10 hard `test` problems at Pro prices gives about 3.75 USD off-peak (7.49 USD at peak), so the old caps would stop the run. As before, the caps are checked before each paid request and only decide whether it is sent; no prompt, model of the main profiles, budget `B_max`/`b_max`, policy or result changes, and no confirmatory run is repeated. The run uses `--run-usd 5.00`. The offline test that pins the configured caps (`tests/test_spend.py::test_real_pipeline_yaml_has_the_caps`) was updated to the new values. - **2026-11-08, exploratory C5-Pro run stopped by the team (operational incident).** Run `20261108T130803Z_C5_experiment_pro_pro_hard` (commit `8f72b02`, clean tree, profile `experiment_pro`, `--run-usd 5.00`; input sha256 `acfd3825…26cf7a66`, the 10 hard `test` problems in dataset order) was stopped on purpose at about 17:23 UTC, together with its whole process tree (REPL, `lake`), because the team had to leave. No code, prompt, model or configuration changed; all calls were off-peak. 5 of 10 problems finished and are kept unchanged: `imo_1965_p2`, `imo_1993_p5`, `imo_1979_p1` (`failed`), `imo_1987_p6` (`budget_exhausted`) and `imo_1978_p5` (`provider_error`: the Autoformalizer request on subgoal 1, the problem's 30th call, got `APIConnectionError: Connection error.` with no HTTP response on all 5 transport attempts, 15:34:50–15:37:28 UTC). The 6th (`imo_1984_p6`) was cut mid-problem after 4 calls and left no row. The last 4 (`imo_1964_p1_2`, `putnam_1964_b2`, `putnam_1995_b1`, `putnam_1965_b2`) were not attempted. The run is **not resumed** and the `provider_error` is **not re-run**: the exploratory table reports the 5 finished rows, the cut problem and the 4 not attempted as such. Real cost 1.9407 USD (151 paid calls; 0.1725 USD of it on the cut problem, in no kept row); ledger total after the run 9.3003 USD. `run_config.json` still shows `status: running` because the run never reached its final rewrite. Clarifications written before any run on `test`: - **2026-11-03, FPR_B check (§4.2), how "the Autoformalizer–Verifier loop with the same budget" is implemented** (`scripts/run_baseline_b.py --check`, `baselines/baseline_b.check_claim`): each claimed proof (B⁺) is the sketch of the Autoformalizer on the trivial plan (the whole theorem as the only subgoal), with the Retriever's lemmas as in C5; up to `critic.k_max` = 3 attempts, each failure classified by κ and followed by the Critic's deterministic feedback (no LLM advice, no Planner, no Generator, no automation pre-pass, so no fixed tactic can stand in for the claimed proof); its own budget of `B_max` = 40 calls, counted apart from C2's own calls (C2's efficiency figures exclude the check; in practice the check makes at most k_max × 2 = 6 calls: one Autoformalizer call and at most one JSON repair per attempt). Acc is Eq. 2 on the assembled theorem. FPR_B = not_verified / (verified + not_verified), where `budget_exhausted` counts as not_verified (the budget is part of the method). A check that ended in `provider_error`, `budget_stop` or `error`, or a row marked `lean_down`, is left out of FPR_B, counted apart and re-run once like a `provider_error` (§5); if it fails again the same way it is reported as not checked. Problems C2 did not claim are not checked.