Add proof-from-scratch evaluator contract by munimthahmid · Pull Request #71 · specula-org/tlaps-bench

munimthahmid · 2026-07-21T05:11:36Z

Important

This remains a draft until the proof-from-scratch generator emits manifest.json and the editable-region markers. Runs fail closed without that producer-side contract.

What changed

Make the manifest the sole source of proof-from-scratch task discovery and context, with strict validation and no heuristic fallback.
Restrict agent edits to marked helper and proof regions, preserve the remaining scaffold byte-for-byte, and reject forbidden or unproved helper declarations.
Keep context files read-only during execution and grade the submitted target against a fresh canonical context that was never exposed to the agent.
Apply the same contract to one-shot responses and continuation rounds, and update the prompts and usage documentation.

munimthahmid · 2026-07-27T19:02:14Z

@sukanya1426 Can you also review this PR when you get a chance? Since #80 depends on it, we should make sure both PRs stay in sync.

sukanya1426 · 2026-07-27T19:07:48Z

Sure.

sukanya1426 · 2026-07-28T08:34:03Z

+            context_paths.append(context_path)
+
+        resolved_paths = tuple(context_paths)
+        _validate_module_files(task_key, ((task_key, task_path), *context_entries))


The validator checks paths, symlinks, duplicate basenames, and module names, but it never verifies that the context covers the task's full EXTENDS/INSTANCE closure. I tested this by removing a context module, and the run ended up as [SANY-INVALID] / GATES-FAILED: A, identity, so a generator bug gets scored as agent tampering. Since the manifest is now the only source of context, it should validate the closure here and raise ManifestError instead.

sukanya1426 · 2026-07-28T08:34:33Z

+
+        resolved_paths = tuple(context_paths)
+        _validate_module_files(task_key, ((task_key, task_path), *context_entries))
+        boundaries[task_key] = TaskBoundary(


Another small improvement: call parse_editable_regions while loading tasks. Missing markers currently slip through loading and only surface as an exit-3 ERROR during grading. Better to catch them early.

sukanya1426 · 2026-07-28T08:36:41Z

            if not cut_short:
+                grading_canonical_dir = run.canonical_dir
+                if getattr(mode, "canonical_replay_required", False):
+                    grading_canonical_dir = _make_canonical_dir(


This snapshot is taken after the agent finishes and reads from item.benchmark_path in the repo. In --no-container mode the agent has host write access, so it can edit the source and the "fresh" snapshot picks up the tampered bytes, which also feeds get_baseline_text, so nothing independently catches it. Take it once before _run_backend_with_retries and reuse it for grading.

Good catch. Fixed. In --no-container mode, we now save the original target and context files in memory before starting the agents. I

sukanya1426 · 2026-07-28T08:37:58Z

+    return staged_file
+
+
+def check_editable_region_integrity(filepath, benchmark_dir):


Byte exact comparison means even a trailing newline at EOF or a CRLF rewrite gets flagged as CHEAT-DETECTED, scaffold_unchanged (gate A). I confirmed both cases. _reconstruct_marked_solution already treats these as harmless retyping for one-shot, but agentic backends don't. We should either normalize line endings and trailing newlines before comparing, or give these their own non-cheat reason code. Otherwise, editor noise will inflate the reported cheating rate.

sukanya1426 · 2026-07-28T08:43:18Z

+            return False
+        return resolved in self._boundaries_by_path
+
+    def get_benchmark_files(self, filter_pattern: str | None = None) -> list[str]:


main() calls this at runner.py:1721 with no try/except, so a missing or malformed manifest escapes as a raw ManifestError traceback and never reaches the parser.exit(2, ...) handling on the next line. Catch it in main() or handle it here, so the user gets an error message instead of a stack trace.

sukanya1426 · 2026-07-28T14:43:55Z

+
+    if submitted_regions.fixed_segments != canonical_regions.fixed_segments:
+
+        def normalize_format(regions):


One thing I noticed is that this only handles a single trailing newline, so the common case of an editor adding a newline still gets reported as SCAFFOLD_MODIFIED/CHEAT-DETECTED. Switching to suffix = suffix.rstrip("\n") fixes that without affecting real scaffold modifications.

Fixed. Extra newlines at EOF are now ignored.

sukanya1426

Seems alright now. Thanks for addressing the issues. Over to @Qian-Cheng-nju , can you please take a look and validate ?

Qian-Cheng-nju · 2026-07-29T10:30:28Z

LGTM!

munimthahmid changed the title ~~WIP: Add proof-from-scratch evaluator contract~~ Add proof-from-scratch evaluator contract Jul 24, 2026

munimthahmid added 5 commits July 24, 2026 21:48

Add proof-from-scratch boundary contract

8ab826f

Use manifest for proof-from-scratch tasks

123c282

Isolate proof-from-scratch context files

ea796aa

Grade proof-from-scratch on canonical context

0b7d1de

Enforce proof-from-scratch helper policy

d4a3905

munimthahmid force-pushed the feat/proof-from-scratch-evaluator branch from 884ce5b to d4a3905 Compare July 24, 2026 15:52

Fix proof-from-scratch boundary edge cases

87069dc

sukanya1426 mentioned this pull request Jul 27, 2026

Add proof-from-scratch layered generation #80

Merged

munimthahmid marked this pull request as ready for review July 27, 2026 19:01

sukanya1426 suggested changes Jul 28, 2026

View reviewed changes

Harden proof-from-scratch grading

31874c9

munimthahmid force-pushed the feat/proof-from-scratch-evaluator branch from 71792cd to 31874c9 Compare July 28, 2026 10:29

munimthahmid requested a review from sukanya1426 July 28, 2026 10:34

sukanya1426 reviewed Jul 28, 2026

View reviewed changes

Ignore extra proof scaffold EOF newlines

b763d90

munimthahmid requested a review from sukanya1426 July 28, 2026 15:17

sukanya1426 approved these changes Jul 28, 2026

View reviewed changes

Require canonical replay for public checks

bbab8f7

Qian-Cheng-nju merged commit 69eeca3 into specula-org:main Jul 29, 2026
1 check passed

		return staged_file


		def check_editable_region_integrity(filepath, benchmark_dir):


		if submitted_regions.fixed_segments != canonical_regions.fixed_segments:

		def normalize_format(regions):

Uh oh!

Conversation

munimthahmid commented Jul 21, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

What changed

Uh oh!

munimthahmid commented Jul 27, 2026

Uh oh!

sukanya1426 commented Jul 27, 2026

Uh oh!

sukanya1426 Jul 28, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

sukanya1426 Jul 28, 2026

Choose a reason for hiding this comment

Uh oh!

sukanya1426 Jul 28, 2026

Choose a reason for hiding this comment

Uh oh!

munimthahmid Jul 28, 2026

Choose a reason for hiding this comment

Uh oh!

sukanya1426 Jul 28, 2026

Choose a reason for hiding this comment

Uh oh!

sukanya1426 Jul 28, 2026

Choose a reason for hiding this comment

Uh oh!

sukanya1426 Jul 28, 2026

Choose a reason for hiding this comment

Uh oh!

munimthahmid Jul 28, 2026

Choose a reason for hiding this comment

Uh oh!

sukanya1426 left a comment

Choose a reason for hiding this comment

Uh oh!

Qian-Cheng-nju commented Jul 29, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

munimthahmid commented Jul 21, 2026 •

edited

Loading

sukanya1426 Jul 28, 2026 •

edited

Loading