Downloads · 30 days
0
qwen3-0.6b-lightweight-semantic-mathlib-search-adapter
Isaac74/qwen3-0.6b-lightweight-semantic-mathlib-search-adapter
qwen3-0.6b-lightweight-semantic-mathlib-search-adapter is a sentence similarity model from Isaac74. Use it when you need a score for how close two texts are. It is set up for peft. The card lists the license as apache-2.0.
What this is: A small, reproducible demo adapter for Qwen/Qwen3-Embedding-0.6B that enables lightweight, LLM-free semantic search over mathlib (Lean 4). Supports both natural language and formula-based search (can be…
Access
Public
Updated Aug 9, 2025
Repo size
2.7 GB
Likes
0
Public
Repo makeup
Click a slice to open those files.
.idx2.6 GB · 95%
At a glance
- Task
- Sentence Similarity
- Library
- peft
- License
- apache-2.0
- Access
- Public
- Created
- Aug 8, 2025
- Updated
- Aug 9, 2025
- SHA
- bec85f83
Base models
Model card
From the Hugging Face model README
Lightweight Semantic Mathlib Search — LoRA Adapter (Demo)
What this is:
A small, reproducible demo adapter for Qwen/Qwen3-Embedding-0.6B that enables lightweight, LLM-free semantic search over mathlib (Lean 4).
Supports both natural language and formula-based search (can be used in combination) for finding Lean theorems or mathematical statements.
Does not support LaTeX syntax search yet.
Data is built from ~180k Lean theorems extracted via LeanDojo for Lean 4.20.1 (there may be minor gaps vs. the full mathlib).
Part of the AITP 2025 submission: “Towards Lightweight and LLM-Free Semantic Search for mathlib4.”
Contents
adapter/adapter_config.json&adapter/adapter_model.safetensors— LoRA weights for the encoderfaiss/<*.idx>— HNSW FAISS index (built for cosine/inner-product search)faiss/*public_index.jsonl— public mapping{ idx, full_name, statement }
DEMO
https://github.com/IsaacLi74/Lightweight-and-LLM-Free-Semantic-Search-for-mathlib4
- Task
- Sentence Similarity
- Library
- peft
- License
- apache-2.0
- Created
- Aug 8, 2025
- Updated
- Aug 9, 2025