File size: 7,417 Bytes
5feffa4
f082004
47d9ef1
 
 
5feffa4
47d9ef1
5feffa4
 
47d9ef1
 
 
 
 
 
 
5feffa4
 
47d9ef1
f082004
999258b
 
 
 
 
47d9ef1
 
 
 
 
999258b
47d9ef1
999258b
47d9ef1
f082004
47d9ef1
 
 
 
 
 
 
f082004
47d9ef1
 
 
 
 
 
 
 
 
 
f082004
47d9ef1
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
f082004
47d9ef1
f082004
47d9ef1
 
f082004
47d9ef1
f082004
47d9ef1
 
 
 
 
 
 
f082004
47d9ef1
 
 
 
 
 
 
f082004
47d9ef1
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
f082004
 
47d9ef1
 
 
 
 
 
 
 
 
 
 
 
f082004
 
47d9ef1
 
 
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
---
title: VerifiableRewardsForScalableLogicalReasoning
datasets: []
colorFrom: blue
colorTo: red
sdk: gradio
sdk_version: 5.34.2
app_file: app.py
pinned: false
tags:
  - evaluate
  - reward
  - reasoning
  - metric
description: >-
    VerifiableRewardsForScalableLogicalReasoning is a metric for evaluating logical reasoning in AI systems by providing verifiable rewards. It computes rewards through symbolic execution of candidate solutions against validation programs, enabling automatic, transparent and reproducible evaluation in AI systems.
---

# Metric Card for Symbolic Judge: Verifiable Rewards for Scalable Logical Reasoning

This metric is part of the SLR framework (AIML-TUDA/SLR-Bench) and provides rewards for logical reasoning tasks.
THe reward model is grounded in the ILP (Inductive Logic Programming) paradigm, testing whether a given hypothesis (logic rule) solves a logical reasoning task.
TO check for entailment, the logic rule is executed against a set of background knowledge and examples, ensuring automatic evaluation that is verifiable, transparent, and reproducible.


### How it Works
- **Input:** The symbolic judge takes as input a candidate hypothesis (logic rule) and an executable validation program containing background knowledge and examples.
- **Execution:** The candidate rule is executed against the validation program using a Prolog interpreter.
- **Correctness Criteria:** The rule is considered correct if it entails all positive examples and rejects all negative examples.
- **Metrics:** The symbolic judge computes a range of evaluation metrics (detailed below).

**Note:** A local Prolog interpreter is required to execute validation programs.

---

### Inputs
- **predictions** (`list` of `str`): Each prediction should be a Prolog rule like "eastbound(T) :- Body."
- **references** (`list` of `dict`): Each reference should contain:
  - **validation_program** (`str`): Prolog program with background knowledge and examples
  - **evaluation_config** (`dict`, optional): Configuration with:
    - **positive_predicate** (`str`): Predicate identifying positive examples (default: "eastbound")
    - **negative_predicate** (`str`): Predicate identifying negative examples (default: "westbound")

### Metrics & Output Values
- **accuracy** (`float`): Proportion of predictions that correctly classify all examples (0.0 to 1.0)
- **partial_score** (`float`): Average proportion of correctly classified examples (0.0 to 1.0)
- **syntax_score** (`float`): Proportion of rules with valid Prolog syntax (0.0 to 1.0)
- **detailed_results** (`list` of `dict`): Per-example results with:
  - **is_correct** (`bool`): Whether the rule correctly classifies all examples
  - **partial_score** (`float`): Proportion of correctly classified examples
  - **syntax_valid** (`bool`): Whether the rule has valid syntax
  - **error** (`str`, optional): Any error messages from Prolog evaluation
  - **exec_time** (`float`, optional): Execution time for evaluation

---
## How to Use with the datasets library
```python
from evaluate import load
from datasets import load_dataset

# Load the symbolic judge for logical reasoning
symbolic_judge = load("AIML-TUDA/VerifiableRewardsForScalableLogicalReasoning")

# load dataset AIML-TUDA/SLR-Bench
ds = load_dataset('AIML-TUDA/SLR-Bench', 'v1-All')
ds_test = ds['test'][:5]

# Prepare the predictions and references
rules = ds_test['ground-truth rule']
references = [{'validation_program': p,
                'evaluation_config': {
                    "positive_predicate": "eastbound",
                    "negative_predicate": "westbound"
                }
               } for p in ds_test['validation program']]
# Compute the evaluation
r2 = symbolic_judge.compute(predictions=rules, references=references)
r2
```

### Outputs

```python
{'accuracy': 1.0,
 'partial_score': 1.0,
 'syntax_score': 1.0,
 'detailed_results': [{'is_correct': True,'partial_score': 1.0,'syntax_valid': True,'error': None,'exec_time1': 0.014362812042236328},
                      {'is_correct': True,'partial_score': 1.0,'syntax_valid': True,'error': None,'exec_time1': 0.012364625930786133},
                      {'is_correct': True,'partial_score': 1.0,'syntax_valid': True,'error': None,'exec_time1': 0.012273550033569336},
                      {'is_correct': True,'partial_score': 1.0,'syntax_valid': True,'error': None,'exec_time1': 0.012486696243286133},
                      {'is_correct': True,'partial_score': 1.0,'syntax_valid': True,'error': None,'exec_time1': 0.012131929397583008}]}
```


---

## Examples

### Example 1: Evaluating a Single Rule

```python
from evaluate import load

symbolic_judge = load("AIML-TUDA/VerifiableRewardsForScalableLogicalReasoning")

validation_program = """
eastbound(train0).
has_car(train0, car0_1).
car_num(car0_1, 1).
car_color(car0_1, white).
car_len(car0_1, short).
has_wall(car0_1, full).

westbound(train1).
has_car(train1, car1_1).
car_num(car1_1, 1).
car_color(car1_1, yellow).
car_len(car1_1, short).
has_wall(car1_1, full).
"""

predicted_rule = "eastbound(Train):- has_car(Train, Car1), car_color(Car1, white)."

results = symbolic_judge.compute(
    predictions=[predicted_rule],
    references=[{"validation_program": validation_program,
                 "evaluation_config": {
                     "positive_predicate": "eastbound",
                     "negative_predicate": "westbound"
                 }}]
)

print(results)
```

### Output Example 1

```python
{'accuracy': 1.0,
 'partial_score': 1.0,
 'syntax_score': 1.0,
 'detailed_results': [
     {'is_correct': True,
      'partial_score': 1.0,
      'syntax_valid': True,
      'error': None,
      'exec_time1': 0.012056350708007812}]
 }

```

### Example 2: Evaluating Multiple Rules

```python
correct_rule = "eastbound(Train):- has_car(Train, Car1), car_color(Car1, white)."
incorrect_rule = "eastbound(Train):- has_car(Train, Car1), car_color(Car1, green)."

results = symbolic_judge.compute(
    predictions=[correct_rule, incorrect_rule],
    references=[
        {"validation_program": validation_program},
        {"validation_program": validation_program}
    ]
)

print(results)
```

### Example 3: Custom Evaluation Configuration

```python
validation_program = """
% Custom problem
parent(john, mary).
parent(john, bob).
parent(alice, bob).
parent(susan, alice).

% Examples
grandparent(susan, bob).
not_grandparent(john, alice).
"""

rule = "grandparent(X, Y) :- parent(X, Z), parent(Z, Y)."

results = symbolic_judge.compute(
    predictions=[rule],
    references=[{
        "validation_program": validation_program,
        "evaluation_config": {
            "positive_predicate": "grandparent",
            "negative_predicate": "not_grandparent"
        }
    }]
)
```

## Citation

```
@misc{helff2025slrautomatedsynthesisframework,
      title={SLR: An Automated Synthesis Framework for Scalable Logical Reasoning},
      author={Lukas Helff and Ahmad Omar and Felix Friedrich and Wolfgang Stammer and Antonia Wüst and Tim Woydt and Rupert Mitchell and Patrick Schramowski and Kristian Kersting},
      year={2025},
      eprint={2506.15787},
      archivePrefix={arXiv},
      primaryClass={cs.AI},
      url={https://arxiv.org/abs/2506.15787},
}
```

## Further References

- [SLR-Bench Dataset](https://huggingface.co/datasets/AIML-TUDA/SLR-Bench)
- [SLR-Bench GitHub Repository](https://github.com/AIML-TUDA/SLR)