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) |