|
32 | 32 | ) |
33 | 33 |
|
34 | 34 | MATH_FIND_DESCRIPTION = """\ |
35 | | -Use this when a task may benefit from a specialized exact mathematical operation, even |
36 | | -if shell code could also calculate the answer. Relevant outcomes include matrix |
37 | | -determinants, polynomial or symbolic computation, structural analysis, examples or |
38 | | -counterexamples, bounded search, formal-environment inspection, and requested |
39 | | -independent verification. Search Jacobian by desired local mathematical outcome, or |
40 | | -inspect one exact operation contract. A capability ID is not required for search or |
41 | | -browse. |
42 | | -
|
43 | | -Available forms: |
44 | | -- Pass `query` as a plain-language description of the desired local mathematical |
45 | | - outcome. The response contains compact operation cards with accepted inputs, output |
46 | | - summary, availability, scope, assurance ceiling, factual relationships, and one |
47 | | - size-bounded validated invocation example when available. |
48 | | -- Optionally filter with `domain` and `mode`. `limit` is between 1 and 20 and defaults |
49 | | - to 5; a smaller requested limit returns less model context. |
50 | | -- Omit all arguments to browse a compact installed catalog. |
51 | | -- When `next_cursor` is present, pass it back with the same filters and limit to |
52 | | - continue without loading the complete catalog. |
53 | | -- Ranking is deterministic retrieval over published IDs, titles, descriptions, and |
54 | | - tags. Match fields and terms are returned; candidates are not recommendations. |
55 | | -- Pass `capability_id` to inspect the exact operation. SUMMARY is compact, CONTRACT |
56 | | - adds the validation-equivalent input schema and validated invocation examples, and |
57 | | - FULL adds complete provider and audit metadata. |
58 | | -
|
59 | | -Weak or empty results do not imply impossibility. They include unranked recovery paths |
60 | | -for query reformulation, filter removal, browsing, and catalog inspection. Every exact |
61 | | -response states the operation's scope rule. |
| 35 | +Search or inspect installed math tools by desired outcome or exact ID. Use when a |
| 36 | +task may benefit from exact computation, search, structural analysis, or a separate |
| 37 | +checker tool—even if shell code could also calculate the answer. |
| 38 | +
|
| 39 | +Forms: |
| 40 | +- `query`: plain-language mathematical outcome (compact tool cards). |
| 41 | +- Optional `domain` filter; `limit` 1–20 (default 5). |
| 42 | +- Omit arguments to browse; follow `next_cursor` with the same filters to continue. |
| 43 | +- Ranking is deterministic lexical retrieval; matches are not recommendations. |
| 44 | +- `capability_id`: exact inspect (SUMMARY / CONTRACT / FULL views). |
| 45 | +
|
| 46 | +Checker tools are separate IDs (often `*.verify`), not a mode switch on producers. |
62 | 47 |
|
63 | 48 | Examples: |
64 | | -- `{"query":"compute an exact matrix determinant","domain":"matrix","mode":"EXPLORE","limit":3}` |
65 | | -- `{"query":"find a counterexample to associativity","domain":"universal_algebra","mode":"EXPLORE","limit":3}` |
66 | | -- `{"query":"eliminate this denominator using the defining relations"}` |
67 | | -- `{}` |
68 | | -- `{"capability_id":"polynomial.compute.gcd"}` |
| 49 | +- `{"query":"compute an exact matrix determinant","domain":"matrix","limit":3}` |
| 50 | +- `{"query":"find a counterexample to associativity","domain":"universal_algebra"}` |
69 | 51 | - `{"capability_id":"polynomial.compute.gcd","view":"CONTRACT"}` |
70 | 52 | """ |
71 | 53 |
|
72 | 54 | MATH_RUN_DESCRIPTION = """\ |
73 | | -Use this to run one selected Jacobian operation with its typed payload. If the payload |
74 | | -shape is unfamiliar, math.find can return the exact CONTRACT. EXPLORE returns proposed, |
75 | | -heuristic, or computed evidence; VERIFY is valid only for an installed checker-backed |
76 | | -contract. |
77 | | -
|
78 | | -The typed `CapabilityResult` keeps execution, scope, completeness, mathematical |
79 | | -conclusion, assurance, obligations, diagnostics, relationships, and artifacts distinct. |
| 55 | +Run one installed math tool by ID with its typed `payload`. Read the mathematical |
| 56 | +value in `output` first, then execution status. If the payload shape is unknown, |
| 57 | +use math.find with view CONTRACT. |
80 | 58 |
|
81 | | -COMPLETED does not by itself establish a mathematical conclusion. One invocation |
82 | | -covers only its exact supplied input or claim, and repeated finite or bounded calls do |
83 | | -not widen that scope. Follow returned `artifact://` references when durable evidence |
84 | | -or a size-separated result is provided. |
85 | | -
|
86 | | -A verification record is claim-bound. Verification of an input, premise, |
87 | | -factorization, or related artifact does not promote a conclusion derived by the model |
88 | | -to `VERIFIED`; the checker record must bind the exact final claim. |
| 59 | +Ordinary tools return calculations. Independent checking uses a separate checker |
| 60 | +tool ID (for example `polynomial.identity.verify` or `case.partition.finite.verify`), |
| 61 | +not a mode on the producer. Failed or incomplete runs are not mathematical conclusions. |
89 | 62 |
|
90 | 63 | Examples: |
91 | | -- `{"capability_id":"integer.compute.gcd","mode":"EXPLORE","payload":{"left":"84","right":"30"}}` |
92 | | -- `{"capability_id":"polynomial.identity.verify","mode":"VERIFY","payload":{"variables":["x"],"left":{"terms":[]},"right":{"terms":[]}}}` |
93 | | -
|
94 | | -These are valid envelopes, not a required research strategy. |
| 64 | +- `{"capability_id":"integer.compute.gcd","payload":{"left":"84","right":"30"}}` |
| 65 | +- `{"capability_id":"polynomial.identity.verify","payload":{"variables":["x"],"left":{"terms":[]},"right":{"terms":[]}}}` |
95 | 66 | """ |
96 | 67 |
|
97 | 68 | OPERATING_GUIDE = """\ |
|
113 | 84 |
|
114 | 85 | ## Search, browse, inspect, and run |
115 | 86 |
|
116 | | -Search with `math.find(query=...)`, optionally filtered by `domain` and |
117 | | -`mode`. Results are compact candidates ranked by deterministic matches against |
118 | | -published descriptor metadata; `matched_on` and `matched_terms` make that retrieval |
119 | | -visible. Ranking is not a recommendation. Follow `next_cursor` with unchanged filters |
120 | | -and limit when a discovery result is truncated. Omit all arguments to browse. |
| 87 | +Search with `math.find(query=...)`, optionally filtered by `domain`. Results are |
| 88 | +compact candidates ranked by deterministic matches against published descriptor |
| 89 | +metadata; `matched_on` and `matched_terms` make that retrieval visible. Ranking is |
| 90 | +not a recommendation. Follow `next_cursor` with unchanged filters and limit when a |
| 91 | +discovery result is truncated. Omit all arguments to browse. |
121 | 92 |
|
122 | 93 | The same tool accepts `capability_id` for exact inspection. SUMMARY is the compact |
123 | 94 | projection, CONTRACT adds the validation-equivalent input schema and examples, and |
|
137 | 108 | and catalog-inspection paths. They do not establish operation absence or mathematical |
138 | 109 | impossibility. |
139 | 110 |
|
140 | | -## Exploration and verification |
| 111 | +## Producers and checkers |
141 | 112 |
|
142 | | -`EXPLORE` returns proposed, heuristic, or computed evidence. Search, generation, |
143 | | -evaluation, solver output, and retrieved memory are not proof. |
| 113 | +Ordinary producer tools return proposed, heuristic, or computed evidence. Search, |
| 114 | +generation, evaluation, solver output, and retrieved memory are not proof. |
144 | 115 |
|
145 | | -`VERIFY` may return `VERIFIED` only when an operator-authorized independent checker |
146 | | -accepts evidence bound to the exact claim, semantics, candidate, scope, certificate |
147 | | -format, and checker identity. Only assurance level `VERIFIED` with a local |
148 | | -verification record is verified. |
| 116 | +A separate checker tool (often a `*.verify` ID) may return `VERIFIED` only when an |
| 117 | +operator-authorized independent checker accepts evidence bound to the exact claim, |
| 118 | +semantics, candidate, scope, certificate format, and checker identity. Only assurance |
| 119 | +level `VERIFIED` with a local verification record is verified. |
149 | 120 |
|
150 | 121 | Verification does not transfer across model-authored deductions. A record accepting |
151 | 122 | premises, inputs, factorizations, or related artifacts does not verify a derived |
@@ -218,7 +189,7 @@ def evidence_check_prompt(claim: str, artifact_uri: str | None = None) -> str: |
218 | 189 | {claim} |
219 | 190 | </claim> |
220 | 191 | {artifact_context} |
221 | | -1. Search with `math.find(query=..., mode="VERIFY")`. |
| 192 | +1. Search with `math.find(query=...)` for a checker tool (often a `*.verify` ID). |
222 | 193 | 2. Treat an empty result as checker unavailability, not evidence for or against the |
223 | 194 | claim. |
224 | 195 | 3. Describe the selected exact capability. Confirm that its semantics, scope, |
|
![devin-ai-integration[bot]](https://avatars.githubusercontent.com/in/811515?v=4&size=40){kind=avatar}
0 commit comments