File size: 4,630 Bytes
7349cb9 feb436e 7349cb9 6ab202c 7349cb9 | 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 | ---
base_model:
- google-t5/t5-base
library_name: transformers
license: apache-2.0
datasets:
- fvossel/groves
language:
- en
pipeline_tag: translation
tags:
- NLTOFOL
- NL
- FOL
- semantic-parsing
- first-order-logic
- formal-logic
- compositional-generalization
---
# Model Card for fvossel/t5-base-groves
This model is a fully fine-tuned version of [`google-t5/t5-base`](https://huggingface.co/google-t5/t5-base). It was trained to translate **natural language statements into First-Order Logic (FOL)** representations.
## Model Details
### Model Description
- **Developed by:** Vossel et al. at Osnabrück University
- **Funded by:** Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) 456666331
- **Model type:** Encoder-decoder sequence-to-sequence model (T5 architecture)
- **Language(s) (NLP):** English, FOL
- **License:** This model was fine-tuned from [`google/t5-base`](https://huggingface.co/google/t5-base), which is released under the [Apache 2.0 License](https://www.apache.org/licenses/LICENSE-2.0), and is itself released under the **Apache 2.0 License**.
- **Finetuned from model:** google/t5-base
## Uses
### Direct Use
This model is designed to translate natural language (NL) sentences into corresponding first-order logic (FOL) expressions. Use cases include:
- Automated semantic parsing and formalization of NL statements into symbolic logic.
- Supporting explainable AI systems that require symbolic reasoning based on language input.
- Research in neurosymbolic AI, logic-based natural language understanding, and formal verification.
- Integration into pipelines for natural language inference, question answering, or knowledge base population.
Users should verify and validate symbolic formulas generated by the model for correctness depending on the application.
### Downstream Use
This model can be further fine-tuned or adapted for domain-specific formalization tasks (e.g., legal, biomedical). Suitable for interactive systems requiring formal reasoning.
### Out-of-Scope Use
- Not designed for general natural language generation.
- May struggle with ambiguous, highly figurative, or out-of-domain input.
- Outputs should not be used as final decisions in critical areas without expert review.
### Recommendations
- Validate outputs carefully before use in critical applications.
- Be aware of possible biases from training data and synthetic data sources.
- Specialized for English NL and FOL; may not generalize to other languages or logics.
- Use human-in-the-loop workflows for sensitive tasks.
- Intended for research and prototyping, not standalone critical systems.
## How to Get Started with the Model
```python
import torch
from transformers import T5Tokenizer, T5ForConditionalGeneration
# Load tokenizer and model
model_path = "fvossel/t5-base-nl-to-fol"
tokenizer = T5Tokenizer.from_pretrained(model_path)
model = T5ForConditionalGeneration.from_pretrained(model_path).to("cuda")
# Example NL input
nl_input = "All dogs are animals."
# Preprocess prompt
input_text = "translate English natural language statements into first-order logic (FOL): " + nl_input
inputs = tokenizer(input_text, return_tensors="pt", padding=True).to("cuda")
# Generate prediction
with torch.no_grad():
outputs = model.generate(
inputs["input_ids"],
max_length=256,
min_length=1,
num_beams=5,
length_penalty=2.0,
early_stopping=True,
)
# Decode and print result
print(tokenizer.decode(outputs[0], skip_special_tokens=True))
```
## Training Details
### Training Data
The model was fine-tuned on the [groves dataset](https://huggingface.co/datasets/fvossel/groves).
### Training Procedure
The model was fully fine-tuned (no LoRA) from `google/t5-base` with:
- Prompt-based instruction tuning
- Single-GPU training with float32 precision
- Preprocessing replaced FOL quantifiers (e.g., `∀`) with tokens like `FORALL`
- Maximum input/output sequence length was 250 tokens
### Training Hyperparameters
- **Training regime:** float32 precision
- **Batch size:** 8 (per device)
- **Learning rate:** 0.001
- **Number of epochs:** 12
- **Optimizer:** AdamW
- **Adam epsilon:** 1e-8
- **Scheduler:** Linear warmup with 500 steps
- **Gradient accumulation steps:** 1
- **Weight decay:** 0.01
- **LoRA:** Not used (full fine-tuning)
- **Task type:** SEQ_2_SEQ_LM
- **Early stopping patience:** 4 epochs
- **Evaluation strategy:** per epoch
- **Save strategy:** per epoch
- **Save total limit:** 12 checkpoints
- **Best model selection metric:** eval_loss |