1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
//! Neural-Symbolic Learning
//!
//! Learning algorithms: rule weight learning, differentiable ILP (Inductive Logic Programming),
//! neural theorem proving helpers, semantic loss, and symbolic rule learning.
use super::neural_symbolic_reasoner::NeuralSymbolicModel;
use super::neural_symbolic_types::*;
use anyhow::Result;
use scirs2_core::ndarray_ext::Array1;
use std::collections::HashMap;
impl NeuralSymbolicModel {
/// Learn symbolic rules from input-output examples.
///
/// Performs a simple differentiable ILP scan: for every dimension pair
/// (j, k) where both input and output exceed 0.5 a candidate rule is
/// generated. Rules are retained when they achieve ≥3 supporting
/// examples with mean confidence > 0.7.
pub fn learn_symbolic_rules(&mut self, examples: &[(Array1<f32>, Array1<f32>)]) -> Result<()> {
let mut candidate_rules = Vec::new();
for (input, output) in examples.iter() {
for j in 0..input.len() {
for k in 0..output.len() {
if input[j] > 0.5 && output[k] > 0.5 {
let antecedent = LogicalFormula::new_atom(format!("input_{j}"));
let consequent = LogicalFormula::new_atom(format!("output_{k}"));
let rule =
KnowledgeRule::new(format!("rule_{j}_{k}"), antecedent, consequent);
candidate_rules.push(rule);
}
}
}
}
for rule in candidate_rules {
let mut support = 0usize;
let mut confidence_sum = 0.0f32;
for (input, output) in examples {
let mut facts = HashMap::new();
for (i, &value) in input.iter().enumerate() {
facts.insert(format!("input_{i}"), value);
}
if let Some((predicate, predicted_value)) = rule.apply(&facts) {
if let Some(index) = predicate
.strip_prefix("output_")
.and_then(|s| s.parse::<usize>().ok())
{
if index < output.len() {
let actual_value = output[index];
let error = (predicted_value - actual_value).abs();
if error < 0.2 {
support += 1;
confidence_sum += 1.0 - error;
}
}
}
}
}
if support >= 3 && confidence_sum / support as f32 > 0.7 {
self.add_knowledge_rule(rule);
}
}
Ok(())
}
/// Compute the combined semantic loss for a prediction against targets.
///
/// The total loss is a convex combination of:
/// - MSE loss (data fit)
/// - Constraint violation loss (logical consistency)
/// - Rule inconsistency loss (symbolic coherence)
pub fn compute_semantic_loss(
&self,
predictions: &Array1<f32>,
targets: &Array1<f32>,
) -> Result<f32> {
// Standard MSE
let mse_loss = {
let diff = predictions - targets;
diff.dot(&diff) / predictions.len() as f32
};
// Constraint violation loss
let constraint_loss = {
let mut facts = HashMap::new();
for (i, &value) in predictions.iter().enumerate() {
facts.insert(format!("output_{i}"), value);
}
let mut total_violation = 0.0f32;
for constraint in &self.constraints {
let satisfaction = constraint.evaluate(&facts);
if satisfaction < 1.0 {
total_violation += (1.0 - satisfaction).powi(2);
}
}
total_violation / self.constraints.len().max(1) as f32
};
// Rule consistency loss
let rule_loss = {
let mut facts = HashMap::new();
for (i, &value) in predictions.iter().enumerate() {
facts.insert(format!("input_{i}"), value);
}
let mut total_inconsistency = 0.0f32;
for rule in &self.knowledge_base {
if let Some((predicate, predicted_value)) = rule.apply(&facts) {
if let Some(index) = predicate
.strip_prefix("output_")
.and_then(|s| s.parse::<usize>().ok())
{
if index < predictions.len() {
let actual_value = predictions[index];
let inconsistency = (predicted_value - actual_value).powi(2);
total_inconsistency += inconsistency * rule.weight;
}
}
}
}
total_inconsistency / self.knowledge_base.len().max(1) as f32
};
Ok(mse_loss + 0.1 * constraint_loss + 0.1 * rule_loss)
}
/// Update rule weights using gradient-like feedback.
///
/// For each rule, the weight is adjusted proportionally to how often
/// it fired and how accurate its predictions were against the provided
/// examples. This implements a rudimentary differentiable ILP update.
pub fn update_rule_weights(
&mut self,
examples: &[(Array1<f32>, Array1<f32>)],
learning_rate: f32,
) -> Result<()> {
for rule in self.knowledge_base.iter_mut() {
let mut gradient_sum = 0.0f32;
let mut count = 0usize;
for (input, output) in examples {
let mut facts = HashMap::new();
for (i, &value) in input.iter().enumerate() {
facts.insert(format!("input_{i}"), value);
}
if let Some((predicate, predicted_value)) = rule.apply(&facts) {
if let Some(index) = predicate
.strip_prefix("output_")
.and_then(|s| s.parse::<usize>().ok())
{
if index < output.len() {
let target = output[index];
// Gradient w.r.t. rule weight: -(target - pred) * pred
let grad = -(target - predicted_value) * predicted_value;
gradient_sum += grad;
count += 1;
}
}
}
}
if count > 0 {
let mean_grad = gradient_sum / count as f32;
rule.weight = (rule.weight - learning_rate * mean_grad).clamp(0.0, 10.0);
}
}
Ok(())
}
/// Neural theorem proving: attempt to prove a target predicate.
///
/// Implements backward chaining with depth-limited search, using neural
/// confidence scores to prune low-probability proof paths.
pub fn prove_predicate(
&self,
target: &str,
known_facts: &HashMap<String, f32>,
max_depth: usize,
) -> Option<f32> {
self.prove_recursive(target, known_facts, max_depth, 1.0)
}
fn prove_recursive(
&self,
target: &str,
known_facts: &HashMap<String, f32>,
depth: usize,
confidence_so_far: f32,
) -> Option<f32> {
// Base case: target is already a known fact
if let Some(&v) = known_facts.get(target) {
return Some(v * confidence_so_far);
}
if depth == 0 {
return None;
}
// Try to find a rule whose consequent matches the target
let mut best: Option<f32> = None;
for rule in &self.knowledge_base {
if let FormulaStructure::Atom(consequent_pred) = &rule.consequent.structure {
if consequent_pred == target {
// Try to prove the antecedent
let ante_val = rule.antecedent.evaluate(known_facts);
if ante_val > 0.0 {
let branch_confidence =
confidence_so_far * rule.confidence * ante_val;
if branch_confidence > best.unwrap_or(0.0) {
best = Some(branch_confidence);
}
} else if let FormulaStructure::Atom(ante_pred) = &rule.antecedent.structure {
// Recurse on the antecedent predicate
if let Some(proved) = self.prove_recursive(
ante_pred,
known_facts,
depth - 1,
confidence_so_far * rule.confidence,
) {
if proved > best.unwrap_or(0.0) {
best = Some(proved);
}
}
}
}
}
}
best
}
}