diff --git a/README.md b/README.md index 63c0f63..15d5c48 100644 --- a/README.md +++ b/README.md @@ -265,6 +265,13 @@ it; re-run the workflow with `refresh_service=true` to move it onto the new imag | `REGISTRY_TOKEN` | secret | a personal access token with `write:package`. **The built-in Actions token is not accepted by Gitea's container registry**, so without this the image is not pushed — it is still built and kept on the runner, and the build does not fail | | `REGISTRY_USER` | variable | only if the pushing account is not the actor | +## Research plan + +The paper plan for this project (ACL 2027 target, ARR deadline 4 Jan 2027) lives in +[`docs/research-plan.md`](docs/research-plan.md), with the work list in +[`docs/TODO.md`](docs/TODO.md) and the acceptance-bar analysis in +[`docs/acl-2027-bar.md`](docs/acl-2027-bar.md). + ## What this does not claim Lean says whether the code is *legal*, and — when there is a proof — whether it is diff --git a/docs/acl-2027-bar.md b/docs/acl-2027-bar.md new file mode 100644 index 0000000..530201b --- /dev/null +++ b/docs/acl-2027-bar.md @@ -0,0 +1,43 @@ +# Reaching the ACL 2027 bar + +Companion to `research-plan.md` and `TODO.md`. Written 2026-10-21. Target: ACL 2027 via ACL Rolling Review (ARR), submission deadline **4 Jan 2027** (AoE), 8-page long paper. + +## What the bar is + +Based on ACL 2025 and the ARR review form (the 2027 form may differ; re-check when published). + +- ACL 2025 accepted 20.3% of committed papers to the main conference and 16.7% to Findings ([program chairs' report](https://www.aclweb.org/adminwiki/index.php/2025Q3_Reports:_Program_Chairs)). +- The [ARR review form](https://aclrollingreview.org/reviewform) scores Soundness, Excitement, Reproducibility, Datasets (1-5) and Software (1-5), plus an overall score: 4 = could be accepted to the main conference, 3 = Findings (soundness and reproducibility are the main criteria), 2 = resubmit next cycle. +- Reviewers write numbered weaknesses (concerns that would rank the paper below other strong submissions). Every likely weakness should already be answered on the page. + +So the goal is an overall score of about 4, with Findings as the realistic floor. + +## Where the paper stands against each score + +| Score | What gets a 4 | Where we are today | What closes it | +|---|---|---|---| +| Soundness | Claims supported by a calibrated evaluation with baselines, CIs and a human check | No results, one model, no human labels | E4-E6 with kappa on 200 overlapping items, 600 audited items, Wilson CIs, paired tests | +| Excitement | A new idea, not a pipeline | Role-level structural fidelity + schema guidance, but 2026 papers already cover the gap and textbook pipelines | Show role alignment beats LLM judges on specific error types; say so in title and abstract | +| Datasets | "Useful" or "Enabling" | Copyrighted book, 89 items | Open-licence split of 1,500+ items with simplex and fidelity labels | +| Software | Usable release | Repo exists, no results | Pinned Docker image, one-command reproduction, tests | +| Reproducibility | Mostly reproducible | Detection varies run to run (80 vs 89 items) | Fixed seeds, logged prompts, 5-repeat variance, pinned Lean and Mathlib | +| Limitations / ethics | Honest and specific | Not written | Checklist in `research-plan.md` section 8.3 | + +## What must be true on 4 Jan + +1. **One headline result with a clean control.** At a fixed false-reject rate on faithful items, role alignment catches X% of "compiles but wrong" items versus Y% for a single LLM judge and Z% for a two-judge ensemble, with per-error-type recall. Everything else supports this. +2. **Human labels you can defend.** Two annotators, kappa >= 0.6 on the overlap, blind to model and filter score. This is the item most likely to slip. +3. **At least 4 models plus a specialised formalizer, and comparisons with existing metrics:** Beyond Compilation's judge rule, BEq+, static-pattern checkers, CriticLean. A 50-item ShadowBench-style check is enough. +4. **Honest positioning.** Do not claim first textbook autoformalization or first gap measurement. Cite Beyond Compilation, ShadowBench, Lean-GAP and ATLAS on page one and say what they lack. +5. **An error analysis reviewers remember:** a taxonomy of natural errors from real pages, a failure-case figure, and the repair finding (compile rate rises, faithfulness does not). +6. **Released, licence-clean artifacts and an anonymized repository.** +7. **A scope that fits 8 pages.** Cut the analogy miner, the Chinese-book study, the homogenization angle and the audit-time study (P2 in `TODO.md`). Keep schema-guided retrieval and proving (E9) only if the schedule holds. + +## Risk and fallbacks + +Eleven weeks is tight. The 8 Dec go/no-go decides the paper: if role alignment works, submit a method + resource paper aimed at the main conference; if it does not beat the baselines, submit an evaluation + resource paper aimed at Findings or the next cycle. Fallback venues: NeurIPS 2027 Datasets & Benchmarks (about May, projected), ITP 2027 (Glasgow, early Aug, dates pending), COLM 2027 (about 30 Mar, tentative). + +## Do now + +- Pilot the headline experiment on the existing 65 items with a quick manual label pass; if role alignment shows no signal there, find out before spending six weeks. +- Check whether ARR requires every author to register as a reviewer for ACL 2027 (the NAACL 2027 call did); missing it can mean desk rejection.