docs: research plan v2 - simplex schema as Lean parameters, detailed experiments
ci / python (push) Has been cancelled
ci / python (push) Has been cancelled
Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FYqwNMyPUHeTbFWg83GQq6
This commit is contained in:
+379
-139
@@ -1,148 +1,388 @@
|
||||
# lean-bench: research plan and paper brief
|
||||
# lean-bench: research plan and detailed paper brief (v2)
|
||||
|
||||
Written 2026-10-21. Status of the system is taken from the repo README and the project notes (rebuild of 2026-09-19). Conference dates were checked on 2026-10-21; items marked *unverified* come from aggregator sites or projections and must be re-checked against the official call.
|
||||
Written 2026-10-21. Version 2 replaces the first brief. Two changes: (1) the **simplex schema** (`archived/schema-simplex`) is now the central method, as requested; (2) every section is expanded to the level of draft text, protocols and metrics.
|
||||
|
||||
## 0. Where the project stands, honestly
|
||||
Evidence base: repo README and code (`leanbench/`, 4,345 lines incl. tests), project notes `lean-bench-rebuild.md`, `runs/p85-110/*`, the archived simplex code, and literature checked on 2026-10-21. Anything marked **[verify]** is from memory or an aggregator and must be checked before it goes in a submission.
|
||||
|
||||
What exists: a working pipeline (page-level detection with quote-anchored spans, vision-OCR for font-mangled PDFs, Lean 4 formalization with one repair pass, Lean verification, type-indexed SQLite store with provenance). One book (587 pages), one 26-page verified run (89 items, about 3.4 items per page).
|
||||
---
|
||||
|
||||
What a reviewer will say today:
|
||||
1. No quantitative result. The only numbers are operational (CI time, OCR failure rate).
|
||||
2. `verified` means Lean accepted the statement, not that the statement says what the book says. The notes already admit "a well-formed statement of the wrong theorem passes every check".
|
||||
3. Detection is not reproducible (80 vs 89 items on the same range).
|
||||
4. One book, one LLM, no baselines, no human annotation.
|
||||
5. The source book is copyrighted, so the data cannot be released as built.
|
||||
## 0. The idea in one page
|
||||
|
||||
The plan below turns each of these into the paper's contribution or removes it.
|
||||
**Simplex, as it exists in the archived code.**
|
||||
- `Role(name, context, choices)`: a named semantic slot with a description and an optional closed set of allowed values (`is_constrained`, `validate_value`).
|
||||
- `Simplex(name, roles: {alias: Role})`: a reusable unit of **at least two** roles. A Simplex is itself a `Role`, so simplices nest; nesting gives a *simplicial complex*. `Equivalence` is the two-role special case.
|
||||
- `State` / `Fact` / `Goal`: a role plus a value. A `Fact` has a value, a `Goal` does not; `SolvingTask.is_completed()` is "every goal resolved".
|
||||
- `SchemaRegistry` (SQLite): `set_role`, `set_simplex`, `search_roles`, `find_by_roles(known_roles)`, `find_solvable(known_role_names)`.
|
||||
- `SchemaParserAgent`: turns a query into a Simplex through a forced tool call whose JSON schema says `minItems: 2`, with a **search-first, reuse-before-create** rule for roles. `AnalogySchemaMiner`: proposes new simplices by the ratio *Simplex B : Role B :: Simplex A : Role A*.
|
||||
|
||||
## 1. Venue decision
|
||||
**Why it is "exactly the Lean parameters".** A Lean declaration is a simplex:
|
||||
|
||||
| Venue | Deadline | Fit | Verdict |
|
||||
|---|---|---|---|
|
||||
| **ACL 2027** (Kyoto, Aug 20-22 2027), via ACL Rolling Review | **ARR submission 4 Jan 2027** (official site); commitment and notification TBA; 8-page long paper | Resource / evaluation paper, NLP + autoformalization. Optional theme on LLM homogenization | **Primary target.** About 11 weeks from today |
|
||||
| ICML 2027 | Abstract ~16 Jan, paper ~22 Jan 2027 (*unverified*, projected from the 2026 cycle; official CFP not out, location South America) | AI-for-math ML audience; bar for a benchmark with no new method is high | Backup if the faithfulness method is strong |
|
||||
| IJCAI 2027 | ~4 / 11 Jan 2027 (*unverified*) | General AI | Not recommended |
|
||||
| ITP 2027 (Glasgow, ~Aug 2-7 2027) | Not published yet | Formal-methods audience; cares about Lean/Mathlib correctness | Good fallback for a trimmed version; watch for the CFP |
|
||||
| COLM 2027 | ~30 Mar 2027 (*tentative*) | LLM-centred | Fallback if ACL misses |
|
||||
| NeurIPS 2027 Datasets & Benchmarks | ~14 / 21 May 2027 (*projected*) | Natural home for the full benchmark | Fallback with a full year of extra experiments |
|
||||
|
||||
Already closed, so not options: ICLR 2027 (25 Sep 2026), CPP 2027 (10 Sep 2026), NAACL 2027 / COLING ARR cycle (12 Oct 2026), AAAI-27, NeurIPS 2026.
|
||||
|
||||
**Recommendation:** target ACL 2027 on the 4 Jan ARR deadline. The work is a resource-plus-evaluation paper, which ACL accepts, and the date is official. Keep ICML (about 22 Jan) as a one-to-two-week-later alternative only if the experiments in 4.3 show a clear method gain. If ARR reviews arrive weak, commit to a later cycle or retarget NeurIPS D&B 2027.
|
||||
|
||||
**What the ACL bar requires** (so the plan is built around it): a clear contribution beyond engineering; a meaningful evaluation with baselines and more than one model; human evaluation or annotation with agreement statistics; released artefacts that can be used (data and code, licence-clean); Limitations section and Responsible NLP checklist; reproducibility details; 8 pages double-blind.
|
||||
|
||||
## 2. Paper framing
|
||||
|
||||
**Working title:** *Compiled is not Faithful: Measuring and Closing the Fidelity Gap in Textbook-to-Lean Autoformalization*
|
||||
|
||||
**One-sentence claim:** Lean acceptance badly overstates the quality of LLM autoformalization of real textbook mathematics; we release a page-grounded benchmark with human fidelity labels, show how large the gap is across models and pipeline stages, and show that a cheap round-trip fidelity check shrinks it.
|
||||
|
||||
Contributions (all must be evidenced in the experiments):
|
||||
1. **lean-bench**, a page-grounded benchmark of textbook items (statements, definitions, exercises) with Lean 4 formalizations, each carrying source hash, page and character span, and human fidelity labels.
|
||||
2. **A measurement of the verified-vs-faithful gap** by model, by item type, by domain, and by pipeline stage (OCR, detection, formalization, repair).
|
||||
3. **A fidelity filter** (round-trip informalization plus judge ensemble, calibrated on human labels) that raises precision of the released set.
|
||||
4. **Type-indexed retrieval** over the verified set, tested as a downstream aid to provers.
|
||||
|
||||
## 3. Brief
|
||||
|
||||
### 3.1 Introduction (about 1 page)
|
||||
- Autoformalization of research-level and textbook mathematics is the bottleneck for formal libraries; existing benchmarks are competition problems or small curated sets.
|
||||
- Textbooks are the real input: PDFs with broken math fonts, items split over pages, definitions that depend on context.
|
||||
- Everyone reports compile rate. Compile rate cannot see a well-typed statement of the wrong theorem. We quantify that.
|
||||
- Preview of findings (to be filled with real numbers): gap size, which stage loses the most, what the filter recovers.
|
||||
- Contributions list as in section 2.
|
||||
|
||||
### 3.2 Related work (about 0.75 page)
|
||||
Group into four threads. Entries are from memory and **must be verified and completed before submission**.
|
||||
- *Autoformalization benchmarks*: miniF2F, ProofNet (undergraduate textbook theorems, the closest prior), PutnamBench, FormalMATH, Lean Workbook, CombiBench. Gap we fill: page-grounded extraction from raw PDFs, human fidelity labels, definitions and exercises, not only theorem statements.
|
||||
- *Autoformalization models and training*: Wu et al. 2022 (few-shot with LLMs), Herald, Kimina-Autoformalizer, Goedel-Prover and DeepSeek-Prover family, repair with compiler feedback and type-check filtering (Poiroux et al. line of work). We use these as baselines, not competitors.
|
||||
- *Faithfulness / semantic equivalence checking*: FormalAlign, back-translation and LLM-judge approaches, ProofNet# style manual correction. We compare our filter against these.
|
||||
- *Document understanding for mathematics*: math OCR (Nougat, Mathpix-style systems), PDF-to-LaTeX pipelines, and statement mining from textbooks. We compare our vision-OCR route and anchor-based span resolution.
|
||||
- *Premise and library retrieval*: LeanDojo/ReProver, Lean search tools (Moogle, LeanSearch). We position type-index retrieval relative to embedding retrieval.
|
||||
|
||||
### 3.3 Key strategy (about 1.5 pages)
|
||||
1. **Ground everything in the page.** Quote anchors, not model-counted offsets; per-item `source_hash`, span and `page_checksum`. This is what makes human audit and re-run cheap, and it is the methodological difference from ProofNet-style curation.
|
||||
2. **Separate four claims that today are conflated:** *detected* (an item exists at this span), *compiled* (Lean accepts), *proved* (no `sorry`), *faithful* (matches the source). The pipeline reports each separately. Fix the overloaded `unverified` label first, since "Lean rejected" and "Lean never ran" currently look identical.
|
||||
3. **Fidelity filter.** Informalize the Lean statement back to natural language with a model that never saw the source, then judge equivalence against the source span with a multi-model ensemble; calibrate thresholds against human labels. Report precision/recall of the filter against humans, not agreement among LLMs.
|
||||
4. **Make every stage ablatable.** OCR mode (text / auto / ocr), window size, repair attempts, model choice, each toggle changes one thing and gets measured.
|
||||
5. **Release without releasing the book.** Use openly licensed sources for the public set (see 4.1); for copyrighted books release only spans' hashes, Lean code and instructions to reproduce, never page text.
|
||||
|
||||
### 3.4 Detailed experiments (about 2.5 pages)
|
||||
|
||||
**E1. Benchmark construction and statistics.**
|
||||
Sources: at least 6-8 books across algebra, analysis, topology, number theory, combinatorics; at least 3 with an open licence. Report items per book, kinds, span lengths, cross-page rate, OCR failure rate. Target 1,500+ items, with a 600-item human-audited core.
|
||||
|
||||
**E2. Detection quality.**
|
||||
Humans mark ground-truth items on 150 pages (stratified by book and by OCR difficulty). Report span precision, recall, boundary exact-match and IoU; breakdown for cross-page items. Ablate window size (1/2/3/5), extractor (text / auto / ocr), detection model. Report run-to-run variance over 5 repeats to address the 80-vs-89 instability.
|
||||
|
||||
**E3. OCR / extraction.**
|
||||
On pages with known font damage, compare embedded text, tesseract, the vision model, and one dedicated math-OCR system on LaTeX token accuracy and on downstream item yield. Includes the auto-mode quality heuristic's accuracy against human judgement.
|
||||
|
||||
**E4. Formalization: compile rate vs fidelity (the central experiment).**
|
||||
Models: at least four general LLMs (e.g. Qwen, one OpenAI, one Anthropic, one DeepSeek) plus at least one specialised autoformalizer. Metrics per model: compile rate, proved rate, human-judged fidelity, and the gap. Breakdown by item kind (definition / theorem / problem), domain, length, dependency on prior context. Report cost per verified-and-faithful item.
|
||||
|
||||
**E5. Human annotation protocol.**
|
||||
Two Lean-literate annotators label each item {faithful, minor drift, wrong, wrong-but-compiles}; third resolves. Report Cohen's kappa; guideline and error taxonomy (missing hypothesis, wrong quantifier, vacuous statement, changed definition, over-general). Include a taxonomy figure; this is the analysis section reviewers will remember.
|
||||
|
||||
**E6. Fidelity filter evaluation.**
|
||||
Compare: no filter, type-check only, single-LLM judge, judge ensemble, round-trip plus ensemble. Report precision/recall/F1 for "faithful" against the human core, and precision of the retained set at fixed recall. Include a negative control (shuffled spans) to show the filter is not rubber-stamping.
|
||||
|
||||
**E7. Repair ablation.**
|
||||
Repair attempts 0/1/3/5. Key question: does repair improve fidelity or only compile rate? Expect compile rate up and fidelity flat or down; if so, that is a headline finding.
|
||||
|
||||
**E8. Downstream use: type-indexed retrieval.**
|
||||
On held-out exercises, give a prover model (a) nothing, (b) embedding-retrieved items, (c) type-index retrieved items, from the verified-faithful set; report pass@k. Also run on faithful vs unfiltered store to show filtering matters downstream. Keep this modest: it supports a contribution, it does not carry the paper.
|
||||
|
||||
**E9. Contamination check.**
|
||||
For each formalization model, test whether items exist verbatim in public Lean corpora (Mathlib docstrings, ProofNet); report results on the clean subset.
|
||||
|
||||
**E10. Error analysis and cost.**
|
||||
Failure cases by pipeline stage, token cost, wall-clock per page, Lean time per item.
|
||||
|
||||
### 3.5 More detailed experiments (second layer, if time allows)
|
||||
- **Scaling:** performance vs book length and vs number of dependencies on earlier chapters; a context-carrying variant that supplies earlier definitions.
|
||||
- **Cross-lingual / non-English books** (project has Chinese-language tooling already): detection and OCR on Chinese textbooks, for the ACL audience.
|
||||
- **Judge bias:** does the judge prefer outputs from its own family? Cross-family judging matrix.
|
||||
- **Human effort study:** time to audit with page-grounded span vs. without; supports the provenance design.
|
||||
- **Robustness to scan quality:** degrade page images (DPI, noise) and measure yield.
|
||||
- **Homogenization angle** (ACL 2027's optional theme): do models converge on the same wrong formalization? Measure agreement among wrong outputs across models.
|
||||
|
||||
## 4. Work plan to the 4 Jan 2027 deadline
|
||||
|
||||
### 4.1 Preconditions (week 1-2, 21 Oct - 3 Nov)
|
||||
- Fix the overloaded `unverified` label; add the `source_pages` coverage table; incremental per-item storage (all three already queued).
|
||||
- Choose the open-licence sources and confirm their licences (do not reuse the uiowa-algebra book for any released file).
|
||||
- Write annotation guideline; recruit two annotators; set up an annotation UI over the existing page-grounded provenance.
|
||||
- Freeze a pipeline version and a model list; log all prompts and model ids.
|
||||
|
||||
### 4.2 Data and runs (weeks 3-6, 4 Nov - 1 Dec)
|
||||
- Ingest all books; produce the item pool; draw the 150-page detection sample and the 600-item core.
|
||||
- Run E2, E3, E4 for all models.
|
||||
|
||||
### 4.3 Annotation and method (weeks 5-9, 18 Nov - 22 Dec)
|
||||
- Human labelling of the core; compute agreement.
|
||||
- Build and calibrate the fidelity filter; run E5-E7.
|
||||
- Go / no-go on 8 Dec: if the filter gives no clear gain over a single-LLM judge, submit as a pure evaluation-and-analysis paper and drop contribution 3.
|
||||
|
||||
### 4.4 Downstream and writing (weeks 8-11, 9 Dec - 3 Jan)
|
||||
- Run E8-E10; write the paper in parallel from 1 Dec; internal review 24 Dec; release the licence-clean data and code package; ARR submission by 3 Jan to leave a day of slack.
|
||||
|
||||
## 5. Risks and mitigations
|
||||
| Risk | Mitigation |
|
||||
| Lean | Simplex view |
|
||||
|---|---|
|
||||
| Annotation too slow | Fix the audited core at 600; stratified sampling; second annotator on a 30% overlap only for kappa |
|
||||
| Fidelity filter shows no gain | Pure analysis paper; the gap measurement is the contribution |
|
||||
| Reviewers call it an engineering paper | Lead with the gap measurement and error taxonomy, not the pipeline |
|
||||
| Licensing blocks release | Open-licence books for the public split; hash-only releases for the rest |
|
||||
| Model API cost or drift | Pin model ids, cache outputs, report dates of calls |
|
||||
| Lean/Mathlib version drift | Pin the image (toolchain + Mathlib revision) per release |
|
||||
| Dates move | ICML and NeurIPS D&B dates are projected; re-check official CFPs before committing |
|
||||
| `(G : Type*) [Group G]` | role `G`, `context` = "carrier", `choices` = admissible type/class constraints |
|
||||
| `(h : P x)` hypothesis | `Fact` role |
|
||||
| conclusion after the final `:` | `Goal` role |
|
||||
| `def` / `structure` being introduced | `own` role (what the thing *is*) |
|
||||
| a lemma used inside a proof | nested simplex (edge in the complex) |
|
||||
|
||||
## 6. Sources checked on 2026-10-21
|
||||
- ACL 2027 site (official): ARR deadline 4 Jan 2027, Kyoto 20-22 Aug 2027.
|
||||
- NAACL 2027 call: ARR deadline 12 Oct 2026 (closed).
|
||||
- ICLR 2027 call: paper deadline 25 Sep 2026 (closed).
|
||||
- CPP 2027 page: paper deadline 10 Sep 2026 (closed).
|
||||
- ITP 2027 site: Glasgow, early Aug 2027, deadlines not yet published.
|
||||
- OpenCurious / trybibby aggregators: ICML 2027, IJCAI 2027, COLM 2027, NeurIPS 2027 (projected, unofficial).
|
||||
`leanbench/typeindex.py` already extracts exactly this split: `input` (binders and hypotheses), `goal` (the conclusion), `own` (definitions). So the type index is a simplex index in all but name. The new work is to make it a **first-class schema that steers inference** instead of a passive index.
|
||||
|
||||
**Four uses of the schema to guide inference** (each is a testable claim):
|
||||
1. **Slot-constrained formalization.** Decode a Lean declaration as filling a pre-declared simplex (typed slots, closed choice sets), the way `register_simplex_schema` forces `minItems: 2` and role reuse.
|
||||
2. **Role-alignment fidelity check.** Extract a *source-side* simplex from the prose (what is given, what is claimed) and compare it role by role with the Lean-side simplex. Missing hypothesis, extra hypothesis, wrong quantifier and swapped goal show up as role mismatches. This is a structural check that Lean cannot do and that does not rely on another LLM's opinion.
|
||||
3. **Schema-guided retrieval.** `find_solvable(known_roles)`: given the facts at hand, return items whose input roles are all covered and whose goal role matches. Compare with embedding retrieval.
|
||||
4. **Schema-guided proof search.** Treat the proof task as `SolvingTask(facts, goals)`; expand by applying a solvable simplex, adding its goal to the facts. Provers are steered by the registry rather than a flat premise list.
|
||||
|
||||
**Paper claim (working):** *Lean acceptance overstates autoformalization quality; a simplex schema derived from the Lean signature gives a cheap, structural, human-auditable fidelity signal and a retrieval/guidance structure that improves both the faithfulness of the released data and downstream proving.*
|
||||
|
||||
**Working title:** *Parameters as Schema: Simplex-Guided Autoformalization of Textbook Mathematics, and Why Compiling Is Not Enough*
|
||||
|
||||
**Honest state of the evidence today**
|
||||
- Pipeline: runs end to end. The pages 85-110 run: 89 detected (48 statements, 41 problems), 65 formalized, 24 skipped, **10 verified, 1 proved** (so compile rate on formalized items is 15%, and 85% of items fail or were not checked, with `unverified` conflating "Lean rejected" and "Lean never ran").
|
||||
- Detection is not reproducible (80 vs 89 items on the same range).
|
||||
- Faithfulness has never been measured. One book, one model.
|
||||
- The simplex code is archived, not integrated, and has defects (section 5.7).
|
||||
- The source book is copyrighted.
|
||||
|
||||
---
|
||||
|
||||
## 1. Venue decision (checked 2026-10-21)
|
||||
|
||||
| Venue | Deadline | Status | Fit |
|
||||
|---|---|---|---|
|
||||
| **ACL 2027** via ACL Rolling Review, Kyoto, 20-22 Aug 2027 | **ARR 4 Jan 2027**, 8 pages long | Official ([2027.aclweb.org](https://2027.aclweb.org/)); commitment/notification TBA | **Primary.** Resource + evaluation + method |
|
||||
| ICML 2027 | ~16 Jan abstract / ~22 Jan paper | **[verify]** projected from 2026 cycle; CFP not out | Backup if E6/E9 show a clear method win |
|
||||
| IJCAI 2027 | ~4 / 11 Jan | **[verify]** projected | Not recommended |
|
||||
| ITP 2027, Glasgow, ~2-7 Aug 2027 | not yet published | CFP pending | Good fallback for the Lean-correctness angle |
|
||||
| COLM 2027 | ~30 Mar 2027 | tentative | Fallback |
|
||||
| NeurIPS 2027 Datasets & Benchmarks | ~May 2027 | projected | Fallback with more time |
|
||||
| Closed | ICLR 2027 (25 Sep), CPP 2027 (10 Sep), NAACL/COLING 2027 ARR cycle (12 Oct), AAAI-27, NeurIPS 2026 | | |
|
||||
|
||||
**What the ACL bar demands, mapped to this plan**
|
||||
|
||||
| Reviewer expectation | Where the plan meets it |
|
||||
|---|---|
|
||||
| Contribution beyond engineering | Role-alignment fidelity signal and schema-guided inference (sections 5, 6: E6, E7, E9) |
|
||||
| Strong baselines and several models | E4/E6/E7 run >= 4 general LLMs + 1 specialised autoformalizer, and compare with 4 existing faithfulness methods |
|
||||
| Human evaluation with agreement | E5: two annotators, kappa, 600-item core |
|
||||
| Statistical rigor | Section 7.6: CIs, paired tests, multiple seeds |
|
||||
| Released artefacts, licence-clean | Section 5.6 and 8: open-licence books public, hashes-only for copyrighted ones |
|
||||
| Limitations, Responsible NLP checklist, reproducibility | Section 8.3 checklist |
|
||||
| Fits 8 pages | Section 3-6 are written to map to a page budget (3.6) |
|
||||
|
||||
---
|
||||
|
||||
## 2. Contributions and hypotheses
|
||||
|
||||
**Contributions**
|
||||
- C1. **A schema view of Lean declarations**: Role / Simplex / nested complex, with a deterministic projection Lean signature -> simplex (extends `typeindex.py`), registry with reuse-before-create role governance.
|
||||
- C2. **Role-alignment fidelity check**: source-side vs Lean-side simplex comparison, with a typed error taxonomy that falls out of role mismatches.
|
||||
- C3. **lean-bench**: page-grounded textbook items with Lean code, simplex annotation and human fidelity labels on a 600-item core.
|
||||
- C4. **Empirical study** of the compile-vs-faithful gap by model, item kind, domain and pipeline stage; and of schema-guided inference vs unguided.
|
||||
|
||||
**Pre-registered hypotheses** (state them before running; report them whether they hold or not)
|
||||
- H1. Compile rate overstates human-judged fidelity by >= 15 points for every model tested, and the gap is larger for tool/feedback-augmented pipelines.
|
||||
- H2. Repair with compiler feedback raises compile rate more than it raises fidelity (gap widens with attempts).
|
||||
- H3. Role-alignment detects >= 70% of human-labelled "wrong but compiles" items at <= 15% false-reject on faithful items, and beats a single LLM judge at equal false-reject rate on missing-hypothesis and quantifier errors. (Threshold is a target, not a result.)
|
||||
- H4. Slot-constrained formalization raises fidelity by >= 5 points over free-form generation with the same model and budget, mainly by reducing missing-hypothesis errors.
|
||||
- H5. Schema-guided retrieval (`find_solvable`) improves prover pass@k over embedding retrieval on exercises that depend on earlier definitions.
|
||||
|
||||
---
|
||||
|
||||
## 3. Introduction: draft text and structure
|
||||
|
||||
### 3.1 Paragraph plan
|
||||
1. **Hook.** Formal libraries grow slowly because turning human mathematics into Lean is expensive; textbooks hold most of undergraduate and graduate mathematics, and LLMs now translate statements fluently.
|
||||
2. **The measurement problem.** Systems and benchmarks are scored by whether Lean accepts the output. But Lean checks types, not meaning: a statement missing a hypothesis, with `∃` for `∀`, or over `ℕ` instead of `ℤ` compiles and is wrong. Concurrent work already shows large gaps on curated statement sets (cite 2606.31002, 2608.29270 **[verify numbers]**); no one has measured it on raw textbooks where extraction error compounds with formalization error.
|
||||
3. **Why textbooks are harder.** Font-mangled PDFs (`D` for `=`, `C` for `+`), items split across pages, definitions that depend on context. Each stage can break meaning silently: in our own pipeline the first server run reported success while storing 0 items.
|
||||
4. **Our observation.** A Lean declaration's parameters are a small typed schema: given objects, hypotheses, a goal. The same schema exists in the prose (what is assumed, what is claimed). Comparing the two *role by role* is a structural check that localizes the error.
|
||||
5. **Approach.** Represent both sides as simplices; use the schema to constrain formalization, to compare, and to retrieve.
|
||||
6. **Findings (fill in).** "On N items from K books, M models compile X-Y% but only A-B% are faithful (gap G points). Role alignment recovers P% of unfaithful-but-compiling items at Q% false rejection; slot-constrained decoding raises fidelity by R points; schema retrieval raises prover pass@8 from S to T."
|
||||
7. **Contributions** (C1-C4).
|
||||
|
||||
### 3.2 Opening paragraph (draft, to be edited)
|
||||
> Formalizing mathematics in a proof assistant remains slow because every definition and statement must be rewritten by hand. Large language models now produce plausible Lean 4 for textbook statements, and benchmarks report the share that the Lean compiler accepts. That number is easy to compute and easy to misread: Lean verifies that a statement is well typed, not that it says what the author wrote. A statement that drops a hypothesis, swaps a quantifier, or silently changes the ambient number system compiles and is wrong. We ask how large this gap is on real textbook pages, where extraction errors from the PDF compound errors from the model, and whether the structure of a Lean declaration itself can be used to detect and reduce it.
|
||||
|
||||
### 3.3 Figure 1 (spec)
|
||||
Left: a PDF page crop (Definition + Proposition). Middle: source-side simplex (roles: `G: finite group`, `n = |G|`, `g: element`; goal: `g^n = e`). Right: Lean-side simplex from `theorem ... (G : Type*) [Group G] [Fintype G] (g : G) : g ^ Fintype.card G = 1`. Colored links per role; one red unmatched role in a failing example (the missing `[Finite G]` or an `ℕ`-for-`ℤ` slip). Caption states compile = yes, faithful = no.
|
||||
|
||||
### 3.4 Claims to avoid (reviewer traps)
|
||||
- Do not claim "verified" means correct; use *compiled*, *proved*, *faithful* as four separate words from the first page.
|
||||
- Do not claim novelty of the idea that compile != faithful (prior work shows it). Novelty is the structural role-level signal, the textbook-scale pipeline with provenance, and the guided inference.
|
||||
- Do not claim the benchmark is large; say what it is (hundreds of audited items from a handful of books) and why.
|
||||
|
||||
### 3.5 Preview results table (to fill)
|
||||
| Model | compile % | proved % | faithful % (human) | gap (pts) | faithful after role filter % |
|
||||
|---|---|---|---|---|---|
|
||||
|
||||
### 3.6 Page budget (8 pages, ACL long)
|
||||
Intro 1.0 | Related 0.6 | Method (simplex, alignment, guidance) 1.8 | Benchmark + protocol 1.0 | Experiments 2.6 | Analysis + conclusion 0.5 | Limitations and ethics on extra pages. Figures: F1 overview, F2 gap by model, F3 error taxonomy, F4 role-alignment ROC, F5 retrieval/guidance. Tables: T1 stats, T2 gap, T3 filter comparison, T4 ablations.
|
||||
|
||||
---
|
||||
|
||||
## 4. Related work: threads, references, and the sentence that separates us
|
||||
|
||||
References marked **[verify]** are from memory/search snippets; confirm authors, year and numbers before citing.
|
||||
|
||||
### 4.1 Autoformalization benchmarks and corpora
|
||||
- **miniF2F**, **PutnamBench**, **FormalMATH**, **CombiBench**, **Lean Workbook**: competition-style or synthetic. **[verify each]**
|
||||
- **ProofNet** (Azerbayev et al., 2023; undergraduate textbook theorems; [arXiv 2302.12433](https://arxiv.org/pdf/2302.12433)): closest prior. Hand-curated, statements only, no extraction from PDFs.
|
||||
- **ProofNet#, RLM25, ProofNetVerif** (Poiroux et al., [arXiv 2406.07222](https://arxiv.org/abs/2406.07222)): fixed 118 of 371 ProofNet entries; found type-check rate correlates only weakly (Pearson 0.655) with human accuracy; proposed BEq/BEq+ symbolic equivalence (BEq+ precision 98.0%, recall 48.3%).
|
||||
- Concurrent 2026 work: **Beyond Compilation** ([arXiv 2606.31002](https://arxiv.org/abs/2606.31002); 227 graduate statements; faithfulness = compile + two-LLM agreement; judge vs human agreement 91.5%; compile-faithful gap from 1.3 to 29.5 points across 8 systems) and **ShadowBench / SA-Pass** ([arXiv 2608.29270](https://arxiv.org/abs/2608.29270); 178 postgraduate-research problems; "shadow" statements checked forward and backward; compile 61.8% vs SA-Pass 11.2% for the best agentic setup). **[verify numbers against the final versions]**
|
||||
- *How we differ:* these start from a clean list of statements. We start from PDF pages, include definitions and exercises, keep page-level provenance, and measure how extraction error adds to formalization error.
|
||||
|
||||
### 4.2 Autoformalization methods
|
||||
- Few-shot autoformalization (Wu et al., 2022 **[verify]**); sampling + type-check filtering + selection ([2406.07222](https://arxiv.org/abs/2406.07222)); Herald, Kimina-Autoformalizer, Goedel-Prover, DeepSeek-Prover-V2 **[verify each]**; agentic Lean workflows (e.g. Numina-Lean-Agent as used in ShadowBench **[verify]**).
|
||||
- *How we differ:* we do not propose another model. We propose a schema layer that constrains and audits any model, and treat these systems as baselines.
|
||||
|
||||
### 4.3 Faithfulness and equivalence checking
|
||||
- **FormalAlign** (Lu et al., [ICLR 2025](https://proceedings.iclr.cc/paper_files/paper/2025/hash/fceedf8c9c0ff51f41b9fe0294ef0070-Abstract-Conference.html); [arXiv 2410.10135](https://arxiv.org/pdf/2410.10135)): learned alignment scorer.
|
||||
- **BEq / BEq+**: symbolic, high precision, low recall (above).
|
||||
- **LLM-judge ensembles** (Beyond Compilation) and **shadow statements** (ShadowBench): behavioural checks that need extra LLM calls or hand-written shadows.
|
||||
- Back-translation / round-trip consistency **[verify specific papers]**.
|
||||
- *How we differ:* role alignment is structural and gives a typed explanation of *which* part of the statement is wrong. It is cheap (one extraction call + deterministic matching), and complements, not replaces, BEq and judges. We evaluate all of them side by side (E6).
|
||||
|
||||
### 4.4 Structured / schema-guided reasoning with LLMs
|
||||
- Schema-constrained decoding and JSON-schema tool calls; type-directed / grammar-constrained generation **[verify specific papers]**; frame semantics and semantic-role labelling as the linguistic precedent for "roles"; analogical structure mapping (Gentner) as precedent for the analogy miner.
|
||||
- Found 2026-10-21 (titles from search results; **read them and confirm claims before citing**): "Schema Key Wording as an Instruction Channel in Structured Generation under Constrained Decoding" ([arXiv 2604.14862](https://arxiv.org/abs/2604.14862)), which suggests the wording of schema keys itself steers the model, so role `name`/`context` strings are a design variable to ablate in E7; "Constrained Decoding Eliminates Structural Failures in Small LLMs but Reveals a Scale-Dependent Semantic Gap" ([arXiv 2609.23742](https://arxiv.org/html/2609.23742v1)), the same structure-is-not-semantics lesson as compile-is-not-faithful, and a useful motivation for pairing slot constraints with role alignment; SLOT ([arXiv 2505.04016](https://arxiv.org/html/2505.04016v1)) and an empirical study of structured-output control ([arXiv 2606.09395](https://arxiv.org/html/2606.09395v1)).
|
||||
- *How we differ:* roles come from the Lean signature itself, so schema and ground-truth parameters coincide; the registry reuses roles across the whole corpus. Our constraint is on *what the declaration is about* (its parameters), not only on output syntax.
|
||||
|
||||
### 4.5 Mathematical document understanding
|
||||
- Math OCR and PDF-to-LaTeX (Nougat and commercial systems **[verify]**), vision LLM transcription; statement mining from LaTeX sources (arXiv-based corpora **[verify]**).
|
||||
- *How we differ:* we handle the font-encoding failure mode specifically (ASCII look-alikes) and tie each OCR page to downstream item yield.
|
||||
|
||||
### 4.6 Premise selection and library search
|
||||
- LeanDojo / ReProver, Lean search engines (Moogle, LeanSearch) **[verify]**; type-based search (Hoogle-like).
|
||||
- Found 2026-10-21 (confirm before citing): LeanSearch v2, global premise retrieval for Lean 4 ([arXiv 2605.13137](https://arxiv.org/abs/2605.13137)); LeanExplore ([arXiv 2506.11085](https://arxiv.org/pdf/2506.11085)); "Premise Selection for a Lean Hammer" ([arXiv 2506.07477](https://arxiv.org/html/2506.07477)); "Combining Textual and Structural Information for Premise Selection in Lean" ([arXiv 2510.23637](https://arxiv.org/html/2510.23637v1)), the closest to a structure-aware retriever and a required baseline in E9. These are text/embedding/graph retrievers over Mathlib; none indexes by the hypothesis/goal role signature of items extracted from textbooks.
|
||||
- *How we differ:* `find_solvable` retrieves by role coverage across a corpus we built from textbooks, including items that are definitions and exercises, not only Mathlib lemmas.
|
||||
|
||||
### 4.7 Positioning table (include in paper)
|
||||
| Work | Input | Fidelity signal | Cost | Localizes error? | Textbook PDFs |
|
||||
|---|---|---|---|---|---|
|
||||
| ProofNet(#) | curated | human | high | n/a | no |
|
||||
| BEq+ | statement pairs | symbolic | CPU | no | no |
|
||||
| LLM judges | statement pairs | LLM | calls | no (text rationale) | no |
|
||||
| ShadowBench | curated | shadows | authoring | partly | no |
|
||||
| **Ours** | **PDF pages** | **role alignment (+ judges)** | **1 call + CPU** | **yes, by role** | **yes** |
|
||||
|
||||
---
|
||||
|
||||
## 5. Key strategy
|
||||
|
||||
### 5.1 Formal setup
|
||||
- A **source item** is a span `s = (hash, page_a:i_a -> page_b:i_b)` with text `t(s)`.
|
||||
- A **Lean item** is code `c` with signature parsed into binder groups.
|
||||
- **Lean-side simplex** `S_L(c)`: deterministic projection (extend `typeindex._split_top_level` / `_top_level_result`):
|
||||
- one role per explicit binder `(x : T)`; `choices` = {T} plus instance binders `[C T]` attached to the same role;
|
||||
- one `Fact` role per hypothesis binder whose type is a `Prop`; one `Goal` role for the conclusion;
|
||||
- `own` role for definitions.
|
||||
- Requirement: at least two roles; items with fewer (e.g. a bare `def`) are stored as degenerate and reported separately.
|
||||
- **Source-side simplex** `S_T(s)`: produced by one LLM call on `t(s)` only (never sees the Lean), as a forced tool call whose JSON schema has `minItems: 2`, fields `alias, name, context, choices, kind in {object, fact, goal}`; role names are resolved against the registry with search-first reuse.
|
||||
- **Alignment** `A(S_T, S_L)`: a bipartite matching on roles by (a) name similarity via registry, (b) kind, (c) type-compatibility of `choices`. Output: matched pairs, unmatched source roles (*missing in Lean*), unmatched Lean roles (*extra in Lean*), type conflicts, kind conflicts. Score = F1 over roles, plus a typed error list.
|
||||
|
||||
### 5.2 Error taxonomy derived from alignment
|
||||
| Role-level signature | Error type |
|
||||
|---|---|
|
||||
| source Fact unmatched | missing hypothesis |
|
||||
| Lean Fact unmatched | extra hypothesis |
|
||||
| matched object, `choices` differ | wrong type / wrong ambient structure (`ℕ` vs `ℤ`, `Group` vs `CommGroup`) |
|
||||
| goal matched, quantifier prefix differs | quantifier error (detected on the goal role's quantifier annotation) |
|
||||
| Lean has fewer than two roles | vacuous / degenerate statement |
|
||||
| goal unmatched | wrong conclusion |
|
||||
Quantifier structure is not a pure role property; record it as a role attribute (`binder_kind`) extracted on both sides.
|
||||
|
||||
### 5.3 Slot-constrained formalization (guided inference, use 1)
|
||||
Procedure per item:
|
||||
1. Build `S_T` from the prose (above).
|
||||
2. Ask the model to emit Lean as **slot fills**: for each role, a Lean binder string, with choices restricted to the role's `choices` when set (e.g. instance classes from a closed Mathlib list), and the goal as a separate field. The final declaration is assembled deterministically, so the signature always has the role structure.
|
||||
3. Lean check; on error, repair only the offending slot (diagnostics map to character ranges, ranges map to slots), not the whole declaration.
|
||||
Ablations: free-form vs slot-filled; slot repair vs whole-declaration repair; open vs closed `choices`.
|
||||
|
||||
### 5.4 Role-alignment filter (use 2)
|
||||
- Compute `A(S_T, S_L)` for every compiled item; accept if score >= tau and no hard error (missing hypothesis, kind conflict). tau calibrated on the 600-item human core to fix false-reject rate.
|
||||
- Combined filter: role alignment AND (round-trip judge, optional). Evaluate each alone and combined.
|
||||
|
||||
### 5.5 Schema-guided retrieval and proof guidance (uses 3 and 4)
|
||||
- `find_solvable(known_roles)`: returns items whose input roles are covered by the given facts. Rank by goal-role match then by coverage tightness.
|
||||
- Proof guidance: `SolvingTask(facts, goals)`; at each step the prover is shown the top-k solvable simplices (with Lean statements) and may apply one; the applied simplex's goal becomes a new `Fact`. Stops when all goals are resolved or the budget ends. This is a thin loop around any prover; the contribution is the retrieval structure.
|
||||
- Nested simplices record which items use which definitions; this is the dependency graph of the book.
|
||||
|
||||
### 5.6 Role vocabulary governance and release policy
|
||||
- **Reuse before create** (from `SchemaParserAgent`): the agent must call `search_roles` on extracted keywords and reuse exact names. Metric: role-vocabulary growth per 100 items and duplicate-role rate (E-S2).
|
||||
- **Analogy mining** (from `AnalogySchemaMiner`): propose new simplices from `Simplex A : Role A :: Simplex B : Role B`; quality-controlled by refusal when the analogy is weak. Evaluate in section 7 only; it is not on the critical path.
|
||||
- **Release policy**: public split = openly licensed books (confirm licence per book); for copyrighted books release hashes, spans, Lean code and simplex annotations, never page text or OCR text. `uiowa-algebra.pdf` stays out of every release.
|
||||
|
||||
### 5.7 Porting work required (the archived code is not drop-in)
|
||||
Found by reading `archived/schema-simplex` on 2026-10-21:
|
||||
- `Simplex` is a `@dataclass` that defines its own `__init__`; the generated `__init__` is therefore not used and **`__post_init__` never runs, so the "at least two roles" check never fires**. Same for `Equivalence` ("exactly 2"). Move validation into `__init__`.
|
||||
- `Simplex.__init__` does not call `Role.__init__`, so `context` and `_choices` are never set; `is_constrained()` on a Simplex raises `AttributeError`.
|
||||
- `schema_builder.py` imports `from role import Role` (absolute) alongside package-relative imports; will not import as a package.
|
||||
- `State`/`Fact`/`Goal` carry a value but no Lean type; add `lean_type`.
|
||||
- `schema_registry.py` has `find_by_roles` and `find_solvable`, but how nested simplices are stored and queried (`keys("schema:*")`) needs a test for depth > 1.
|
||||
- Add: Lean signature -> simplex projection, role attributes (`binder_kind`, `instance_of`), alignment function, and unit tests in the style of the existing 12 test modules.
|
||||
|
||||
### 5.8 Separation of claims (carried from v1)
|
||||
Report four independent flags per item: `detected`, `compiled`, `proved`, `faithful` (human, then filter). Split the overloaded `unverified` into `rejected_by_lean` and `lean_not_run`. Add the queued `source_pages` coverage table and incremental storage first, so every statistic can be recomputed.
|
||||
|
||||
---
|
||||
|
||||
## 6. Detailed experiments
|
||||
|
||||
Common protocol: Lean/Mathlib image pinned (Lean 4.33.1 image from the project); every model call logged with model id, date, temperature, prompt hash; 3 seeds where sampling is involved; items keyed by `sha1(source hash + span)` so runs are comparable; human labels stored with annotator id.
|
||||
|
||||
### E0. Port and unit-validate the simplex projection (week 1-2)
|
||||
- *Question:* does the deterministic Lean -> simplex projection cover the corpus?
|
||||
- *Data:* the 65 existing items plus 300 items from other books.
|
||||
- *Metrics:* % items with >= 2 roles; % hypotheses recovered vs manual count on 100 items; failure classes (tactic-block binders, `variable` inheritance, implicit universes).
|
||||
- *Pass bar:* >= 95% structural agreement with manual parse; otherwise fix before any other experiment.
|
||||
|
||||
### E1. Corpus and benchmark construction
|
||||
- *Sources:* 6-8 books across algebra, analysis, topology, number theory, combinatorics, at least 3 openly licensed **[confirm licences]**, one non-English (Chinese) for the second-layer study.
|
||||
- *Targets:* >= 1,500 items; 600-item stratified audited core (by book, kind, page range, OCR status).
|
||||
- *Report:* items per book/kind, items per page, span length, cross-page rate, truncated rate, OCR replaced/failed pages, roles per item, role vocabulary size.
|
||||
- *Reference point:* 89 items over 26 pages = 3.4/page, projecting about 2,000 for the 587-page book.
|
||||
|
||||
### E2. Detection quality
|
||||
- *Setup:* two annotators mark every item on 150 stratified pages (50 per difficulty tier: clean text / mild damage / heavy damage).
|
||||
- *Systems:* current detector with window 1/2/3/5; extractor text/auto/ocr; 3 detector models; baseline regex on "Theorem/Lemma/Definition/Exercise" headers.
|
||||
- *Metrics:* span precision, recall, F1; exact-boundary match; token-IoU; cross-page recall; unresolved-anchor rate; run-to-run Jaccard over 5 repeats (to quantify the 80 vs 89 instability).
|
||||
- *Analysis:* error classes (merged items, split items, missed exercises (a)/(b) sub-items, hallucinated spans).
|
||||
|
||||
### E3. Extraction / OCR
|
||||
- *Systems:* embedded text; tesseract; `qwen-vl-max` at 150/200/300 dpi; one dedicated math-OCR system **[choose]**.
|
||||
- *Metrics:* LaTeX token edit distance on 100 hand-corrected pages; formula-level exact match; downstream item yield and compile rate; cost per page; accuracy of the `auto` quality heuristic (threshold 0.75) vs human "page is damaged" judgement (ROC).
|
||||
- *Check:* the ASCII look-alike failure (`D` for `=`, `C` for `+`) as its own error class.
|
||||
|
||||
### E4. Compile vs faithful gap (central measurement)
|
||||
- *Systems:* >= 4 general LLMs (one each from Qwen, OpenAI, Anthropic, DeepSeek families) + 1 specialised autoformalizer, same prompt and repair budget; same 600-item core.
|
||||
- *Metrics per system:* compiled %, proved %, faithful % (human), gap = compiled - faithful; cost (tokens, USD) per faithful item; Lean time per item.
|
||||
- *Breakdowns:* statement vs definition vs problem; algebra vs analysis etc.; short vs long; dependency on earlier context (needs earlier definition) yes/no.
|
||||
- *Test:* paired McNemar between systems; bootstrap CIs for gap.
|
||||
- *Tests H1.*
|
||||
|
||||
### E5. Human annotation protocol
|
||||
- *Label set:* faithful / minor drift / wrong-but-compiles / does-not-compile / not-formalizable.
|
||||
- *Procedure:* two Lean-literate annotators label all 600; third adjudicates disagreements; 200-item overlap for kappa; guideline with 30 worked examples; annotators see the source page crop and the Lean code, **not** model identity or filter scores.
|
||||
- *Report:* Cohen's kappa overall and per class; confusion matrix; annotation time per item (supports the provenance design).
|
||||
- *Also annotate:* the error type from the taxonomy in 5.2, and the gold source-side simplex for 150 items (to evaluate extraction of `S_T` separately).
|
||||
|
||||
### E6. Role-alignment fidelity filter (main method)
|
||||
- *Systems compared on the same core:*
|
||||
1. no filter (compile only)
|
||||
2. type-check only
|
||||
3. single LLM judge
|
||||
4. two-judge agreement (as in Beyond Compilation **[verify]**)
|
||||
5. BEq+ against a reference formalization, where one exists (ProofNet-style subset)
|
||||
6. shadow-style check on 50 hand-built items (small, illustrative)
|
||||
7. **role alignment** (ours)
|
||||
8. role alignment + judge
|
||||
- *Metrics:* precision, recall, F1 for "faithful"; ROC-AUC for alignment score; recall of "wrong-but-compiles" at fixed false-reject 10%; per-error-type recall (missing hypothesis, extra hypothesis, type, quantifier, goal); cost per item (calls, CPU).
|
||||
- *Controls:* shuffled spans (alignment must fail), identity (Lean vs its own back-translation), and judge self-preference (judge from same family as generator vs different).
|
||||
- *Quality of S_T itself:* role precision/recall of source-side extraction against the 150 gold simplices; sensitivity to extractor model.
|
||||
- *Tests H3.*
|
||||
|
||||
### E7. Slot-constrained vs free-form formalization
|
||||
- *Design:* same model, same budget, three arms: free-form; slot-filled with open choices; slot-filled with closed choices (instance classes from a Mathlib list).
|
||||
- *Metrics:* compiled %, faithful % (human on the core, filter elsewhere), error-type distribution, tokens per success.
|
||||
- *Controls:* matched number of Lean calls.
|
||||
- *Tests H4.*
|
||||
|
||||
### E8. Repair ablation
|
||||
- *Design:* repair attempts 0/1/3/5; whole-declaration vs slot-level repair.
|
||||
- *Metrics:* compiled %, faithful %, and **faithfulness-of-newly-compiled** (fraction of items that became compiling through repair and are faithful).
|
||||
- *Expectation:* compile up, faithfulness of the new compilers low (consistent with the Beyond Compilation observation that Lean feedback gains are partly unfaithful **[verify]**).
|
||||
- *Tests H2.*
|
||||
|
||||
### E9. Schema-guided retrieval and proof guidance
|
||||
- *Data:* 200 exercises with a reference statement and a dependency on at least one earlier definition or result in the same book; store built from the faithful, filtered items of the other books plus Mathlib docstrings.
|
||||
- *Arms:* no retrieval; BM25 over statements; embedding retrieval; type-index (current `search`); `find_solvable` role coverage; oracle (gold dependencies).
|
||||
- *Provers:* two open provers + one API model, pass@1 and pass@8, fixed timeout.
|
||||
- *Metrics:* retrieval recall@k of gold dependencies; proof success; steps used.
|
||||
- *Controls:* store filtered vs unfiltered (shows filtering matters downstream); store with shuffled roles (shows structure, not just text, matters).
|
||||
- *Tests H5.*
|
||||
|
||||
### E10. Contamination
|
||||
- *Procedure:* string and normalized-statement match of each item against public Lean corpora and ProofNet; evaluate E4 on the clean subset; ask models to complete the item from the title only.
|
||||
- *Report:* clean-subset deltas.
|
||||
|
||||
### E11. Cost, time and reliability
|
||||
- *Report:* tokens, USD, wall-clock and Lean time per page and per faithful item; failure counts per stage; silent-failure checks (the three faults the project found only on the server: empty-env key shadowing, container drift, overloaded `unverified`).
|
||||
|
||||
---
|
||||
|
||||
## 7. More detailed experiments (second layer, in priority order)
|
||||
|
||||
### 7.1 Role vocabulary and registry quality (S2)
|
||||
- Growth curve of distinct roles vs items; duplicate-role rate before and after the reuse-before-create rule; human judgement on 200 role pairs the registry merged and 200 it kept apart (precision/recall of dedup).
|
||||
- Effect of dedup on retrieval (E9 with and without dedup).
|
||||
|
||||
### 7.2 Nested simplices and the dependency graph (S3)
|
||||
- Build the book's dependency graph from nesting; evaluate edge precision on 100 hand-labelled dependencies; test whether context-carrying formalization (feeding already-formalized definitions) fixes the "needs earlier definition" failures seen in E4.
|
||||
|
||||
### 7.3 Analogy mining (S4)
|
||||
- Run `AnalogySchemaMiner` for N rounds; humans rate 200 proposed simplices as meaningful / forced; report acceptance rate and whether accepted simplices cover items previously degenerate (< 2 roles). Keep as optional/appendix: it must not hold up the main results.
|
||||
|
||||
### 7.4 Judge bias and cross-family control (S5)
|
||||
- Full matrix: generator family x judge family; self-preference gap; alignment extractor family x generator family.
|
||||
|
||||
### 7.5 Robustness (S6)
|
||||
- Page-image degradation (dpi, noise, rotation) vs detection and compile; prompt paraphrase robustness of `S_T` extraction (cf. robustness literature **[verify]**).
|
||||
|
||||
### 7.6 Statistical analysis plan
|
||||
- All headline rates with Wilson 95% CIs; between-system differences by paired McNemar; gap CIs by bootstrap (10,000 resamples over items, clustered by book).
|
||||
- Sample size: with 600 audited items, a proportion near 50% has about +-4 points half-width; a paired comparison with 20% discordance detects about a 6-point difference at 80% power (approximate; recompute with the observed discordance).
|
||||
- Seeds: 3 for any sampled arm; report mean +- sd; no cherry-picked seed.
|
||||
- Multiple comparisons: Holm correction across the pre-registered hypotheses H1-H5.
|
||||
|
||||
### 7.7 Cross-lingual and homogenization (S7)
|
||||
- One Chinese-language textbook: detection, OCR, compile and faithful rates vs English.
|
||||
- ACL 2027's optional theme (homogenization **[verify theme wording on the final call]**): do different models converge on the same *wrong* formalization? Measure agreement among wrong outputs across models.
|
||||
|
||||
### 7.8 Human effort (S8)
|
||||
- Time to audit an item with page-grounded span and side-by-side simplices vs. with raw PDF and Lean code only (20 items x 2 annotators, crossover).
|
||||
|
||||
### 7.9 Budget (rough, recompute after pilot)
|
||||
- Tokens: ~3k in + 1k out per formalization call; with ~1.5 calls per item average and 2,000 items per model per pass = about 9M tokens per model per pass; 5 models x 3 arms (E4/E7/E8) is about 135M tokens before judges. Judges and extraction add roughly 40%.
|
||||
- Lean: about 10-30 s per item on the 4 cpu / 14 GiB runner; 2,000 items x 5 models x 3 arms is on the order of 100-250 CPU-hours, so use more than one runner or reduce the sample for arms E7/E8 to the 600 core.
|
||||
- Human: 600 items x 2 annotators x ~3 min = 60 hours plus adjudication.
|
||||
|
||||
---
|
||||
|
||||
## 8. Work plan to 4 Jan 2027, risks, checklists
|
||||
|
||||
### 8.1 Timeline
|
||||
| Weeks | Dates | Work | Exit gate |
|
||||
|---|---|---|---|
|
||||
| 1-2 | 21 Oct - 3 Nov | Fix `unverified` label, `source_pages`, incremental storage; port simplex (5.7); E0; choose books and confirm licences; annotation guideline | E0 >= 95% |
|
||||
| 3-4 | 4 - 17 Nov | Ingest all books (E1); build annotator tooling; recruit annotators; pilot 50 items | pilot kappa >= 0.6 |
|
||||
| 5-6 | 18 Nov - 1 Dec | E2, E3, E4 runs; start labelling core | E4 table done |
|
||||
| 7-8 | 2 - 15 Dec | E5 labelling finished; E6, E7, E8; **go/no-go 8 Dec** | role alignment beats single judge on at least two error types, or fall back to an evaluation paper |
|
||||
| 9-10 | 16 - 29 Dec | E9, E10, E11; second-layer (7.1, 7.4) if time; figures | all main tables frozen 24 Dec |
|
||||
| 11 | 30 Dec - 3 Jan | Writing polish, checklist, artifact package, submit ARR by 3 Jan | submitted |
|
||||
Writing starts 1 Dec in parallel; related work and method sections can be drafted now.
|
||||
|
||||
### 8.2 Risks
|
||||
| Risk | Likelihood | Mitigation |
|
||||
|---|---|---|
|
||||
| Role alignment does not beat LLM judges | medium | Position as complementary and cheaper, with error localization; paper becomes evaluation + taxonomy |
|
||||
| Annotators unavailable / slow | medium | Shrink core to 400; keep 150-item overlap; use project members for pilot |
|
||||
| Archived simplex code needs more rework than planned | medium | Re-implement the minimal Role/Simplex/State in `leanbench/` rather than porting everything; analogy miner stays optional |
|
||||
| Compute for Lean at scale | medium | Second runner; reduce arms to core; cache by `sha1(code)` |
|
||||
| Licensing blocks release | medium | Open books only; hashes-only for others |
|
||||
| Concurrent work (2606.31002, 2608.29270) overlaps | high | Cite and compare directly; emphasise PDF-to-Lean pipeline, provenance and role-level localization; recheck arXiv weekly until submission |
|
||||
| Dates shift | low-medium | ICML/NeurIPS dates are projected; recheck CFPs monthly |
|
||||
|
||||
### 8.3 ACL / ARR checklist
|
||||
Limitations section (LLM dependence of `S_T`, one formal system, few books, annotator expertise); Responsible NLP checklist (compute, licences, annotator pay and instructions); data statement for the release; reproducibility package (pinned image, prompts, seeds, scripts); no author-identifying text in artifacts; anonymized repository for review.
|
||||
|
||||
### 8.4 Deliverables
|
||||
`docs/research-plan.md` (this file); registry + projection + alignment code with tests; annotation tool; dataset release package (licence-clean); paper draft.
|
||||
|
||||
---
|
||||
|
||||
## 9. Sources checked on 2026-10-21
|
||||
- ACL 2027 site: ARR 4 Jan 2027; Kyoto 20-22 Aug 2027.
|
||||
- NAACL 2027 call (ARR 12 Oct 2026, closed); ICLR 2027 call (25 Sep 2026, closed); CPP 2027 page (10 Sep 2026, closed); ITP 2027 site (Glasgow, early Aug 2027, deadlines pending).
|
||||
- Aggregators (unofficial, projected): ICML 2027, IJCAI 2027, COLM 2027, NeurIPS 2027.
|
||||
- Literature: [ProofNet](https://arxiv.org/pdf/2302.12433); [Poiroux et al.](https://arxiv.org/abs/2406.07222); [FormalAlign](https://arxiv.org/pdf/2410.10135); [Beyond Compilation](https://arxiv.org/abs/2606.31002); [ShadowBench](https://arxiv.org/abs/2608.29270).
|
||||
- Local: `lean-bench` repo, `runs/p85-110`, `archived/schema-simplex`.
|
||||
|
||||
Reference in New Issue
Block a user