GIF

Inspiration

Every week brings ML papers that report a number: "76.1% top-1", "+2.3 BLEU over the baseline". Most readers can't check it. Re-running an experiment takes compute, a weekend and a lot of patience, and when the result doesn't match you never know whether the paper is wrong or your setup is. Reviewers face the same problem at scale.

Coding agents can now write a training script from a paper in minutes, so we asked an obvious question: can an agent re-run the paper and tell you whether the number holds? We found a second question just as important: why should anyone believe the agent? An LLM that writes the code, runs it and then grades its own homework is not evidence.

So Paper2Proof is built around one idea: the model does the work, deterministic code makes the call, and you can check both.

What it does

You enter an arXiv ID at https://paper2proof.com. Paper2Proof then:

Ingests the paper (LaTeX source when available, PDF otherwise) and extracts its quantitative claims: metric, dataset, reported value, baseline, number of seeds, and where each one comes from in the paper.
Discovers the official code (the authors' own links first, then Tavily search ranked by a small model) and plans an experiment that fits a fixed budget. A plan estimated above $0.60 waits for your approval.
Provisions packages, data and the repository through a policy decided by code (denylist, typosquat checks, a minimum release history, wheels only, hash-locked). Our provisioner never runs what it downloads.
Lets a Coder model write the experiment and fix it against smoke runs in a Nebius Token Factory Sandbox with networking disabled.
Runs the experiment over at least 3 seeds in a fresh Token Factory Sandbox, on CPU, offline and with no secrets.
Returns a deterministic verdict for each claim: REPRODUCED, REPRODUCED_AT_REDUCED_SCALE, NOT_REPRODUCED (shown as "Not reproduced under our conditions", with the conditions next to it) or INCONCLUSIVE with a reason code.
Packs everything into a signed Proof Bundle: the claims, the plan, the exact workspace, the runner image digest, the logs, the measurements, the verdict inputs, the cost receipt and a script to re-run the judged attempt.

Live runs are invite-only, runs are private by default, and the public gallery is curated by hand. Any gallery run can be replayed at 10× speed without executing anything.

How we built it

A finite-state machine, not a free-roaming agent. A run moves through fixed steps: INGESTING → EXTRACTING_CLAIMS → DISCOVERING → PLANNING → AWAITING_APPROVAL → PROVISIONING → SMOKE_TESTING → EXECUTING → ANALYZING → VERDICT. Each step is resumable and idempotent. The only agentic loop is the Coder's, bounded at 8 smoke runs, and the Coder is told how many it has left. Every model call and every job goes through a ledger and a budget check before it is made. The UI follows the run live over SSE.

Models on Nebius Token Factory, by role. The roles are reader, planner, coder, judge, vision and utility, all on open NVIDIA Nemotron models: Nemotron 3 Super reads and codes, Nemotron 3.5 Super VL reads tables and figures, Nemotron 3 Nano ranks and repairs, Nemotron 3 Ultra with reasoning plans and explains. They resolve at startup against GET /v1/models from a config file (no hard-coded model IDs or prices). Paper text is always wrapped as untrusted input before it reaches a prompt.

The verdict is a pure function. The judge model only writes the explanation, from a Facts block written by code; it never decides, and an explanation that names another verdict is replaced by a template. For an absolute claim with reported value v (optionally ± σ), metric m and n ≥ 3 seeds at full scale, we first flip lower-is-better metrics so that higher is always better. Then we compute the mean x̄, the sample standard deviation s, a 95% Student-t interval [ℓ, h] = x̄ ∓ t(0.975, n−1) · s / √n, and a tolerance w = max(2σ, 2% · |v|, the metric's absolute tolerance). The rule, in order:

REPRODUCED                       if x̄ ≥ v − w
INCONCLUSIVE (IMPLAUSIBLE_GAP)   else if x̄ and v have the same sign and x̄ / v is outside [1/2, 2]
NOT_REPRODUCED                   else if h < v − w
INCONCLUSIVE (HIGH_VARIANCE)     otherwise

The gap rule exists because the experiment is written by a model: a value more than twice off the paper's is a broken run, a stand-in or a unit mismatch, not evidence against the paper. At reduced scale an absolute claim is always INCONCLUSIVE. For a relative claim ("our method beats the baseline by δ"), we test the per-seed differences Δ instead. The claim is reproduced when the whole interval of Δ is above zero and its mean is at least ρ · δ, with ρ = 0.5: the improvement must be real and at least half as large as claimed. When the paper also states the method's own value, the same gap rule applies to the measured method value at full scale. The engine has 100% test coverage, enforced in CI, plus property-based tests, and its config is hashed into every verdict.

Untrusted code never touches the control plane. The control plane (FastAPI, the React UI and the orchestrator) runs on a VPS behind a TLS reverse proxy. Code written by an LLM or taken from a paper's repository runs only in Nebius Token Factory Sandboxes:

a fresh microVM per smoke run and per experiment (4 vCPU, about 4 GB), with networking disabled and no API keys;
inputs uploaded by content hash and mounted read-only, the job dropped to an unprivileged user, and only a fixed list of result files harvested back and parsed as untrusted data;
the runner image pinned by digest: the backend refuses any other image;
deterministic job names with a get-by-name lookup before every spawn, so a retry never creates a duplicate;
the agent can only request packages, and deterministic code validates and installs them.

Guards against a model that grades itself. A script that admits it uses a proxy, a stand-in or dummy data for the paper's method or data cannot finish until it changes, and the run's Limitations name the line. A script that starts processes or runs other files is refused before it spends a smoke run.

Proof Bundles are signed with Nebius KMS (ECDSA P-256 over the hash of the bundle's manifest), scanned for secrets before packing, and the public key is published, so anyone can verify a bundle offline.

The designed deploy is still in the repository. GPU jobs on an NVIDIA L40S in an isolated Nebius AI Cloud project, behind an allowlisting egress gateway, with the control plane on a Serverless endpoint, are implemented, tested and in Terraform. Our tenant never got the non-GPU vCPU quota that the gateway and the endpoint need, and the isolated GPU job test never passed, so the live service runs every experiment on CPU in Sandboxes, behind the same job interface.

The rest of the stack:

Backend: Python 3.12, FastAPI, pydantic v2, SQLAlchemy (async), SQLite in WAL mode replicated to Nebius Object Storage with Litestream.
Frontend: React + Vite + TypeScript, with types generated from the OpenAPI schema.
Infra and observability: Terraform for the Nebius infrastructure, GitHub Actions for CI, OpenTelemetry traces with one trace per run.

Evaluation

Latest round, through the live pipeline:

Set	Result	Cost
A: 10 synthetic scikit-learn papers we wrote, 16 claims (8 true, 8 deliberately false)	accuracy 1.0 (16/16), 0 false accusations	about $0.28 for the set
B: 5 real papers (Distillation, CatBoost, InterpretML, NAU, KAN)	3 runs reached a verdict, all Inconclusive with a stated reason (CatBoost on real Adult data, KAN, Distillation); 2 failed before one (InterpretML: sandbox disk; NAU: no passing smoke run); 0 false accusations	about $0.74 for the set
C (claim extraction) and the routing ablation	not run for this submission	—

Set A accuracy over our rounds: 0.5 → 0.81 → 0.94 → 0.81 → 0.69 → 0.94 → 1.0 → 0.94 → 1.0. Model variance remains, and every miss became a check in code: the last one, a Coder that added an option the paper does not give to scikit-learn's data generator, is now named to it before it can finish. Set B is the hard set. CatBoost ran on the real Adult data: its logloss came out at 0.274 against the paper's 0.2695, but its edge over LightGBM was smaller than claimed, so Inconclusive. KAN beat the MLP on all three claims with errors about 40 times the paper's, so Inconclusive (IMPLAUSIBLE_GAP); an earlier round had called a similar run Reproduced on a stand-in function, which is why that rule exists. InterpretML did not fit the sandbox's disk, and on NAU the Coder ran out of smoke runs.

Challenges we ran into

Trusting the cache. Our first provisioner both parsed untrusted datasets (parquet) and wrote the shared package cache, whose digests later runs trust. A malicious dataset could have poisoned the cache for everyone. We split it into two jobs. The provision job writes the cache and only ever sees package names and wheels. The fetch job handles the repository and datasets and can't reach the cache at all.
Symlinks everywhere. Jobs write files the control plane later reads, so a job can plant a link where a file should be. We spent real time making every read and write refuse links, junctions and FIFOs. On POSIX each path component is opened relative to its parent with O_NOFOLLOW. Windows has no such API, so there we check that the file we opened is the file we checked.
A null that broke every run. An end-to-end test on the real runner image found that our manifest serialized unset fields as null, which our own JSON schema rejects. Every real execution would have ended as a contract error. Contract tests against the production serialization are now mandatory.
No quota, three days before the deadline. With no CPU quota for the gateway and no working isolated GPU job, we moved the experiments into Token Factory Sandboxes behind the same job interface: inputs uploaded by content hash, a privilege drop inside the microVM, outputs harvested between random markers, and a host-side index to keep job names deterministic on a service that has none. The Sandboxes importer refused images referenced by digest, so we import by tag and record the image only after checking that the tag resolves to the pinned digest.
A Coder that quietly changes the question. On real papers the Coder sometimes measured another model or random data when the paper's was hard to get offline, and said so only in a comment. That became the stand-in tripwire and the implausibility rule.
Platform gaps. Some Nebius services were missing what we expected: no OTLP ingest for application metrics, and tracing ingest documented only for gRPC. We logged each gap as product feedback and designed around it.
Two people, one deadline. We kept shared contracts (schemas, domain types, specs) in small commits merged first, and every security-sensitive change went through a dedicated review before merging.

Accomplishments that we're proud of

A verdict you can recompute by hand from the bundle.
An honest third answer. Inconclusive with a reason (too few seeds, high variance, reduced scale, an implausible gap) is a valid result, and we never round it up to a yes.
A security model written down as non-negotiable invariants and enforced by tests, not by good intentions.

What we learned

The hard part of an AI scientist is not writing code. It is deciding what counts as evidence, and keeping the model out of that decision.
Real papers fail on the environment first: data that cannot be fetched offline, packages without wheels, setups that need more attempts.
Reproducibility is mostly bookkeeping: image digests, seeds, data hashes, exact package versions. If it isn't in the bundle, it didn't happen.
Budget checks before every call change the design. Cost becomes a first-class input to planning, not a surprise on the invoice.

What's next

Run the claim-extraction set and the routing ablation, and grow the real-paper set.
GPU experiments on Nebius AI Cloud when quota allows: the path is already implemented.
A public gallery of curated runs, with authors invited to respond.