技能 编程开发 理论论文可复现性与严谨性检查

理论论文可复现性与严谨性检查

v20260724
focs-reproducibility
本指南提供了一套针对理论计算机科学论文的严谨化方法论,旨在确保论文的最高可检查性。它详细介绍了五个关键实践:建立假设记录表、冻结定理陈述以防止版本漂移、审计外部引用定理、为计算步骤提供证书,以及规范错误更正(errata)流程。确保证明在最严格的学术审阅中通过。
获取技能
418 次下载
概览

FOCS Reproducibility

FOCS has no reproducibility checklist and asks for no artifacts (2026 CFP, checked 2026-07-08). At a proofs venue, "reproducing" a result means an independent expert can re-derive it from the paper alone. That property — checkability — is engineerable, and papers engineered for it survive both refereeing and the decade of scrutiny that follows a FOCS acceptance. Four practices below build it.

1. The hypothesis ledger

Every assumption a theorem consumes should be visible at the theorem, not scattered across ambient conventions declared in Section 2. Keep a ledger during writing:

Hypothesis Introduced Used by Discharged or standing?
$G$ simple, connected §2 conventions Thm 1, 3; Lem 4.2 standing
$\varepsilon < 1/\log n$ Thm 3 statement Lem 5.1–5.4 standing — stated in Thm 3 ✓
oracle access to exact eigenvalues §5 ¶1 (silent!) Lem 5.3 must surface in Thm 3

The audit question for each row: does the formal statement of every theorem that transitively needs this hypothesis mention it? Silent standing hypotheses are the most common correctness complaint theory referees file, and the cheapest to fix before submission.

2. Statement freeze across versions

A FOCS project lives as at least three documents — the HotCRP submission, the arXiv/ECCC full version, and eventually the IEEE proceedings version. Theorem statements must be bit-identical across them; a bound that strengthens silently between submission and arXiv is, to a referee who checks, either sloppiness or misconduct. Enforce the freeze mechanically by extracting and diffing labeled statements:

# extract_statements.sh — run against any two versions of the source
for src in "$1" "$2"; do
  awk '/\\begin{(theorem|lemma|corollary)/,/\\end{(theorem|lemma|corollary)/' \
      "$src"/*.tex | tr -d ' \n' | sha256sum
done
# identical hashes => no drift in any formal statement

Legitimate post-submission improvements go into a dated "changes since submission" note in the arXiv version, never into silent edits (see focs-camera-ready for the endgame version ledger).

3. The imported-theorem audit

Most FOCS proofs stand on external results, and the failure mode is citing a theorem for slightly more than it says. Before the freeze, audit every import:

  • Locate the exact statement in the cited source — theorem number, page, and version (arXiv preprints renumber theorems between versions; pin the version, per focs-related-work).
  • Transcribe its hypotheses into your ledger and check your invocation supplies all of them. The classic bug: importing a bound proved for constant-degree instances into an unbounded-degree argument.
  • Check parameter regimes. "For sufficiently large $n$" in the source must be compatible with the $n$ your recursion actually feeds it.
  • If the imported proof is folklore or unpublished, prove it in your appendix; "well known" is not a citation a referee can check.

4. Certificates for computed steps

When a proof step is a computation (focs-experiments), checkability means a stranger can re-verify without trusting your code: publish the certificate (the enumerated cases, the SAT solver's proof trace, the exact rational arithmetic transcript), ship a minimal independent checker, pin both with hashes, and state in the proof what object certifies what claim. A referee who can re-run a 40-line checker in a minute treats the step as proved; one who is asked to trust an opaque 4,000-line search does not.

5. Errata as a first-class object

Checkability extends past acceptance. FOCS papers are cited for decades, and the community's memory of an error is shaped by how it was handled:

  • Maintain the changelog in the arXiv version as the single erratum channel; a correction buried in a later paper's footnote does not reach readers of the original.
  • Downgrade honestly: if a repaired lemma now yields a weaker bound, the changelog and the abstract both change — leaving a stale headline bound on a corrected paper is the reputational worst case.
  • Notify identifiable downstream users directly when a result they built on moves; theory's dependency graph is small enough that this is feasible and expected.

Pre-freeze checkability review

Run as a dedicated pass, separate from proofreading:

  1. Ledger complete; no silent standing hypotheses (§1).
  2. Statement hashes identical between submission source and full-version source (§2).
  3. Every external import located, transcribed, regime-checked (§3).
  4. Every computed step certified and independently checkable (§4).
  5. One non-author has re-derived the most delicate lemma from the paper text alone — the strongest single predictor that referees will succeed too.

A paper passing all five is not guaranteed acceptance; it is guaranteed not to be rejected for the reasons authors most regret, and it is camera-ready for the public record that FOCS culture expects the full version to become.

信息
Category 编程开发
Name focs-reproducibility
版本 v20260724
大小 5.32KB
更新时间 2026-07-28
语言