Create README.md

README.md

@@ -0,0 +1,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-nl-to-fol
+
+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:** bfloat16 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