| --- |
| license: apache-2.0 |
| library_name: pytorch |
| tags: |
| - premise-selection |
| - theorem-proving |
| - lean |
| - mathlib |
| --- |
| |
| # DAPS Selector |
|
|
| The graph-aware DAPS premise selector produced after Phase 2 training on Mathlib. The `main` branch contains this Phase 2 checkpoint, `daps_selector.pt`.  |
|
|
| ## Download weights |
|
|
| ```python |
| from huggingface_hub import hf_hub_download |
| |
| checkpoint_path = hf_hub_download( |
| repo_id="DAPS-Math/DAPS-selector", |
| filename="daps_selector.pt", |
| revision="main", |
| ) |
| ``` |
|
|
| Project page: [DAPS](https://relational-conjecturing.github.io/Dependency-Aware-Premise-Selection/). |
|
|
