juihuichung/awakening-proofnet-runs

Awakening — ProofNet tool-use inference runs

ProofNet (186 Lean 4 problems) inference outputs for the COLM 2026 paper "Awakening: minimal agentic replay recovers tool use in formal-math fine-tuned LLMs". These are the runs behind the ProofNet columns of Table 2 (tab:proofnet_main) — Goedel-Prover-V2-32B before and after post-hoc SFT on 100 / 1K / 18K Lean agentic traces, sampled 32× per problem with the LeanSearch retrieval tool available.

Companion release: `awakening` (training recipes, data, BFCL eval) and `awakening-leansearch-v4.9.0` (the exact ChromaDB retrieval index these runs queried).

Layout

scores/<run>/          meta_summary*/ verbatim: per-problem solve counts, pass@k
                       ladder, retrieval-grounding stats   (1.9 MB total)
proofs/<run>.tar.gz    extracted Lean code + per-generation compilation verdicts
                       (pass / complete / errors / verify_time)   (133 MB total)
traces/<run>.tar.gz    full multi-turn traces: system prompt, model reasoning,
                       <tool_call> leansearch queries, tool responses, final proof
                       (685 MB total)
code/                  inference client + the retrieval gateway it called
analysis/              the analysis scripts and report the paper's prose was written from
verify_tables.py       recomputes every ProofNet number in Table 2 from scores/

Run python verify_tables.py — it prints each computed value next to the value printed in the paper. All 30 cells match exactly.

Runs

Checkpoint → on-disk source mapping for the rows without an HF link: awakening/checkpoints/MANIFEST.md, tiers 2 and 3. RUNS.md records each run's original della path and job date.

Conventions

Read these before comparing against your own numbers:

• —pass@k = first k generations. A problem counts as solved if any of its first k sampled generations compiles. This is not the unbiased 1 - C(n-c,k)/C(n,k) estimator; that estimator gives visibly different pass@8 values on the same data.
• —Normalized by 186. Problems whose generations all failed to parse still sit in the denominator.
• —Retr. is the share of pass@32-solved problems whose compiled proof cites at least one theorem identifier returned by LeanSearch (string match on the identifier), i.e. solved_with_retrieved_ratio_over_solved_num at level pass@32 in meta_summarize.json.
• —Panel B + 100 / + 1K were sharded across two GPU jobs over disjoint halves of the benchmark; those runs carry split1/ and split2/ subdirectories whose solve counts add.
• —compilation_result is a stringified Python dict, not JSON — ast.literal_eval it. Success is the complete field.
• —Generations are named <problem_id>_g<0..31>, in sampling order.

Reproducing a run

1. 1.Serve the retrieval index (awakening-leansearch-v4.9.0, see its README) — code/retrieval_gateway.py, exposing /api/v1/retrieve_one on port 1789.
2. 2.Serve the checkpoint with vLLM.
3. 3.code/inference_retrieval_async.py --retrieval-gateway http://<host>:1789 ... drives the tool loop: the model emits <tool_call>{"name": "leansearch", "arguments": {"query": ...}}</tool_call>, the gateway returns theorem names + signatures, the loop feeds them back as a tool message.
4. 4.Compile the extracted Lean with a Lean 4 REPL and summarize.

Known gap: the compilation records carry no toolchain metadata, so the exact Lean/Mathlib version of the verifier (distinct from the v4.9.0 Mathlib the retrieval index was built from) is not pinned by these artifacts. If you need bit-identical compilation verdicts, ask before assuming a version.

Provenance

Runs were produced Nov 2025 – Mar 2026 on della (Princeton HPC). Original paths are recorded per run in scores/<run>/**/SOURCE_PATH.txt and in RUNS.md.