PutnamBenchTracker

#!/usr/bin/env python3
"""
Reconstruct the true PutnamBench SOTA timeline by combining:
1. Git commit history of results.json (for models added in real time)
2. Manual corrections for models whose paper/announcement dates differ
   from when they were added to the leaderboard.

Saves CSV and generates a plot.
"""

import subprocess
import json
import csv
from datetime import datetime
from pathlib import Path

import matplotlib.pyplot as plt
import matplotlib.dates as mdates

REPO_DIR = "/tmp/putnam_bench_repo"
CSV_FILE = Path(__file__).parent / "putnam_bench_top1.csv"
PLOT_FILE = Path(__file__).parent / "putnam_bench_sota.png"

# ── Manual date overrides ──
# When a model's real announcement/paper date differs significantly from
# when it was added to the PutnamBench leaderboard, we use the real date.
# Sources are noted inline.
REAL_DATES = {
    # Seed-Prover v1 (329): arXiv 2507.23726, S2 publication_date 2025-07-31.
    # Added to leaderboard Aug 20, but paper was Jul 31.
    ("Seed-Prover (ByteDance)", 329): "2025-07-31",
    # Hilbert (462): arXiv 2509.22819, published Sep 26 2025.
    # Added to leaderboard Oct 6.
    ("Hilbert", 462): "2025-09-26",
    # Aleph Prover run 1 (500): page says "as of November 30, 2025".
    # BusinessWire press release Dec 2; leaderboard commit Dec 1.
    ("Aleph Prover", 500): "2025-11-30",
    # Seed-Prover 1.5 (581): arXiv 2512.17260 posted Dec 19 2025.
    # Added to leaderboard Dec 27 (by which time Aleph run 2 was already up).
    ("Seed-Prover 1.5 (ByteDance)", 581): "2025-12-19",
    # Aleph Prover run 2 (637): logicalintelligence.com/aleph-prover_300.html
    # says "published on December 22". The git initially had 622 on Dec 23,
    # later corrected to 637 on Dec 31 (same run, misformalization fixes).
    ("Aleph Prover", 637): "2025-12-22",
    # Aleph Prover run 3 (668): logicalintelligence.com/aleph-prover_1000.html
    # says "published on January 6, 2026". Git commit was Jan 11.
    ("Aleph Prover", 668): "2026-01-06",
}

# The 622 entry was a transient git value, later corrected to 637 (same run).
# We skip it entirely.
SKIP_ENTRIES = {("Aleph Prover", 622)}


def get_commits():
    """Get all commits that touched results.json, oldest first."""
    result = subprocess.run(
        ["git", "log", "--all", "--format=%H %ai", "--",
         "docs/results.json", "results.json"],
        capture_output=True, text=True, cwd=REPO_DIR,
    )
    lines = result.stdout.strip().split("\n")
    commits = []
    for line in reversed(lines):
        parts = line.split(" ", 1)
        sha = parts[0]
        date_str = parts[1].strip()
        dt = datetime.fromisoformat(date_str)
        commits.append((sha, dt))
    return commits


def get_results_json(sha):
    """Extract results.json content at a specific commit."""
    for path in ["docs/results.json", "results.json"]:
        result = subprocess.run(
            ["git", "show", f"{sha}:{path}"],
            capture_output=True, text=True, cwd=REPO_DIR,
        )
        if result.returncode == 0 and result.stdout.strip():
            try:
                return json.loads(result.stdout)
            except json.JSONDecodeError:
                continue
    return None


def extract_all_lean_entries(data):
    """Extract all (name, lean-wsolution) pairs from a results.json snapshot."""
    entries = {}
    for name, info in data.items():
        solved = info.get("num-solved", {})
        try:
            score = int(solved.get("lean-wsolution", 0))
        except (ValueError, TypeError):
            score = 0
        clean_name = name.strip()
        # Keep the highest score if a name appears multiple times
        if clean_name not in entries or score > entries[clean_name]:
            entries[clean_name] = score
    return entries


# Normalize name variants to a canonical form
NAME_NORMALIZE = {
    "Goedel-Prover (V2)": "Goedel-Prover-V2",
    "Self-Play Theorem Prover": "Self-play Theorem Prover",
    "Aleph Prover (Logical Intelligence)": "Aleph Prover",
    "Seed-Prover": "Seed-Prover (ByteDance)",
}


def normalize_name(name):
    return NAME_NORMALIZE.get(name, name)


def main():
    commits = get_commits()
    print(f"Found {len(commits)} commits touching results.json\n")

    # Track when each (model, score) first appeared in the git history
    # model_key -> { "first_seen_git": datetime, "score": int }
    first_seen = {}

    for i, (sha, dt) in enumerate(commits):
        date_str = dt.strftime("%Y-%m-%d")
        data = get_results_json(sha)
        if data is None:
            print(f"  [{i+1}/{len(commits)}] {sha[:7]} {date_str} — SKIP")
            continue

        entries = extract_all_lean_entries(data)
        for raw_name, score in entries.items():
            name = normalize_name(raw_name)
            key = (name, score)
            if key in SKIP_ENTRIES:
                continue
            if key not in first_seen and score > 0:
                first_seen[key] = dt
                print(f"  [{i+1}/{len(commits)}] {sha[:7]} {date_str} — NEW: {name} = {score}")

    print(f"\nFound {len(first_seen)} unique (model, score) entries with score > 0\n")

    # Build a list of all entries with their effective date
    all_entries = []
    for (name, score), git_dt in first_seen.items():
        # Use manual override date if available, otherwise git date
        override = REAL_DATES.get((name, score))
        if override:
            effective_dt = datetime.fromisoformat(override).replace(
                tzinfo=git_dt.tzinfo if git_dt.tzinfo else None
            )
            print(f"  DATE OVERRIDE: {name} ({score}): "
                  f"git={git_dt.strftime('%Y-%m-%d')} -> real={override}")
        else:
            effective_dt = git_dt

        all_entries.append({
            "name": name,
            "score": score,
            "effective_date": effective_dt,
            "git_date": git_dt,
        })

    # Sort by effective date
    all_entries.sort(key=lambda e: (e["effective_date"], e["score"]))

    # Reconstruct the SOTA timeline: at each point in time, who had the
    # highest lean-wsolution score?
    sota_timeline = []
    current_best_score = -1
    current_best_name = None

    for entry in all_entries:
        if entry["score"] > current_best_score:
            current_best_score = entry["score"]
            current_best_name = entry["name"]
            sota_timeline.append({
                "date": entry["effective_date"].strftime("%Y-%m-%d"),
                "datetime": entry["effective_date"],
                "top1_name": current_best_name,
                "top1_score": current_best_score,
            })

    print(f"\n{'='*60}")
    print(f"SOTA Timeline ({len(sota_timeline)} transitions):")
    print(f"{'='*60}")
    for s in sota_timeline:
        print(f"  {s['date']}  {s['top1_name']:40s}  {s['top1_score']}")

    # Write CSV
    print(f"\nWriting {CSV_FILE}...")
    with open(CSV_FILE, "w", newline="") as f:
        writer = csv.DictWriter(
            f, fieldnames=["date", "top1_name", "top1_score"])
        writer.writeheader()
        for s in sota_timeline:
            writer.writerow({
                "date": s["date"],
                "top1_name": s["top1_name"],
                "top1_score": s["top1_score"],
            })
    print(f"Saved {len(sota_timeline)} rows to {CSV_FILE}")

    # Separate SOTA entries from non-SOTA entries
    sota_keys = {(s["top1_name"], s["top1_score"]) for s in sota_timeline}
    non_sota = [e for e in all_entries if (e["name"], e["score"]) not in sota_keys]

    # Notable non-SOTA models to label (the rest are just grey dots)
    NOTABLE_NON_SOTA = {
        "GPT-5 (ReAct, 10 turns)", "Ax-Prover (Axiomatic AI)", "Ax-Prover",
        "Bourbaki", "DSP+", "Goedel-Prover-SFT",
        "o4-mini-high", "gemini-2.5-pro-exp-0325",
        "Deepseek R1", "COPRA (GPT-4o)",
    }

    # ── Plot ──
    print(f"Generating plot → {PLOT_FILE}...")
    from adjustText import adjust_text

    dates = [s["datetime"] for s in sota_timeline]
    scores = [s["top1_score"] for s in sota_timeline]
    names = [s["top1_name"] for s in sota_timeline]

    fig, ax = plt.subplots(figsize=(10, 6))

    # Non-SOTA models as grey dots
    ns_dates = [e["effective_date"] for e in non_sota]
    ns_scores = [e["score"] for e in non_sota]
    ax.scatter(ns_dates, ns_scores, s=30, color="#bbb", zorder=2,
               edgecolors="#999", linewidths=0.5, marker="o", alpha=0.7)

    # Labels for notable non-SOTA models
    ns_texts = []
    for e in non_sota:
        if e["name"] in NOTABLE_NON_SOTA:
            txt = ax.text(
                mdates.date2num(e["effective_date"]), e["score"],
                f"  {e['name']}  ({e['score']})",
                fontsize=6, color="#777",
                zorder=2,
            )
            ns_texts.append(txt)

    # SOTA line (linear interpolation)
    ax.plot(dates, scores, linewidth=2.5, color="#2563eb", zorder=3,
            marker="", linestyle="-")

    # SOTA milestone diamonds
    ax.scatter(dates, scores, s=90, color="#f59e0b", zorder=5,
               edgecolors="#b45309", linewidths=1.2, marker="D")

    # SOTA labels
    sota_texts = []
    for d, s, n in zip(dates, scores, names):
        txt = ax.text(
            mdates.date2num(d), s,
            f"  {n}  ({s})",
            fontsize=7.5, fontweight="bold", color="#1e3a5f",
            bbox=dict(boxstyle="round,pad=0.3", facecolor="lightyellow",
                      edgecolor="gray", alpha=0.85),
            zorder=6,
        )
        sota_texts.append(txt)

    # Adjust all labels together to avoid overlaps
    all_texts = sota_texts + ns_texts
    adjust_text(
        all_texts, ax=ax,
        arrowprops=dict(arrowstyle="-", color="gray", lw=0.5),
        expand=(2.0, 2.0),
        force_text=(1.5, 2.0),
        force_points=(0.5, 0.5),
    )

    ax.set_title(
        "PutnamBench — SOTA Over Time (672 problems)",
        fontsize=14, fontweight="bold",
    )
    ax.set_xlabel("Date", fontsize=12)
    ax.set_ylabel("Problems Solved", fontsize=12)
    ax.xaxis.set_major_formatter(mdates.DateFormatter("%b %Y"))
    ax.xaxis.set_major_locator(mdates.MonthLocator(interval=2))
    fig.autofmt_xdate()
    ax.grid(True, alpha=0.3)
    ax.set_ylim(bottom=0)

    plt.tight_layout()
    plt.savefig(PLOT_FILE, dpi=300, bbox_inches="tight")
    print(f"Plot saved to {PLOT_FILE}")


if __name__ == "__main__":
    main()