Fix inconsistencies in README

README.md

@@ -9,7 +9,7 @@ base_model:
 
 # **RocqStar Ranker Embedder**
 
-A self‑attentive embedding model for premise / proof selection in Rocq‑based interactive theorem proving (ITP). RocqStar is fine‑tuned from CodeBERT so that distances in the embedding space correlate with proof similarity rather than with surface‑level statement overlap. It replaces BM25/Jaccard similarity in retrieval‑augmented generation (RAG) pipelines such as **CoqPilot**, leading to higher proof success rates on the IMM‑300 benchmark.
+A self‑attentive embedding model for premise / proof selection in Rocq ITP. RocqStar is fine‑tuned from CodeBERT so that distances in the embedding space correlate with proof similarity rather than with surface‑level statement overlap. It replaces BM25/Jaccard similarity in retrieval‑augmented generation (RAG) pipelines such as **CoqPilot**, leading to higher proof success rates on the IMM‑300 benchmark.
 
 ## Model Details
 
@@ -19,7 +19,7 @@ RocqStar is a 125 M‑parameter Transformer encoder (768‑dim hidden size) wi
 
 * **Model type:** Transformer encoder with self‑attentive pooling
 * **Language(s):** Rocq / Coq (Gallina) syntax (tokens)
-* **License:**: Apache‑2.0
+* **License:** Apache‑2.0
 * **Fine‑tuned from:** `microsoft/codebert-base`
 
 ### Model Sources
@@ -27,12 +27,6 @@ RocqStar is a 125 M‑parameter Transformer encoder (768‑dim hidden size) wi
 * **Repository:** [https://github.com/JetBrains-Research/big-rocq](https://github.com/JetBrains-Research/big-rocq)
 * **Paper:** (coming soon)
 
-## Bias, Risks, and Limitations
-
-* **Domain limitation:** Trained only on Rocq projects; performance degrades on other languages or heavily tactic‑macro‑based proofs.
-* **Data leakage:** May memorise proofs present in training data and surface them verbatim.
-* **Proof similarity assumption:** While improved over BM25, cosine distance may still fail on very long or highly creative proofs.
-
 ## How to Get Started
 
 Go to [https://github.com/JetBrains-Research/big-rocq](https://github.com/JetBrains-Research/big-rocq). In subdirectory `ranker-server` you can find the server that you need to run to be able to use the model from the CoqPilot plugin. Also it may be used as a reference example of how to do inference with the model. 
@@ -46,8 +40,8 @@ Go to [https://github.com/JetBrains-Research/big-rocq](https://github.com/JetBra
 
 ### Training Procedure
 
-* **Objective:** InfoNCE with temperature T = 0.07
-* **Batch size:** 512 pairs (effective) – gradient accumulation = 8×64
+* **Objective:** InfoNCE 
+* **Batch size:** 32
 * **Optimizer / LR:** AdamW, lr = 4e‑6, linear warm‑up 10 %, 22k steps
 * **Hardware:** 1× NVIDIA H100 GPU, 160 GB RAM, 14 h wall‑clock
 
@@ -71,4 +65,4 @@ Go to [https://github.com/JetBrains-Research/big-rocq](https://github.com/JetBra
 
 #### Summary
 
-RocqStar delivers consistent gains, up to 28% relative improvement over token‑overlap retrieval, especially for medium‑length theorems where proof similarity diverges most from statement similarity.
+RocqStar delivers consistent gains, up to 28% relative improvement over Jaccard-index based retrieval, especially for medium‑length theorems where proof similarity diverges most from statement similarity.