scribe judge (SOUND / UNSOUND / UNDETERMINED) + best-of-n sampling#17
Merged
Conversation
scribe judge --gadget <toml>: the verdict engine as one command. Prover runs first (a kernel-accepted proof settles the question and sound gadgets usually prove in 1-2 iterations); only on exhaustion does the adversarial refuter run. Verdicts carry kernel-checked artifacts and STABLE documented exit codes so third parties can script judge in their own CI: 0 SOUND / 1 UNDETERMINED / 2 UNSOUND / 3 infrastructure error. Best-of-n sampling (--samples-per-iter K on judge, verify, refute, proof-pilot, and halva-bridge): K attempts per iteration, kernel filters. Design per review amendments: - Replay determinism preserved: the journal records EVERY candidate (CandidateRecord: response, status accepted/build_failed/patch_rejected/ duplicate/not_tried, build output) plus the acceptance index; --replay applies source_after states as before, and pre-best-of-n transcripts load unchanged (serde defaults, round-trip tested). - Candidates are hash-deduplicated before the build phase (low-temperature samples collapse to identical proofs; builds dominate cost) and tried shortest-first, ties broken by sampling order for determinism. - Sampling is concurrent (Backend now Send + Sync; scoped threads), builds sequential with early exit; feedback on total failure is the LAST tried candidate's error, matching the file state on disk. - Lake-build mode only; LSP mode warns and samples once. Live validation: judge(boolean-check, samples-per-iter=2) → SOUND exit 0 at iteration 1; judge(zero-indicator negative) → prove exhausts, refuter finds the counterexample at iteration 1 → UNSOUND exit 2. 8 new tests (planner dedupe/ordering/reject paths, old-journal compat, judge and refute arg parsing); workspace green; clippy clean.
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 265889203b
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| }; | ||
|
|
||
| // ── Phase 1: prove ─────────────────────────────────────────────────────── | ||
| let prove_scaffold = lean_emit::emit_lean(&gadget).unwrap_or_else(|e| { |
There was a problem hiding this comment.
When scribe judge --gadget is run on a gadget TOML without soundness_spec, this phase calls emit_lean, whose existing fallback emits a theorem with conclusion True; an LLM can close that trivial scaffold and the command exits SOUND even though there was no spec to judge. The refuter path already treats this as MissingSpec, so judge should check gadget.soundness_spec before starting the prover or use an emitter that requires it.
Useful? React with 👍 / 👎.
…ss under partial sampling failures Review findings on #17: - High: make_backend (and require_api_key) exited 1 internally on missing keys/URLs/unknown backends, so 'scribe judge --backend anthropic' without ANTHROPIC_API_KEY exited 1 — violating judge's documented exit-3 infrastructure contract. make_backend now returns Result and the CALLER owns the exit code: judge exits 3, verify/refute/demo/proof-pilot/halva-bridge keep their documented 1. Verified: judge → 3 (missing key and unknown backend), refute → 1. - Medium: partial concurrent-sample failures were filtered out before planning, so candidate records omitted them and sample_index/accepted_sample no longer referred to the original K requested samples. plan_candidates now consumes the raw Result vector: failed requests are recorded in place with status "request_failed" (error in build_output, empty llm_response) and surviving candidates keep their original indexes. 'The journal records every candidate' now includes sampling failures; new unit test pins it.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The verdict engine as one command, plus kernel-filtered sampling — built to the three review amendments.
scribe judge
scribe judge --gadget benchmark/suite/02-boolean-check.toml # SOUND: lean/ZkGadgets/Bench/Judgeboolean_check.lean (exit 0)Prover first (a kernel-accepted proof settles the question; sound gadgets prove in 1–2 iterations, so this order minimizes expected cost) — refuter only on exhaustion. Stable, documented exit codes for third-party CI (amendment 3):
Best-of-n (
--samples-per-iter Kon judge/verify/refute/proof-pilot/halva-bridge)CandidateRecord: response, statusaccepted/build_failed/patch_rejected/duplicate/not_tried, build output) plus the acceptance index.--replayappliessource_afterstates exactly as before; pre-best-of-n transcripts load unchanged (serde defaults, round-trip tested).Backendis nowSend + Sync; scoped threads); builds are sequential with early exit, so success costs one build. On total failure the feedback is the last tried candidate's error, matching the file left on disk. Lake-build mode only; LSP mode warns and samples once.Live validation (claude-sonnet-5)
judge boolean-check --samples-per-iter 2→ SOUND, exit 0, iteration 1 (concurrent sampling exercised for real)judge zero-indicator(planted is-zero bug) → prove exhausts → refuter finds the counterexample at iteration 1 → UNSOUND, exit 28 new tests; workspace green; clippy clean. Per the sequencing note: this lands before the crates.io extraction so proof-pilot's 0.1 API ships with
--samples-per-iter.