Skip to content

Commit b59059a

Browse files
committed
feat(learning): boundary filter — only dotted aspects reach domain_hints / primary_domain
Two sites enforce: a string is a valid domain key iff it contains '.'. - gnn_augment_tactics filters state.metadata["aspects"] before sending to /gnn/rank, so structural tags like "axiom"/"constructor" never pollute Julia's PROVER_DOMAIN_WEIGHTS key space. - primary_domain in meta_controller skips non-dotted aspects when selecting the canonical domain for outcome recording. Adds two unit tests confirming primary_domain skips "axiom" and falls through to "unspecified" when only structural tags are present. Parser literals (8 sites listed in THEOREM-METADATA-MIGRATION.md) remain unchanged and harmless under this filter. https://claude.ai/code/session_01YPqu7gti4azBach6ZvpRFJ
1 parent 4f0477b commit b59059a

2 files changed

Lines changed: 20 additions & 1 deletion

File tree

src/rust/agent/meta_controller.rs

Lines changed: 16 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -756,8 +756,11 @@ pub enum PlanOutcome {
756756
/// the first aspect (lexicographically? no — order-as-given so the user
757757
/// can prioritise). Empty aspect list → "unspecified".
758758
fn primary_domain(goal: &AgenticGoal) -> String {
759+
// Only dotted "category.aspect" strings are valid domain keys; structural
760+
// meta-tags (e.g. "axiom", "constructor") do not reach the learning loop.
759761
goal.aspects
760-
.first()
762+
.iter()
763+
.find(|s| s.contains('.'))
761764
.cloned()
762765
.unwrap_or_else(|| "unspecified".to_string())
763766
}
@@ -772,6 +775,18 @@ mod tests {
772775
use crate::core::{Goal, Term};
773776
use crate::verification::confidence::TrustLevel;
774777

778+
#[test]
779+
fn test_primary_domain_skips_structural_tags() {
780+
let goal = dummy_goal(vec!["axiom", "arithmetic.natural_numbers"]);
781+
assert_eq!(primary_domain(&goal), "arithmetic.natural_numbers");
782+
}
783+
784+
#[test]
785+
fn test_primary_domain_all_structural_returns_unspecified() {
786+
let goal = dummy_goal(vec!["axiom"]);
787+
assert_eq!(primary_domain(&goal), "unspecified");
788+
}
789+
775790
fn dummy_goal(aspects: Vec<&str>) -> AgenticGoal {
776791
AgenticGoal {
777792
goal: Goal {

src/rust/provers/mod.rs

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1540,6 +1540,10 @@ pub(crate) async fn gnn_augment_tactics(
15401540
.get("aspects")
15411541
.and_then(|v| serde_json::from_value(v.clone()).ok())
15421542
.unwrap_or_default();
1543+
// Boundary filter: only dotted "category.aspect" strings reach the learning-loop
1544+
// key space. Structural meta-tags without a dot (e.g. "axiom", "constructor")
1545+
// are excluded here so they never pollute domain_hints or training records.
1546+
let aspects: Vec<String> = aspects.into_iter().filter(|s| s.contains('.')).collect();
15431547
let result = gnn.rank_premises_with_aspects(&graph, &aspects).await;
15441548
// Prepend apply tactics for top premises (in score order, before heuristic hints)
15451549
let mut gnn_tactics: Vec<Tactic> = result

0 commit comments

Comments
 (0)