[Evaluation]: Jacobian is available but unused across a four-case conjecture canary

[yuelgrace1810-ops]

Area

Agent evaluation, MCP tool discovery, recently solved conjecture reliability.

Reproduction

A frozen four-case canary was run with gpt-5.6-terra at low reasoning under three conditions:

1. no Jacobian;
2. ordinary Jacobian availability;
3. the same Jacobian surface plus a frozen 99-word selective operation-grounding card.

Prompts, sandbox, unified-exec mode, timeouts, and model configuration were otherwise held fixed.

Jacobian treatment fixture:

• revision: fb33f6f471ab8044186501bc2626e9f32a024c0b
• policy: COMPUTE_VERIFY_NO_RETRIEVAL
• bundled independent checkers installed
• 329 capabilities
• reasoning log off

The MCP server logs show successful initialization, tool listing, and clean session shutdown for every treatment session. There were no transport or checker-readiness failures. The ordinary condition is therefore available but unused, not the transport failure previously tracked by #406/#435.

Observed result

Metric	No Jacobian	Ordinary Jacobian	Selectively grounded Jacobian
Runs	4	4	4
Runs discovering Jacobian	—	0/4	4/4
Jacobian calls	—	0	26
Correct headline conclusions	4/4	4/4	4/4
Fully correct required intermediate certificates	3/4	3/4	4/4
Total wall time	159.6 s	186.7 s	178.0 s
Input tokens	232,327	351,875	683,196
Uncached input tokens	31,623	63,363	70,844

The ordinary treatment used shell or built-in computation instead of math.find/math.run in every case, despite prompts requesting independent verification when suitable tooling was available.

The bunkbed case demonstrates why final-scalar scoring is insufficient. With edge order (a₀b₀,b₀b₁,b₁a₁,a₁a₀):

• state 0011 connects a₀ to b₁ through a₀–a₁–b₁;
• state 0110 leaves a₀ isolated.

The no-Jacobian answer swapped these two rows. The ordinary-Jacobian answer compressed 0000–0110 into a row declaring both pairs disconnected, which incorrectly includes 0011. Both nevertheless reported the correct aggregate scalars 9/16 and 7/16. The selectively grounded run printed the fully correct 16-state certificate, but its three graph-reliability calls failed input validation; the certificate was completed manually and was not tool-verified.

Interpretation boundary

This is one repetition per case and does not estimate a stable treatment effect. It establishes:

• a concrete post-Make math.find and math.run the canonical MCP surface #511 available-but-unused reproduction across four independent workflows;
• a 0/4 to 4/4 discovery change under a bounded guidance intervention;
• one certificate-correctness improvement that scalar-only grading would miss;
• substantial context cost: the grounded condition used 2.24× the no-Jacobian uncached tokens and 1.12× the ordinary-treatment uncached tokens.

It does not identify tool names, initialization guidance, unified-exec presentation, model policy, or prompt wording as individually causal. The third condition is a prompting intervention, not SFT/RL and not a replication of arXiv:2608.00326.

This overlaps with the evaluation question left open when #505 was closed, but does not reopen its shipped contract. It is related to #503 but is not a name-only experiment.

Recommended next step

Do not change the public MCP contract from this pilot alone. Repeat the ordinary and grounded conditions on transformed/held-out variants and add a negative control. Score:

• discovery before shell fallback;
• successful discovery-to-execution continuation;
• exact checker use;
• final and intermediate certificate correctness;
• irrelevant/repeated calls;
• input/uncached tokens and elapsed time.

Any routing change should preserve the observed certificate-correctness gain while reducing search calls and context. Tool invocation itself must not be rewarded.

[yuelgrace1810-ops]

Follow-up held-out evidence (2026-08-08):

A second four-case suite covered Boolean-cube extremal search, Bruhat/polynomial support, a matroid Tutte counterexample, and a Gröbner-basis slice. Same model (gpt-5.6-terra, low reasoning), fresh contexts, same frozen Jacobian revision.

After correcting one experiment-fixture omission (the Merino–Welsh prompt said formulas were supplied but had omitted them) and selectively rerunning only that case:

• ordinary Jacobian: discovery in 0/4 runs;
• 99-word selective-grounding card: discovery in 4/4 runs;
• cumulative across both independent four-case suites: ordinary discovery 0/8 versus grounded discovery 8/8;
• headline and required finite invariants in this second suite: 4/4 in control, ordinary, and grounded conditions;
• second-suite aggregate input tokens: control 154,540; ordinary 155,123; grounded 608,323 after replacing the invalid fixture run;
• wall time: control 193.9 s; ordinary 211.2 s; grounded about 260.4 s after the same replacement.

The grounding intervention therefore transfers strongly for discovery, but still has a large context cost and did not improve final correctness on the second suite. Tool use itself remains unscored.

Trajectory detail also matters: on the Stillman case the grounded model found and inspected the correct Gröbner capability, then made four invalid calls because two sparse polynomial term lists were not in descending lexicographic order. The operation failed closed, and the model still completed correctly by hand. That diagnostic friction is being handled as a separate localized contract-message fix; it is not evidence for changing the routing architecture proposed here.

This strengthens the issue’s evidence from one suite to two independent suites. The next routing experiment should preserve selective search but reduce catalog/contract bytes and stop after a clear unavailable/incompatible route.

[yuelgrace1810-ops]

Correction to the telemetry in my preceding follow-up comment:

The omitted-formula Merino–Welsh fixture affected all three conditions, so all three original Merino cells must be excluded and replaced by the corrected-prompt reruns. The symmetric corrected second-suite totals are:

• control: 170,396 input tokens, about 211.9 s;
• ordinary Jacobian: 169,324 input tokens, about 210.8 s;
• grounded Jacobian: 608,323 input tokens, about 260.4 s.

The qualitative conclusions are unchanged:

• second-suite ordinary discovery 0/4 versus grounded 4/4;
• cumulative ordinary discovery 0/8 versus grounded 8/8;
• second-suite mathematical correctness 4/4 in every corrected condition;
• no successful relevant math.run in the second suite;
• no second-suite correctness benefit, with materially higher grounded context cost.

The external runner is also being strengthened to archive prompt-overlay bytes and bind each effective prompt digest, preventing this accounting/provenance ambiguity in future runs.

[yuelgrace1810-ops]

One further current-main correction: merged PR #818 (enrich-domain-validation-diagnostics) already addresses the Stillman recoverability problem on current main.

Replaying the exact malformed payload at current main now returns:

• path: generators/0/polynomial
• hint: polynomial terms must use descending lexicographic order

The original frozen evaluation revision returned only the generic Use canonical sparse QQ polynomials and inspect the operation limits. hint. Therefore I will not publish the locally prepared polynomial diagnostic branch; it would duplicate merged work.

The same replay also shows that #818 makes the earlier graph-reliability failure actionable (path=graph, hint naming ordered declared endpoints), so that local draft fix is likewise being withheld as superseded.

The next useful test is behavioral: compare recovery under the frozen generic diagnostic versus current-main enriched diagnostics, rather than add more diagnostic code.

[yuelgrace1810-ops]

Behavioral follow-up for merged PR #818 is complete.

A six-case sparse-polynomial recovery A/B compared the frozen generic diagnostic with current-main enriched diagnostics:

• canonical unchanged request: 1/1 success in both;
• first corrected execution valid: 4/4 in both;
• safe GF(5) unsupported-domain stop: 1/1 in both;
• unsupported VERIFIED claims: 0/6 in both;
• model-visible MCP calls: generic 7, enriched 5;
• input tokens: generic 317,775, enriched 264,943;
• wall time: about 105.6 s versus 81.9 s (directional only).

On the five malformed/unsupported cells, enriched diagnostics reduced calls 6→4 and input tokens 254,614→218,429 (~14.2%). The benefit came from avoiding two extra contract lookups; validation, mathematics, assurance, and fail-closed stopping were unchanged.

Conclusion: #818 already resolves the localized recovery issue. No additional diagnostic PR will be opened. This reinforces the broader routing recommendation: measure useful execution and safe stopping separately from discovery, and avoid rewarding calls themselves.

[yuelgrace1810-ops]

New positive-path held-out evidence (2026-08-08), using a published counterexample rather than an authored toy fixture:

Case. Brent–Yedidia Conjecture B, order-22 circulant from arXiv:1801.00399. The exact displayed matrix has determinant -216409254831025; its magnitude exceeds the paper's binary extreme-point maximum 2^21 * 102546588 = 215055782117376 by 1353472713649. The matrix/value were independently preflighted with clean-room Bareiss and Python-FLINT.

Control vs selectively grounded Jacobian (gpt-5.6-terra, low reasoning, identical effective task prompt):

• final mathematics and theorem scope: correct in both;
• control: 0 MCP calls, 118,602 input tokens, 59.0 s;
• grounded: 7 MCP calls (5 math.find, determinant compute + verify), 278,913 input tokens, 47.9 s;
• grounded completed the exact producer→independent-checker chain and bound verification to the full inline 22×22 matrix;
• control recomputed the scalar with local scripts, but used the label VERIFIED for its own second calculation without an operator-authorized verification record. The grounded run correctly distinguished COMPUTED from VERIFIED.

This is the first held-out case in these conjecture evaluations where grounded Jacobian both executed the relevant producer/checker successfully and improved assurance correctness, while also reducing elapsed time by about 11.1 s. The cost remains substantial: 2.35× input tokens and five discovery/contract calls. One final math.find for elementary integer product/difference occurred after determinant verification and was unnecessary.

Interpretation: this supports #845's existing routing/context-efficiency scope; it does not justify a new issue or capability. The desirable outcome is now clearer: preserve the successful exact compute→verify path and assurance benefit while reducing discovery/contract traffic and post-terminal search.

[yuelgrace1810-ops]

Three-arm cross-family follow-up (2026-08-08): exact terminal reliability for the Gladkov–Pak–Zimin bunkbed proof gadget (G_6), an 11-edge bounded instance of Lemma 5.1.

Same model/settings and frozen task prompt:

• control: correct (1365/2048), 0 calls, 153,721 input / 17,273 uncached tokens, 69.8 s;
• ordinary Jacobian availability: correct (1365/2048), 0 calls, 198,859 input / 17,099 uncached tokens, 88.4 s;
• selective-routing card: correct (1365/2048), 7 calls (5 discovery/contract, graph-reliability compute, rational-identity verify), 242,282 input / 35,690 uncached tokens, 61.1 s.

The routed run successfully exhausted all 2,048 edge subsets and returned 1,365 connecting states. It correctly kept that graph result at COMPUTED because the installed portfolio has no claim-bound graph-reliability checker, while labeling only the separately checked rational identity VERIFIED.

This adds cross-family evidence for the issue's core routing result: ordinary availability was ignored, while explicit selective routing produced genuine useful execution. It did not improve final correctness here; all three answers were correct. Context remains the weakness: the routed transcript exposed about 855,769 serialized MCP-result bytes, dominated by five discovery/contract responses and the complete 2,048-state ledger.

Important correction to the preregistration: graph reliability currently has a producer but no independent checker. Therefore this is not a full producer→checker success like the prior determinant case, and it does not establish a new capability gap from one case. No duplicate issue or PR is being opened.

[yuelgrace1810-ops]

Additive weak-model evidence: routed tool use can remain subproblem-incomplete

A fresh held-out gpt-5.4-mini/low-reasoning comparison used Hu–Zhang's 2026 Xin–Zhang tridiagonal determinant conjecture at n=9, t=37. The frozen prompt required two independent subproblems: (1) construct C=29I-T and compute/verify det(C); (2) independently evaluate ∏_{i=1}^8 (29-i(8-i)) and compare.

• Control: exact matrix, determinant 10335717392, factors 22,17,14,13,14,17,22,29, and equality were all correct.
• Selectively routed Jacobian: correctly discovered and completed matrix.determinant.compute → matrix.determinant.verify, obtaining an authorized VERIFIED determinant for the exact matrix. It then manually mis-evaluated the product as factors 28,25,20,13,4,-7,-20,29, product 2263840000, and falsely concluded that the published specialization disagreed.

Treatment telemetry: 4 MCP calls (2 find, compute, verify), 40,496 visible MCP-result bytes, 101,599 input / 12,767 uncached tokens, 64.14 s. Control: 60,882 input / 4,178 uncached tokens, 39.46 s.

This is not a determinant/checker defect: the exact bound determinant was correct and independently accepted. It is new evidence that successful routing to one operation does not guarantee decomposition/routing of every exact subproblem needed by the final claim. The evaluation rubric must therefore score terminal cross-checks and subproblem coverage, not merely whether any producer/checker chain completed. No duplicate issue or code change is proposed from this one cell.

Persistent result ledger: outputs/xin-zhang-tridiagonal-weak-model-result-20260808.md (local audit workspace).

[yuelgrace1810-ops]

Additive weak-model evidence: successful verification can bind the wrong mathematical object

A gpt-5.4-mini/low-reasoning point-input variant of the Solymosi–Perles seven-point incidence case exposed a wrong-input assurance failure. This run is not independent source evidence: after execution, the shared-workspace inventory showed that the same theorem/artifact lineage had already been evaluated with a dual-line prompt. It is retained only as a prompt-variation trajectory and excluded from treatment-effect aggregates.

The task supplied seven rational projective points and asked for their complete collinearity ledger, allowing point–line duality. The selectively grounded arm:

• found the projective line-arrangement materializer on its first search;
• inspected both producer and verifier contracts;
• manually computed the correct six triples, three ordinary pairs, histogram {2:3,3:6}, and pair closure 21=C(7,2);
• then passed the six primal collinearity lines, rather than the seven dual lines (one per supplied point), to the materializer;
• obtained a legitimate operator-authorized VERIFIED record for that different six-line arrangement; and
• incorrectly claimed the requested seven-point audit was VERIFIED and bound to “the supplied dual line coefficients above.”

The operation and checker behaved correctly. Their contracts and scope identify the exact supplied line arrangement, and there were no invalid calls, retries, or execution failures. Classification is model mathematical translation / evidence-binding failure, not a repository checker defect.

Telemetry: 5 calls (3 math.find, 2 math.run), 32,246 visible result bytes, 33,715 argument+result bytes, 118,127 input tokens, 60.227 s. The no-Jacobian control returned the same correct finite mathematics and conservatively labeled it COMPUTED.

This strengthens the issue’s existing rubric recommendation: successful producer→checker execution is insufficient. Before awarding VERIFIED, scoring should mechanically require that the operation input matches the expected mathematical object count and canonical identifiers, and that the verification record descends from that exact input. No new capability or interface proposal is justified from this duplicated lineage.

Persistent local ledger: outputs/solymosi-perles-point-input-duplicate-result-20260809.md.

[yuelgrace1810-ops]

Independent current-main replication from a distinct finite-extension-field domain:

• Source: Niedbala Giraudin, arXiv:2607.15305v2 (2026), explicit Carlitz–Wieferich quintic over F_(19^3).
• Model: gpt-5.4-mini, low reasoning; frozen no-Jacobian control versus selective-grounding treatment.
• Both arms correctly reproduced the full bounded certificate: the prime-degree Rabin irreducibility conditions, F_4=0 modulo P, exact input digest, and the v2 scope correction (no gcd-equality claim).
• Control: 118.12 s, 0 MCP calls, 130,153 input tokens (109,696 cached).
• Grounded: 124.81 s, 8 math.find calls, 0 math.run calls, 297,531 input tokens (267,904 cached).
• Delta: +6.69 s and +167,378 input tokens, with no correctness, certificate, or assurance gain.

The grounded trajectory kept widening searches and inspecting adjacent prime-field modular-polynomial contracts even though none accepted extension-field coefficients. It ultimately computed the certificate locally and accurately reported that no Jacobian artifact or verification record was produced.

This supports #845's routing/context-cost concern in a new domain: successful discovery can correctly expose a portfolio boundary, but repeated contract discovery after that boundary is already clear adds large context without advancing to execution. This is not evidence of an unsound operation or a missing one-off theorem helper.