Repository navigation
Add a semantic review skill for Formal Conjectures - #4899
williamjblair wants to merge 26 commits into
Conversation
|
#4810 is already nearly ready to submit, so its PR may precede the new workflow. I’m still happy to pilot the workflow on it if the timing works; otherwise I can use it on my next formalization. |
|
All good @bocowgill, feel free to try out on the next formalization. We can treat this as a WIP and get some more feedback before considering merging to main |
70e8ddf to
23b836a
Compare
williamjblair
changed the title
a83f3d2 to
9050d79
Compare
A second-pass semantic review for Formal Conjectures pull requests. It answers one question, whether the Lean statement says what its cited source says, and leaves style, naming and imports to CI and AGENTS.md. The default path is one pass: bind the scope, run the focused build, read the cited source, compare meanings, report or stop. Escalation has named triggers, so the expensive work (whole-document reads, cross-references, Lean witnesses, history) runs when something calls for it rather than on every file. Findings carry a witness, what that witness shows and does not show, and the smallest proposed change. The output is publishable to GitHub as-is, and the review is advisory: it does not approve, merge, label, or touch a contributor branch. evals/evals.json records the measurement history, including a three-arm run against no skill and against an earlier version of this skill, over eight cases built by reverting merged fixes onto main. This skill matches the unaided reviewer's cost and wall clock, catches a case the unaided reviewer misses, and files a quarter as many items. The false-positive control returns CLEAN with no findings, where both other arms file nits. That run also records the measure the earlier iterations lacked. A suite where every case has a planted defect rewards recall and charges nothing for a finding that should not have been filed, so the file now reports findings filed alongside pass rate.
7850c34 to
75b35e7
Compare
The monolithic defect-classes reference becomes four rubric files - _common, source-fidelity, statement-soundness, metadata-hygiene - the shape TauCetiProject/TauCetiReview uses, so a finding names the kind of defect it is, coverage is checkable per angle, and the rubrics could be judged independently by a runner without rewriting them. SKILL.md's compare step routes through the angles; the fast path is otherwise unchanged. The restructure initially regressed exactly the verification behaviours the assertion hardening of iterations 9-11 exists to detect, and the eval loop caught and repaired it: witnesses are checked rather than argued, escalation is mandatory for any verdict-setting finding, a source construction runs as a positive control when faithfulness rests on it, and a formal_proof root link stays a finding even after private resolution. Post-fix runs restore the ceiling on both active cases, 9/9 on 940 and 8/8 on ClaudesCycles, with each rule attributable to the single assertion it flipped. iteration_16 records the loop.
|
Restructured toward the shape The eval suite earned its keep on the way: the restructure initially regressed exactly the verification behaviours the iteration 9–11 assertion hardening exists to detect (witnesses argued rather than checked; no positive control; a root |
| Use the workflow's isolated scratch tools when supplied. Otherwise, keep the witness outside | ||
| the source tree and import the module under review in the trusted execution environment: | ||
|
|
||
| ```bash |
There was a problem hiding this comment.
Maybe also worth mentioning that the review should collect cache first - otherwise in my experience it's quite common to get agents that just rebuild all of mathlib
| description: Use this skill for semantic review of Formal Conjectures statements against their cited mathematical sources, including suspected misformalisation and contested review findings. Check meaning and the support for proof or status claims. Do not use it solely for Lean build errors, proof search, formatting, or operating the review-report tooling. | ||
| license: Apache-2.0 | ||
| --- | ||
|
|
There was a problem hiding this comment.
I think this skill is quite close to being mergeable independently. What do you think of splitting it off from the rest of this PR so we can review and merge the rest (eval harness) separately?
williamjblair
changed the title
|
Thanks Paul! Added the cache step and moved the eval harness to #6869 so the skill can be reviewed on its own. Both builds are passing now. |
mo271
left a comment
mo271
left a comment
There was a problem hiding this comment.
Thanks for taking a stab at this!
My very general feeling is that this is not really needed, at least at this level of detail given the capabilities of current models and there might be some cost of having those files directly in the repo.
However, given that it would be fantastic to have more help with the reviews , so I am open to get this merged quickly (or let @Paul-Lez handle it).
I would prefer more concise and minimal SKILLs that focus on non-obvious aspects.
Also it is not clear to me why there should be different SKILLS/instructions for reviewing versus creating a contribution in principle. it seems like the automatic review prompt should mainly be "check if the guides on how to foramlise a problem were followed." So everything in these skills here (except for maybe checking out a pr (which shouldn't need explicit instruction anyway) and checking the proofs in a formal_proof link), should perhaps rather be part of AGENTS.md or some other place?
| If removal refuses because the worktree has changes, preserve or inspect them; do not force it. | ||
| Report final-file line numbers rather than patch offsets. If the PR cannot be resolved, report | ||
| that scope as INCOMPLETE rather than silently reviewing a different revision. | ||
|
|
There was a problem hiding this comment.
here I feel like a halfway capable model knows exactly how to check out files, how to use git worktree or tmp dir and can decide on its own how to do this best. These instruction seem to specific and might actually do some harm in some setups? It seems like they have been extracted not because those are the best way of doing things, but rather because the model that wrote them is doing it this way
|
|
||
| This checks that `<RHS>` can be passed to that implication. It does not recover the original | ||
| answer hole or prove exact correspondence of the complete declaration. For that, use an | ||
| available FC exporter that preserves answer annotations and checks the extracted type in Lean. |
There was a problem hiding this comment.
also seems overly specific, and answer(sorry) for Prop valued sorry is going away soon anyhow
| source's `P` is vacuous the slot is forced to `True`, so `answer(False)` is unstatable. | ||
| The linter does not see section variables (#1407); read the binders off the elaborated | ||
| statement. *LatinSquare* (confirmed): two declarations picked up `variable {n : ℕ}` | ||
| and `Odd n → …` is vacuous at even `n` (#5009, #5060). |
This branch has not been deployed
4 participants
Adds an advisory skill for comparing Lean statements with cited sources, checking statement meaning and proof/status claims, and reporting findings and coverage gaps. Includes focused rubrics, Lean checking references and an AGENTS.md link. Maintainers decide acceptance.
Manual review setup fetches the pinned Mathlib cache with
lake exe cache getfrom the reviewed project root after pinning the checkout and before Lean builds or scratch checks. Cache failures remain explicit; builds cover only affected modules.The review-report tools, evaluation harness and frozen fixtures are preserved separately in draft #6869. This PR contains only the skill and its documentation; no CLI or model-authentication setup is required.
Validation: skill validation passes; all 16 local documentation links resolve; all six shell examples parse; whitespace checks pass. No Lean modules change, so Lean builds and cache downloads were not run for this documentation split.
Merge order: this PR and metadata #5375 are independent; the harness draft #6869 depends on this PR. Roadmap: #4394. Supersedes #5341.