purewhite42
/

dependency_retriever_f

@@ -1,144 +1,69 @@
 ---
-datasets: []
-language: []
-library_name: sentence-transformers
 pipeline_tag: sentence-similarity
 tags:
-- sentence-transformers
-- sentence-similarity
-- feature-extraction
-widget: []
 ---
-# SentenceTransformer
-This is a [sentence-transformers](https://www.SBERT.net) model trained. It maps sentences & paragraphs to a 1024-dimensional dense vector space and can be used for semantic textual similarity, semantic search, paraphrase mining, text classification, clustering, and more.
-## Model Details
-### Model Description
-- **Model Type:** Sentence Transformer
-<!-- - **Base model:** [Unknown](https://huggingface.co/unknown) -->
-- **Maximum Sequence Length:** 8192 tokens
-- **Output Dimensionality:** 1024 tokens
-- **Similarity Function:** Cosine Similarity
-<!-- - **Training Dataset:** Unknown -->
-<!-- - **Language:** Unknown -->
-<!-- - **License:** Unknown -->
-### Model Sources
-- **Documentation:** [Sentence Transformers Documentation](https://sbert.net)
-- **Repository:** [Sentence Transformers on GitHub](https://github.com/UKPLab/sentence-transformers)
-- **Hugging Face:** [Sentence Transformers on Hugging Face](https://huggingface.co/models?library=sentence-transformers)
-### Full Model Architecture
 ```
-SentenceTransformer(
-  (0): Transformer({'max_seq_length': 8192, 'do_lower_case': False}) with Transformer model: XLMRobertaModel
-  (1): Pooling({'word_embedding_dimension': 1024, 'pooling_mode_cls_token': True, 'pooling_mode_mean_tokens': False, 'pooling_mode_max_tokens': False, 'pooling_mode_mean_sqrt_len_tokens': False, 'pooling_mode_weightedmean_tokens': False, 'pooling_mode_lasttoken': False, 'include_prompt': True})
-  (2): Normalize()
-)
 ```
-## Usage
-### Direct Usage (Sentence Transformers)
-First install the Sentence Transformers library:
-```bash
-pip install -U sentence-transformers
-```
-Then you can load this model and run inference.
-```python
-from sentence_transformers import SentenceTransformer
-# Download from the 🤗 Hub
-model = SentenceTransformer("sentence_transformers_model_id")
-# Run inference
-sentences = [
-    'The weather is lovely today.',
-    "It's so sunny outside!",
-    'He drove to the stadium.',
-]
-embeddings = model.encode(sentences)
-print(embeddings.shape)
-# [3, 1024]
-# Get the similarity scores for the embeddings
-similarities = model.similarity(embeddings, embeddings)
-print(similarities.shape)
-# [3, 3]
-```
-<!--
-### Direct Usage (Transformers)
-<details><summary>Click to see the direct usage in Transformers</summary>
-</details>
--->
-<!--
-### Downstream Usage (Sentence Transformers)
-You can finetune this model on your own dataset.
-<details><summary>Click to expand</summary>
-</details>
--->
-<!--
-### Out-of-Scope Use
-*List how the model may foreseeably be misused and address what users ought not to do with the model.*
--->
-<!--
-## Bias, Risks and Limitations
-*What are the known or foreseeable issues stemming from this model? You could also flag here known failure cases or weaknesses of the model.*
--->
-<!--
-### Recommendations
-*What are recommendations with respect to the foreseeable issues? For example, filtering explicit content.*
--->
-## Training Details
-### Framework Versions
-- Python: 3.11.9
-- Sentence Transformers: 3.0.1
-- Transformers: 4.44.2
-- PyTorch: 2.4.0+cu121
-- Accelerate: 0.33.0
-- Datasets: 2.21.0
-- Tokenizers: 0.19.1
-## Citation
-### BibTeX
-<!--
-## Glossary
-*Clearly define terms in order to be accessible across audiences.*
--->
-<!--
-## Model Card Authors
-*Lists the people who create the model card, providing recognition and accountability for the detailed work that goes into its construction.*
--->
-<!--
-## Model Card Contact
-*Provides a way for people who have updates to the Model Card, suggestions, or questions, to contact the Model Card authors.*
--->

 ---
+license: apache-2.0
+language:
+- en
+base_model:
+- BAAI/bge-m3
 pipeline_tag: sentence-similarity
+library_name: transformers
 tags:
+- lean4
+- dependency-retrieval
+- formal-mathematics
 ---
+<div align="center">
+  <h1 style="font-size: 1.5em;">[ICLR'25 Spotlight] Rethinking and Improving Autoformalization: Towards a Faithful Metric and a Dependency Retrieval-based Approach</h1>
+  <div style="display: flex; justify-content: center; gap: 8px; flex-wrap: wrap;">
+    <a href="https://choosealicense.com/licenses/apache-2.0/"><img src="https://img.shields.io/badge/License-Apache%202.0-blue.svg" alt="License: Apache 2.0"></a>
+    <a href="https://github.com/leanprover-community/mathlib4"><img src="https://img.shields.io/badge/Lean-4-orange" alt="Lean 4"></a>
+    <a href="https://github.com/Purewhite2019/rethinking_autoformalization"><img src="https://img.shields.io/badge/GitHub-%23121011.svg?logo=github&logoColor=white" alt="GitHub"></a>
+  </div>
+  <h2>Qi Liu, Xinhao Zheng, Xudong Lu, Qinxiang Cao, Junchi Yan* (* indicates Correspondence author)</h2>
+  <h2>Sch. of Computer Science & Sch. of Artificial Intelligence, Shanghai Jiao Tong University</h2>
+</div>
+Please refer to the [📺GitHub repo](https://github.com/Purewhite2019/rethinking_autoformalization) and
+[📃Paper](https://openreview.net/pdf?id=hUb2At2DsQ) for more details.
+## 📈 Performance
+| **Bench**     | **Fmt** | **Method** | **Recall@5** | **Precision@5** |
+|---------------|---------|------------|--------------|-----------------|
+| **ProofNet** | F    | BM25       | 0.16%        | 0.11%           |
+|               | F    | DR         | 35.52%       | 22.89%          |
+|               | F+IF  | BM25       | 0.00%        | 0.00%           |
+|               | F+IF  | DR         | 32.47%       | 20.32%          |
+|   **Con-NF**  | F    | BM25       | 4.41%        | 2.37%           |
+|               | F    | DR         | 24.32%       | 14.05%          |
+|               | F+IF  | BM25       | 9.86%        | 6.95%           |
+|               | F+IF  | DR         | 27.91%       | 17.57%          |
+## ⚙️ Usage
+- [🤗`purewhite42/dependency_retriever_f`](https://huggingface.co/purewhite42/dependency_retriever_f): Dependency retriever whose inputs are formatted using only formal declarations , SFTed from [🤗`BAAI/bge-m3`](https://huggingface.co/BAAI/bge-m3)
+- [🤗`purewhite42/dependency_retriever_f_if`](https://huggingface.co/purewhite42/dependency_retriever_f_if): w/ oracle dependency retrieval whose inputs are formatted using both formal declarations and informal descriptions, SFTed from [🤗`BAAI/bge-m3`](https://huggingface.co/BAAI/bge-m3)
+```shell
+python -m retriever.retrieve_dr \
+    --model_path /path/to/the/model \
+    --save_path /path/to/output/results \
+    --eval_set ... # {proofnet, connf}
 ```
+## 📚 Citation
+If you find our work useful in your research, please cite
+```bibtex
+@inproceedings{
+liu2025rethinking,
+title={Rethinking and improving autoformalization: towards a faithful metric and a Dependency Retrieval-based approach},
+author={Qi Liu and Xinhao Zheng and Xudong Lu and Qinxiang Cao and Junchi Yan},
+booktitle={The Thirteenth International Conference on Learning Representations},
+year={2025},
+url={https://openreview.net/forum?id=hUb2At2DsQ}
+}
 ```
+# License
+This project is released under the Apache 2.0 license. Please see the [LICENSE](https://github.com/Purewhite2019/rethinking_autoformalization/blob/main/LICENSE) file for more information.
+# Contact
+Feel free to discuss the paper/data/code with us through issues/emails!
+- Qi Liu: [email protected]