SATURN: SAT-based Reinforcement Learning to Unleash LLMs Reasoning

Thank you for your valuable comments. We will address your concerns point by point.

Q1: Which aspects of the difficulty estimation metric are most crucial?

Thank you for your insightful and professional question. In our early exploration, we conducted an ablation study of the SAT difficulty estimation metric on our SATURN‑2.6K test set. The dataset contains 10 categories of problems with 100 instances each, totaling 1,000 problems (Appendix G).

📊 Selected SAT Problem Difficulty $(n, k, l)$

The pass@3 results are shown below:

📊 Full pass@3 results on SATURN-2.6k (Test Set)

We then performed linear regression between each difficulty metric and model pass@3 (averaged across four models, with variance reported). The metrics capture different aspects including sparsity and structural complexity of SAT, as derived in Appendix C. The results are as follows:

📊 Metric Comparison Table

Our metric $\log_2(k) + 2 \cdot \log_2(l) - n + \frac{k}{n}$ combines both solution sparsity and structural complexity, and achieves the best overall correlation. The ratio between the solution space and the LLM’s search space is the most crucial aspect. On SATURN‑7B, the R² value is about 0.5 because pass@3 already achieves over 90% on easy problems, which limits the observable linear correlation in that range. Due to rebuttal length constraints, the corresponding figures are shown in Appendix Figures 9 and 10.

We will include this ablation study in future revisions to strengthen the paper. Thank you again for your valuable suggestion.

Q2: (Optional) Is the author's metric good at estimating difficulty for CDCL SAT solvers?

This is an excellent question. To fairly compare with LLM results, we tested a CDCL SAT solver on the SATURN-2.6k test set (see Appendix G). The results are as follows:

  Total instances:   1000
  Satisfiable:       1000
  Unsatisfiable:     0
  Valid SAT Models:  1000
  Model Accuracy:    100.00%
Total time taken: 0.14 seconds

It show that the CDCL SAT solver significantly outperforms current LLMs, even DeepSeek-R1.

Next, we focused on 3-SAT problems with 100 variables, varying the number of clauses $l$ from 200 to 800 in steps of 5. We recorded the solving time across SAT instances of increasing clause numbers. Due to rebuttal format limits that forbid image uploads, we provide the solving times as a list, where the values represent solver runtimes:

['3.30e-05', '4.01e-05', '7.00e-05', '3.02e-04', '2.46e-03', '1.48e-03', '1.26e-03', '8.68e-04', '5.51e-04', '4.76e-04', '4.25e-04', '3.95e-04', '2.98e-05']

Since the list is too long, for clarity we report the average of every 10 consecutive numbers. As a result, heuristic SAT solvers still rely on traditional phase transition theory as their difficulty metric. The difficulty estimation we present in the paper is specifically designed to simulate human-like and LLM-like search, verification, and backtracking processes in solving SAT. Our metric is based on the solution space and the search space of SAT problems.

We also discuss this distinction in Section 2.3 of the paper: However, RSB theory is designed for heuristic SAT solvers. For humans or LLMs solving SAT problems through logical steps like trial, verification, and reasoning, such solver-like phase transitions are hardly observable in human-like thinking processes.

Weakness 1: Logic-RL is quite similar, although, of course, there is value in SATURN's data generation methodology.

Thank you for your comment. We agree that SATURN and Logic-RL share the same perspective about LLM reasoning. However, SATURN offers three key advantages: (1) Controllable difficulty. SAT-based generation with our estimator allows stable, fine-grained curriculum control. (2) Better format following. LLMs trained with SATURN is easier to follow the required output format after RL, and (3) Stronger results. Our main experiments in RQ3 show that, SATURN consistently outperforms Logic-RL on math and programming tasks. Detailed results can be found in Appendix L.

Weakness 2: Why is this metric the best choice.

Please see the response to Q1.

Weakness 3: The syntax constraint (e.g., "\boxed{}") is unclear until the appendix.

We apologize for the confusion. In the revised version, we have moved this key information from the appendix to the main text.

Weakness 4: It is not obvious outside of the appendix that all queries are constructed to be satisfiable.

Thank you for the thoughtful and professional suggestion. We will clarify in the main text that all generated SAT queries are satisfiable by construction. This design avoids calling a SAT solver for ground-truth. We appreciate the reviewer for pointing out the need to make this explicit.

Finally, thank you very much for recognizing our work. Your suggestions are highly valuable to us. We sincerely appreciate your feedback!

Thank you for your follow-up comment. We would like to provide further clarification for Q2, including our benchmark selection and additional evaluation results:

1. Benchmark choice. Our original evaluation followed the widely adopted setup of DeepSeek-R1 [1], including AIME 2024/2025, AMC 2022/2023, Math500, GPQA-D, and LiveCodeBench, which are recognized as highly challenging benchmarks.

2. Additional benchmarks. Following [2,3], we further evaluate on GSM8K [4], Minerva Math [5], and OlympiadBench [6], which are also recognized as challenging benchmarks. The results are shown below:

Our method consistently improves over R1-Qwen on all new benchmarks, further demonstrating its effectiveness across challenging reasoning tasks.

Finally, we appreciate your constructive feedback. Please feel free to contact us if you have any further questions.

References
[1] Guo, Daya, et al. "Deepseek-r1: Incentivizing reasoning capability in llms via reinforcement learning." arXiv preprint arXiv:2501.12948 (2025).
[2] Hu, Jingcheng, et al. "Open-reasoner-zero: An open source approach to scaling up reinforcement learning on the base model." arXiv preprint arXiv:2503.24290 (2025).
[3] Zeng, Weihao, et al. "Simplerl-zoo: Investigating and taming zero reinforcement learning for open base models in the wild." arXiv preprint arXiv:2503.18892 (2025).
[4] Cobbe, Karl, et al. "Training verifiers to solve math word problems." arXiv preprint arXiv:2110.14168 (2021).
[5] Lewkowycz, Aitor, et al. "Solving quantitative reasoning problems with language models." arXiv preprint arXiv:2206.14858 (2022).
[6] He, Chaoqun, et al. "Olympiadbench: A challenging benchmark for promoting agi with olympiad-level bilingual multimodal scientific problems." arXiv preprint arXiv:2402.14008 (2024).

Q1: How do you ensure that SAT tasks require multi-step reasoning?

We demonstrate the LLM’s multi-step logical reasoning in our Weakness 2 analysis.

Due to the rebuttal length limit, we cannot include the full SAT solving traces here. More reasoning examples are provided in Appendix K and in the supplementary materials.

Q2: How about SATURN vs. SFT?

Our setting is RLVR, where no supervised data with intermediate CoT annotations are available; only a verifier checks whether the LLM’s final answer is correct. RL encourages the model to explore reasoning paths on its own, which SFT cannot achieve without costly CoT annotations, which are unavailable in our dataset.

A detailed discussion is provided in Weakness 3.

Q3: Would training on richer formal logic problems (e.g., QBF, theorem proving) would better?

Thank you for this insightful question. We answer from two perspectives.

1. There is some work on RL training for theorem-proving tasks [4]. However, the difficulty of these problems is hard to control, which makes curriculum design challenging. This is an advantage of SAT, as we can generate large-scale instances with adjustable complexity.

2. Our work is an initial exploration of how SAT can enhance the reasoning capability of LLMs. QBF is a natural extension of SAT that incorporates quantifiers into propositional logic, and we plan to explore QBF in future work to provide richer logical problems.

Q4: How does SAT generalize to semantic understanding or abstraction tasks?

Thank you for raising this important point. We agree that semantic understanding is an important capability of the LLM. However, the RLVR community (e.g., Deepseek-R1 [5], OpenAI O-series model [6]) mainly focuses on evaluating the reasoning capability of LLMs, with benchmarks in domains such as math and code. Semantic understanding or other tasks are largely out of scope for current RLVR studies, though future work may explore it.

Q5: Have you tested model behavior on harder SAT instances?

We sincerely thank the reviewer for this clear and important question. Yes, we have evaluated SATURN-2.6k (Test Set) on SAT problems beyond 3-SAT, including 4-SAT and 5-SAT. We selected 10 categories of problems with 100 instances each, totaling 1,000 problems.

📊 Selected SAT Problem Difficulty $(n, k, l)$

The pass@3 results are shown below:

📊 Full pass@3 results on SATURN-2.6k (Test Set)

More detailed experimental results can be found in Appendix G of the paper.

Weakness 1: Overly simple SAT datasets

Thank you for your comment. We address the concern as follows:

1.Difficulty should match LLM's capability. As shown in our RQ1 experiments, even SAT instances far from the classical phase transition remain non‑trivial for LLMs. Simply increasing SAT hardness would not better build reasoning capabilities, if the LLM cannot yet solve easier cases.

2.LLMs are not simply doing pattern matching. Appendix L, the supplementary materials, and CoT examples provided in Weakness 2 demonstrate that the models perform strictly step‑by‑step, clause-by-clause reasoning, rather than pattern matching.

3.Curriculum learning ensures effective training. Our framework strictly progresses from easy to hard, enabling both models from 1.5B to 7B parameters to gradually build reasoning capabilities.

Weakness 2: Whether SAT is suitable for reasoning skills

We appreciate the reviewer’s professional question regarding. We agree that understanding the underlying mechanisms is important. To this end, we offer key supporting evidence.

A recent study, Cognitive Behaviors that Enable Self-Improving Reasoners, or, Four Habits of Highly Effective STaRs [1], identifies four core habits shared by expert human reasoners and LLMs: (1) verification, (2) backtracking, (3) subgoal setting, and (4) backward chaining. These behaviors are domain-agnostic and fundamental for solving general reasoning tasks. And [2] proposed the same concept of meta-ability. The meta-ability represent general reasoning patterns that can be generalized across SAT, math, and programming tasks. In the following, we present additional case studies to illustrate how SATURN works.

Case 1

To better understand how SATURN promotes these behaviors, we provide a case study comparing SATURN and a baseline model on the same SAT instance:

¬A∨¬B∨¬D ∧ ¬B∨¬C∨D ∧ A∨¬B∨¬C ∧ A∨C∨E ∧ B∨C∨D

R1-Distill-1.5B fails on this instance. Its trace is shown below:

Wait, in the solution, D=0, so clause 3: A ∨ ¬B ∨ ¬C → 0 ∨ 0 ∨ 1 → True.

Yes, that's correct.

Clause 4: A ∨ C ∨ E → 0 ∨ 0 ∨ 0 → True.

Clause 5: B ∨ C ∨ D → 0 ∨ 0 ∨ 0 → True.

So, I think that's a valid solution.

The model skips verification of earlier clauses and fails to backtrack after contradictions. The reasoning is shallow and linear. It does not apply backward chaining from goal constraints.

In contrast, SATURN-1.5B produces the following trace:

Hmm, that's a contradiction. So, my assumption that B=False leads to a problem with clause 1. Therefore, B cannot be false.

So, B must be true. Let me backtrack.

Earlier, I assumed A=True, and then B=False led to a contradiction. So, B must be true.

Let me restart with A=True and B=True.

Then, let's look at clause 1: ¬A ∨ ¬B ∨ ¬D. Since A and B are true, ¬A and ¬B are false, so for the clause to be true, ¬D must be true. Therefore, D must be false.

So, D=False.

This trace shows verification of clause satisfaction, backtracking after an invalid assumption, and backward chaining from clause structure to variable assignments. These capabilities help the model reason accurately across steps. Additional examples illustrating these reasoning behaviors are provided in Appendix K, RQ4, and the supplementary materials submitted with the paper.

Weakness 3: Lack of RL Analysis

Thank you for the valuable comment. We address your concern from two perspectives:

1. RL improves reasoning and generalization. Prior work (e.g., SFT Memorizes, RL Generalizes: A Comparative Study of Foundation Model Post-training) shows that SFT often overfits to training data. In contrast, RL helps the LLM self-explore and check its reasoning steps. This leads to better reasoning and generalization.

2. RL reduces the need for data. SFT needs carefully prepared training data with CoT anotation, which is difficult collected. However, reinforcement learning with verifiable rewards (RLVR) makes it practical to improve reasoning without extensive supervised data.

Weakness 4: Modest improvements

We clarify that our model is not trained on additional math or code tasks. The observed improvements therefore come from enhanced reasoning learned from SAT tasks, rather than domain transfer or data variance. This is a reliable improvement in the model’s own reasoning capability, as also illustrated in Weakness 2 and in Appendix.

Moreover, these math and code benchmarks are relatively difficult among current benchmarks. The experimental results in paper's RQ3 show that SATURN's performance improvement exceeds prior methods.

---

[1] Gandhi, Kanishk, et al. "Cognitive behaviors that enable self-improving reasoners, or, four habits of highly effective stars." arXiv preprint arXiv:2503.01307 (2025).

[2] Hu, Zhiyuan, et al. "Beyond'Aha!': Toward Systematic Meta-Abilities Alignment in Large Reasoning Models." arXiv preprint arXiv:2505.10554 (2025).

[3] Chu, Tianzhe, et al. "SFT Memorizes, RL Generalizes: A Comparative Study of Foundation Model Post-training." arXiv preprint arXiv:2501.17161 (2025).

[4] Dong, Kefan, and Tengyu Ma. "Stp: Self-play llm theorem provers with iterative conjecturing and proving." arXiv preprint arXiv:2502.00212 (2025).

[5] Guo, Daya, et al. "Deepseek-r1: Incentivizing reasoning capability in llms via reinforcement learning." arXiv preprint arXiv:2501.12948 (2025).

[6] Jaech, Aaron, et al. "Openai o1 system card." arXiv preprint arXiv:2412.16720 (2024).

We sincerely appreciate your follow-up comment.

Since our SAT datasets cannot provide CoT annotations due to their result verification nature, we trained an SFT-only baseline on the Math training dataset [1], which is the source of the Math500 benchmark and contains step by step problem solutions:

{
  "input": "How many nonzero terms are in the expansion of $$(x+4)(2x^2+3x+9)-3(x^3-2x^2+7x)?$$
Please reason step by step, and put your final answer within \\boxed{}.",
  "output": "First, we multiply a degree-$1$ term and a degree-$2$ term, so we have a degree-$3$ polynomial. We subtract a constant times a degree-$3$ polynomial, so we can have at most a degree-$3$ polynomial, so at most $4$ terms. However, we are unsure if any of the terms will subtract to zero, so we must multiply out the polynomials:  \
$
\n&(x+4)(2x^2+3x+9)-3(x^3-2x^2+7x)\\\\\n&\\qquad=x(2x^2+3x+9)+4(2x^2+3x+9)-(3x^3-6x^2+21x)\\\\\n&\\qquad=2x^3+3x^2+9x+8x^2+12x+36-(3x^3-6x^2+21x)\\\\\n&\\qquad=2x^3+11x^2+21x+36-(3x^3-6x^2+21x)\\\\\n&\\qquad=2x^3-3x^3+11x^2+6x^2+21x-21x+36\\\\\n&\\qquad=-x^3+17x^2+36.\n\
$
As we can see, the linear term drops out, and we are left with $\\boxed{3}$ terms.",
  "answer": "\\boxed{3}"
}

We follow the template of DeepSeek-R1-Distill-Qwen-1.5B to construct the training data:

<｜begin▁of▁sentence｜><｜User｜>{input}<｜Assistant｜><think>{output}<\think>\n\n{answer}

We use the TRL framework [2] for SFT. To ensure fairness in dataset size, we randomly select the most difficult Level-5 1,000 problems from the math training set for one epoch of SFT. The training hyperparameters are:

The results are shown below:

Consistent with the observations in SFT Memorizes, RL Generalizes [3], SFT improves performance on math related benchmarks (AIME, AMC, and Math500) that are similar to its supervised training domain. However, it slightly degrades on LiveCodeBench, exhibiting alignment tax [4], where SFT to a narrow domain compromises performance on other tasks. In contrast, RL training on SAT (Saturn) improves performance across all benchmarks, reflecting enhanced general reasoning.

Finally, thank you again for your valuable comment. Please let us know if further details are needed.

References

[1] Hendrycks, Dan, et al. “Measuring Mathematical Problem Solving with the MATH Dataset.” NeurIPS, 2021.

[2] von Werra, Leandro, et al. TRL: Transformer Reinforcement Learning. GitHub, https://github.com/huggingface/trl.

[3] Chu, Tian, et al. “SFT Memorizes, RL Generalizes: A Comparative Study of Foundation Model Post Training.” arXiv preprint arXiv:2501.17161, 2025.

[4] Ouyang, Long, et al. "Training language models to follow instructions with human feedback." Advances in neural information processing systems 35 (2022): 27730-27744.

We are grateful for your detailed review and valuable suggestions. Each point you raised is addressed below.

Q1: Could you provide more intuition or empirical validation for the chosen difficulty metric?

Thank you for your insightful and professional question. In our early exploration, we conducted an ablation study of the SAT difficulty estimation metric on our SATURN‑2.6K test set. The dataset contains 10 categories of problems with 100 instances each, totaling 1,000 problems (Appendix G).

📊 Selected SAT Problem Difficulty $(n, k, l)$

The pass@3 results are shown below:

📊 Full pass@3 results on SATURN-2.6k (Test Set)

We then performed linear regression between each difficulty metric and model pass@3 (averaged across four models, with variance reported). The metrics capture different aspects including sparsity and structural complexity of SAT, as derived in Appendix C. The results are as follows:

📊 Metric Comparison Table

Our metric $\log_2(k) + 2 \cdot \log_2(l) - n + \frac{k}{n}$ combines both solution sparsity and structural complexity, and achieves the best overall correlation. The ratio between the solution space and the LLM’s search space is the most crucial aspect. On SATURN‑7B, the R² value is about 0.5 because pass@3 already achieves over 90% on easy problems, which limits the observable linear correlation in that range. Due to rebuttal length constraints, the corresponding figures are shown in Appendix Figures 9 and 10.

We will include this ablation study in future revisions to strengthen the paper. Thank you again for your valuable suggestion.

Q2: How does SATURN work?

We appreciate the reviewer’s professional question regarding why training on SAT problems helps generalization to other domains such as math and code. We agree that understanding the underlying mechanisms is important. To this end, we offer key supporting evidence.

A recent study, Cognitive Behaviors that Enable Self-Improving Reasoners, or, Four Habits of Highly Effective STaRs [1], identifies four core habits shared by expert human reasoners and LLMs: (1) verification, (2) backtracking, (3) subgoal setting, and (4) backward chaining. These behaviors are domain-agnostic and fundamental for solving general reasoning tasks. And [2] proposed the same concept of meta-ability. The meta-ability represent general reasoning patterns that can be generalized across SAT, math, and programming tasks. In the following, we present additional case studies to illustrate how SATURN works.

Case 1

To better understand how SATURN promotes these behaviors, we provide a case study comparing SATURN and a baseline model on the same SAT instance:

¬A∨¬B∨¬D ∧ ¬B∨¬C∨D ∧ A∨¬B∨¬C ∧ A∨C∨E ∧ B∨C∨D

R1-Distill-1.5B fails on this instance. Its trace is shown below:

Wait, in the solution, D=0, so clause 3: A ∨ ¬B ∨ ¬C → 0 ∨ 0 ∨ 1 → True.

Yes, that's correct.

Clause 4: A ∨ C ∨ E → 0 ∨ 0 ∨ 0 → True.

Clause 5: B ∨ C ∨ D → 0 ∨ 0 ∨ 0 → True.

So, I think that's a valid solution.

The model skips verification of earlier clauses and fails to backtrack after contradictions. The reasoning is shallow and linear. It does not apply backward chaining from goal constraints.

In contrast, SATURN-1.5B produces the following trace:

Hmm, that's a contradiction. So, my assumption that B=False leads to a problem with clause 1. Therefore, B cannot be false.

So, B must be true. Let me backtrack.

Earlier, I assumed A=True, and then B=False led to a contradiction. So, B must be true.

Let me restart with A=True and B=True.

Then, let's look at clause 1: ¬A ∨ ¬B ∨ ¬D. Since A and B are true, ¬A and ¬B are false, so for the clause to be true, ¬D must be true. Therefore, D must be false.

So, D=False.

This trace shows verification of clause satisfaction, backtracking after an invalid assumption, and backward chaining from clause structure to variable assignments. These capabilities help the model reason accurately across steps.

Case 2

We observe the same behaviors in LiveCodeBench.

You are given an array of positive integers nums.
An array is called product equivalent if the product of all elements equals gcd(arr) * lcm(arr).
Return the length of the longest product equivalent subarray.
A subarray is a contiguous non-empty sequence of elements in the array.

The R1-Distill-7B gives the following incorrect CoT:

Initialize current_gcd to 0 (or None)\n    Initialize current_lcm to 1\n    For each j from i to len(nums)-1:\n        current_product *= nums[j]\n        current_gcd = gcd(current_gcd, nums[j]) if current_gcd is not None else nums[j]\n        current_lcm = lcm(current_gcd, nums[j]) if current_gcd is not None else nums[j]\n
...
class Solution:
    def maxLength(self, nums: List[int]) -> int:
        max_len = 0
        n = len(nums)
        for i in range(n):
            current_product = 1
            current_gcd = nums[i]
            current_lcm = nums[i]
            for j in range(i, n):
                current_product *= nums[j]
                current_gcd = math.gcd(current_gcd, nums[j])
                # Incorrect: uses current_gcd instead of current_lcm
                current_lcm = math.lcm(current_gcd, nums[j])
                if current_product == current_gcd * current_lcm:
                    current_length = j - i + 1
                    if current_length > max_len:
                        max_len = current_length
        return max_len

This model incorrectly updates current_lcm using current_gcd. It fails to verify whether the condition is preserved after each step. It also does not backtrack or revise when the invariant breaks.

SATURN-7B corrects the error with a single key change:

current_lcm = (current_lcm * nums[j]) // math.gcd(current_lcm, nums[j])

This update uses the previous LCM, maintaining the correct invariant. The change reflects step-by-step verification and inference from the problem condition. The model traces through the logic and only updates when valid.

In summary, SATURN shows consistent use of verification, backtracking, and backward chaining across general reasoning tasks. These reasoning strategies, learned from SAT, enable generalization to unfamiliar domains through principled logical behavior. Additional examples illustrating these reasoning behaviors are provided in Appendix K and the supplementary materials submitted with the paper.

Q3: Have you investigated any strategies for overcoming the plateau?

Your question is very professional and forward-looking. Thank you for raising it.

Following the insights from the DeepScaleR [3], we explored extending the RL context length from 8k to 12k and then to 16k tokens to overcome the plateau. The effect was limited, and extremely long responses can trigger OOM under our compute constraints.

Our experiments confirm that SAT problems serve as an effective complement to math and code tasks. The plateau may be addressed through mixed hybrid curriculum training with SAT and math data. Due to time constraints, we conducted a very simple experiment: We fine-tuned SATURN-1.5B using RL for 50 steps on the GSM8K dataset. The results are as follows:

The idea of a hybrid curriculum with other reasoning tasks is excellent, and we will focus on it carefully in our future work.

Weakness 1: Transferability

Please see the response to Q2.

Weakness 2: Justification for Difficulty Metric

Please see the response to Q1.

Finally, we thank you for your thoughtful review and your recognition of our efforts.

---

[1] Gandhi, Kanishk, et al. "Cognitive behaviors that enable self-improving reasoners, or, four habits of highly effective stars." arXiv preprint arXiv:2503.01307 (2025).

[2] Hu, Zhiyuan, et al. "Beyond'Aha!': Toward Systematic Meta-Abilities Alignment in Large Reasoning Models." arXiv preprint arXiv:2505.10554 (2025).

[3] Luo, Michael, et al. DeepScaleR: Surpassing O1-Preview with a 1.5B Model by Scaling RL. 2025. Notion Blog.

Dear Reviewer np9g,

Thank you so much for your follow-up comment. We truly appreciate your recognition of our work and your dedicated review, which have been very helpful for improving our paper.

Please feel free to share any further thoughts or questions.

---

Thank you for your response. I'm sure you have addressed my concerns. I will keep my score of 4.

As a small note, we noticed that your comment appears under another reviewer’s thread, just in case it was unintentional.

Best regards, Authors

Thank you very much for your helpful comments. We respond to your concerns point by point in the following.

Q1: Why does SATURN work?

We appreciate the reviewer’s professional question regarding why training on SAT problems helps generalization to other domains such as math and code. We agree that understanding the underlying mechanisms is important. To this end, we offer key supporting evidence.

A recent study, Cognitive Behaviors that Enable Self-Improving Reasoners, or, Four Habits of Highly Effective STaRs [1], identifies four core habits shared by expert human reasoners and LLMs: (1) verification, (2) backtracking, (3) subgoal setting, and (4) backward chaining. These behaviors are domain-agnostic and fundamental for solving general reasoning tasks. And [2] proposed the same concept of meta-ability. The meta-ability represent general reasoning patterns that can be generalized across SAT, math, and programming tasks. In the following, we present additional case studies to illustrate how SATURN works.

Case 1

To better understand how SATURN promotes these behaviors, we provide a case study comparing SATURN and a baseline model on the same SAT instance:

¬A∨¬B∨¬D ∧ ¬B∨¬C∨D ∧ A∨¬B∨¬C ∧ A∨C∨E ∧ B∨C∨D

R1-Distill-1.5B fails on this instance. Its trace is shown below:

Wait, in the solution, D=0, so clause 3: A ∨ ¬B ∨ ¬C → 0 ∨ 0 ∨ 1 → True.

Yes, that's correct.

Clause 4: A ∨ C ∨ E → 0 ∨ 0 ∨ 0 → True.

Clause 5: B ∨ C ∨ D → 0 ∨ 0 ∨ 0 → True.

So, I think that's a valid solution.

The model skips verification of earlier clauses and fails to backtrack after contradictions. The reasoning is shallow and linear. It does not apply backward chaining from goal constraints.

In contrast, SATURN-1.5B produces the following trace:

Hmm, that's a contradiction. So, my assumption that B=False leads to a problem with clause 1. Therefore, B cannot be false.

So, B must be true. Let me backtrack.

Earlier, I assumed A=True, and then B=False led to a contradiction. So, B must be true.

Let me restart with A=True and B=True.

Then, let's look at clause 1: ¬A ∨ ¬B ∨ ¬D. Since A and B are true, ¬A and ¬B are false, so for the clause to be true, ¬D must be true. Therefore, D must be false.

So, D=False.

This trace shows verification of clause satisfaction, backtracking after an invalid assumption, and backward chaining from clause structure to variable assignments. These capabilities help the model reason accurately across steps.

Case 2

We observe the same behaviors in LiveCodeBench.

You are given an array of positive integers nums.
An array is called product equivalent if the product of all elements equals gcd(arr) * lcm(arr).
Return the length of the longest product equivalent subarray.
A subarray is a contiguous non-empty sequence of elements in the array.

The R1-Distill-7B gives the following incorrect CoT:

Initialize current_gcd to 0 (or None)\n    Initialize current_lcm to 1\n    For each j from i to len(nums)-1:\n        current_product *= nums[j]\n        current_gcd = gcd(current_gcd, nums[j]) if current_gcd is not None else nums[j]\n        current_lcm = lcm(current_gcd, nums[j]) if current_gcd is not None else nums[j]\n
...
class Solution:
    def maxLength(self, nums: List[int]) -> int:
        max_len = 0
        n = len(nums)
        for i in range(n):
            current_product = 1
            current_gcd = nums[i]
            current_lcm = nums[i]
            for j in range(i, n):
                current_product *= nums[j]
                current_gcd = math.gcd(current_gcd, nums[j])
                # Incorrect: uses current_gcd instead of current_lcm
                current_lcm = math.lcm(current_gcd, nums[j])
                if current_product == current_gcd * current_lcm:
                    current_length = j - i + 1
                    if current_length > max_len:
                        max_len = current_length
        return max_len

This model incorrectly updates current_lcm using current_gcd. It fails to verify whether the condition is preserved after each step. It also does not backtrack or revise when the invariant breaks.

SATURN-7B corrects the error with a single key change:

current_lcm = (current_lcm * nums[j]) // math.gcd(current_lcm, nums[j])

This update uses the previous LCM, maintaining the correct invariant. The change reflects step-by-step verification and inference from the problem condition. The model traces through the logic and only updates when valid.

In summary, SATURN shows consistent use of verification, backtracking, and backward chaining across general reasoning tasks. These reasoning strategies, learned from SAT, enable generalization to unfamiliar domains through principled logical behavior. Additional examples illustrating these reasoning behaviors are provided in Appendix K and the supplementary materials submitted with the paper.

Q2: Have you evaluated SATURN on SAT problems beyond 3‑SAT?

We sincerely thank the reviewer for this clear and important question. Yes, we have evaluated SATURN-2.6k (Test Set) on SAT problems beyond 3-SAT, including 4-SAT and 5-SAT. We selected 10 categories of problems with 100 instances each, totaling 1,000 problems.

📊 Selected SAT Problem Difficulty $(n, k, l)$

The pass@3 results are shown below:

📊 Full pass@3 results on SATURN-2.6k (Test Set)

More detailed experimental results can be found in Appendix G of the paper.

Q3: Why does Saturn-7B perform worse on AIME24/25?

Thank you for the important question. We appreciate the reviewer for pointing out the performance gap on AIME24/25. We believe this drop is primarily due to the limitations discussed in Section 5, especially Limitation ❶: Knowledge limitations ❸ Plasticity and Forgetting.

For instance, SATURN-7B failed on the following AIME 2024 problem:

Let $ABCDEF$ be a convex equilateral hexagon in which all pairs of opposite sides are parallel. The triangle whose sides are extensions of segments $AB, CD,$ and $EF$ has side lengths 200, 240, and 300. Find the side length of the hexagon.

After manual checking, SATURN-7B generates a mostly correct reasoning chain, but makes a small mistake at the final step by incorrectly applying the harmonic mean formula: $s = \frac{3}{\frac{1}{200} + \frac{1}{240} + \frac{1}{300}} = 240$ The correct relation is based on geometric decomposition: $s \left( \frac{1}{200} + \frac{1}{240} + \frac{1}{300} \right) = 1 \quad \Rightarrow \quad s = 80$

This error shows that the model selects a plausible-looking formula. SAT enhances the reasoning ability. But due to the potential issue of catastrophic forgetting in RL, certain math knowledge may be weakened. When the forgotten knowledge exceeds the improvement from enhanced reasoning, it appears as a drop in benchmark performance, especially on AIME, which is the hardest among these benchmarks.

However, it can be addressed through mixed hybrid curriculum training with SAT and math data. Due to time constraints, we conducted a very simple experiment: We fine-tuned SATURN-1.5B using RL for 50 steps on the GSM8K dataset. The results are as follows:

In future, we will focus on hybrid curriculum with other types of reasoning tasks.

Q4: How does response length differ between curriculum learning and mixed training?

Thank you for your question. Your question is very insightful and highly professional. We are glad to address the difference between the curriculum approach and the mixed training approach. We retained the logs from the mixed training ablation on Qwen2.5-7B-Instruct-1M. Since external links and images are not allowed, we present the response length at each step as a list:

[903.2, 1012.1, 1176.8, 1135.0, 1026.6, 842.7, 836.2, 852.7, 846.8, 852.6, 823.7, 777.5, 754.6, 769.4, 875.6, 943.7, 865.6, 803.7, 839.3, 793.5, 869.5, 926.2, 947.8, 961.4, 953.0]

Since the list is too long, for clarity we report the average of every 10 consecutive numbers. As shown, during the early stage of training, the response length increases slowly. After around 50 steps, it drops sharply and struggles to grow again. As a result, the final responses of the mixed training approach are noticeably shorter compared to the curriculum approach.

Weakness1: Why does SATURN work?

Please see the response to Q1.

Finally, your feedback is highly valuable to us, and we appreciate your recognition of our contribution.

---

[1] Gandhi, Kanishk, et al. "Cognitive behaviors that enable self-improving reasoners, or, four habits of highly effective stars." arXiv preprint arXiv:2503.01307 (2025).

[2] Hu, Zhiyuan, et al. "Beyond'Aha!': Toward Systematic Meta-Abilities Alignment in Large Reasoning Models." arXiv preprint arXiv:2505.10554 (2025).

Dear Reviewer SUsx,

Thank you for your comment and for carefully reviewing our paper. We appreciate your recognition of our work. And we will include the responses to each question in future versions.

We are happy to discuss any further questions at any time.

Best regards, Authors