Skip to content

Commit abd2215

Browse files
hyperpolymathclaude
andcommitted
feat(gnn): thread domain_hints through GnnGuidedSearch — activate weight-guided ranking
Phase 2 of the GNN feedback loop: now that /training/update populates PROVER_DOMAIN_WEIGHTS in Julia, callers can route goal aspects through the rank_premises path so Julia's weight-guided multiplier actually fires (instead of always using the empty-aspects fast path). - GnnClient::rank_premises_with_aspects(graph, aspects) — new method; populates GnnRankRequest.domain_hints from the caller's aspect slice. rank_premises(graph) is now a thin wrapper that passes &[] (no behaviour change for existing callers). - GnnGuidedSearch::rank_premises_with_aspects(state, premises, aspects) — same pattern; rank_premises remains the no-aspect convenience wrapper. Future agent code passing AgenticGoal.aspects automatically activates the closed-loop scoring without any further wiring. - build_request_payload now takes aspects and writes them into domain_hints; existing tests pass &[]. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
1 parent 11bc8a6 commit abd2215

2 files changed

Lines changed: 58 additions & 10 deletions

File tree

src/rust/gnn/client.rs

Lines changed: 33 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -242,6 +242,23 @@ impl GnnClient {
242242
/// If the server is unavailable, returns an empty result with
243243
/// `from_server: false`.
244244
pub async fn rank_premises(&self, graph: &ProofGraph) -> GnnInferenceResult {
245+
self.rank_premises_with_aspects(graph, &[]).await
246+
}
247+
248+
/// Rank premises with goal-aspect hints for weight-guided scoring.
249+
///
250+
/// Identical to [`rank_premises`] but populates the `domain_hints` field
251+
/// in the request so Julia can apply accumulated training weights from
252+
/// `PROVER_DOMAIN_WEIGHTS` (updated by `POST /training/update`). This
253+
/// activates the closed-loop feedback path: prior proof outcomes on the
254+
/// same domain influence current premise scoring.
255+
///
256+
/// Pass an empty slice for behaviour identical to [`rank_premises`].
257+
pub async fn rank_premises_with_aspects(
258+
&self,
259+
graph: &ProofGraph,
260+
aspects: &[String],
261+
) -> GnnInferenceResult {
245262
if !self.server_available {
246263
debug!("GNN server not available, returning empty ranking");
247264
return GnnInferenceResult {
@@ -253,7 +270,7 @@ impl GnnClient {
253270
};
254271
}
255272

256-
match self.call_rank_api(graph).await {
273+
match self.call_rank_api(graph, aspects).await {
257274
Ok(result) => result,
258275
Err(e) => {
259276
warn!("GNN ranking failed: {}", e);
@@ -269,8 +286,12 @@ impl GnnClient {
269286
}
270287

271288
/// Internal: call the /gnn/rank endpoint.
272-
async fn call_rank_api(&self, graph: &ProofGraph) -> Result<GnnInferenceResult> {
273-
let payload = self.build_request_payload(graph);
289+
async fn call_rank_api(
290+
&self,
291+
graph: &ProofGraph,
292+
aspects: &[String],
293+
) -> Result<GnnInferenceResult> {
294+
let payload = self.build_request_payload(graph, aspects);
274295
let url = format!("{}/gnn/rank", self.config.api_url);
275296

276297
let response = self
@@ -307,7 +328,7 @@ impl GnnClient {
307328
}
308329

309330
/// Build the request payload from a proof graph.
310-
fn build_request_payload(&self, graph: &ProofGraph) -> GnnRankRequest {
331+
fn build_request_payload(&self, graph: &ProofGraph, aspects: &[String]) -> GnnRankRequest {
311332
let (edge_src, edge_dst, edge_weights) = graph.sparse_adjacency();
312333

313334
let edge_kinds: Vec<String> = graph
@@ -360,7 +381,7 @@ impl GnnClient {
360381
num_gnn_layers: self.config.num_gnn_layers,
361382
use_attention: self.config.use_attention,
362383
},
363-
domain_hints: vec![],
384+
domain_hints: aspects.to_vec(),
364385
}
365386
}
366387

@@ -426,11 +447,17 @@ mod tests {
426447
extractor.extract_features(&mut graph);
427448

428449
let client = GnnClient::new();
429-
let payload = client.build_request_payload(&graph);
450+
let payload = client.build_request_payload(&graph, &[]);
430451

431452
assert_eq!(payload.graph.num_nodes, graph.num_nodes());
432453
assert_eq!(payload.graph.num_edges, graph.num_edges());
433454
assert_eq!(payload.graph.edge_src.len(), graph.num_edges());
455+
assert!(payload.domain_hints.is_empty());
456+
457+
// With aspects: the same payload but with domain_hints populated
458+
let aspects = vec!["arithmetic.factorisation".to_string(), "crypto.hash.sha256".to_string()];
459+
let payload_with = client.build_request_payload(&graph, &aspects);
460+
assert_eq!(payload_with.domain_hints, aspects);
434461
}
435462

436463
#[tokio::test]

src/rust/gnn/guided_search.rs

Lines changed: 25 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -160,23 +160,39 @@ impl GnnGuidedSearch {
160160

161161
/// Rank available premises for the current proof state.
162162
///
163+
/// Convenience wrapper around [`rank_premises_with_aspects`] that passes
164+
/// no domain hints — equivalent to `rank_premises_with_aspects(state, premises, &[])`.
165+
pub async fn rank_premises(
166+
&mut self,
167+
state: &ProofState,
168+
available_premises: &[Theorem],
169+
) -> Vec<ScoredPremise> {
170+
self.rank_premises_with_aspects(state, available_premises, &[]).await
171+
}
172+
173+
/// Rank available premises with goal-aspect hints for closed-loop scoring.
174+
///
163175
/// This is the main entry point. It:
164176
/// 1. Builds a proof graph from the state
165177
/// 2. Extracts features
166-
/// 3. Queries the GNN server (if available)
178+
/// 3. Queries the GNN server (if available), passing `aspects` so Julia
179+
/// can apply accumulated `PROVER_DOMAIN_WEIGHTS` from prior outcomes
167180
/// 4. Computes symbolic scores
168181
/// 5. Combines and ranks results
169182
///
170183
/// # Arguments
171184
/// * `state` - Current proof state (goals + context)
172185
/// * `available_premises` - Theorems that could be applied
186+
/// * `aspects` - Goal aspect tags (e.g. from `AgenticGoal::aspects`).
187+
/// Empty slice = behaviour identical to [`rank_premises`].
173188
///
174189
/// # Returns
175190
/// Premises ranked by combined score (highest first).
176-
pub async fn rank_premises(
191+
pub async fn rank_premises_with_aspects(
177192
&mut self,
178193
state: &ProofState,
179194
available_premises: &[Theorem],
195+
aspects: &[String],
180196
) -> Vec<ScoredPremise> {
181197
self.stats.total_calls += 1;
182198

@@ -187,8 +203,13 @@ impl GnnGuidedSearch {
187203
// Step 2: Extract features
188204
self.feature_extractor.extract_features(&mut graph);
189205

190-
// Step 3: Get GNN scores (if server available)
191-
let gnn_result = self.gnn_client.rank_premises(&graph).await;
206+
// Step 3: Get GNN scores (if server available); aspects flow through
207+
// as `domain_hints` so Julia's rank_with_gnn can apply per-domain
208+
// weights accumulated from past proof outcomes.
209+
let gnn_result = self
210+
.gnn_client
211+
.rank_premises_with_aspects(&graph, aspects)
212+
.await;
192213

193214
let gnn_scores: HashMap<String, f32> = if gnn_result.from_server {
194215
self.stats.gnn_calls += 1;

0 commit comments

Comments
 (0)