| Name | satquest JSON |
| Version |
0.1.2
JSON |
| download |
| home_page | None |
| Summary | A Verifier for Logical Reasoning Evaluation and Reinforcement Fine-Tuning of LLMs |
| upload_time | 2025-08-30 19:51:50 |
| maintainer | None |
| docs_url | None |
| author | None |
| requires_python | >=3.10 |
| license | MIT License Copyright (c) 2025 Adam Yanxiao Zhao Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. |
| keywords |
llm
reasoning
evaluation
reinforcement-learning
|
| VCS |
 |
| bugtrack_url |
|
| requirements |
No requirements were recorded.
|
| Travis-CI |
No Travis.
|
| coveralls test coverage |
No coveralls.
|
# SATQuest: A Verifier for Logical Reasoning Evaluation and Reinforcement Fine-Tuning of LLMs
[Preprint Paper](./SATQuest-paper.pdf)
[](https://opensource.org/licenses/MIT)
[](https://github.com/sdpkjc/SATQuest)
[](https://pypi.org/project/satquest/)
## 🚀 Quickstart
```python
# Install dependencies
# pip install datasets satquest
from datasets import load_dataset
from satquest import CNF, create_problem, create_question
item = load_dataset('sdpkjc/SATQuest', split='test')[0]
cnf = CNF(dimacs=item['sat_dimacs'])
# cnf.shuffle()
problem = create_problem('SATSP', cnf) # or 'SATDP', 'MaxSAT', 'MCS', 'MUS'
question = create_question('math') # or 'dimacs', 'story', 'dualstory'
prompt = problem.accept(question)
answer = problem.solution # reference answer
reward = int(problem.check(answer)) # 1 if answer is correct, 0 otherwise
```
## Dataset Generation
[]([https://huggingface.co/sdpkjc/](https://huggingface.co/collections/sdpkjc/satquest-6820687d856b96f869921e53))
```bash
# Run dataset generation
uv run --group gen gen_cnf_dataset.py --hf-entity {YOUR_HF_ENTITY} --seed 9527
uv run --group gen gen_cnf_rft_dataset.py --hf-entity {YOUR_HF_ENTITY} --seed 9527
```
## Evaluation
```bash
# Run evaluation
uv run --group eval eval_model.py \
--exp-name {YOUR_EXP_NAME} \
--wandb-project "SATQuest-Eval" \
--hf-dataset-name "sdpkjc/SATQuest" \
--p-type-list SATSP \
--q-type-list math \
--llm-model "gpt-4o" \
--max-tokens 16384 \
--temperature 0.6 \
--num-example 10 \
--stream True \
--cnf-shuffle False \
--n-repeat 1
```
### Evaluation Parameters
- `exp-name`: Name of your experiment
- `wandb-project`: Weights & Biases project name
- `hf-dataset-name`: HuggingFace dataset name
- `p-type-list`: Problem types to evaluate (e.g., "SATSP", "MaxSAT", "MCS", "MUS", "SATDP_SAT", "SATDP_UNSAT")
- `q-type-list`: Question types to evaluate (e.g., "math", "dimacs", "story", "dualstory")
- `llm-model`: LLM model to use for evaluation
- `max-tokens`: Maximum tokens for LLM response
- `temperature`: Temperature for LLM generation
- `num-example`: Number of examples to evaluate
- `stream`: Whether to stream LLM responses
- `cnf-shuffle`: Whether to shuffle CNF formulas
- `n-repeat`: Number of times to repeat evaluation
The evaluation results will be logged to Weights & Biases.
## Reinforcement Fine-Tuning (RFT)
```bash
# Run RFT training
CUDA_VISIBLE_DEVICES=0,1,2,3 nohup uv run --group rft trl vllm-serve --model "Qwen/Qwen2.5-7B-Instruct" --tensor_parallel_size 4 --max_model_len 16384 --gpu_memory_utilization 0.9 --enable_prefix_caching True &
CUDA_VISIBLE_DEVICES=4,5,6,7 uv run --group rft accelerate launch --num-processes 4 --config-file zero3.yaml rft.py --model-id "Qwen/Qwen2.5-7B-Instruct" --p-list SATSP --q-list math --exp-name "test" --server-ip "0.0.0.0"
```
### RFT Parameters
- `model-id`: Base model to fine-tune (default: "Qwen/Qwen2.5-7B-Instruct")
- `p-list`: Problem types for training (e.g., "SATSP", "MaxSAT", "MCS", "MUS", "SATDP_SAT", "SATDP_UNSAT")
- `q-list`: Question formats for training (e.g., "math", "story")
- `exp-name`: Name of your experiment
- `server-ip`: IP address for VLLM server
## Citation
```bibtex
@misc{satquest2025,
author = {Yanxiao Zhao, Yaqian Li, Zihao Bo, Rinyoichi Takezoe, Haojia Hui, Mo Guang, Lei Ren, Xiaolin Qin, Kaiwen Long},
title = {SATQuest: A Verifier for Logical Reasoning Evaluation and Reinforcement Fine-Tuning of LLMs},
year = {2025},
publisher = {GitHub},
journal = {GitHub repository},
howpublished = {\url{https://github.com/sdpkjc/SATQuest}},
}
```
Raw data
{
"_id": null,
"home_page": null,
"name": "satquest",
"maintainer": null,
"docs_url": null,
"requires_python": ">=3.10",
"maintainer_email": "Yanxiao Zhao <pazyx728@gmail.com>",
"keywords": "LLM, reasoning, evaluation, reinforcement-learning",
"author": null,
"author_email": "Yanxiao Zhao <pazyx728@gmail.com>",
"download_url": "https://files.pythonhosted.org/packages/2f/31/2ac149667fa8d39611dd7ea462de0414e76566853b25801fca115015ac68/satquest-0.1.2.tar.gz",
"platform": null,
"description": "# SATQuest: A Verifier for Logical Reasoning Evaluation and Reinforcement Fine-Tuning of LLMs\n\n[Preprint Paper](./SATQuest-paper.pdf)\n\n[](https://opensource.org/licenses/MIT)\n[](https://github.com/sdpkjc/SATQuest)\n[](https://pypi.org/project/satquest/)\n\n\n\n## \ud83d\ude80 Quickstart\n\n```python\n# Install dependencies\n# pip install datasets satquest\n\nfrom datasets import load_dataset\nfrom satquest import CNF, create_problem, create_question\n\nitem = load_dataset('sdpkjc/SATQuest', split='test')[0]\ncnf = CNF(dimacs=item['sat_dimacs'])\n# cnf.shuffle()\n\nproblem = create_problem('SATSP', cnf) # or 'SATDP', 'MaxSAT', 'MCS', 'MUS'\nquestion = create_question('math') # or 'dimacs', 'story', 'dualstory'\nprompt = problem.accept(question)\nanswer = problem.solution # reference answer\nreward = int(problem.check(answer)) # 1 if answer is correct, 0 otherwise\n```\n\n## Dataset Generation\n\n[]([https://huggingface.co/sdpkjc/](https://huggingface.co/collections/sdpkjc/satquest-6820687d856b96f869921e53))\n\n```bash\n# Run dataset generation\nuv run --group gen gen_cnf_dataset.py --hf-entity {YOUR_HF_ENTITY} --seed 9527\n\nuv run --group gen gen_cnf_rft_dataset.py --hf-entity {YOUR_HF_ENTITY} --seed 9527\n```\n\n## Evaluation\n\n```bash\n# Run evaluation\nuv run --group eval eval_model.py \\\n --exp-name {YOUR_EXP_NAME} \\\n --wandb-project \"SATQuest-Eval\" \\\n --hf-dataset-name \"sdpkjc/SATQuest\" \\\n --p-type-list SATSP \\\n --q-type-list math \\\n --llm-model \"gpt-4o\" \\\n --max-tokens 16384 \\\n --temperature 0.6 \\\n --num-example 10 \\\n --stream True \\\n --cnf-shuffle False \\\n --n-repeat 1\n```\n\n### Evaluation Parameters\n\n- `exp-name`: Name of your experiment\n- `wandb-project`: Weights & Biases project name\n- `hf-dataset-name`: HuggingFace dataset name\n- `p-type-list`: Problem types to evaluate (e.g., \"SATSP\", \"MaxSAT\", \"MCS\", \"MUS\", \"SATDP_SAT\", \"SATDP_UNSAT\")\n- `q-type-list`: Question types to evaluate (e.g., \"math\", \"dimacs\", \"story\", \"dualstory\")\n- `llm-model`: LLM model to use for evaluation\n- `max-tokens`: Maximum tokens for LLM response\n- `temperature`: Temperature for LLM generation\n- `num-example`: Number of examples to evaluate\n- `stream`: Whether to stream LLM responses\n- `cnf-shuffle`: Whether to shuffle CNF formulas\n- `n-repeat`: Number of times to repeat evaluation\n\nThe evaluation results will be logged to Weights & Biases.\n\n## Reinforcement Fine-Tuning (RFT)\n\n```bash\n# Run RFT training\nCUDA_VISIBLE_DEVICES=0,1,2,3 nohup uv run --group rft trl vllm-serve --model \"Qwen/Qwen2.5-7B-Instruct\" --tensor_parallel_size 4 --max_model_len 16384 --gpu_memory_utilization 0.9 --enable_prefix_caching True &\nCUDA_VISIBLE_DEVICES=4,5,6,7 uv run --group rft accelerate launch --num-processes 4 --config-file zero3.yaml rft.py --model-id \"Qwen/Qwen2.5-7B-Instruct\" --p-list SATSP --q-list math --exp-name \"test\" --server-ip \"0.0.0.0\"\n```\n\n### RFT Parameters\n\n- `model-id`: Base model to fine-tune (default: \"Qwen/Qwen2.5-7B-Instruct\")\n- `p-list`: Problem types for training (e.g., \"SATSP\", \"MaxSAT\", \"MCS\", \"MUS\", \"SATDP_SAT\", \"SATDP_UNSAT\")\n- `q-list`: Question formats for training (e.g., \"math\", \"story\")\n- `exp-name`: Name of your experiment\n- `server-ip`: IP address for VLLM server\n\n\n## Citation\n\n```bibtex\n@misc{satquest2025,\n author = {Yanxiao Zhao, Yaqian Li, Zihao Bo, Rinyoichi Takezoe, Haojia Hui, Mo Guang, Lei Ren, Xiaolin Qin, Kaiwen Long},\n title = {SATQuest: A Verifier for Logical Reasoning Evaluation and Reinforcement Fine-Tuning of LLMs},\n year = {2025},\n publisher = {GitHub},\n journal = {GitHub repository},\n howpublished = {\\url{https://github.com/sdpkjc/SATQuest}},\n}\n```\n",
"bugtrack_url": null,
"license": "MIT License Copyright (c) 2025 Adam Yanxiao Zhao Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the \"Software\"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. THE SOFTWARE IS PROVIDED \"AS IS\", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. ",
"summary": "A Verifier for Logical Reasoning Evaluation and Reinforcement Fine-Tuning of LLMs",
"version": "0.1.2",
"project_urls": {
"Documentation": "https://github.com/sdpkjc/satquest#readme",
"Homepage": "https://github.com/sdpkjc/satquest",
"Issues": "https://github.com/sdpkjc/satquest/issues",
"Source": "https://github.com/sdpkjc/satquest"
},
"split_keywords": [
"llm",
" reasoning",
" evaluation",
" reinforcement-learning"
],
"urls": [
{
"comment_text": null,
"digests": {
"blake2b_256": "4fcd15dd3ad856fc88b76b96d49cccdd3f83d97da5b63e530be2e9fd539cf066",
"md5": "fabefd473ca5515a3869c2b671b40c35",
"sha256": "8840be8f670dae92fbd1a965ae1dd3899c54a5ac6ad6bf5ddae22074e16fcaf4"
},
"downloads": -1,
"filename": "satquest-0.1.2-py3-none-any.whl",
"has_sig": false,
"md5_digest": "fabefd473ca5515a3869c2b671b40c35",
"packagetype": "bdist_wheel",
"python_version": "py3",
"requires_python": ">=3.10",
"size": 12477,
"upload_time": "2025-08-30T19:51:48",
"upload_time_iso_8601": "2025-08-30T19:51:48.791526Z",
"url": "https://files.pythonhosted.org/packages/4f/cd/15dd3ad856fc88b76b96d49cccdd3f83d97da5b63e530be2e9fd539cf066/satquest-0.1.2-py3-none-any.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": null,
"digests": {
"blake2b_256": "2f312ac149667fa8d39611dd7ea462de0414e76566853b25801fca115015ac68",
"md5": "6ec8b1f64e386383c2a55e7a99c5b798",
"sha256": "bc41fdc7714844eced1dc46a9d76fb820df02880b29f2beeb2430c1a1ced69d3"
},
"downloads": -1,
"filename": "satquest-0.1.2.tar.gz",
"has_sig": false,
"md5_digest": "6ec8b1f64e386383c2a55e7a99c5b798",
"packagetype": "sdist",
"python_version": "source",
"requires_python": ">=3.10",
"size": 13647,
"upload_time": "2025-08-30T19:51:50",
"upload_time_iso_8601": "2025-08-30T19:51:50.284333Z",
"url": "https://files.pythonhosted.org/packages/2f/31/2ac149667fa8d39611dd7ea462de0414e76566853b25801fca115015ac68/satquest-0.1.2.tar.gz",
"yanked": false,
"yanked_reason": null
}
],
"upload_time": "2025-08-30 19:51:50",
"github": true,
"gitlab": false,
"bitbucket": false,
"codeberg": false,
"github_user": "sdpkjc",
"github_project": "satquest#readme",
"travis_ci": false,
"coveralls": false,
"github_actions": false,
"lcname": "satquest"
}
