PENCIL: Long Thoughts with Short Memory
Authors: Chenxiao Yang
Nathan Srebro
David McAllester
Zhiyuan Li
Venue: ICML 2025 poster (2025)
Keywords: Large language models
chain-of-thought
Primary area: deep_learning->large_language_models

Abstract: While state-of-the-art LLMs have demonstrated great promise of using long Chains-of-Thought (CoT) to boost reasoning, scaling it up to more challenging problems is fundamentally limited by suboptimal memory usage — intermediate computations accumulate indefinitely in context even no longer needed for future thoughts. We introduce PENCIL, which incorporates a novel reduction mechanism into the autoregressive generation process that recursively clean up intermediate thoughts based on patterns learned from training. By alternately generating and erasing, PENCIL can think deeper to solve harder problems using shorter context and less computes. Empirically, for example, we demonstrate PENCIL with a small 25M-parameter transformer and 2048 context length solves Einstein's puzzle — a task that challenges much larger models like GPT-4. Theoretically, we prove PENCIL can perform universal efficient computation by simulating any Turing machines with optimal time and space complexity, and thus can solve arbitrary computable tasks that are otherwise intractable for vanilla CoT.

PENCIL: Long Thoughts with Short Memory
Chenxiao Yang'
Nathan Srebro
David McAllester'
Zhiyuan Li'
Abstract
Sabharwal, 2023; Feng et al., 2024; Li al., 2024b) - it suffers from the inherent write-only limitation: partial com- putation remains in the context even when no longer needed for future thought generation. This design becomes particu- larly problematic for inherently hard reasoning tasks, where no efficient algorithm exists and thus reasoning inevitably spans many steps, foreing the context length to grow indefi- nitely. This not only demands excessive memory resources that become impractical for computationally hard tasks, but could also degrades the model's s ability to effectively retrieve information in the context, even when the maximum length is not exceeded (Liu et al., 2024).
While state-of-the-art LLMs have demonstrated great promise of using long Chains-of-Thouus (CoT) to boost reasoning, scaling it up to more challenging problems is fundamentally limited by suboptimal memory usage intermediate com- putations accumulate indefinitely in context even no longer needed for future thoughts. We intro- duce PENCIL, which incorporates a novel reduc- tion mechanism into the autoregressive genera- tion process that recursively clean up intermedi- ate thoughts based on patterns learned from train- ing. By alternately generating and erasing, PEN- CIL can think deeper to solve harder problems using shorter context and less computes. Empiri- cally, for example, we demonstrate PENCIL with small -arammeeeterr transformer and 2048 con- text length solves Einstein's 's puzzle- task that challenges much larger models like GPT-4. Theo- retically, we prove PENCIL can perform universal efficient computation by simulating any Turing machines with optimal time and space complexity, and thus can solve arbitrary computable tasks that are otherwise intractable for vanilla COT.
Memory management is a major issue in modern computer systems. Turing machines, for example, can overwrite tape cells and reclaim space for new computations, while high- level programming languages rely on stack frames, func- tion calls, and garbage collection to discard unneeded data. While some previous works have attempted to augment LLMs with external memory (e.g. (Gao et al., 2023; Wang et al., 2024)), they often lack a direct mechanism for recla- mation of no longer needed memory as stack deallocation or garbage collection. This paper proposes PENCIL, which introduces cleaning mechanisms to CoT for space-efficient and long-chain reasoning.
In a nutshell, PENCIL combines a next-token generator (e.g.. a decoder-only transformer) and a reduction rule, and applies the reduction rule whenever possible throughout the standard iterative next-token generation process to reduce context length. In this paper, we focus on simple yet universal reduction rule motivated by the function call stack in modern computers.
1. Introduction
Recently, there has been a surge of interest in reasoning with Chain-offThough (CoT) (Wei et al., 2022) and gen- erating longer thoughts test-time to tackle larger-scale and more complicated problems (OpenAI, 2024; Guo et al., 2025; Snell et al., 2024; Muennighoff et al., 2025). CoT is an iterative generation process: each intermediate reason- ing step is appended to the current context and treated as the input in subsequent reasoning. The context grows until reaching final answer. While such an iterative model is theoretically powerful capable, in principle, of tackling many intricate problems given unlimited length (Merrill &
C [CALL] T [SEP] A [RETURN] CA (I)
where [CALL], [SEP], J, and [RETURN] are special to- kens that separate the context (C), thoughts (T), and answer (A) in the sequence. Once a computation completes (marked by [RETURN]) ), all intermediate reasoning steps (those be- tween [CALL] and [SEP]) ) will be removed, merging the answer back into the context. Importantly, this process can be applied recursively, allowing for hierarchical reasoning structures similar nested function calls programming. PENCIL alternates between standard CoT-style generation
'Toyota Technological Institute at Chicago. Correspondence to: Chenxiao Yang <ehenxiao@@ waaiiiaaattiiccu.... edic.edu>.
Proceedings of the 42nd International Conference Machine Learning. Vancouver, Canada. PMLR 267, 2025. Copyright 20255 by the author(s).
PPENCIL ENables Context-efficient Inference and Learning

---

PENCIL: Long Thoughts with Short Memory
Prompt: A toy store put together party bage for birthday. They made 3 blue bags with 5 toys each and red bags with toys each. How many toys were used total?
L'nddo prompt 1 [CADL] Let's break this problem down into parts! [cass] First, let's figure how many toya
Chain-of-Thooe Thoought
blue bags. Looking the blue bags, bags with toys each, muttiplying 3 15. [SEP] There were 15 toys blue bage. [8370R8]]
Let's break this problem down into parts! First, let's figure out how many loys were all blue bags. Looking at the blue bage, they made 3 bags with loys each, so mulliplying x 5 = 16. There were 15 loys in all blue bagg. That's just part the story though how many toys were in all red bags. Looking at the red bags, they made bags with loys each, so mulliplying x B. There were toys all red bage. Now that we know both amounts, we can find the total loys by adding the toys from blue and red bags together: used in total.
Response: :
"Cndor [CAM Lat's break this problem down into parts! There ware toya bage.
need know
[EndDE Pecmpt] ] [CAss] Let's break this probiem down into parts! There were toys all blue bags. [CALa] That's just part of the story though- we still need to know how [SRP] There bags, they made bags toys toys
many toys all red bags, Looking
each, mulliplyyng
bags. [R37URM]
23. There 23 toys
[3ndOPPooppt I I break this problem down into parts! There blue bags.
loys
bage.
PENCIL
LindDE Peompt) ] [eaus] Let's break this problem down into parts! There were 16 toys blue There find total toys adding toys There were toys used total. [RETUSS]]
Response: : There were 23 loys used in total.
red New that red bags together: 8
both amounts, we can
Mudel Generation
Context [CAas]] Interneciate Thoughts [BEP] Anewer [ARIUR
Landoe Veanpt) There were 23 toys used in total
Reduction Rule
[inDDEPeomp J There were 23 toys used in total. (EndDE7exx.)
Context Answer]
(a) PENCIL
(b) Hidden thoughts of PENCIL
Figure I: A toy example illustrating how PENCIL would potentially solve an arithmetic problem. Bold text indicates content generated in the current iteration, content highlighted in blue indicates intermediate thoughts to be erased by the reduction rule. See a concrete example of the complete thinking process for solving QBF in Fig. 2 and Einstein's 's puzzle in Fig. 8.
and this reduction step, automatically discarding unneeded thoughts based on patterns learned from training. Figure gives a hypothetical example of how PENCIL might be applied to natural language thoughts.
See discussions about related work in Appendix A. Codes are available at https: / //tgthub..t/tt/////// wwtcchub.coooococc chr26195/ PENCIL.
2. PENCIL: Iterative Generation & Reduction
We train and evaluate PENCIL on SAT, QBF, and Einstein's puzzle- - tasks that inherently require exponential com- putation time. PENCIL effectively reduces the maximal CoT length (i.e. the space requirement) from exponential to polynomial. Consequently, under fixed architecture and context window, PENCIL allows solving larger-sized prob- lems whereas CoT fails due to exploding context length. Furthermore, by continually discarding irrelevant tokens, PENCIL can significantly save training computes and con- verge faster even when memory or expressiveness is not a bottleneck. Notably, on the 5x5 Einstein puzzle- - a chal- lenging natural- languuag logic puzzle that even large models like GPT-4 struggle with PENCIL achieves 97% success rate by using small transformer with 25M-parameter and 2048-token context.
Chain-of- Thhoughh (CoT) (Wei et al., 2022) allows language models to generate intermediate reasoning steps before pro- ducing final answer. Formally, given finite alphabet Σ, let π Σ' + Σ be a next-token predictor, which maps an input sequence (2,, ,Tn) E Σ" to the next token In++1 E Σ. Correspondingly, we can define a sequence-to- sequence mapping f Σ' + >" as
[x un) A (#I,..., Iny ((), In))
which concatenates the next token to the current context. For brevity, we will write f instead of fx when the context is clear. CoT with l: steps is denoted as f : E" + Σ* where f _ f o fk-1 and f & f. Given any input se- quence x = #2........... .n) E E", each application of extends the sequence by one token, such that fx()) E I= Throughout this paper, we use shorthand T.j to denote (z1,..., 22)) and Fyy the subsequence from x; to 2j. for any string x E Σ* longer than j.
Theoretically, we show that PENCIL with a fixed finite- size decoder-only transformer can perform universal space- efficient computation, by simulating Turing machine run- ning in T steps and S space with (T) generated tokens and maximal sequence length ((S). This indicates its power for solving any computational tasks with optimal time and space efficiency. This is significant improvement over standard CoT, which require context length to grow pro- portionally with OTT), making them fundamentally unable to solve problems requiring extensive computation within fixed memory constraints.
The iterative generation process of CoT is inherently limited by its write-once nature; that is, once written, intermedi- ate computations permanently occupy the context, regard- less of their relevance in the subsequent reasoning steps. Consequently, the context length would eventually grow overwhelmingly large for complex reasoning problems. To address this, we introduce PENCIL, which is CoT equipped
2

---

PENCIL: Long Thoughts with Short Memory
with a reduction rule that enables selective elimination of reasoning traces, allowing the model to generate longer thoughts to solve larger problems with less memory.
[SEP], [RETURN]) as in the standard CoT, and the re- duction rule & as defined in (1) that serves reduce the context and clean the memory. Formally, we define one step and k-steps of PENCIL as PENCIL = x o f and PENCIL f.f = (Φo Namely, each step of PENCIL first generates the next token as in standard CoT and then applies the reduction rule o, deleting the intermediate computations if the new sequence matches the pattern.
2.1. The Reduction Rule and PENCIL
A reduction rule (a.k.a. rewriting rule) (Baader & Nip- kow, 1998) is formal mechanism originated from logic for transforming one expression to another via predefined patterns and ultimately reaching a final normal form, i.c. the answer. serves as a fundamental model of computa- tion in classic functional programming languages such as A-calculus (O Donnell, 1985), and proof assistants for au- tomated theorem proving and reasoning (Wos al., 1992). Mathematicallly, the reduction rule can be thought of as sentence-tosequeene function Φ : Σ* + Σ", which in this paper is from a longer sequence (II,...,,ta xta) E 2" to a shorter one (I......,.T;.) E E where S a.
2.2. Alternated Generation and Reduction Process
The alternated generation and reduction process of PENCIL can also be interpreted by grouping the f functions that are interleaved by ineffective reduction steps (where & does not match the pattern):
PENCILE = fkket o oooooooo fhr o o..... 0.... op........... o fr
(4)
where = E1 k2 and k; denotes the number of tokens generated between the (i 11th and i-th effective reduction. Here is the total number of effective reductions, assuming the model terminates with a [EOS] token indicating stop generation. This process alternates between two phases
The Reduction Rule Let E oUt (CALL), [SEP], [RETURN] } be the extended alphabet including three spe- cial tokens that indicate certain structures of the reasoning trace. Given the new alphabet, we can instantiate the rule Φ as (I), where
Generation:
2(0) a fli a....... p (x)
C E [[CALL,)), [SEP], [RETURN] })"
T E (EU((SEP), [RETURN]] })"
(3)
a11-0.5)
(5)
Reduction: (11055) a
gh x 0 sh (x)
A (EU ([CALL))))
are subsequences separated by the special tokens. The al- lowance of difference special tokens in C, T, A ensures that: 1) the [RETURN] token is the last [RETURN] token in the sequence; 2) the [SEP] token in (I) is the one immediately before the [RETURN] token; ; 3) and the [CALL] token is immediately before the [SEP] token.
where z0() represents a generated sequence ending with [RETURN] except for 2=(++1) which ends with the [EOS] token, and (+(+0.5) represents the reduced sequence after each effective reduction, with (0.5) و defined as the input prompt. The complete reasoning trace can be expressed as:
Intuitively, C can be understood context that can include information that is either directly relevant to solving the cur- rent problem or irrelevant but useful for solving future prob- lems; T represents the intermediate thoughts for deriving the answer and A represents the answer. If the input sequence satisfy the pattern C [CALL] T [SEP] A [RETURN], the rule will activate. Consequently, the entire intermediate thoughts and the special token triplet will be removed, with the answer being merged back into the context. Otherwise if the pattern is not satisfied, the rule will leave the input sequence unchanged.
(1)
(1.5)
((++0.5)
M
((++)
(6)
That is, at each iteration i, PENCIL first generates from ((--0.5), which could be understood the prompt for the current iteration, to (x((), prompt-response pair that ends with the [RETURN] token; then PENCIL applies the reduc- tion rule to transform the prompt-response pair 2(1) into a new prompt (1+0.55 for the next iteration i +
Space Efficiency To compare the space efficiency of CoT and PENCIL, we define scaffolded CoT as the trace that would be produced by PENCIL but without actually remov- ing the thoughts (We refer to it as "scaffolded" because it includes the special tokens that mark the hierarchical reasoning structure.) Formally, for any input sequence x, scaffolded CoT is defined as
important to note that the inclusion of [CALL] in C enables nested reasoning structures critical for achieving op- timal space efficiency, while allowing [CALL] in A enables tail recursion optimization for better efficiency as will be discussed in Sec. 3.
(x x x00)
x (((+00)))
PENCIL consists of a learnable next-token predictor f as defined in (2) which is responsible for generating the inter- mediate reasoning steps (including special tokens [CALL],
where z(0) (F-00.) represents the tokens generated at iteration The max sequence length in PENCIL. is
3

---

PENCIL: Long Thoughts with Short Memory
Prompt: :2v:::2211:00 41 (2 -2 12
Generation
Reduccion
Chain-of-Thougee
(cacs, Question: prefic.trom 3.2 Try 2- False [CAS2]]
-.teddificoppc (CMG)) Questoon profee 4om Try huaiee [CASA3 Queatore
/Roa22//oopp:: [DKLL Queetor: partic
Question: prafxx_trom
- False [Caak]
protie from v Try I Palae [cssa] Questoon: enaicale In Palae Fale Check P0 1u True Cress #1 2 (SEP) Anower Fake ERETE001
2 11y2 Faise (1500) Queston pata fo Ty Paae
Question: evaluste 1 Faasee 2 Falce Check 80 (2
1 Check (1 (1 2) False (SBP; Answer:
False |RSTURM (888) Answer: False IRSTURM Tiy
Try Pube
Answer (RETUSM)
>9 TP
Fake
(CALL) Quesiio: fremx__rrm
C.PAkR cneel (ontzC Dusget prok Pore + Try 2- Foloo Answer Faloo Bry 3 Thus jonssy Queetion: prefic from v Try a Filne jesssa Gusetoo:: meluae i Falce True Check 10 a'll The Check 11 11 Thus Check (2) True true Check
/kaatt (DKU)) Queaber park homm
[[AaL]] Question: ovalunte = False 2- Thuo Chack 90
TTy = Areowr Pales Try - Thi (CKUA)
v v
True Check 81 (1 2 True Check #2
Gandon prete Jun 32 2- hake Arower
True Check ( -1 v 2)
True Check 2 1
Formuls True (SE2)
Check M4
Chock JoI
Creck
2- True Pormun
lyy
Farsa Armoer Thae
Anewer True [RETORM) Try 1 = True (catr] Question:
(cndooe (CAAL)) presto i_ Jrom 2 Try 2 Paaes Acuncen Palie Try 2 True (carci Gusden pooks from Try
[josdicieoop:: i. [Dkaa) Cuentoe parki hom Tiy farss Arewer Fale Try (Th05))
evaluate 1- True 2= True Check NO (2 - 1) True
Ainwor Than Try The pcatel Quastion:: asakane a This Trun Check 201 by--Ph True Check (1v2) True Check v2 True Check Jo ym Passe (288) Arswer Pulas (saccsay)
Check
True Check
True Check (->
Guedio predic vn Try
2 1) Faise (SEP) Answer: False [3RTUR)] [SSP]
The True Knewor Filte
Answer Faise [arTURN] [SEP] Answer: False
-=ISscodPooppt) (SALL) Quediion peelle Jumm 22 Try 2- rabu Acomea Pubee Try 2- Trae [0823) Checlt pot Notre fly hates Anoaa
Fi (OALL Quedtoo protic trn 32 habu Aroven: hibe by trw
[NEEUUIN]
Fabr ESEP) Arswent Polae (ERr0asy
Arama: Fube
PENCIL
Coastion pritic from aiyy Paker Amssar Paise 2ry Tris Aneeer Fubee (aany) Anawer: Faaes (actsay
Answer:
Figure 2: The complete thinking process of PENCIL on a small-sized QBF instance. The "..."
".." at the beginning of thought hides the prompt. Bold text represents newly generated thoughts, while blue highlights indicate thoughts to be removed.
Maximum Length
125500
Maximum Length
|50000
Maximum Length
150000
w/o Reduction
wio Reduction Reduction
wio Reduction
10000
Reduccion
120000
120000
w/ Reducciion
7500
205
90000
90000
ML0044
x0 122
5000
60000
60000
2500
30000
30000
01
0
5
6
7
8
10
3
7
8
Problem Size
Problem Size
Problem Size
(a) SAT
(b) QBF
(c) Einstein's 's puzzle
Figure 3: Maximal sequence length with and without the reduction rule.
[ax f1x:0113 whereas CoT has a length of n + k. As we will demonstrate in Sec. 3, their difference becomes particularly significant (i.e. (| < n + k) for complex reasoning tasks, where the context length of CoT can grow exponentially while the context length length of PENCIL is kept polynomial.
threshold 4.267 where instances are empirically hardest to solve and satisfiability probability transitions sharply from to (Selman et al., 1996). QBF is a PSPACE-complete problem that generalizes SAT by adding universal (V) and existential (3) quantifiers. Each instance is quantified Boolean formula in Prenex normal form, e.g., 3xy Vrgg (I1 V -a2 V ar)) A (-wn) V V22 V -r3). We set the probability of a variable being existentially quantified as 0.5.
Computational Benefits Moreover, even though the total number of predicted tokens or reasoning steps is the same with or without reduction, PENCIL can significantly save computes by maintaining a substantially shorter context for each generated token. We discuss in Appendix B the computational benefit of PENCIL in terms of the FLOPs for generating sequence and empirically quantify it in Sec. 4.
We consider using the DPLL algorithm to solve the SAT problem, and solving the QBF problem by recursively han- dling quantifiers and trying variable values. The PENCIL reasoning traces are generated as we run the algorithm. Both algorithms recursively explore variable assignments by splitting on an unassigned variable x; and trying branches x; True and x; = False. The reduction rule wraps each branch with [CALL], [SEP] J and [RETURN], which creates a hierarchical binary tree structure. See Fig. 2 for a concrete example.
3. Thinking with PENCIL
We next demonstrate how the reduction rule can be applied to several concrete computationally intensive problems.
3.1. SAT and QBF
Without the reduction rule, the context must retain the com- plete recursive trace - all partial assignments and interme- diate formulas - leading to worst-case exponential space complexity ((2)). For PENCIL, once a branch returns, its intermediate reasoning steps are discarded, therefore search paths will be discarded, preserving only the final answer.
SAT is a canonical NP-complete problem. We consider the 3-SAT variant, where each instance is a Boolean formula in conjunctive normal form with clauses of length three, e.g. (x1 V -22 V z2) A (-x1 V Z2 V -T3). The ratio between number of clauses and variables is set as 4.3, larger than the
4

---

PENCIL: Long Thoughts with Short Memory
This reduces the maximal length to (n), bounded by the search tree depth. As shown in Fig. 3, mal sequence length drops from 13, 804 to 2, 507 for SAT and from 151, 661 to 649 for QBF.
[SEP], [RETURN] as we run the algorithm, and then trans- form the long scaffolded CoT sequence into a set of smaller sequences {x((), xx(2) (((1)) } that ends with either [RETURN] or EOS.
10, the maxi-
During training, the loss function is crucial for the success of training PENCIL. In particular, we need not compute loss on every single token in each shorter sequence z²(1), but only those that are generated starting from last iteration's reduction step (i.e. (((.))))) We maintain an index for each (x()) for storing the information of the index where the model generation starts. We can either feed all shorter sequences into one batch (which is our default choice in experiments), which makes it possible to reuse the KV cache of other sequences to reduce training computes, or randomly sample from these sequences from all problem instance, which would lead to similar performance.
3.2. Einstein's ' Puzzle
Einstein's Puzzle We further consider Einstein's puz- zle (Prosser, 1993), classic constraint satisfaction problem where the model must learn to reason in natural language. Each problem instance consists of a list of houses with dif- ferent attributes (e.g., color, nationality, pet), and given a set of constraints or clues as the prompt (e.g. the green house is immediately birds), the goal is to determine the attributes of each house through logical deduction. The original puzzle has size 5 x 5 (5 houses and 5 attribute categories, totaling 25 vari- ables), which presents a significant challenge for language models to solve - even GPT-4 fails to solve it with few-shot CoT (Dziri et al., 2024).
the right of the one who keeps
Implementation Unless otherwise stated, for model ar- chitecture, we choose a 6-layer transformer with 10.63M parameters for SAT and QBF problems, and an 8-layer transformer with 25. parameters for the more complex Einstein's puzzle. All experiments use a context window of 2048 tokens and rotary positional encoding (Su et al., 2024); we truncate the sequence the maximal context window to fit into the model for all methods if it exceeds the model's capacity. We use the same batch size and learning rate for all methods across experiments.
Special Use Case: Summarization A notable special case of the reduction rule used for solving Einstein's 's puzzle is when the answer itself leads to another question: when A = [CALL] T' (1) becomes
C [CALL] T [SEP] [CALL] T [RETURN]
C [CALL] T'.
This mimics the tail recursion in functional programming where a function's 's returned value is another function call. A practical application of this rule is to simplify an originally complex question by iteratively reducing it, through some intermediate reasoning steps, to more tractable form. In Sec. 5 we will use this to prove PENCIL's space efficiency.
Experimental Setting We adopt the online learning setting where models train until convergence with unconstrained data access, mirroring the common scenarios in language model training where data can be effectively infinite (Hoff- mann et al., 2022). To ensure fair comparison, we include special tokens in the CoT, which might benefit its training by introducing additional structural information.
See Fig, 8 for an illustration of how reduction rules can be applied to solve the Einstein puzzle, which consists of the following steps in one round of iteration: (a) Propa- gating constraints to eliminate impossible attributes com- binations; (b) Use the tail recursion rule to merge results from constraints propagation and update the house states; (c) Iteratively explore different solution branches and discard intermediate reasoning steps from each branch, only pre- serving the final answer. As shown in Fig. 3, for 5x5 puzzle, the maximal sequence reduces dramatically from 151, 192 to 3, 335 (without tail recursion this number is 7, 705).
Evaluation Protocol We evaluate on a held-out validation set of 100 problem instances using two metrics: accuracy (percentage of correct predictions) and trace rate (percent- age of reasoning steps matching the ground truth). For all problems, the labels for different classes are balanced.
4.1. Results on SAT and QBF
Performance As shown in Table 1, both CoT and PENCIL significantly outperform the baseline (i.e. without using CoT) and achieve almost perfect performance (2 95% ac- curacy) on small problems (n < 6 for SAT and 5 for QBF). While CoT's performance degrades sharply when problem size increases dropping to 50% accuracy on SAT and 61 % on QBF when n = 10, PENCIL maintains near-perfect ac- curacy across all problem sizes. Furthermore, PENCIL's consistently high trace rate (above 90% for most problem sizes) indicates that it precisely follows the intended algo- rithm's 's reasoning steps.
4. Experiments
Training The training of PENCIL is nearly identical to that of CoT with a key difference being how the data is processed. Specifically, the training pipeline of PENCIL consists of the following steps:
For data preparation, we implement the algorithms for solv- ing the problems mentioned in Sec. 3. generates the corre- sponding scaffolded CoT (7) with special tokens [CALL],
5

---

PENCIL: Long Thoughts with Short Memory
5
7
10
5
7
9
10
Baseline
Acc.
66
57
46
51
46
51
49
51
Bascline
Acc.
90
82
85
68
60
69
71
66
Acc.
100
100
100
99
84
63
54
50
Acc.
100
100
97
94
74
72
69
73
CoT
CoT
TR.
99.6
99.0
98.0
96.2
74.0
69.9
63.8
51.4
TR.
100
100
98.3
93.9
65.1
49.4
40.7
32.8
Acc.
100
100
100
99
99
100
100
100
Acc.
100
100
100
100
100
100
100
100
PENCIL
PENCIL
TR.
100
99.0
97.1
95.9
91.8
93.3
92.9
83.0
TR.
100
100
100
100
100
100
100
100
Table 1: Performance on SAT (left) and QBF (right). Ace denotes the Accuracy (%) and TR denotes the trace rate (%).
10
Solvable
Size Size
Solvable Problem Size
C 70
Solvable
Problem Size
Problen
CUT 98%
CUT 93%
PENCIL PENCIL
12
CoT 95% PENCIL - 95%
PENCIL 95%
2
5.0
7'5
16.0
30
130 Inference Time (s)
Inference Time (s)
Inference Time (8)
(a) SAT
(b) QBF
Einstein's 's puzzle
Figure 4: Comparison of maximally solvable problem size (with 95% accuracy) given different inference time budgets.
CaT
PENCIL
CoT
PENCIL
CoT
PENCIL
CaT
PENCIL
Accuracy (%)
100
100
100
1004
Accuracy
Accurccy
Accurecy
100.0
100.0
60-
100.0
100.0
40-
40-
-0
100
100
100
Training Loss Trace Rate (%)
100
&
Training Loss Trace Rate
100.0
Trace Rate
100.0
40
100.0
Trace
40
20-
100.0
8
100.0
100.0
Training Los
Training
0.0 0.5 1.0
1.3 2.0 2,5
0.0 0.3 0.4
0.6 0.8
1.0 Tell
0.0
0.6 1.2
1,
24
3,0
0.00 0,25 0.50 0.75 1.00 1,25 1.50
Training FLOPs
Tet0
Training FLOPs
Training FLOPs
lell
Training FLOPs Iee2
(a) QBF n = 3
(b) QBF n = 4
(c) QBF
(d) QBF 6
Figure 5: Comparison of convergence speed for training on the QBF problem (with n ranges from 3 to 6). Circles and vertical lines indicate the first time each method reaches optimal performance. The x-axis is the FLOPS budget for self-attention calculated based on (11). See Fig. 9 in Appendix where the x-axis is the number of iterations.
Test-Time Scalability Figure 4 compares the test-time scalability of CoT and PENCIL given different inference time budget. For both SAT and QBF problems, PENCIL can effectively solve larger problems with increased time budget, handling up to n 10 with inference time around 10s and 40s respectively while CoT struggles to scale up even when given more time. This is because the reduction rule enables PENCIL to keep the reasoning length growing polynomially rather than exponentially with problem size, significantly reducing the requirement of space during generation.
lems CoT's space consumption becomes prohibitively large and will cause out-of-memory, we only report results for n 3 to 6. The results show that PENCIL can effectively save computation, and thus can consistently achieve better performance under the same compute budget and converge faster, with the gap becoming more significant as problem size increases.
4.2. Results on Einstein's 's Puzzle
Besides of the original challenging 5x5 Einstein's 's puzzle, we also consider two simplified variants: 3x3, 4x4. For each size of the puzzle, we generate 10, 000 training in- stances by randomly assigning attributes to houses and de- riving valid constraints that ensure a unique solution. The accuracy is evaluated based on whether the model can suc- cessfully answer the question "who owns the Fish" on 100 unseen validation samples.
Convergence Figure 5 compares the convergence speed of CoT and PENCIL on the QBF problem given fixed train- ing FLOPs budget calculated based on (1 (11). To isolate the impact of memory constraints, which limit the expressive- ness of models, we allow unlimited context window length in this experiment, enabling both methods to potentially achieve perfect performance. Since since for larger prob-
6

---

PENCIL: Long Thoughts with Short Memory
Puzzle Size
CoT
PENCIL
CoT
PENCIL
100
3 x
Accuracy (%)
25
97
iParameters
10.63M
48
61
97
99
99
99
85
Trace Rate (%)
2.97
78.27
70
4 X
Accuracy (%)
34
100
3.15M
45
54
92
95
98
98
55
Trace Rate (%)
8.33
86.52
0.40M
39
38
43
52
38
44
40
x 3
Trace Rate (%)
Accuracy (%)
99.37
99
99.66
99
5i2
1024
2048
512
1024
2048
25
Context Length
Context Length
Table 2: Comparison of performance w/o and with the reduction rule on Einstein's 's puzzle.
Figure 6: Effects of model size and context length on accuracy for 3x3 Einstein's puzzle.
Main Results Table reports the performance with and without using the reduction rule solve different sizes of Einstein's puzzles. Remarkably, PENCIL solves the original 5x5 puzzle at 97% accuracy using only 25.19M parameters (significantly smaller than GPT-2) and 2048 context length (the same as GPT-2), with average inference time per sam- ple 42.98s. In comparison, CoT fails catastrophically on puzzles beyond 3x3, with accuracy dropping to 25% (i.e. close random guessing) on 5x5 puzzles, despite using the same architecture and training.
time (i.e. S < T). To the best of our knowledge, PENCIL is the first approach that provably enables universal space- efficient computation for transformers. A direct implication of Theorem 5.1 is:
Corollary 5.2. With polynomial maximal context length (to input length), PENCIL with transformers can solve all problems in PSPACE (solvable by Turing machine using polynomial space) while standard CoT with any poly-time next-token generator can only solve P (solvable by Turing machine using polynomial time).
As shown in Figure 6, PENCIL achieves consistently high accuracy with sufficient model ca- pacity (with 2 3.15M parameters, i.e. a 4-layer transformer) even with limited context length, while CoT requires both larger models and longer context to achieve comparable performance. However, when the model size too small, both methods fail to solve the puzzle effectively, suggesting minimum model capacity threshold.
Effects of Model Size
It is well-known that C NP C PSPACE and widely- conjectured that P _ PSPACE (a weaker assumption than the famous 7 NP hypothesis). Under this assumption, any PSPACE-complete problem (e.g., QBF (Stockmeyer & Meyer, 1973) cannot be solved by CoT using polynomial length. In contrast, PENCIL can solve these problems with polynomial maximal context length, which is a significant improvement in the computational power Similarly, under a slightly stronger yet widely- accepted assumption called Exponential Time Hypothesis (ETH, Impagliazzo & Paturi (2001)), even SAT requires exponential length and thus cannot be solved by CoT efficiently.
5. Universal Space-Efficient Computation
natural theoretical question arises as to how powerful is PENCIL on general tasks? In this section, we answer it by theoretically showing that PENCIL can perform universal space-eflicient computation for solving any task. More specifically, we prove that PENCIL using transformers as the base model can simulate Turing machines with optimal efficiency in both time and space. Our main result can be summarized informally as follows (see detailed statements in Theorem 1, Appendix H):
Proof Overview an overview and the key ideas for the proof of Theorem 5.1 (the complete proof deferred to Appendix H). In high level, the proof contains the following three steps:
The remaining of this section provides
We define new abstract computational model called Autoregressive Machine, which formalizes the com- putation of Turing machines as process of generating token sequences (as illustrated in Figure 7(a)), and introduces the State Function that transforms sequences into shorter ones (i.e. the state) representing Turing machine's 's configuration.
Section 5.1:
Theorem 5.1 (Main, Informal). For any Turing Machine, there exists a fixed finite-size transformer such that for any input, on which the computation of Turing Machine uses T steps and S space, PENCIL with this transformer computes the same output with O(T) generated tokens and using maximal context length of O(S).
We show that by iteratively simulating the next-token generation of the autoregressive machine and summarizing the generated tokens into its state periodically, PENCIL can reduce the maximal context length to the opti- mal level OSS) while maintaining the running time at (T')
Section 5.2:
This result significant improvement over CoT (Pérez et al., 2021; Merrill & Sabharwal, 2023), which showed that even though CoT can perform universal computation, it does so inefficiently; that is, it requires the context length to grow at the same rate as the time (TT) required to solve those problems. This is fundamental limitation since most meaningful computations require much less memory than
PPlly-tmme next-token generator includes transformers, state- space models (Gu et al., 2021). Exceptions include usage of infiitte-reccssion version of transcendental functions like exp.
7

---

PENCIL: Long Thoughts with Short Memory
Turing Machine
Autoregressive Machine
Chain-of-Thouge
Start
Q
Input
Step
Step 2
Step 3
Step 1-11
Step
Step fy+1
Accept/ Ploject
Total Steps (Time)
Max Length ((Time)
Step
8(g),
(1), 1,
1
PENCIL
Stop
0)))
(2h 1,
Statel
State
Step t+1
Stop 9,1
[SRP]
State!+11
State 8.s
[RCTORN]
1
State
Simulate
Step
A(g.. 1)
(e), 0-)
Statefrrl
State 5.
1
New State
Total Steps (Time)
Max Length (Space)
Impat
Step
Step
Stopp
Turing Machine
(b) How PENCIL Simulates Turing Machine
Figure 7: (a) Autoregressive machine encodes each step of Turing machine's 's computation as a triplet containing the state, tape symbol, and movement direction. (b) PENCIL simulates Turing machine iteratively using two phases: simulating computation steps from the previous state (i.e. State("),, and summarizing into the new state (i.e. (tate
(as illustrated in Figure 7(b)).
computational traces of M, where the mapping x + s(x) erases irrelevant information while preserving the essential information for future computation.
Section 5.3: Finally, we form new programming language called Full-Access Sequence Processing (FASP) and use it to establish that, under specific choices of the model archi- tecture, finite-sized transformers are expressive enough to perform this iterative generation and summarization process, thus completing the proof.
Correspondingly, time complexity z) can be defined as the number of steps the autoregressive machine M takes to halt on input z. Space complexity S(M, s, x) is defined as the maximal length of the states (s o f (xx) for all steps k. This quantifies the minimal memory required to continue the computation at any point.
5.1. Autoregressive Machine and Complexity
We begin by defining autoregressive machine as a general purpose computation model. It subsumes Turing machine as an example and can potentially include other models.
Example: Turing Machine Indeed, Turing machine can be represented as autoregressive machine by letting each transition step produce a single token (encoding the new state, symbol, and head movement), formalized as follows (see proof in Appendix D):
Definition 5.3 (Autoregressive Machine). An autoregres- sive machine is tuple M (E, n, Exccepts Enjea), where Σ* + Σ is a next-token gen- Pejectt C Σ are accepting and rejecting erator, and Eaceep: Σ
Σ is finite alphabet,
Lemma 5,5 (Turing Machine as MM). Any Turing machine TM can be represented as a autoregressive machine MMM associated with a state function 8TM that preserves its time and space complexity.
tokens. For any input æ E Σ" M iteratively generates one token per step and appends it to the current sequence, with (xx) denoting the sequence after iterations where (x( (1r, T (z)). The machine halts when it generates token in Eacepp or Ereject-
Specifically, the time complexity of .MM equals the Turing machine's total step count, and the space complexity of MTM matches the Turing machine's actual memory usage.
To achieve space efficiency in computation, we need mech- anism to compress the growing computational trace into a minimal representation that preserves only the information necessary for future steps. This is formalized by:
5.2. Space and Time-Efficient Simulation using PENCIL
For proving Theorem 5.1, we consider a variant of PENCIL with a simplified reduction rule ø', whichis already powerful enough for space-efficient universal simulation
Definition 5.4 (State Function). A function s : " Σ' is a state function of a autoregressive machine M (E, n, Excoptt: Exejec) if (1) π o s = π,; (2) for all x x' E", **s(<) s(x') = s( y)) =((a', v)) (3)
T [SEP] T [RETURN] =
T
(9)
This rule uses one less special token than our initial re- duction rule (1) and can be expressed by it through tail recursion (8), i.e. by substituting T +- [CALL] T and T' + [CALL] T in (9). For our proof, we simply set T = sT),, since the state contains the minimal informa- tion for future computation per definition. Therefore, the question remains as to when trigger (9) and summarize:
Note the above definition automatically implies that the future trace of the autoregressive machine M, i.e. x² (*) for k = 1,2, 2, .... can be uniquely determined by the state function of M. Formally, sc fl o = s f and k = s+1 o s for any k 2 (see Lemma I.1 in Appendix). In other words, s defines a equivalent class over all possible
8

---

PENCIL: Long Thoughts with Short Memory
Space-Efficient but Time- Inefficiett Solution Naively, if PENCIL trigger the summarization procedure too frequently, e.g. after every new token generation, the maximal context length would be bounded by (S)) However, this approach would blow up the time complexity by a factor proportional to the space complexity, i.c. O(S T), making it highly time inefficient.
Closed Operators) for writing the program and allows defin- ing customized operators. Depending on positional encod- ing and activation functions allowed to use in transformers, FASP has different variants supporting an increasingly rich family of primitives. A formal introduction of FASP and variants thereof is deferred to Appendix F and G.
FASP is useful for the proof because precisely charac- terizes the class of functions that can be implemented by finite-size transformers with average-hard casual attention, denoted by HTF (see formal definition in Definition E.9):
Space and Time Efficient Solution To achieve both op- timal time and space efficiency (up to some multiplicative constant), PENCIL can keep generating new tokens to sim- ulate running autoregressive machine, and trigger the sum- marization only when the length of T exceeds a certain threshold. In particular, we define the time (i.e. the number of tokens generated so far) to apply i-th summarization/r- duction rule & as the smallest integer larger than 4--1 such that length of the state T is smaller than half of the length of T - - 8 "x),, where o /xx'(x) is the state reduced from the last iteration and i; - 4--1 is the number of simulated steps of autoregressive machine in the current iteration. Correspondingly, we can define the trace of PENCIL as (0(()
Lemma 5.7 (Theorem F.2, Informal). FASP HTP.
Thus our proof reduces to a FASP program that executes the space and time efficient solution mentioned in Sec 5.2.
FASP is more powerful than RASP (Weiss et al., 2021) because RASP cannot simulate certain hard attentions, its selection mechanism uses boolean condition function based only query and local key. As a result, RASP cannot even retrieve the value vector of the key that is the closest to the query. which is essential in our construction (FASP code).
Program high level, the program implements the fol- lowing three operations simultaneously (which is exactly the premise of Proposition 5.6):
oso (x), [SEP], sc (z) [RETURN] (10)
where so ft (z) is equivalent to for o f (a) per Definition 5.4. In short, PENCIL compresses the current sequence into its state representation whenever its length exceeds twice the state length, enforcing space stays within (SS) without performing reductions so frequently that the overall time cost exceeds (T)) Formally:
1. Summarization Trigger:
Detecting when to transition from the simulation phase to summarization phase by dy- namically comparing the length of the current sequence with the its state length throughout the generation process.
2. Simulation: During the simulation phase, generating the next token of the autoregressive machine that simulates one step of the Turing machine.
Proposition 5.6. For any autoregressive machine M (E, Encept, Enejea) with state function if next-token predictor S., accurately generates the next token in (10) from the prefix for every on any input x E Σ', then PFNCIL sng d' can simulate M by using O(T(M..)) steps and a maximal sequence length of O(S(M, s, x)).
3. Summarization: During the summarization phase, com- puting the compressed state representation of the current token sequence.
Note that this result applies not just to Turing machines but to any computational model representable as an autoregres- sive machine with a suitable state function.
The specific program given in Appendix H, which com- pletes the proof for Theorem 5.1. This technique can also be used be prove other expressiveness results of transformer with CoT, e.g. Merrill & Sabharwal (2023).
5.3. FASP for Proving Transformer Expressiveness
Now we complete our proof by demonstrating that trans- formers are indeed expressive enough to produce the trace described in (10) under specific architectural choices includ- ing Gated ReLU activation (Dauphin et al., 2017), positional embedding n + nt, and average-hard casual attention (Mer- rill et al., 2022); details are specified in Appendix E.
6. Conclusion
This paper identifies a fundamental limitation of CoT where intermediate computations accumulate indefinitely in the context, and introduce PENCIL to address this. PENCIL adopts a simple reduction rule to "clean up" unneeded rea- soning steps as soon as they are finalized. This mechanism effectively transforms long traces into compact representa- tions, enabling efficient training and allowing the model to handle substantially larger problems under the same memory constraints. Extensive experiments are done to demonstrate the effectiveness of PENCIL to handle inherently challeng- ing tasks with less computes and smaller memory.
Full-Access Sequence Processing (FASP) Since directly constructing a transformer is challenging. following Weiss et al. (2021): Yang & Chiang (2024), we developed novel programming language called FASP, where each code in FASP represents a sequence srguuence-to-mmeeddin to-embedding mapping. The language defines set of primitives or functions (termed
9

---

PENCIL: Long Thoughts with Short Memory
Impact Statement
Friedman, D., Wettig, A., and Chen, D. Learning trans- former programs. Advances in Neural Information Pro- cessing Systems, 36, 2024.
The goal of this paper to advance our understanding of the reasoning capabilities language models. There is no immediate negative societal impact as far as we can foresee unless language models used for unethical purposes.
Fu, Q.. Cho, M., Merth, T., Mehta, S., Rastegari, M., and Najibi, M. Lazyllm: Dynamic token pruning for efficient long context Ilm inference. arXiv preprint arXiv:2407. htl::2407.14057, 2024.
References
Arora, S. and Barak, B. Computational complexity: mod- ern approuch. Cambridge University Press, 2009.
Gao, Y., Xiong, Y., Gao, X., Jia, K., Pan. J., Bi, Y., Dai, Y., Sun, J., and Wang, H. Retrieval-augmented generation for large language models: A survey. arXiv preprint arXiv:2312. 10997, 2023.
Baader, F. and Nipkow, T. Term rewriting and all that. Cambridge university press, 1998.
Garrison, E. Memory makes computation universal, remem- ber? arXiv preprint arXiv:2412.17794 2024.
Beltagy, I. Peters, M. E., and Cohan, A. Long- former: The long-document transformer. arXiv preprint arXiv:2004.000 05000, 2020.
Gu, A., Goel, K., and Ré, C. Efficiently modeling long sequences with structured state spaces. arXiv preprint arXiv:2111.00396, 2021.
Besta, M., Blach, N., Kubicek, A., Gerstenberger, R., Pod- stawski, M., Gianinazzi, L., Gajda, J., Lehmann, T., Niewiadomski, H., Nyczyk, P., et al. Graph of thoughts: Solving elaborate problems with large language models. In Proceedings of the AAAI Conference on Artificial In- telligence, volume 38, pp. 17682-17690, 2024.
Guo, D., Yang, D., Zhang, H., Song. J., Zhang, R., Xu, R., Zhu, Q.. Ma, S., Wang. P., Bi. X., et al. Deepseck-rl: In- centivizing reasoning capability in Ilms via reinforcement learning. arXiv preprint arXiv:2501.12948. 2025.
Chen, W. Ma, X., Wang, X., and Cohen, W. W. Program of thoughts prompting: Disentangling computation from reasoning for numerical reasoning tasks. arXiv preprint arXiv:2211.12542 2022.
Hoffmann, J., Borgeaud, S., Mensch, A., Buchatskaya, E., Cai, T., Rutherford, E., Casas, D. d. L.., Hendricks, I.. A., Welbl, J., Clark, A., et al. Training compute-optimal large language models. arXiv preprint arXiv:2203.15556. 2022.
Choromanski, K., Likhosherstov, V., Dohan, D., Song, X., Gane, A., Sarlos, T.. Hawkins, P., Davis, J., Mohiuddin, A., Kaiser, L., Rethinking attention with performers. arXiv preprint 1XXx:20009.1499.. 2020.
Impagliazzo, R. and Paturi, R. On the complexity of k- sat. Journal of Computer and System Sciences, 62(2): 367-375, 2001.
Dauphin, Y. N., Fan, A., Auli, M., and Grangier, D. Lan- guage modeling with gated convolutional networks. In International conference on machine learning, pp. 933- 941. PMLR, 2017.
Jiang. H., Wu, Q., Lin, C.-Y., Yang, Y., and Qiu, L. Llmlin- gua: Compressing prompts for accelerated inference of large language models. arXiv preprint urXiv:2310.057: 2023.
Drozdov, A., Schärli, N., Akyürek, E., Scales, N., Song, X., Chen, X., Bousquet, O., and Zhou, D. Compositional semantic parsing with large language models. In The Eleventh International Conference on Learning Repre- sentations, 2022.
Kaplan, J., McCandlish, S., Henighan, T., Brown, B., Chess, B., Child, R., Gray, S., Radford, A., Wu, J., and Amodei, D. Scaling laws for neural language models. arXiv preprint urXiv:2001.08300 2020.
Dziri, N., Lu, X., Sclar, M., X. L., Jiang, L., Lin, Y., Welleck, S., West, P., Bhagavatula, C., Bras, R., al. Faith and fate: Limits of transformers on compositionality. Advances in Neural Information Processing Systems, 36, 2024.
Khot, T., Trivedi, H., Finlayson, M., Fu, Y., Richardson, K., Clark, P., and Sabharwal, A. Decomposed prompting: A modular approach for solving complex tasks. arXiv preprint arXiv:2210.0244 2022.
Kim, S., Shen, S., Thorsley, D., Gholami, A., Kwon, W., Hassoun, J., and Keutzer, K. Learned token pruning for transformers. In Proceedings of the 28th ACM SIGKDD Conference on Knowledge Discovery and Data Mining, pp. 784-794, 2022.
Feng, G., Zhang. B., Gu, Y., Ye, H., He, D., and Wang, L. Towards revealing the mystery behind chain of thought: a theoretical perspective. Advances in Neural Information Processing Systems, 36, 2024.
10

---

PENCIL: Long Thoughts with Short Memory
Kitaev, N., Kaiser, L., and Levskaya, A. Reformer: The efficient transformer. arXiv preprint arXiv:2001.04451 2020.
Nawrot, P., Lañcucki, A., Chochowski, M., Tarjan, D., and Ponti, R. M. Dynamic memory compression: Retrofitting Ilms for accelerated inference. arXiv preprint arXiv:2403.09633 2024.
Kojima, T., Gu, S. S., Reid, M., Matsuo, Y., and Iwasawa, Y. Large language models are zero-shot reasoners. Ad- vances in neural information processing systems, 35: 22199-22213, 2022.
Nowak, F., Svete, A., Butoi, A., and Cotterell, R. On the representational capacity of neural language mod- els with chain-of-thought reasoning. arXiv preprint arXiv:2406. 2024.
Li, Y., Huang, Y.. Yang, B., Venkitesh, B., Locatelli, A., Ye. H., Cai, T., Lewis, P., and Chen, D. Snapkv: Lim knows what you are looking for before generation. arXiv preprint 2rX4v:2404. 14469, 2024a.
Nye, M., Andreassen, A. J., Gur-Ari, G., Michalewski, H., Austin, J., Bieber, D., Dohan, D., Lewkowycz, A., Bosma, M., Luan, D.. et al. Show your work: Scratchpads for intermediate computation with language models. arXiv preprint arXiv:2112.00114 2021.
Li, Z., Liu, H., Zhou, D., and Ma, T. Chain of thought em- powers transformers to solve inherently serial problems. arXiv preprint arXiv:2402.12877 2024b.
O'Donnell, M. J. Equational logic as a programming lan- guage. Springer, 1985.
Lindner, D., Kramár, J., Farquhar, S., Rahtz, M., McGrath, T., and Mikulik, Traer: Compiled transformers as laboratory for interpretability. Advances in Neural Infor- mation Processing Systems, 36, 2024.
OpenAL.
Learning to reason with 1lms, Septem- ber 2024. URL /tttpp:://ppeaii... index/ sitesoowwwit-22
Liu, C., Lu, S.. Chen, W.. Jiang, D., Svyatkovskiy, A., Fu, S., Sundaresan, N., and Duan, N. Code execu- tion with pre-trained language models. arXiv preprini arXiv:2305.05338 2023.
Pérez, J., Barceló, P., and Marinkovic, Attention turing- complete. Journal of Machine Learning Research, 22 (75):1-35, 2021.
Prosser, Hybrid algorithms for the constraint satisfac- tion problem. Computational intelligence, 9(3):268-299, 1993.
Liu, N. F., Lin, K., Hewitt, J., Paranjape, A., Bevilacqua, M.. Petroni, F., and Liang, P. Lost in the middle: How language models use long contexts. Transactions of the Association for Computational Linguistics, 12:157-173, 2024.
Ramachandran, P., Zoph, B., and Le, Q. V. Searching for activation functions. arXiv preprint 17X1v:17100059411, 2017.
Long, Large language model guided tree-of- tcc-of-thought. arXiv preprint arXiv:2305.0822 2023.
Sel, B., Al-Tawaha, A.. Khattar, V., Jia, R., and Jin, M. Algorithm of thoughts: Enhancing exploration of ideas in large language models. arXiv preprint arXiv:2308, 10379. 2023.
Madaan, A., Tandon, N., Gupta, P., Hallinan, S., Gao, L., Wiegreffe, S., Alon, U., Dziri, N., Prabhumoye, S., Yang, Y., et al. Self-refine: Iterative refinement with self- feedback. Advances in Neural Information Processing Systems, 36, 2024.
Selman, B.. Mitchell, D. G., and Levesque, H. J. Generating hard satisfiability problems. Artificial intelligence, 81 (1-2):17-29, 1996.
Merrill, W. and Sahharwal, A. The expresssive power of transformers with chain of thought. arXiv preprint arXiv:2310.07923, 2023.
Shazeer, N. Glu variants improve transformer. arXiv preprint arXiv:2002.05222,, 2020.
Merrill, W., Sabharwal, A., and Smith, N. A. Saturated transformers are constant-depth threshold circuits. Trans- actions of the Association for Computational Linguistics, 10:843-856, 2022.
Snell, C., Lee, J., Xu, K., and Kumar, A. Scaling Ilm test- time compute optimally can be more effective than scal- ing model parameters. arXiv preprint arXiv:2408.03:: 033114 2024.
Muennighoff, N., Yang, Z., Shi, W., Li, X. L., Fei-Fei, L., Hajishirzi, H., Zettlemoyer, L., Liang, P., Candès, E., and Hashimoto, T. sl: Simple test-time scaling. arXiv preprint arXiv:2501 2025.
Stockmeyer, L. J. and Meyer, A. R. Word problems requir- ing exponential time (preliminary report). In Proceedings of the fifth annual ACM symposium on Theory of comput- ing, pp. 1-9, 1973.

---

PENCIL: Long Thoughts with Short Memory
Strobl, L., Merrill, W., Weiss, G., Chiang. D., and Angluin, D. What formal languages transformers express? survey, Transactions of the Association for Computa- tional Linguistics, 12:543-560 2024.
Heavy-hitter oracle for efficient generative inference of large language models. Advances in Neural Information Processing Systems, 36:34661-347100 2023.
Zhou, D., Schärli, N., Hou, L.., Wei, J., Scales, N., Wang. X., Schuurmans, D., Cui, C., Bousquet, O., Le, Q. et al. Least-to-most prompting enables complex reasoning in large language models. arXiv preprint arXiv:2205.10662, 2022.
Su. J., Ahmed, M., Lu, Y., Pan, S., Bo, W., and Liu, Y. Roformer: Enhanced transformer with rotary position embedding. Neurocomputiing. 568: 127063, 2024.
Suzgun, M. and Kalai, A. T. Meta-prompting: Enhancing language models with task-agnostic scaffolding. arXiv preprint (tt::2401.129544 2024.
Zhou, H., Bradley, A., Littwin, E., Razin, N., Saremi, O., Susskind, J., Bengio, S., and Nakkiran, P. What algo- rithms can transformers learn? study in length general- ization. arXiv preprint arXiv:2310 10. 16028, 2023.
Wang, W., Dong, L., Cheng, H., Liu, X., Yan, X., Gao, J., and Wei, F. Augmenting language models with long-term memory. Advances in Neural Information Processing Systems, 36, 2024.
Wei, J., Wang, X., Schuurmans, D.., Bosma, M., Xia, F., Chi, Le, Q. V., Zhou, D., et al. Chain-of-thought prompting clicits reasoming in large language models. Advances in neural information processing systems, 35:24824-24837, 2022.
Weiss, G., Goldberg, Y., and Yahav, E. Thinking like trans- formers. In International Conference Machine Learn- ing. pp. 1 11080-10 11090 PMLR, 2021.
Wos, L.,, Overbeek, R., Lusk, E., and Boyle, Automated reasoning introduction and applications. McGraw-Hill, Inc., 1992.
Yang, A. and Chiang, D. Counting like transformers: Com- piling temporal counting logic into softmax transformers. arXiv preprint arXiv:2404.0433 04393, 2024.
Yao, S., Yu, D., Zhao, J., Shafran, I., Griffiths, T., Cao, Y., and Narasimban, K. Tree of thoughts: Deliberate problem solving with large language models. Advances in Neural Information Processing Systems, 36, 2024.
Zaheer, M., Guruganesh, G., Dubey, K. A., Ainslie, J., Al- berti, C., Ontanon, S., Pham, P., Ravula, A.. Wang, Q. Yang, L., et al. Big bird: Transformers for longer se- quences. Advances in neural information processing systems, 33: 33:17783-17297, 2020.
Zelikman, E., Wu, Y., Mu, J., and Goodman, N. Star: Boot- strapping reasoning with reasoning. Advances in Neurul Information Processing Systems, 35:15476-15488, 2022.
Zhang, D., Tigges, C., Zhang, 7.., Biderman, S., Raginsky, M., and Ringer, Transformer-baste based models are not yet perfect learning to emulate structural recursion. arXiv preprint 2rXiv:2401.1290 2024.
Zhang, Z., Sheng, Y., Zhou, T., Chen, T., Zheng, L., Cai, R., Song, Z.., Tian, Y., Ré, C., Barrett, C., al. H2o:
12

---

PENCIL: Long Thoughts with Short Memory
(a)
(b)
Prompt:
Constraint The green house is immedistely to the right of the one who keeps tirds
[CALL]
[CAra]
[CALL)
Curannty categany
Currentyy the pet category of
$ considering
House allows tollowing
allows the following
constraints, the possible values for the pet category of House #1 have been namroved down to Some constraints remain unsatisfied and thus puzzle is still not fully solved s Since House #1 color category still two possible
Constraint 2: The Bxit is immediately to right the German
options: birds doge, or fish... Let's consider constraint [CALL]
options: arns cogs, or
Let's consider constraint
House #1 is's color reducess to Let's consider constrrint 2
Constraint 3
The one who keeps dlgga the same house es the red house
Since green must
immediately to the right of Birds, we remove "green" from House #1 (it can't be in the leftmost position it's supposed to be the right of something else) [SXP]
Now we've considered all
Constraint 4: The one who keeps kinds is immediately the right of the Swede
constralints, summarize
[SXP]
red,
Who owns fish?
[CALL]
explore each option separately
After considering all constraints, the possible values for the pet category of House 41 have been narrowed down to
$ Let us suppose House blue
$ House 41's color reducos to possibilities bluue and
PENCIL
[CALL]
[EETUR]]
$ Currently, the pet category of House allows only possibility dogs ...
[RETORN]
Solution:
(--.)
House
2
(CALC)
Color
Red
Blue
Green
$ Currently, the calegory House ar allowe following
[CALC]
Nationality
Swede
German
options: dogs, Let's consider constraint $ House #tts color reduces possibiities blue and red...
$ Aller considering rnng all constraints, the possible values for the pet cateearry of House #1 have been narroved down to
Dogs
Birds
The Brit the fish
Figure 8: A simplified illustration of the algorithm for generating the thinking process for Einstein's puzzle (3x3). The puzzle requires determining attributes of each house (Color: Blue/Green/Red, Nationality: Bri/GGrrann/Sedde, Pet: Birds/Dogs/Fish) given set of constraints, with each house having unique attributes. The "..." in the arrow denotes omitted thoughts for conciseness; the "..." in the box denotes omitted thought. See the complete example in Appendix M.
A. Related Work
Structured Reasoning A key distinction of scaffolded reasoning approaches stems from how space is managed during generation. At one extreme, Chain-of Thouuht (Wei et al., 2022: Nye et al., 2021; Kojima al., 2022) demonstrates that explicit intermediate steps can dramatically improve performance on complex problems, but at the expense of unbounded context growth. This limitation has motivated approaches leveraging reasoning structures such as trees and graphs (Yao et al., 2024; Long, 2023; Besta et al., 2024; Sel et al., 2023; Chen et al., 2022), adopting task decomposition strategies (Zhou et al., 2022; Drozdov et al., 2022; Khot et al., 2022) or some other prompting frameworks (Zelikman et al., 2022; Madaan et al., 2024; Suzgun & Kalai, 2024). While these methods enable more complex reasoning patterns, they require carefully crafted prompts and multiple rounds of interactions, whereas our approach achieves structured reasoning through end-to-end training.
Test-Time Scaling Extensive work has focused on addressing the computational bottlenecks of transformer architectures, particularly during long-context inference. One line of research explores architectural innovations through sparse and local attention patterns (Beltagy et al., 2020; Kitaev et al., 2020; Zaheer et al., 2020; Choromanski et al., 2020), while another focuses on memory optimization via KV-ccche reduction (Zhang et al., 2023; Fu et al., 2024; Li et al., 2024a; Nawrot et al., 2024) and strategic context pruming (Kim et al., 2022: Jiang et al., 2023). However, these approaches still rely on token prediction that fundamentally treats the context window as append-only storage, leading inherently inefficient space utilization.
LLMs as Programming Language Recent work has also explored intersections between programming languages and LLMs. For example, Weiss et al. (2021) proposes a language called RASP, programs in which can be encoded into and learned by transformers (Lindner et al., 2024; Friedman et al., 2024; Zhou et al., 2023). Liu et al. (2023) empirically shows that language models can be pre-trained to predict the execution traces of Python code. The reduction rule introduced in this work draws inspiration from term rewriting systems (Baader & Nipkow, 1998), a foundational means of computation in functional programming. This enables language models to explicitly emulate recursion that is otherwise hard to learn (Zhang et al., 2024), and manage space efficiently by erasing irrelevant contents in memory and focusing attention on those that are useful.
Computational Power / Limitation of CoT While transformers can theoretically simulate Turing machines (Pérez et al., 2021; Merrill & Sabharwal, 2023; Strobl et al., 2024; Nowak et al., 2024) with CoT, their practical computational power is fundamentally constrained by context window limitations. Particularly, we show that even with CoT, transformers with
13

---

PENCIL: Long Thoughts with Short Memory
inherent space constraints would fail handle problems requiring extensive intermediate computation. This parallels classical space-bounded computation theory, where memory management is crucial for algorithmic capabilities (Arora & Barak, 2009; Garrison, 2024). Our approach addresses this limitation by enabling more efficient use of the context.
B. Computational Benefits of PENCIL
To quantify the computational gap between PENCIL and CoT, consider using standard causal-masking transformer and an ideal case where one uses KV cache for storing key and value matrices for subsequent computation, the corresponding FLOPs for self-attention (which is typically the bottleneck for very long sequences, Kaplan et al. (2020) for more precise method for estimating the FLOPs) required for problem instance Σ" is proportional to:
(Ir(i-0.8)) + (xx + 1) (1211) 12((--0.11)
generated (1400.5)))
(11)
E.,, (lx(0 n 1.440.. (0
+ |
length of answer
where (4) n (++0.55 represents the shared context C before the [CALL] token, and (.(++055) (1))) denotes the answer between [SEP] and [RETURN] tokens. The first term accounts for model generation steps, while the second term captures
the computation cost of reduction steps where KV cache must be recomputed for A after merging it back into the context (since the prefix has been changed).
C. Additional Experimental Results
CoT
PENCIL
CoT
PENCIL
CoT
PENCIL
Accuracy (%)
100
Accurcyy (%)
100
Accurncy (%)
100-
100
100.0:
To0.0
80-
100.0
Accuracy
10l6o
60-
160.0
60
100.0
100.0
40
20
20
Training Loss Trace Rate (%)
100
100
Trace Rate (%)
Truce Rate (%)
100
80
100.0
100.0
%
100.0
100.0
40-
100.0
Training Trace
40-
100.0
40
100.0
20-
Training Loss
Training Loss
5000 10000
15000 Iterations
20000
5000 10000
15000 Iterations
20000
12000 24000 Iterations
Iterations
(a) QBF n
(b) QBF n =
(c) QBF n 5
(d) QBF n =
Figure 9: Comparison of convergence speed for training on the QBF problem (with n ranges from 6). Circles and
vertical lines indicate the first time each method reaches optimal performance. The x-axis is number of iterations.
D. Turing Machine as Autoregressive Machine
We will restate the definition of single-tape Turing machine, then show how each of its steps can be turned into tokens generated by autoregressive machine MTM. associated with state function that captures only the machine's 's current configuration.
D.1. Definition of Turing Machine
A single-tape Turing machine is defined by:
Definition D.1 (Turing Machine). single-tape Turing machine works on infinitely long "Tape" on both of its ends with
14

---

PENCIL: Long Thoughts with Short Memory
cells indexed by integers &. It is specified by 7-tuple
TM- = (AA, b, Q 90, 6, Quccept. Qrejea),
(12)
where:
A is a finite tape alphabet.
E A is the designated blank symbol.
Q is finite
of control states.
Qu Q is the initial control state.
8: 0:Qxal A
Q x (A (b)) x {-1,0,1) is the transition function.
Qacoopt C Q is the set of accepting states.
reject C Q is the set of rejecting states, disjoint from Quccept-
Computation of Turing Machines. the beginning of the computation, the initial tape content of E A is set by the input a E (A) {6]))* for the cells indexed from 0 through |o| - 1 and the other cells contain b. The head of the machine the position |o| and its control state initialized to go E Q. For convenience we use the pt to denote the head position at step L. In each time step 0 S f, the machine computes (g' ,',
a'''''') d') 5(4, at), where q is the control state of the Turing
machine step and aę of [Pe] is the symbol on the infinite-long tape before step t update o' at the Turing machine's head position pr. Then the Turing machine moves its position to p++1 Pr + d', change the symbol on the current tape to a', and updates its new control state to Q++1 = g'. The Turing machine halts only when reaching an accept/reject state in Q Quceep U reject: otherwise it runs forever. We denote the output of Turing machine on input a by TM(a), and we set (M( = 1 the final state Raceept and TM( = 0 is the final control state Qreject-
The computation of Turing machine intrinsically an iterated process - applying the same transition rule å until the halting condition is met. Such iterated models can naturally be described an autoregressive machine (Appendix D.2). We will give the formal definition (Definition D.6) of Turing Machine as autoregressive machine in Appendix D.2. Towards that, we will first introduce few more useful notations.
Definition D.2 (Configuration)) The configuration of Turing machine is defined as the tuple of (g, o' .P) E QxAxxZ C, where q is its current control state, a is the current symbols on the tape, starting from the leftmost non-blank one to the rightmost non-blank one, and is its current head position relative to the leftmost non-blank symbol. The configuration can be thought as a snapshot or the "global" state of Turing machine, which completely determines its future computation steps.
,',) p) E C, we define We also extend the update rule to the configuration space as follows: for any configuration (q,
8(g o. & 5(g, o' [pl])
(13)
Definition D.3 (Space of Update and Update Rule). We define the space of the update as the range of transition function 6, denoted by
= Q (A (-1.0.1)
(14)
Given a configuration c= (g,o',p) E C' and update x = (4', d) E Σ, we define the updated configuration of c with x as
Update(I,c) (q. o'
(15)
where ÿ p + d, and 0'[ o'i for all i E Z and ō' [p] = We denote the update function as Update(c, æ).. We also extend the notion of update function to any sequence of updates Tin = (x1. 2n)) E Σ and and configuration c, where we define Update(c, x 1..) =
2 1),-1), recursively.
Given the update rule 6, the transition rule of the configuration of the Turing machine is defined as
9s : - x Z
x
ga(g. o
Update(6(q.c o', p), (q. .p))
Denoting configuration as at step t as c = (q,, of p.) E Q - x Z with co = (qu. ob lo)). ). the configuration of Turing Machine at each step & can be formally defined as (gt-1, o P++1) g8(9e, of Pt) 9 ++1 (co).
15

---

PENCIL: Long Thoughts with Short Memory
Definition D.4 (Translationally Equivalent Configurations). Two Turing machine configurations c (41, (1 and
22 (g2, 22 P2) are said to be translationally equivalent (denoted by e 02)if:
1. They have the same control state: 91 q2
2. There exists an integer such that:
Their tape contents are equivalent up to translation: of oggi k] for all i e Their head positions equivalent up to the same translation: 71 P2 + k
Translationally equivalent configurations will produce the same future computation behavior, differing only in the absolute positions of symbols the tape, which is formally described by the following Lemma D.5.
We omit the proof of the following lemma, which is straightforward from the definition of Turing machine configuration and update rule.
Lemma D.5 (Translational Equivalence of Turing Machine Configurations). For any Turing machine TM and any configu- rations C₁, 02 C, if C1 c2, then ò(ci) ó(c2) and that for any update E 2, Update(cI, x) Update(c2, æ). As result, of (ci ) ~ o (c2) for any k E N.
D.2. Construction of Autoregressive Machine
We now build autoregressive machine MTM from TM by letting each Turing step correspond to the generation of single token (new state, symbol written, head movement).
Definition D.6 (Autoregressive Representation of a Turing Machine). Let TM (A, b, Q, go. 8, Quceept, Qrajec) be single-tape Turing machine. We define a autoregressive machine
MTM = (E, T, Enccept. Enejec)
(16)
as follows:
Alphabet/ Tokens x (-1,100}: (-1,00) Each token (g. a, d) E represents a configuration that means "the machine transitions to state g, writes symbol a on the current cell, and moves the head in direction d," where N indicates "no move" if desired. Furthermore, we let Encceps Queeep (A) xb))x(()xxx 1, and Ereject Qreject x (A) (b)) (-1, 0).
Next-Token Generator Σ* > Σ: Let co (20, b², 0) be the initial configuration of the Turing machine, we define the next-token generator by (-) 8(Update(co. )). That is, given an input token sequence = (II,..., #a) E Σ", the next token is the next Turing Machine update after the configuration C₂ obtained by applying the updates 3ı, Tn to the initial configuration cn-
Definition D.7 (Maximum and Minimum Non-Blank Positions). For any tape configuration of E AA with finitely many non-blank symbols and position p, we define:
[']]]] # b), which is the position of the rightmost non-blank symbol on the tape or head max pos(a') = max (j E &
position, whichever is larger.
min.pos (a') = min(j e Z d'[s] * b), which is the position of the leftmost non-blank symbol on the tape or head position, whichever is smaller.
Definition D.8 (Embedding Function from Turing Machine to Autoregressive Machine). Given Turing machine TM and its corresponding autoregressive machine MTM. we define an embedding function
embed C Σ"
that maps Turing machine configuration e c= (g, p) C to sequence of tokens in E* that represents the configuration in the autoregressive machine, where a' only has finitely many non-blank symbol 6. Specifically:
embed(g, o'. = (I,, T2,.,2....,. T.n)
NNot we only need consider the case where min min_pos p max pos((oss since Turing Machine has write non-blank tokens on every tape cell visits.
16

---

PENCIL: Long Thoughts with Short Memory
where n max-pos(o') mi min.pos(d') [max.pos(o') p- 1|+ and each x2 (ys, Uz, dj) is defined as:
= o' Σ dj min
(17)
and
d: ww=ccmmpteemoveeeeccc d=c_rppptteenoooo.p.oooooooooaad
(18)
+1 if i -aw.poopoo) -
+1 if = max pos - min. 1 Ap max (os +1
if max.pos micl)oosminnpp//o1 1 A max.pos(o')
-1 n 2 i max_pos(o") - min + Ap S max max-pos(d') - 1.
This is a standard construction used to show transformer can simulate Turing machine (Pérez et al., 2021; Merrill et al., 2022) which allows the tape contents be reconstructed from the computation history.
From the definition of the embedding function, series of tokens in Σ of Autoregressive Machine that encode the control state, the symbols the tape, and the head position. The embedding function is translationally invariant by defintiinn and we omit the proof here.
that the embedding of configuration of Turing Machine into
Lemma D.9 (Embedding is Translationally Invariant). For any Turing machine TM and any configurations cı, 02 C, C1 C2, then embed((1)) em)ed(c2).
Theorem D.10. The autoregressive machine MTM defined in Definition D.6 faithfully simulates the Turing machine TM in the sense that, for any input x E A,," the output of MTM on x (accept or reject) is the same as the output of TM on x.
More specifically, the equivalence is established by the following property. Recall co = (go, 122 12,0), 0), holds that for any configuration = (g. o', ,p) C' and non-negative integer
Update(co: f (embed(c))) ~ g (c).
(19)
Proof of Theorem D). 10. We will prove equation (19) by induction on k. First, recall that for any input sequence Σ* (x) is defined as @(Update(co- zz), where 5 is applied to the configuration resulting from updating the initial configuration with the sequence
Base Case (k = 0): For any configuration c c= (q, ,pp) p) E C, we need to show Update(co, embed(c)) c.
Let's denote Mmiin = min min.poa(a') and Mmax = max.pos(o'). By Definition D.8, embed(c) is a sequence (x1, ,2, where each token x; = (gi, a;, d,) encodes the state q, the symbol at a specific position, and movement direction.
When apply this sequence to the initial configuration co (go, 6², 0), we perform the following operations:
1. The embedding first writes all non-blank symbols from the leftmost position main to the rightmost position Maax by moving right. 2. If needed, additional movements are generated to ensure the head ends at the correct position p. 3. All
tokens share the same control state 4-
After applying the entire sequence embed(() to cp. we obtain a configuration c' (g',a" , pp) where:
d' = q (all tokens in the embedding share the same control state)
o o' + mminn for all E {0, 1,... Mmax mmmi) (the tape contents are shifted)
o b for all other positions
p' p Maiin (the head position is shifted accordingly)
This defines translational equivalence between d' and with translation constant min as:
1. They have the same control state: g'
17

---

PENCIL: Long Thoughts with Short Memory
2. The tape contents are translated: d" a'li + k] for all E Z
3. The head positions are translated: p' +
Therefore, (pd)ee()).ebbee(()) ~ which proves the base case.
Inductive Step: Assume equation (19) holds for some k 2 i... Update(co,
(/ (embed(c)) ~ (c)..
Let d Update(co: 1 (embed(c))) By the induction hypothesis, c4 ~ (c).
For the (A: + 1)-th step, we have:
1 (embec(c) (f* (embed(c)) = ((((((eea(())))) (f* (embed(c)), 8(())
(20)
Therefore:
Update(co. 1 (embed Update(c 8((4)) g)((4)
(21)
By Lemma D.5, since of ~ o8 (c), we have:
ga(c)) (x( 98 (c)
(22)
This proves that Update(co. f (embed(c))) ~ g k+t (c), completing the induction.
Since acceptance or rejection depends only on the final state (which preserved exactly the relation ~), MTM accepts æ and only if TM accepts v.
D.3. Construction of State Function 8TM
Although M writes out every Turing step, we can define a state function STM that condenses the final sequence into a minimal representation of the tape.
Definition D.11 (State Function STM). Let MTM (E, n Exccpps Erejoc) be the autoregressive machine representation of Turing machine from Definition D.6. We define its state function STM E- + E" as the following
8TM (x) = embed(Update((a.:)))
Var E",
(23)
where = (4o. b²,00 0) is the initial configuration.
We claim that the constructed STM satisfies all three properties in Definition 5.4:
(1) Next-Token Preservation (i STM = T): We need to prove that for any x E E', (STM(x)) x(x). Let Update(co, æ) be the configuration after applying sequence æ the initial configuration co. By definition of STM, we have (zM(2) = embed(c). By the definition of in Definition D.6, T(x) 8(Updtte(c), 2)) 5(c). Similarly, (Z)) = x ((mbbed(c) = (aapi))==UUpppppaa 5(Update(Co- (m))d From Theorem D. Equation (19) with k = 0. we have Update(Co, embed(c)) ~ c. Since 5 is invariant under translational equivalence (Lemma D.5), we have 5(Update(co. embed(c))) = 8(c). Therefore, ((STM(#)) = 8(c) = π (x)), which proves the property.
(2) Future-Trace Preservation: We need to prove that for any x, x Σ" and y Σ" if STM(x) STM(x'), then (TM((z,)) v)) = sTM((x',w)). Let Update(co, æ) and c' Update(co. z²). By definition of STM. STM(2) embed(c) and sTM(2') embed(c'). Since sTM(2) = STM (z'), we have embed(c) = embed(c'). This implies that e~ c', as embed maps translationally equivalent configurations to identical sequences. For any sequence of tokens (Vi..... .ma) E Σ", let cy = Update(c, y) and d, = Update(c'. y). By Lemma D.5, since c ~ c', we have ~ cy. Therefore, (TM( y)) embed(c,) = embed (c,)) = STM ((x', v)). which proves the property.
(3) Idempotence (M7 STM): We need to prove that for any E Σ", STM(STM(x)) (*M Let = Update(co. 2). By definition, (z) = embed(c). Now, (TM(STM(Z)) STM (embed((()) = embed (abbee(Uppaaeeco. embed(c))). From Theorem 10 Equation (19) with & = 0, we have Update(co, embee((c)) ~ c. Since embed maps translationally equiv- alent configurations to identical sequences by Lemma D.9, we have: STM (z)) = camee(UUddatee embed(c))) = embed(c) (z) This completes the proof.
18

---

PENCIL: Long Thoughts with Short Memory
Proof of Lemma 5.5 (Time and Space Preservation). By construction, each Turing step of TM corresponds to precisely one token generation under the next-token predictor in MTM- Consequently, the total number of tokens generated before halting matches the Turing machine's step count, ensuring time complexity is preserved exactly. Moreover, the state function STM "compresses" the entire history of tokens into short sequence that encodes only the currently used tape cells plus head position. Since a Turing machine at most needs space proportional to the number of non-blank cells and the head's location, the maximum length max; (STM (z))] is bounded by the tape usage of TM. This shows space complexity is also preserved. Hence, the TM and 8TM simulate TM optimally in both time and space.
E. Notations and Transformer Architecture
Let Σ. be finite vocabulary. A decoder-only transformer To Ex - E with h heads, L layers, hidden dimension d. and feed-forward width w is defined as follows, with all parameters and operations in R. We will first introduce the standard transformer architecture then list all non-standard architectural modifications useful for proving the main theorem.
E.1. Standard Notations
Definition E.1 Sembedi-Em Function Space). H(B is defined as the class of all functions mapping from E' - B. We also define H = Uaen- H(R") as the union all such classes across real spaces of all output dimensions.
Definition E.2 (Canonical Extension to Seq-to-Seq Function). Let A, B be two arbitrary sets and function 3 : AA" + B be a mapping from sequences to elements from to B. We define its canonical sequence-to-sequene extension 1/ : AA + B
as follows: for any input sequence x = =x11...... , xn) E A" of length n to an output sequence constructed iteratively as
[+)]]; = (t) xz) for i= = I,...,n
(24)
where Zi, .,,..., F; is the prefix of length i of sequence Definition E.3 (Probability Simplex). For any natural number n, the n-dimensional probability simplex (with n + 1 coordinates) is defined as
n+1
A
(II, 2n+1) R
z
0,
Vi
In 1]
(25)
Definition E.4 (Softmax). For any vector I and temperature parameter B 0, the softmax function softmax, R
is defined as:
exp(x1/3) Σイ exp(x;/3)
(softmax,(x))
for i I,...,
(26)
where 1 denotes the (m diddennnsal probability simplex. When 3 1, simply write softmax without the subscript.
In our analysis we will consider the instance-wise limit when B O, which leads the Average-Hard Attention (AHA) (Merrill et al., 2022) or Hardmax:
Definition E.5 (Hardmax), For any vector æ R", define the hardmax function, softmaxo R" A as the instance-wis limit of 0 temperature limit of softmax
softmaxg(z) A lim softmax (z).
(27)
8-+0
The following lemma shows the explicit form of the hardmax function. Its proof is deferred to Appendix J.1.
Lemma E.6 (Hardmax Explicit Form). For any vector E R", the zero-temperature softmax function outputs uniform distribution over the set of indices achieving the maximum value:
if i E arg mag,ax Tj otherwise
[softmaxo (x)); =
aarg max, myl
(28)
0
19

---

PENCIL: Long Thoughts with Short Memory
E.2. Transformer Layers
Below we define the modules used standard transformer architecture. For simplicity, we define each module as a parametrized function mapping from sequences to embeddings (Definition E.1), which can be extended to sequences-to sequuuneses by the canonical extension (Definition E.2).
1. Token Embeddings (TE) A Token Embedding layer parametrized by parameters OTE E [Rdx is a function TErrs" Σ + R. which maps each element x E Σ to a d-dimensional vector @Tæ(z) E R We abuse the notation and extend the definition to sequences, that is, TE Σ* >> IRd where TE( Fn) T=( for any positive integer n and 21;-..,2p Σ.
2. Positional Embedding (PE) For dpæ E N. let ΦPE NN-+ Rdoe be a parameter-free feature function." 4 A positional embedding layer parametrized by parameters Opg E Rdxdpe, PEere N+ - RR maps each position E N+ to a d-dimensional vector PE(i) - OPE ΦPE(1). We abuse the notation and extend the definition to sequences, that is, PEerp Σ- Ed where PE( PE(n) Opg Φpg(n) for any positive integer n and 21,..., E.
3. Attention A (parameter-free) Attention mechanism with temperature parameter B N
0 is a function ATTN;: (RAATTN x RAATTS x - + RETTT for dATTN, d'TTN E N+. For sequence of tuples of query/key/value vectors (g:, Ky, 1 E (RdATTN RdATTN Bd the attention mechanism computes:
a = softmax
(
(nnnk)) k))))m))) E R",
(29)
where 3 is the temperature parameter. our analysis we will use B + 0 (see Definition E.5) and we denote ATTN, by AHA (Average-Hard Attention). The output of attention is then computed as a weighted sum of value vectors:
ATTN s aeNN Ky 04)
azuz.
(30)
4. Single-Head Self-Attention Layer (SA) A Single-Hear Head Self-Attention layer parametrized by parameters ASA = (Wo, WK, Wv, Wo) is a function SAaya (Red)* -> TRd For a sequence of embeddings (h1, hin,..., the projection matrices Wo, Wk, Wv, Wo E Idsa xxd map each embedding to query, key, and value vectors:
q= WQ has k, = WK hy, Uj Wy hy-
(31)
For a decoder-only (causal) transformer, the last position n. can only attend to positions j < n. The output is computed using the attention mechanism:
SA (h1, he...., h2)) = WT ATTNN((g: k2 1t)
(32)
5. Multi-Head Self-Attention Layer (MHA) A Multi-Heed Self-Attention layer parametrized by parameters OMHA (0gA A ( is function MHA (Rdd)* - Rd, where each 8 = (W W K. W W for k = 1..... H parametrizes a separate single-head attention. For sequence of embeddings (h1, hg,..., .., hn) E (Rdy", the multi-head attention output is defined as the concatenation of outputs from all individual attention heads:
H
MHA (h2, h2 ... ha)
Σ SA (h1, he, .......... hn))
(33)
This formulation allows the model to jointly attend to information from different representation subspaces.
6. Feed-Forward (FF) A -red-Forward layer with single activation function a I + R and parametrized by parameters 8FF = -Wo, W....., Ws) is function FFg RRd. - IRdd, where Wo. W,,..., WR E ddd
Bpp
der Σ WoSt 1=1
d
d
FF opg (h))a
Σ
W Wi.gehep By: Σ W2 hy
Weicchr
(34)
'A particular case which we will interested is the 1-dimensional feature (r =
'We note our definition of multi-head attention is slightly different from the most classic definition of transformer, where the dimension of each head the model dimension divided by the number of heads. We inflate the head dimension to model dimension for each head ensure more attention heads always better so things are simplified.
20

---

PENCIL: Long Thoughts with Short Memory
We also extend our definition of Feed-Forward layer to the case with finite set of activation functions, denoted by create a copy of feedforward layer for each of the activation function and define FFörr
TACT- In this LOcTACT FF OFF.- with OFF = (DET.) where OFF,e is the parameter of the feedforward layer with activation function σ. Similar to token embedding, we extend the definition to sequences, that is, FFeer: Rdd + Rd where Fr (hi....,h,, hn) = Fr (h,,) for any positive integer n and hı...., hn E R
7. Identity and Residual Connections For any embedding dimension d N we will use the identity function ida (R + R to represent the residual connections in transformer layers. Similar to token embedding, we extend the definition to sequences, that is, ida Rd + Rd where ida(hı,..... hn) hn for any positive integer and h E R.A
8. Linear Projection Layer A Linear Projection Layer parametrized by parameters Ornos E Rderosse xd is function PROJepROJ : (I + Rdrros, For sequence of embeddings (h1, .i,...,,,,,, the linear projection layer applies linear transformation to the last embedding in the sequence:
PROJepnos (h1, hg........................ .......,,)))) 8PROJ hn.
(35)
9. Decoding Layer A (Greedy) Decoding Layer is a special projection layer followed by argmax, parametrized by ODEC E I gxx, where dPROJ = [Σ]. For a sequence of embeddings (1,,,,,.,,,,,))) the decoding layer first applies a linear projection to the last embedding:
DECreRd (h1, he,..., hn) IDEC hn E R Σ
(36)
Then, the next token is deterministically selected by taking the argmax:
In+1 arg max [DECo (h1, hg.... hn)lu- xe
(37)
Here we assume the argmax is well-defined, i.e., the maximum is unique.
Definition E.7 (Transformer Layer). A single transformer layer Horma Opp (IRd)- - Rd with residual connection and set of activation fucntions TACT, and average-hard attention is defined as:
TF FooSHA OFr (FF + ida) (MHA0MHA + idd)
(38)
The sequence-to-seqqeence version of the layer is defined as:
TF Oxaax
(FFøge + idda (MHA0 ida)
(39)
Definition E.8 (Transformer as Next-Toker Generator). Let (ØTE, ( (0/2) ODE)) be the parameters of the transformer. The end-to-end next token generator Ty Σ + defined as:
Tg DECRDEC
(Otz) TF o(n o
[Eεpe + TEaTs)
(40)
where Of means the composition of functions fr ft-10.... ft
E.3. Function Classes Implementable by Transformers
To understand what kind of next-token generator can be implemented by a transformer in the sense of Definition E.8, it is very useful to understand the class of seq-to-emhedding functions implementable by transformers. After all, the next-token generator is a functions implementable by transformers as follows:
function followed by a decoding layer. We define the class of seq-to-embedding
Definition E.9 (Class of Embedding Functions Implementable by Transformers). For any positive integers dPROJ, we define HTFFeee:TACr) (drRO1) the class of seq-to-embedding functions vé Σ* - RRdroo that can be computed by fixed-size transformers (independent of the length of input sequence). That is, there exist positive integers d, dpr, dsa. H.L. and (OTE, (0 W (off)) L ODeC) with matching dimensions such that:
PROJApROS
(O
TF
*PE + TE
(41)
Finally we define HTFC) EN! HTFlope:TAcn (drnos).
21

---

PENCIL: Long Thoughts with Short Memory
Finally, we define the function class that can be implemented by a token embedding layer, a positional embedding layer, single-head attention layer, multi-head self-attention layer, feed-forward layer, a linear projection layer, transformer layer, and a decoding layer, with all possible input embedding dimensions and output embedding dimensions, as MIe. Hrg. TSA, TMHA, TEP, TPROJ: TIF, TDEC respectively.
For simplicity, we do not assume rounding like standard floating point arithmetics like (Li et al., 2024b) and forward pass of transformer is done full precision. However, because we only use average-hard attention and do not use layernorm, all the intermediate computation in the forward at position n only requires O(log(n)) precision. More concretely, all the intermediate steps can be written exactly as ratio of two integers bounded by a polynomial of n independent of the input (but depending on Turing Machine). In the later parts of paper, will still use I to be the codomain of the seq-to- aeq-to-embedding funcitons, but it can easily be replaced by Qhe with polynomial upper bound (in terms of input length) for the denominators and numerators.
E.4. Closed Operators
Definition E.10 (Average Hard Attention Operator). For any d, E N+, we define the average-hard attention operator aha: M((B") x M((R") x H((B") + H(R")) ) as the operator induced by average-hard attention AHA. Formally, for any three seq-to-embedding functions q, k E H(R))) and v E H(R")) and any integer n, and any sequence x E Σ", we define
aha(q, k. (z))
(q,
Σ a5u(215)
(42)
j5n
where softmax, ((9(x)- ((=1;)))==1 are the attention weights using the hardmax function from Definition E.5. (I, kt, (xx) is a sequence of length n where the ith term is (g(Z):)) k(mra), v(()::) Specifically, aj is non-zero only for positions j that maximize the dot product ((x) k(z1.)), with equal weight assigned to all such maximizing positions.
Definition E. (Local Operator). We say an operator w H(R()) x H(Rdds x x H(RRde)) + H(R")) is local for some positive integers ks d', and {d, } iff there exists a function dw RE di + Rd such that for any ths E H(R)), w(th1.... vx) = tww o [,h,...., rhb..
Definition E.12 (Direct Sum and Concatenation). We use [u, u| denotes the concatenation of vectors u and v. For two real vector spaces d and Rdd their direct sum [R < ddd is defined as the set of the concatenation of their individual elements:
Rd + d
{[01, 02] in E Rd 02 E Rdd = Rdd+
(43)
For two functions Φ : Rd - R and Φ2 R2 + R their direct sum Φ1 ① d2 : Rd @ Rd + Rd @ RR defined as:
(01 + ([V1, v2]) = ( (v1). (222 for all U1 E Rd Up R
(44)
For two function spaces Ti { Rd + Rdd) and Ts {g : Rd + RR,. J. their direct sum Ti @ Ta is defined as:
T T2 (f g I Tı, g E T2)
(45)
where each element is function from Rd @ R2 to R @ R
For two seg-to-embedding functions 4/1 E H((R1)) and the E H(R4),, their concatenation [w1, E+ - Rdi+ is defined as:
(2]x)) = (a), [2() for all x e Σ". Definition 1.13 (Closed Operators). A closed operator is a mapping w: H(R4)) x H(Rd2) x x... x H(Rde)) - H((R")). for some positive integer k, that is wWy,...., 1/x) E (TF((OP::TACT) for any $1,...,, thk E HTFFooe:TACTT]
(46)
F. Full-Access Sequence Processing
Following the footsteps of (Weiss et al., 2021; Yang & Chiang, 2024), we define more powerful version of RASP, called Full-Access Sequence Processing language. Our language is poewrful than RASP and C-RASP in the following two senses: (1). FASP support sequence of vectors as opposed to sequence of numbers only. (2). We allow simulating standard hard attention mechanism, while RASP must decide whether to "select" (attend) some entry only based on the indivual pair of key and query, but not the comparison between the rest pairs. FASP is provably equivalent to the expressiveness of transformers with werage-hard attention and casual masking.
22

---

PENCIL: Long Thoughts with Short Memory
Definition F.1 (FASP). Let OPE: N+ PE be feature function for positional embedding and TACT be the class of activation functions. We define the F FASP (ØTE; TACT] program the process of defining a sequence of token-sequence-to- embedding ,1,..., th H using FASP (PP: TACT] operators. The program is defined as follows: at each step & E [n], the program maintains a set of defineable seq-to teebedding functions St, and defines new function by concatenation functions in S,, or applying local operators (corresponding to MIP), or non-local operators (corresponding to average-hard attention) to some function in S, Finally we add the newly defined function to St, which yields S141. In detail, we define the defineable functions at step / E [n]:
S. a HTE U (ÔPE) U (0: 11sist-1)
(47)
Note this also implies that S, S {1b).
2/ at step f has be defined by applying one of the following four primitive operators on already-defiend functions from S,
1. Concatenation: 2h = [t,, 1 where 1i, v E St. This operator concatenates the output embedding vector of two
functions into a longer vector.
2. Average-Hard Attention: 1/2 = aha(t, vi, " where t. vi, r E S, and chaa have the same output dimension. This implements average-hard attention with query vi key w', and value v/",.
3. Linear Projection:
th Φ o vb, where vo E St and @ is a linear transformation with arbitrary output dimension.
4. Nonlinear Activation: t/x = Φ th, where Φ I + R E TACT, v E S2 (((k) for some positive integer k.
We denote the set of such final outputed seq-to-embedding functions defineable by FASPas some the with position embedding óPE and activation functions TACT as FASP [ASP[OPE; TACT].
In particular, when we want to use FASPto define represent a function mapping from sequence of tokens E" to single token in Σ, we could simply require to the embedding of dimension of [Σ), assume an implicit order over Σ so the index maps to a token in Σ and return the index (token) with the largest value in the last function defined."
Theorem F.2 For any positional encoding feature function ΦPE and activation function class TACT, it holds that FASP [ TACT] (TF(OPE:TACTT)-
The high-level idea towards the proof of Theorem F.2 is to show that the four operators that generates new functions in FASP [ASP[OPE; TACT] are also closed under the class of embedding functions that can be implemented by transformers, namely HTF(APE:TACT)) We defer its full proof to Appendix J.2 and only sketch the high-level idea via providing some key lemmas below.
As the base case, i.e., when the number of transformer layers is 0, we know that the class of seq-to-embedding functions simply the class of embedding functions, including both token embedding and positional embedding. Lemma F.3. The function classes corresponding to token embedding and positional embeddings are subsets of (TF(OrE::TAcT) Formally, Hre, HTE C "MTF(pe::AAcr)
Next we will also identify two main types of closed operators: concatenation and transformer layer, where the latter includes local operators by feedforward networks with non-linear activation functions and non-local operators by average-hard attention.
Lemma F.4 (Closedness Under Concatenation, Direct Sum, and Sum). We have the following closedness property for seq-to-embedding functions under concatenation, direct sum, and sum:
1. For any set H {HPE, HTE), for any 4/1, 1/2 E H, their concatenation [4/,, 4/2l E H.
2. For any d, E N, let Od.d' : Rdd + Rdd be the zero function (mapping every input to 0 E R.)). For any set T E (TsA, TMHAA, Trr, Trnos}. (a). Oa, E T and (b).for any & E T, the direct sum & t Os E ET.
3. For any set T E (TMHA, TFF, J.ROJ). T = T (or + Φ2 01,22 E TJ. Moreover, TMHa is the sum closure of
TsA. that is, TMHa = 12/=0, 03 E TSA h N
'We allow multi-variable activation functions like Gated ReI.U (ReGLU), x. 1 xlyl+.
We could assume an arbitrary order to break ties, but we omit this for simplicity. In our examples we always ensure the argmax unique
23

---

PENCIL: Long Thoughts with Short Memory
4. For any set T (TMHA, TEP, TRRoJ, TIF, (ida d E NJ), for any $1,02 T, their direct sum Φ1 @ th2 E ET.
Lemma F.S. The concatenation operator is closed over HiP that is, [:-]] H #TFF(eEE:AACT) 7 HIFidmiTTarr
Lemma E66 (Local Closed Operators). A local operator wi is closed over T that is, w. HTF TACT] (d)) x HrF (eTr) (d2) x .... x HLFForr:TAcrr (d&) + Hirjere:Terri (Bd)) for some positive integers k. d', and {d. Ji its equivalent local function &w can be implemented by a multi-layer network with activation functions in TACT
Besides the local operators induced feedforward networks, we also have the following non-local closed operator induced by attention (Lemma F.12).
Lemma F.7 (AHA Closed Operator). Average-hard attention is closed operator over (TF(ere:TArr) that is, for any 4, k E (TPcdrs:TAcr) (R2)) and v E HTF[(rr: (R'") we have aha k v) E (TF(dde:Tacr)) (IRd")
The proof of Lemma F.12 is similar to that of Lemma F.11, which uses the definition of HTF(dPE:TAC)) and the closedness property of concatenation (Lemma F.10). The proof is straightforward and omitted.
E1. Custom Operators in FASP
To further improve the convenience of coding in FASP and proving certain functions can be expressed by constant depth transformers uniformly, we introduce an extension to FASP, which instead of allowing the four primitive operators, we also allow other closed operators Definition E. 13.. Below we are going to introduce a specific grammar that allows us to build new custom operators that are commonly used in transformer models. These operators are not primitive operators in FASP, but be easily implemented by composition of the primitive operators defined in Definition F.1. Those custom operators are closed under the class of embedding functions that can be implemented by transformers, namely H Hi(jon:TAcr) since each primitive operator is closed.
Definition F88 (Custom Closed Operators). Let w H(R2)) H(R42) x... H(R4x) H(Rd") ) be an operator and let its input be .i...., dhz We say is a custom closed operator if it can be expressed as a composition of primitive operators in FASPand other previously defined custom closed operators..
In detail, the definition of w via composition similar to FASPand is as follows:
at each step t E [nl, the program maintains a set of defineable scg-to--mbe functions S, & HTE U {ΦPE} U (1/ S i S - 1) و S k).
at each step & E [n)]. the program defines a new function 1aa by applying either one of the four primitive operators in FASP, or a previously defined custom closed operator to some functions in S,. the operator w returns the last function defined in the program, i.c., vn. input of ei....., ER.
When the definition via composition is short, also write them in an inline format without explicitly naming the intermediate dh..
Example E9 (Addition). We define the addition operator add: H(R) x H(R) + H(R) the operator that takes two seq-to-embedding functions vo, vi E H(Rd) and outputs their element-wise sum:
add(v, (x) = (xxx) + (x) for all x E Σ*
(48)
Lemma F.10. The concatenation operator is closed over HTF[(er:TACrT) that is, [: H2 M - HTF (TFRRORRTTACC))
Lemma F.11 (Local Closed Operators). A local operator is closed over HTr(dee:Txerr) that is, HTT[oee:TAer (d1) x (dz) x ... x HTF(deE:TAcrr (d&) - HTF ( (R'") (R for some positive integers k. d', and {de 1 its equivalent local function /h can be implemented by a multi-layer network with activation functions in TACT
Besides the local operators induced feedforward networks, we also have the following non-local closed operator induced by attention (Lemma F.12).
Lemma F.12 (AHA is Closed Operator). Average-hard attention a closed operator over HyFFore: that is, for any k E HTFFope:TAcrr (IRd) and v E HrFijee:TAer) (1""", ), we have aha(g, k, v) E HTF(ove:TAcr (IR
*Those operators cannot be defined with w
24

---

PENCIL: Long Thoughts with Short Memory
The proof of Lemma F.12 is similar to that of Lemma F.11, which the definition of (TF(cre:TAcr) and the closedness property of concatenation (Lemma F.10). The proof is straightforward and omitted.
The addition operator is custom closed operator, as it can be expressed as composition of the primitive operators in FASP:
Algorithm Implementation addition operator, add( v/2)
Input Two seq-to-emiee -o-tee--beddiigg functions 1/ 1/2 E (((I)))
Output: seq-to-embedding function 1² E (()
Veat [0', 1/2] // Concatenate the two functions
16* < (Vea)1 (Vea)2 // Linear transformation summation over both coordinates
return 6
Alternatiell,, in the inline format for composition, we can simply write: add(1) a/r) v + +.
F.2 Fine-Grained Types of Beq-to-Embedding Functions
So far we have been talking about ceq-to-embedding functions whose ranges are IR It turns out to be useful to consider more fine-grained types of seq- toeebeddd functions whose range are only subset of Rd The main benefit of restricting output types is that it also simmplifies the construction of following operators, they they only need be defined on teg-bo--mbe functions with smaller domains. In particular, will be interested in and use the following three types:
Binary Beq-to--mmedddig Functions: These are seg-bo-embed functions whose range is 13d. We denote the set of all such functions as 70( 1)²).
Integer ton-ted-mmddinngg Functions: These are seq-to-embedding functions whose range is 2d, We denote the set of
all such functions HzZz)..
One-Hot Sem-to-Embedding Functions: Given finite set A, define H(onehot (A)) as the class of seq- to to-embedding functions whose range is the set of one-hot encodings of elements in A. Specifically, for any v E (oneoo((())) and any input E E", (b())) E (ea E A} where ea E {0, 1]14| is the one-hot encoding of element a E A. (See definition of onehot below, Definition F.13)
One-hot embedding will be particularly useful at the last line of FASP, when we need to take argmax of the output embedding to get the final token. recommended practice here for the readability of the code here is to ensure the last embedding before argmax computes the one-hot embedding of the desired output token.
Definition F.13 Hot Encoding). We define the one-hot encoding operator onehot A A + {0, (0,14 for any finite set A as:
[onehot)(a)]: [1 if is the i-th element of A under some fixed ordering
(49)
otherwise
We use onehot (A) & (onehota(a) E A} to denote the set of all one-hot encoding operators for all finite sets A. The inverse operation, which maps a one-hot vector back to the corresponding element, is denoted as onehot -1 {0. 1)|AI + A, defined as:
A
onehot (v) where is the i-th element of A and 2s
(50)
When the set A is clear from context, we may simply write onehot and onehot -1 for brevity,
G. Notable Special Cases of FASP
In this section, we would like to discuss some special cases of FASP that are of particular interest. We consider four special cases of FASP, from less expressive to more expressive (see Lemma G.1), that are particular interest: FASP (0; [-1..]] (Ap- pendix G.I). FASP [O; [+,, x] (Appendix G.2), (Appendix G.4).
[+,,, x] (Appendix G.3) and FASP(seq]_en: [[] x]
25

---

PENCIL: Long Thoughts with Short Memory
We first formally define the above mentioned positional embeddings and activation functions. We start with positional embeddings.
0: N - {0). We use 0 to denote the constant position embedding that always outputs 0, which equivalent to not having positional encoding.
is fs.iirs:: N+ - {0, 1. We use is First to denote the function that outputs if the input the first position and O otherwise. That is, is is_firrss is..frrs(mn)
1[2 1].
seq len N+ + N+. We use seq 1en denote the identity mapping over N+, which returns the position index itself. That is, seq_len(n))
This allows the model to directly access the current sequence length.
Now we define the non-linear activation functions that will used in this subsection.
:e + R. We define ReLU(z) [x]+ max(2, 0) to bethe ReLU activation function, which outputs the input if it is positive and 0 otherwise.
multiply(orx) R x IR + R. We use x to denote the multiplication function, which outputs the product of its two inputs.
square: RR + IR. We use this to denote the square function, which outputs the square of its input, i.e., square(x) = x². ReGLU: IR + R. We use this denote the ReGLU (Rectified Gated Linear Unit) activation, which multiplies the first input by the rectified second input, that is, ReGI.U(r v) x[y]+-
Lemma G.1. Let ΦPE and Ppp be two feature functions for positional embedding, and TACT and TKoT be two sets of activa- tion functions. If <PE E FASP [ TACT) and TACT C FASP (ØPE; TACT]. then FASP (pp: TAcT) C FASP (ppp; TACT].
Proof of Lemma G.I. Since 6' E FASP[OPE: TACT], there exists a program in FASP(OPE; TACT] that computes oPE Similarly, for each activation function a' E TÁTT. there exists a program FASP ( TACT] that computes o'. Given any program in FASP (de T.TT]. we can transform it into a program in FASP [ TACT] by: (1) replacing each use of d'g with its implementation in FASP [óPE; TACT], and (2) replacing each activation function o' TAer with its implementation in FASP (Ør:: TACT]. This transformation preserves the functionality of the original program, showing that FASP FASP[Ore: TXcr] C FASP (Ør:; TACT]-
Theorem G.2 (Hierarchy of FASP Variants). The following containment relations hold between variants of FASP:
FASP (0; [+] S FASP[O; (0; H+, x] S FASP[is. [++, x] FASP[see [+,, x]
(51)
where each inclusion represents a strict increase in expressiveness.
Why we care about FASP[O; [-++ x] Most modern LLM architectures use 2-layer MLP with gated linear units (GLU) (Dauphin et al., 2017) as the activation function (Equation (34)), such as SwishGLU (Shazeer, 2020), which a variant of GLU with Swish activation (Ramachandran et al., 2017). For simplicity, we focus on ReGLU, which is a variant of GLU with ReLU activation (Dauphin et al., 2017), and also the limit of SwishGLU the Swish activation approaches ReLU by letting + 00.
Theorem G.3 (Equivalent Expressiveness of Different Activation Sets). The following function classes are equivalent:
PASP [0: H+ x| = FASP 00; [+ square] = FASP (0; ReGLU].
|- x] = FASP [0: H+ square] = FASP ReGLU] by showing that both FASP 00: [+,+ square] and FASP [0; ReGLU are equivalent to FASP (0; [+), x].
Proof of Theorem G.3. We prove that FASP [0:
Equivalence of FASP (0; H++ x] and FASP 00; []+ square]: For the forward direction (FASP(O: x] FASP[O: square)), we show that multiplication can be expressed using square and ReLU:
S
multiply(r,,) = xxy= (x y)² - square(x + v) square(z) -quareuur
(52)
2
For the reverse direction (FASP(0; (0; [+,,, square] C FASP(O; H+, x)), we observe that square is simply multiplication with itself:
square(ı) x² = x =
(53)
26

---

PENCIL: Long Thoughts with Short Memory
Equivalence of FASP D; [++, x] and FASP (); ReGLU): For the forward direction (FASP(0; x] S FASP ReGLU)).
need to show that both ReI.U and multiplication can be expressed using ReGLU:
ReLU(x) [x]+ ReGLU(2, 1)
(54)
multiply(z,9) x ReGLU(I, ReGLU(z,
(55)
For the reverse direction (FASP(O: C FASP 0: [++, x)), directly express ReGLU using ReLU and multipli-
cation:
ReGLU(z, = x[y]+ x |u|+ mil_muutpyy((,Reeul
(56)
Therefore, FASP[O; (0; M++ x] = FASP H+, square] FASP [0; ReGLU].
G.1. Expressiveness of FASP (0; [++]
By Lemma F.11, all the local operators that can be written MLP with ReLU activation are in FASP (0; H+]. This includes:
1. Arithmetic operators over reals (addition, subtraction, max, min):
add H(R) x H(R) + H.).. See Example F.9. We also write 1/1 + 1/2 for add(()), 1/2).
minus H(R) X H(R) - (RR), mi minuss(e (1),, th2) A add(V1,-$22) We also write t/1 U22 for minus(Vi, 122).
max : H(R) X K(R) - H().), max(111 s/2) [wh1 4/2.
min H(R) x H(R) - ((R), minmmhi vb2) _ [[mi - -22)+
2. Boolean operators(AND,, OR, NOT, XOR): For any 4/1, 4/2 H((0, 1}), boolean operators are defined as:
and : H([0, H((0,1)) - H((0, 1)), and( 1/2) - min( v12). We also denote it as shi A 1/2. tb. We also denote it as ーt- defined as: (ot é
not :
or: ((((0 1)) 1}). defined as: (r 1/2) a ((10/1 A -2/2). We also denote it as 1/1 th2.
xor: N((0, 13) x H((0,1)) (({O, 13), defined as: xor 1h2) & (vi V t/22 -(11 122). We also denote
vh V 1/2
3. Comparison operators over integers (less than, equality, etc.):
leq(t), r/2): For every input x E Σ", the less-than-or-equal operator leq H(Z)) x H(ZZ) - H((0, 1)) returns 1 if the first argument d is less than equal to the second argument 4/2, otherwise it returns 0. Because it is comparison operator defined only over integers, it admits the following equivalent definition:
leq(V1, v2) [2/2 wh + 1]+ [x/2 +h1++
(written as t/1 S 1/2))
(57)
The remaining comparison operators can be derived from less, which all have type H(Z) x H(Z) H.(O,, 13):
geq(t/, v2) (1/(122, v/) (written 4/1 2 v/2)
(58)
equal( v/2) A leq(11, 122 A leq(t)2 th1) (written as t = xb2)
(59)
less( v/2) leq(t), 1) (written as sh < 1/2)
(60)
greatez((), 22) Less( v1) (written as uy > v/22)
(61)
neq(U), (2) not(equal (W), tb)) (written as w # vb2)
(62)
It is worth noting that equal be extended vector inputs, Uden+ HZZ H(Z²) by comparing each coordinate of the two vectors and take the logical AND of all the results. Similarly we extend neq to vector inputs by still setting it to be not o equal.
4. All operators on finite discrete inputs (with one-hot encoding). Namely all operators with signature H(onehot (At)) x ..... An. In particular this includes the kronecker- product operator @ H(onehot (A1)) x H(onehot(AA)) - H(onehot x A2), where
H( onehot (A2)) x..... ......x H((oneot (An)) + for finite sets A1, A2....,
(2)))) (wi 8 (2)) Φi (1) 3 (2(x),
(63)
27

---

PENCIL: Long Thoughts with Short Memory
for any x Σx. Here @ on RHS is just the usual kronecker product in on vector space. For simplicity, we will an A1 and 02 E A2 to denote the coordinates of t/ and 4/2 respectively, and use (01, (2) to denote the coordinate of 1i @ 2/2. We can construct 1 @ the by setting (t11 @ (a) 1 andu2a2 for all ai E A and d2 E Ag. 9
We can also define the following non-local closed operators:
1. Running Average: For any &h E H(RR), the rumning average operator average H(R) - H(RR computes the average of all prefix function values. For any input e " of length
_ n
(v)
((ng)
(64)
This can be constructed using average-hard attention with constant queries and keys: average( _ aha(1, 1,)
2. Running Maximum: For any E H(R), the running maximum operator seq_ma H(R) H(R) returns the maximum value across all prefixes. For any imput z E E' of length n:
seq (axmxx(
max ((11)) j=
(65)
This can be constructed as seq_max(1) (ha dh, 4). where the position with maximum value receives all attention.
3. Running Minimum: For any 1 (R), the rumning minimum operator seq.min H(R) H(R) returns the minimum value across all prefixes. For any input E* of length
seq.min(v)(x) = min ((T)))
(66)
j=1.....m
This can be implemented by negating the maximum of the negated function: seq min(t)) -seq max(-1)).
4. Running Logical AND: For any H((0, 1)), the rumning logical AND operator seqland: H({0, 1}) H(10, 1)) computes the conjunction of all prefix values. For any input E E* of length
seq (1)
A (m1g))
(67)
Since binary values are used, this is equivalent to the running minimum: seq.and(v) - seq.min(v).
5. Running Logical OR: For any E H((0, 1}), the running logical OR operator seq.or: H((0, 13) H((0,1))
computes the disjunction of all prefix values. For any input x: E* of length
n
seq_or(i)xz) V ((ns))
(68)
Since binary values are used, this is equivalent to the running maximum: seq or(w) A seq max(
G.2. Expressiveness of FASP (0: [+, x]
FASP[O; [+ x] allows more activation function, I, y X y on top of FASP [++] discussed in the previous section.
We first recall that multiplication activation induces the following multiplication operator mult tiply H(R) x H(R) +
HRR), which is defined as:
multiply(ih, (x) A (x)) (/2(2r)
(69)
for any Et We will use 4/1 the, v/2 4/2, or th ths to denote mul t teltpplylle (111, 1/2) hereafter.
In FASP [0; H4 x] we have the following closed operator:
Note this construction uses the fact that each coordinate of th, is boolean. We cannot define the kronecker product on infinite domains integers or reals without multiplication/squrree// Rel a activation. Will return to this next subsection (Appendix G.2).
28

---

PENCIL: Long Thoughts with Short Memory
Conditional Operator We define conditional operator if_then_else: HH(0011) x H(R4) x H(R4) H(RR.) for control flow, which selects between values based condition:
then e se(Wond Virues Vralse Vrrasee Viroae (xr) if //ond (2)
(70)
(laae(() if (eona(()) 0
This can be constructed directly from previously defined closed operators:
if.then.ee ee elsellleseeee (Weond, Vinee vitalse) - Weonnd Virne + (-rhand)) vhtake).
(71)
G.3. Expressiveness of FASP(is first; [+,
We first recall the definition of is first:
is first() = 1m 1].
(72)
where [|: is the indicator function. In practice, it is important for language model to know whether the current position the first position, and it standard to use [BOS] token to indicate the beginning of the sequence. By using is fi First position embedding, we achieve the similar effect as using [BOS] token. is easy to prove that LLM cannot count without any positional embedding, even with softmax attention. Concretely, without positional encoding, for any parameter A, any token a E Σ, any integer n., Io (a"") (a).). So in some sense is-first is the minimal positional embedding that allows LLM to count.
Simply adding is ssffrrst position embedding allows us to define the following closed operators in FASP firsti [++), and thus also in FASP
[+], x]:
i inv_seq.len: We define inv_seg_len()) = 1/n as the inverse of sequence length by constructing
inv_seq.len en average(seq.len = 1).
(73)
This operator computes the inverse of the current sequence length, which is useful for normalizing operations that depend on sequence length.
is pos A: We define is pas k(n)= [n kt] as the indicator function for the k-th position. This can be constructed as:
kkk + +) inv_seq.len) A geg (k<A + 1) inw.seq.len - -- 1) = gk k-
(74)
(0)) - H((0, is defined as (e))(1)) = [++ + 1] - [+] geqo satisfies that for any x E E', geqo())(z) = = 1f (2x) 2 and 0f (xx)) S -1.
where geg.
This works because at position n. we have inv.seq.len())
1/n. When n k. both k + 1 k(k + 1)/n
k + 1-1 k(k + 1)/k = k
(A: 1)
and lck + 1)/n k- = k(k + 1)/k: k 1 (A + - so
both terms are < O. When n & k. at least one of the expressions will be > 0. making the result false.
rha: We define Rightmost- Hard Attention rha H(Z²) x H(z") x H(RR) + ((Rd) as the hard-attention which
breaks tie by picking most recent argmax of attention score for any positive integer d, d'. That is, for any x E Σ":
( thk (x) (x133))
(75)
where j* is the rightmost position with maximal query-key key match:
j = max [j| (x) the (21.)) max (y the (x1)))
(76)
kgn
This can be implemented using the aha primitive with augmented query and key vectors:
Tha thk v.)) aha ([b5, 1), [b inv.seq.Jen], v.).
(77)
For any two positions j < with identical query-key match scores in the original space, the augmented scores will differ by 1/j + 1/j', which is always positive since - > -1/j' when j < j This ensures that when multiple positions have the same original match score, the rightmost position (largest j) will achieve the highest augmented score, making rha select it as the unique maximum.
We also have the following variant of rightmost hard attention rha which relies on the multiplication activation, ri rightmost best ma match:
29

---

PENCIL: Long Thoughts with Short Memory
Rightmost Best Match For any positive integer d, d', we define righttmost.eest.mat H(Z4) H(RR) - H H(TR)) as the variant of rightmost hard attention which minimizes the &2 distance between key and query, as supposed maximize their inner product. That is, for any E 2":
H(Z2))
i ghtmost best match( the (x) (
(78)
where j* is the rightmost position with maximal query-key match quantified by the l2 norm:
j" = max
arg min JSn
II (z) - thx (x))))))))
(79)
This can be implemented using the rha and the multiplication operator:
rightmost.best maat:iomtttteettttttttttttttee mat ch the 1h)) - rha (1 11, [2 -bx vnu 20)
(80)
For ant input v, this definition retrieves the value the position & that maximizes 21/, (x) (he(())))))))) the (x1 T Tuu (21.))))) or equivalently, minimizes (x)) (x1:)1
Rightmost Exact Match For any positive integer d, d', we define r rightmost.exact match H(Z") H(22') x H(R)) M(R")) H(R") the variant of rightmost best match (and thus variant of rightmost hard attention) which returns the value di, associated with the rightmost key the that exactly matches the query 1hg and otherwise returns the default value tha. That is, for any E "":
rightmost.exact
vx, te va)
Aff then else(righttmsss best mat match((ig Pk thk) uo Vo tba).
(81)
G.4. Expressiveness of FASP len;
[:]+,
We end this section by considering the most expressive case FASP(seq_ []4, x] so far, where seq_len is the identity mapping over N+. With positional embedding seq-len, we can define the following partial sum operator, Σ. which is closed in FASP (seq x]. and thus also FASP[see.lee 1en; [+]t, x].
Partial Sum
We define sum : HR) > (R) as the operator that computes the running sum. That is, for any x E Σ":
sum(v)(x) Σ ((1r))
(82)
This can be constructed by scaling the average operator, i.e., sum(t) average seq_len.
We note that the ability of transformer to express or compute seq-len (e.g., in terms of precision) is necessary to define the partial sum operator, as the sum of the constant token embedding of value 1 immediately gives the sequence length, weich implies that any transformer class that can compute partial sum necessarily can also compute seq-len, even without any non-linear actiation function.
We also note that with sum as a closed operator in FASP aaaq len; [++,, x], it is clear that FASP (seq len; [++, x] is a superset of C-RASP (Yang & Chiang, 2024).
H. Proof of Theorem 5.1: Main Result
We state the formal version of Theorem 5.1 as follows:
Theorem H.1 (Main). Let TM = (A, b, Q, go. Quccept, Qrejez) be any single-tape Turing machine that has time complexity T(x) and space complexity ((z) on input x (A (b))*. There exists a transformer with constant depth, constant embedding dimension, Gated ReLUU activation, and positional embedding n n, average hard attention, such that for the next-token predictor Th implemented by this transformer and the reduction rule o' defined in (9), the following holds:
1. PENCIL produces the same output (accept or reject) as TM on T.
2. The total number of tokens generated by PENCIL, s. is ((T())).
3. The maximal context length used by PENCILL # during generation most (S())).
30

---

PENCIL: Long Thoughts with Short Memory
Problem Setup Our goal is construct learnable model that can replicate PENCIL's model generation process, since the reduction process be realized by the reduction rule. Specifically, each iteration starting from compressed state
0.5)
f4 (x) "",
(83)
we need to construct model that can autoregressively produce the extended sequence
f f fso (z), [SEP], (x), [RETURN]) E E"
(84)
Intuitively, (1) includes newly generated block of uncompressed tokens representing the computations of Turing machine, followed by separator [SEP], , followed by an updated compressed state representing Turing machine's ' current memory, and finally the token [RETURN].
The base case (0.55) - x serves as the initial prompt. Iteration then starts from (1-0.5) and ends with 2+1), Here π Ex' + E the next-token generator in the autoregressive machine that simulates Turing Machine, where E = Q A (-1,0,1). To implement this mapping, PENCIL uses a transformer the next-token generator my: E* - Σ where transformer vocabulary is V A Σ U [[SEP], 1, [RETURN] } and 0 is the transformer parameter. It suffices to show that there is next-token generator x' E FASP [m; [-] +) x] (or equivalently, expressible by a transformer with n + n positional embedding, average-hard attention and Gated ReI.U activation) that can
1. simulate the next-token generator in the autoregressive machine that simulates Turing Machine.
2. generate the special token [SEP] the earliest time that the length will be halved after summarization.
3. simulate the summarization process.
Transformer Construction FASP Program: The construction of the transformer is defined by the following FASP program where each line uses close operator to construct new transformer model in the desired class. For readability, use colored keywords: orange for primitive functions, red for non-local closed operators, and blue for local closed operators. We below clarify the new primitive seq-to teggt--mmeddinng functions used here. 10
1.
Maps token to one-hot encoding of the symbol part of the token, extracting the symbol from state-symbol-move triples. Returns one-hot vector in the symbol alphabet space.
Σ onehot (A)
2. get Σ + {-1, 0, 1}- Maps a token to a scalar value representing the move direction (-1 for left, 0 for stay, I for right) extracted from state saate--ymoll-ovve triples.
3. get-state Σ + onehot(Q)) Maps a token to a one-hot vector of the state part, extracting the state information from state-symbol-move triples.
Most of the closed operators used in the program below are all already defined in Appendix G, except transition. which maps one hot embedding of state and symbol to the onehot embedding of (next state, next symbol, next move) in E. The following program thus completes the proof of Theorem 5.1
1eWe are proving for the simplified reduction rule only. The proof extends the original PENCIL. reduction rule in traiihhtforwand manner.
31

---

PENCIL: Long Thoughts with Short Memory
Detect separator token is_sep (get_token = onehot ([SEP)))
exist_sep or (is_sep)
Phase masks to distinguish between simulation and summarization phases sim phase mask not exist_ sep sum thaase_mas exist_sep and (not is is_sep)
Position tracking for Simulation, frozen in SUMMARIZATION (after [SEP] is generated)
noxt_sim_pos = seq_sum [get_move and sin_phaso_mask,
current_sim_pe = next_sim_pos (get_nove and sim_phase_mask)
max_pos seq max (ar_maaxureet_sim_oooo
min_pos seq seq_ming mi__iin (oo_rminccurret_sin___
@xpecteddssm_lese
max_pos min_pes ReLU [max_pos- next_sim_paa -1)
SIMULATION Phase Get current symbol head positien
current_symbel rightmost_exact_mant (next_sim_ saarrent_sin_posgeeteee onehot (b)
Compute next step based on transition function
simulation_step transition (get_state, current_symbol]
Decide whether continue simulation switch to summarization end sinulaitlttinn sequence_ len >= expected_ sereected_uu_aee len simulation-i__then.comm (end_simulation, onehot ( [SEP]), simulation_step)
SUNMARIZATION Phase
current_sum_pos sem (get_move and sum sum_shaspssseee ham_phase_masee current_sum_len len sum (sum_phase_mask)
Decide the next move in SUMMARIZATION PHASE
next wwwputeepppccceeeeeee.eeceeeeeee (current_ len, next sim pos, pos, min pos)
By construction, exact match always happens.
(currenttssrruu www.rrrenttssuppppomiippooooo current_sin get.e____oooggee_ybbbbbb
summary_step = get_state & summary_symbol & onehct (next_move)
Check if we 'vee reached the final position in sumnarization end__ste summary = ccurrent_sum_ieet
expected_sum_iet summary = if if_then_else (end_summary, onehot [RETURN], summary_stap))
MAIN Select appropriate action based on current phase result (echeennssseexist___eeeeeeeeeeee sumrary, simulation)
32

---

PENCIL: Long Thoughts with Short Memory
I. Omitted Proofs from Section 5 for Genreal Autoregressive Machines
Lemma I.1. Let s be a state function of autoregressive machine M = (E, n. Eaccopt, Erejea).. It holds that so f = 80 80 and that x*+1 wh+t for any k 2 0.
Proof of Lemma I.I. For any 2 E E.. we have that s² = s()). Now let x x= 5(2), = and y x(2) (s(2)))
since s(x) = s(x'), we have s(xx,)) s((=', (()) which further implies that
s ((=((()))) <(<,,))) =((x',())) s(fx()))-
(85)
Therefore, 8 Ja 8 o fa- Now we use induction to prove that s f os s f for all h E N+ The base case k = 1 is already proved. Now suppose s f o ss= so f we have
8 k++ os - so Jm os 00 0
= 80 0
(86)
which completes the induction.
Now we turn to the second part, which simple consequence of the first part. Note that for k 2 1, x² f
fk-1. By first part, f#-1 fä-1 s.s. This completes the proof of the second part.
L.1. Proof of Proposition 5.6
Recall that we partition the full generation into segments indexed by i [4] where is the total number of iterations and each iteration corresponds to one effective reduction. Let to O, and for each 2 1, define f; to be the smallest integer greater than 4-11 such that
Is f (x)) S f oso
(87)
where| ||| denotes sequence length. In words, is the next time step at which the (compressed) state is at most half the length of the newly generated segment. Each iteration i therefore covers times from 4-11 + 1 to 4.
We let (1) denote the sequence
200 &
f.- (x), [SEP], s ffh (z), [RETURN]).
(88)
Applying &smmll then discards tokens except the final compressed state
(1+.55) & ssoft (z)
(89)
which is treated as the initial sequence for the next iteration.
Bounding the Maximum Sequence Length (Space) Consider any point immediately before the [RETURN] of iteration
i. By definition of 4, we have
Is f/ (x))
1 - 880 o80 (x))
(90)
2
Hence, if we look at the entire sequence (88) its length is at most
2|so f-) - 2 + f2) + = ((((,s,2))
(91)
Here the additional "42" accounts for the two special tokens [SEP] and [RETURN], plus small constant overhead. Because s f(-1(()) (and also s (x)) is at most S(M, s, x) in length, we conclude that at every [RETURN), the sequence is (SS(M, 8, x)) long. This implies the maximum context length under PENCIL never exceeds OSSM, a)).
Bounding the Total Number of Tokens (Time) Next, we show the total tokens generated (summing over all iterations) is x)) The critical point is that our reduction rule does not trigger too frequently: if we were to compress immediately after every single token (c.g. each Turing-machin step), we would incur an excessive time overhead. By only reducing when the sequence grows sufficiently large relative to the state size, we avoid inflating the total time cost. Formally, define
f A (6-4-1) + 880 f (x)
2,
(92)
33

---

PENCIL: Long Thoughts with Short Memory
which represents the (length) of generating the new tokens in iteration i, plus the two special tokens (such [SEP] and [RETURN]) We wish to bound Ei=1 l. From the definition of l,, follows that
(4-) + Is fz))()))) 2 2 2 f
(93)
Summing up (93) from 1 to I gives us
(1r (4--6) (0) + 1800 2
Σ ss S (z))
(94)
where Is o f (x)] Since ł, S. a)) (the total number of steps for M), each iteration's generation cost can be bounded by a linear function of t plus the space used by the states. Concretely, summing up & over é yields
Σ
4
(ts 1-)) + (so + 2) s 2t 2I + (x))
(95)
Since S 1 (each iteration covers least one time step) and ł S T(M, x), we conclude 6
Conclusion Together with our bound on the maximum sequence length, this shows that PENCIL simulates M using both optimal space S(M, 8, x) and optimal time T(M, x). Thus, we complete the proof of Proposition 5.6.
J. Omitted Proofs
J.1. Omitted Proofs in Appendix E
Proof of Lemma E.6. Let M arg max; 2y be the set of indices achieving the maximum value, and let Zmax = max, Zy- For any E M, we have x; = maxx, and for any $ M, we have x; < mmax- Consider the softmax function with temperature 3:
exp(xi/3)
(=)) = ΣE=1 exp xxp(2;/3)
exp(xx/B)
ΣjENs exp(xmax/!! + EE exp(x,/3)
For i E M, as +
expl (mmax/ /3)
lim (s) 8-0
lim 8-+0
MM eepp(mmas (3) + Ejen exp(x;;3))
lim 8 [ + j.eM exp((x, xmmxaax 3/3)
Since 2y < Fmax for all j & M, we have (x, fmax) - -00 as 3 + and thus exp((x, 2max)/33) + 0. This gives:
lim (x))) = M
for all i E M
(96)
For i &f M, we have:
exp(x;/3)
lim (x))
lim
8-30
MM exp(xmax/ >jen exp(xx133
exp((x; - Imaax) 1)
lim
M
Ejem exp((x, xmaxx
34

---

PENCIL: Long Thoughts with Short Memory
Since T4 Tmax we have (x, Tmax)/ x as B 0, so exp((2r, Imax)/3) 0, giving:
lim [softmax((=)]: for all i M 8
(97)
This proves that softmaxo(1) distributes probability mass uniformly over the indices achieving the maximum value of T.
J.2. Omitted Proofs in Appendix F
Proof of Theorem F.2. We will prove the theorem by showing both directions of the inclusion: FASP(OPE: TACT] C and (TTrr C FASP TACT].
HTF HTF(dpe: (dp::
Direction 1: FASP FASP[ TACT] C Terrl We show that any function definable in FASP can be implemented by a transformer. We prove this by induction on the number of steps in the FASP program. The base case trivial as the initial set of definable functions S includes token embeddings HTE and positional embeddings ΦPE, which are directly implementable by transformer embedding layers, as established Lemma F.3.
For the inductive step, assume that all functions in S, can be implemented by transformers. Consider new function t defined at step t. We need to show that the HTr(oee:TAcr)) There are four possible operators:
1. Concatenation: If the = [bb, 1 where 1b al E St, then by the induction hypothesis, both z0 and a can be implemented by transformers. By Lemma F.10, we know that concatenation is a closed operator over HTFFore:TAcr]- thus the E HTF [cc::]]
2. Average-Hard Hard Attention: If the = (ha (1,, s/, ") where vh v v3" E St. by Lemma F.12, average-haid attention is a closed operator over HTF(drE:TACTT]- Therefore, the E HIF(dee:Tacrl-
3. Linear Projection: If t/2 W v where & E S; and W is matrix, this defines a local operator per Definition E. I. By Theorem 1,1,, any local operator implementable by a network with quadratic and ReLU activations is closed over (TTe)rE:TAAcT] Linear projection falls into this category, so vhe E HTF(soe:TACTI-
Nonlinear Activation: If vh = & o & where & TACT and e E S,, this also defines a local operator. Since the activations in TACT can be implemented by networks with quadratic and ReLU activations (as assumed in our framework), Theorem F.11 ensures that v HTT(are:TAcT))
Thus, any function in FASP|OrEs TAcT] can be implemented by transformer, establishing that FASP(OrE: TACT] C (TFTT
Direction 2: (TFT( S FASP TACT] We need to show that any transformer can be expressed as a FASP program. We prove this by induction on the number of layers in the transformer.
For the base case, a O-layer transformer just consists of token and positional embeddings, which are already in the initial set of definable functions Sn in FASP.
For the inductive step, assume that any transformer with I. layers can be expressed in FASP. Consider transformer with L + layers. The first L layers can be expressed in FASP by the induction hypothesis. Let's denote this as thz We need to show that adding the (L + 1) layer maintains expressibility in FASP.
The (T. + 1) layer consists of a multi-head self-attention sublayer followed by a feed-forward network:
The multi-head attention can be decomposed into h single-head attention, each of which can be expressed as aha(Wa) viz, W L'z, W .Zz) for i e (I....,h] h), where W W and W are the query, key, and value projection matrices for the i-th head. The outputs of these heads are concatenated and projected through Wo. which can be represented linear projection in FASP.
Multi-Head Attention:
2. Ferd-Forward Network: The feed-forward network applies a linear transformation followed by a nonlinear activation and another linear transformation. This can be directly expressed in FASP using the linear projection and nonlinear activation.
3. Residual Connections: The residual connections simply add the input to the output of each sublayer, which can be
expressed as addition (which a linear transformation) in FASP.
35

---

PENCIL: Long Thoughts with Short Memory
Therefore, any transformer with L layers be expressed in FASP, establishing that HTFlore:TAeri FASP ( TACT]-
Combining the two directions, we have [ASP| TACT] = HTF (Pe::Tar))) which completes the proof.
Proof of Lemma F.4. We prove each claim separately:
(1) Token and Positional Embeddings: For any 11, 1/2 E HTE, let 1/1 : E - Rd and 4/2 : IR be parameterized by OFR E (R24) and FF E (IRd)) respectively. We define [1h,, v2] : I - Rdd parameterized by ÓTE E (R2)) where for each a E Σ. (re(o) = (o), 0 (o)) This directly implements the concatenation, showing that (V1, V2l HTE.
The case for positional embeddings follows similarly. For any 1h, 1/2 HpE with parameters 0 Ogg xdde,
Rdd and
define [4/1, 1/2] HpF with parameters OPp (0pg: 0bgl E IR (2
(2) Zero Function and Direct Sum with Zero: The statement that 0 T is straightforward as each operator allows setting all parameters (weight matrices and biases) to zero
For Φ + 0a, E T, consider any ø E T:
For TSA: Given ø = SABsa with parameters OSA (Wq, WK, Wv, Wo), we define & @ 0 as SAL with parameters ASA = (W Wk Wv, Wo) where:
We
WK]
Wv 0
W/=
Wk
Wi
W Wo o]
For TMHA: The proof follows from the fact that TMha is composed of multiple TSA attention heads.
For TEP: it suffices to prove for the sub feedforward network corresponding to each activation E TACT- Given
R* + and Φ = FF 6rs.. with parameters OFF,o = (Wi) we define & () 0 as FF with parameters
a
W/ [W; 0
For TPROJ: Given PROJepaos with parameter OProS e dd we define 0a,æ PROJ of
pRoS with
OprOJ = [Orros 0].
(3) Closure Under Addition: For any T E (TMHA, TEF, TPROJ}. we T
For TMHA:: The sum Φi + d2 of two multi-head attention modules can be implemented by concatenating their attention
heads into single module with h1 + hı heads.
For TEP: The sum of two feed-forward networks can be implemented by doubling the intermediate dimension and summing their outputs through appropriate matrix concatenation.
For TPROJ: The sum of two projection layers is simply implemented by adding their parameter matrices.
By definition, TMha the sum closure of TsA since multi-head attention is the sum of outputs from single-head attention modules.
(4) Direct Sum Closure: For any set T E (TMHA, TFF, TpRoJ, {ida E N}}, for any Φ1 T with input dimension di and output dimension d', and d2 T with input dimension d2 and output dimension d'2, their direct sum Φ1 ① Φ2 T. This can be proved by decomposing the direct sum
02
(01 ① 0) (0 Φ2)
(98)
where 0 represents the appropriate zero function. From claim (2), know that Φ1 0,,00 d2 T, and from claim (3), know that T T + T. Therefore, Φ1 @ d2 T.
For the identity function, note that id,: (Rd)* + Rd can be implemented by any of the above operators with appropriate parameter choices. For instance, in TMHA, we can set each head to implement identity by using Wa = Ww = Wy = and Wo = I/h where is the number of heads. For TEP, we can set Wo = W1 = 0. W2 = 0, by = by = 0, and b2 = 0. The direct sum of identity functions remains an identity function: ida, 4 ida, ida, +gg which is again implementable by
36

---

PENCIL: Long Thoughts with Short Memory
the same operators with appropriately sized parameters. For TTE: Given any transformer layers Φ1, 22 TTF, where h1 (Rd1)* - Rd and Φ2 : (IRd))) - I= with parameters MHA- f and 8 MHA fpp respectively, we need to show
Φi @ d2 E TTF.
By definition of TTE and transformer layers (Definition 3.16), we have:
Φ1
FF o
+ ida;
MHA
idds
(99)
2
FF 0FF
+ idda
MHA
idde
(100)
MMH
For the direct sum Φ1 @ th,, we have:
Φ1 @ 02
FF
@
FF
- (ida, @ idda))
((MHA
$ MHA
( ) + (ids, @ iddss)
(101)
MIHA
FF
C
FF
- idd:+ds)
(MHA
E MHA
+ iddi +dz
(102)
7F
MIHA
MHA
From our earlier results: FF
OFF
TFF (claim 4) 2. ida, Gida; = ida, 4 (claim 4) MHA
@MHA
MIR
MHH
TMha (claim 4)
Therefore, @1 @ Φ2 can be expressed as a transformer layer, which means Φ1 @ 02 TIF.
Proof of Lemma F.10. We need to prove that for any 11 2/2 HTF(dee:Teer) their concatenation [& v/2l HTF TAcT] Let th E' Rd and th2 En + R2 be two sequence-to-ene tombbeddt-- functions in HrFFeee:TACr) By definition, for E {1, there exist token embedding TE; E HTE, positional embedding PE; E HpB, transformer layers TF. E TIF for f E f1....,,4 L. and projection PROJ; TPROJ such that:
a PROJ: LOLE,FF., (PF+ TE:)
(103)
Without loss of generality, we assume L1 = L2 = L (if not, pad the shallower transformer with identity layers since ida E TrF). We construct transformer that computes [y/1, tha] as follows:
1. Initial embedding layer: By Lemma F.4(1), we construct token and positional embeddings TE = [TE1, TEg] e HTE and PE [PE, PE2] E HrE-
2. Transformer layers: For each l E (1....,L) L}, we define TF. TF1, @ TF2, E TIF by Lemma F.4(4).
3. Projection layer: We define PROJ PROJj PROJ, TPRoJ by Lemma F.4(4).
Thus, [b/,, v/2] = PROJ o (F,) o (PF++ + TE) is expressible by a valid transformer with a constant number of layers, which proves [4)1, w/2] E HTF[oue:TACT)!
Proof of Lemma F.1.. First we claim that if ow can be implemented by 2-layer feedforward network with ReGLU activation, then w is closed over HiFF@pe:TAcri This is because for any th: E HrFfere/Ticrl (d;), we have [di,..., thx E HTF(oPe:TACr)) (xCT) since concatenation is closed. Suppose tui....,u1u can be expressed as:
dx PROJepnos 1 TF oonnn obr)
(PE + TErrE)
(104)
Now, applying 2-layer feedforward network ow to this concatenated output means:
w(ti, wh)) & (Ivi...., vhol)
(105)
Adding 2-layer feedforward network ow,, after this means:
w/k) = tw o PROJornos o (Oten TF TF of
(PE + TE
(106)
37

---

PENCIL: Long Thoughts with Short Memory
To prove this remains in :TFlee::TAcr]) implements zero attention (all weights set to 2. OfF implements ow PRROJerno.
construct additional transformer layer TF SHHA 0
where: MHA
This is valid because the linear projection PROJepros network in ow Specifically, if &w has parameters (Wo, Wi, W2, bo, b1,b2) and PROJaproz has parameter matrix 0proJ. then &w o PROJernos is equivalent to a feedforward network with parameters: (Wo, W1, W2, b, b/ (2) (Widrnos, W1 WrORROJ 22, bo. bi, b2).
be absorbed into the first layer of the feedforward
Therefore, w 1/s)) PROJe o (O/= 1OL++TTP T :fp (PE-TEP, E Hrrjers:Terr where 0 implements the combined function Pw PROJernos and PROJ Pnos the identity projection. This completes the proof of the claim,
Since composition of closed operators remains closed, the above claim extends to any number of layers, which are just composition of 2-layer networks. This completes the proof of Lemma F.11.
38

---

PENCIL: Long Thoughts with Short Memory
K. Example: Boolean Satisfiability (SAT)
K.1. Chain-of-Thoughh
Prompt:
<lstartoftext 1> [4 4 V
(
V
{
+
2 V
4
V
2 J
I
V 4 J A
A
V
A
(
4
V
2 V 3
4 V
V
2
} A [ n V 1
V
) 2
A
[
V
2
V
-
3
)
A
V - 3
A
3
A
3
-
A
A
2
V
<
<lendofprompt
|>
Response:
[CALL] Question: V - 2 )
A
2 V
A
V 3 A V 2 A
2 (- V
4
V 2
)
2
A
A 3
-.4 V A
A (
3
2 v 4 33)
V (V2) (
V
3 V
Try
True [CALL] Questions ( V V
(-2 V
(3
V
A
) A A ( A (4V-2 3
( 4 V A ( 2 V
A 3
V 2 2 A (3V- 1 41 1 4 2 A
V Try 2 True [CALL] Question: ( 4 V 3 A ((3)
( (3V41 A ( 3 A (3V-4
A (- 4 Found 3 Let 3 True [CALL] Question: (4) A (4) Found Let = True [SEP]
Answer: False (RETURN) [SEP] Answer: False (RETURN] Tzy 2 False [CALL] Question: (
A ((4) ) A 3 V 1 (- V - 3 A ( 4.V - 3 A VVV44 ) ( 3 1 A ( V Found
4 Let 4 True [CALL] Question: (-3) A (3) Found -3 Let 3 False [SEP] Answer: False
[RETURN] [SEP] Answer: False [RETURN] [SEP] Answer: ralse [RETURN] Iry 1 Falsee [CALL] Quest
V
V 2 ( 3 4
3 2 4 ( ( 2
(4 2 V
{ V )
A ( 3
V
3 V
V (
( V
Try True [CALL] Question: (
4
A ( V 4
( V 3
A
1 3 A ( V.V 4 Found - Let 4 False [CALL]
Question: (- 3 J A ) ( 3 Found
Let False [SEP] Answer: False [RETURN] [SEP]
Answer: False [RETURN] Try 2 Talse [CALL] Question: (33 V ( A (~ 4 A (- V 3
3 V 4 A ( V
A ( h
31 A ( 7 3
3 4 A A 133V
Found
Tet
False [CALL] Question: 3 A 31 (-3) ( A (3) Found 3 Let 3 True (SE2)
Answer: False [RETURN] [SEP] Answer: False [RETURN] [SEP] Answer: False [RETURN] [SEP]
Answer: False [RETURN] </endoftext
K.2. PENCIL
Prompt:
<lstartoftext(>> |> (4V - 3 V
2
A
4
V 4
-
2
V
A
[ - V - 1 3 ) A (
3
V
4
V
2
)
A A
V - 2 V 1 V
4 V A ( - 1 V
V
2
A
1
V
V
A
(
4
V - 2 V 3 ) A (
- 4
V
L
V
-
3
V
4 4 } A ( - 3 V
1 V - 4
)
A
V
2
V
-
3
)
A
2
V
4 V - 3
A 3
V
V
A
3
V
4 A
2
A
2
<
Response:
Answer:
False <lendoftex: 1>
K.3. Internal Thinking Process of PENCIL
Model Generation (1)
[CALL] Question:
V
4
V
1
)
A
A
V 1) A -V-33V11V2220
V
V {
V
}
)
( ( A {
2
)
V
3
I
A
A ( v (2V-3V
2
4 } [
V
3
V
)
(
V
3
Try
True [CALL] Question: (-4 A
V A
V
A
( 2
V
4
A
( ( V 4 A (-31 3
(-4V33 (
3 3.V 4 A (
4
V
2
V
3
Try
True [CALL] Question: { (7 V 7 (-3
4 A
Tzy 3
True [CALL] Question: (-4) 4 A A ( ( (4)
Found
Let 4
False [SEP]
Answer:
Falae
[RETURN]
Reduction Rule (1)
39

---

PENCIL: Long Thoughts with Short Memory
[CALL]
Question:
(-
V
V
1
A
V
2 V
A ) -
- A
V
V 1 1 A - 3 V
A
V 3 A
V
1
V
-
3
)
A
3
V
1
4
-
1
V
2
- 4
A
[ - 3 - -
A -
V T 4 A
V
-
1
V
3
T
A
2
V 3
1 } - 3V4) A ( V 7 --V-33 (-
A (
A 3 V A
4V A
V
3
V
2
)
A
(
2
V
Try
1= True [CALL] Question: ( 3
2 A
V
A
2
V
4
A
(-433 A V
3
V
2
V
Try
True [CALL] Question:
) A
Try
True Answer: False
Model Generation (2)
[CALL] Question: (-3 V
1
) )
A
V
V
2
A )
V
3 V - A 3V A V
+ V 33D J { 4 V 1 V
3
A
3
V
1
V
4
A
V 2 - 4 A V-3V-1V A
2 4
V
3
A
2
V
A
V 3 (2V-3V
V
V 3
V
2
V
Try
True [CALL] Question:
(-4V A
V A
( 4 V
3
4) A V 2 V
)
Try
True [CALL] Question: (74V 3 3 A V
Try
True Answer: False Try False [CALL] Question: ( Found
Let Talse [SEP]
Answer:
True [RETURN]
Reduction Rule (2)
[CALL] Question: (-3
1
)
V
A
1 A V
[
V
1 V
)
1
V
4
)
V
4
- V A
2 V )
V
3
A
2
3
A
(
1
V 3 A -
V L J A
V
3
V
2 ) A
V
2
V
-
3
1
Try
True [CALL] Question: (-4V- A
2 J A
A
( 2
V
A
3
V 4
A ( 3332. V V (-4V3
2
I 1
3 V
A
[
4
V
2
V
- 3 )
Try 2
True
[CALL] Question: ( 4 VV-33 - A V
) A - 4
Tzy 3
True Anawer: False Try
False Anawer: True
Model Generation (3)
[CALL] Question: (- 3 V
4
V
1
)
A
V
2
A
-
V
V
1
A
> 3 V V
A
{ A
V 3 ) A V
1
V
3
)
A
3
V
1
V
4
)
A
V
2
V
- 4
A
(
- V 1 4
7 3
V J 4 )
A
V
-
1
V
3
Y
A
2
V
1
V
3
A
1
V 4 V
A V
A
{
2
V
V 1 A
V
3
V 2
)
A
(
4
V
2
V
-
3
Try
1
True [CALL] Question: (-4 - 3
A V
2 A
A
2
V
4
A
V 4
A
( 3 2 V - (-4V3
V
A
4
V
2
V
3
)
Try
True [CALD] Question: 4 V - (-33
V
11
4 ))A A
Try
True Answer: False Try False Answer: True [SRP] Answer: True
RETURN]
Reduction Rule (3)
[CALL] Question: - V
4
V
1
)
A
V
2
A
V
V
A 3 A
V 3 4
V
1
V
3
)
A
V
1
V
4
A
2 -
A 3 4 A
2 4 )
V
3
A
V 4 3 (2 3
4
3
V
Y
3
}
Try
[CALL] Question: (-4V
2 A
V
A True
(-4V3
4
V
2
V
Try
True
Answer:
Model Generation (4)
[CALL] Question: (- V
1
)
A
A
1 A 3 -1 4
V 3 ( V
)
V
( - V A
2 )
V
A (
(
4
V 2 I A V 3
V
2
)
(
V - 3 ) Try
True [CALL] Question: (-4V -
A
2
V
)
V 4 ) A (- V A ( (
( 2
V ( 4 V
2
V
Try
= True Answer: True [SBP] Ansker: True [RETORN]
Reduction Rule (4)
[CALL]]
Question: ion: (
)
A
V 1 ( 3 2 { V
{ 4 V 1 V
)
1
V
4
)
A
V
2
(
1 4 A L
V 4 ) A
V
1
V
3
A 2
3
A
( A (2
A C 2
4 A V 3
V
2
)
A
V
3
I
TrY
1
True Answer: True
40

---

PENCIL: Long Thoughts with Short Memory
Model Generation (5)
[CALL] Question: (- 3 V
4
V
) )
A
V
2
A
-
4
V - 1 ( 3
A 4
V 3 1 A { 4 1 V
3
A
3
V
1
V
4
A
( VLVVV 4 v (-3
V
2
V - 4
A
V - A
V
1
V
3
Y
A
2
3
A
3 ( V
v A [ V 3
V
2
2
V
3
Try
True Answer: True [SIP)
Answer: True
RETURN]
Reduction Rule (5)
Answer: True
Model Generation (Final Response)
Answer:
True </endoftext(>>
L. Example: Quantified Boolean Formula (QBF)
L.1. Chain-of- -hoouhhht
Prompt:
<lstartoftext 1> V 3
3 #2 47
3 V #3 (3V1) #4 (- 3
#5
(
P6 ( 4 V
V
v <lendofproopt |>
Response:
[CALL)] Constions
prwEix_fron V. Tay Zalae [CALL] Quest cuestioon pewfix_tron V Try Falus [CALL] Queatiins prefix_ãron 3 Try Falas [CALA] Check
Queation: 3.V.) True Check (.3 (.V. Palxe [GRP] Ansvers Talxe (RECUUR) [SXP] Answers Palxe [3XTUR]] Try True [CAUL]
[CALL] Queations
Queasions Fretix_ V Try 2 Yalle (CALL) Question ions avalaate 1 Tzue 2 Faine 3 Valam 4 ralse Check 40 1 V. 3.1 Toue Check
11 3.3 V.V. 1 Trun Coecs #2 3.3 1.V.1. Iran Check #3 I- 1 M.m V.n Teue Check 84 C.1 V.M. Trae Chack 1- 3 Crue [80P] Teus Coeck
[RETURN] Try 3.M. True Check C.3 [EALL]
Yrus True Valan Palue Check 40 (
Zeue Check 43 (
- 4 Izue Check #4 1 V.n 1.) Teue Check 45 (- 4 V. V.3. Tzue
Tzue Cheak 86 1 m. 4 V. Seua Check #3 (.4
True Pozmala 1290 [SRP] True (CAES) Doastiions prefix_tros
Ansoent Troe [RITUUR)) [SXP]
True [RNTTRR)] [GXP] Ansvers True [RETURN]
evaluabe True Check #2 C.V. V.V. Palee 188P] Ansvert Faloe [RETUUN" [ERP] Answers Talae [ASTURM] Try True CALL. Question: pretixcfron V.2 Try 2 Falae [CALL] Queations eveluace 1 True Valae False 4 Teue Check 40 (5V 3 True Teue Check #3 Min 3
46
I True theck #1 I-m
Coeck 3.V. 3.v.l 1.1. Teue Chack #2 1.3
Froe Chack P6 1
Zeue Check 45 4
Check
[ARTURN] Try
Oues:ion:
evslcate True 2 Troe Falue True Check
3 Trae Check #1 1 3.V. Teue Check (
True Check
n L. V. 4. Tree Cbeck #6 -. Yrus Iruw Check 45 ( 4 V. V.V. Zzue theck #6 1. 1.4
Teue Check #7 1. V.V. 1.3 Seun Pormala (AETORR)) [GRP] Anewert True (RETURN [SRP] Answert True [RETURE)
[S39] Annvers True [ASTURR)) [5XP] Anever:
Guestion: pratix_tron
Tey Palce 2 False True False Check #0 1.3 3 True Check E: (- v.v. Tree Check #2 I
poedix_fton
pretix_tran
CAES' Scestion: evaluste
3.3. True Check #6 C- V.V. True Check 47 1 Palze [GXP] Ansvees Malie [RITUUR) [SEP] Anewess Palau [XXTURN] Tey Teue [SALL] Quaations precix_Fron V. 2 Falle (CALL] True
True Check 13 I 1 V-- 3.v v. True Check #4 T V Trom Check 45 I 1i-4
Questions evaluate
Troe Check 1
Check
Hrue Check (.3 V.-. Troe Check
True Check 45 V.A. Trow Chack 87
True Formala- Trae [SXF] Anavect True (RKTURK) Tey 2 Ze08 [CAIN] Dowecion: evalusbe From 2 True 3. True 6 ralse chack e0
True Check
True Check
True Check
V.VV 3.V.--
Check #4 C.T.
True Check
[RETURN]
RETURN] [SZP. Amswess Troe [ASTTUR)] Try Yruw [CALL]] Quaat sonz prefix_from Tay Palas (CALL) Doestions prefix_from Tey
Palee [CALE] Questionn exaluate Palde 2 Palse 3 True True Check 40 < 3.3.V 3.1 True Check #1 1-33 3.V. 3.3. True Check #2 Check (CAGL) Question: evaluate
3 V.V. True Check
Troe Check
Check 46 in V.4. True Check
True Check #c V.V. 3 True Check 41 V.3 V.1.1 Trae Check #2 1 3 True Check #3 1-- V 3 V. (.). True Check #4 C.1 V
True Formula Tree (6EP] Anoverz True [RE7URM)
False
True
True Check 45 C v.v. 1.1. Troe Check 96 1 4 True Check #7 V.V. 1.1.1 3. True Mormals Trow [SXP] Anavent True [ECTURN] [5XP]
AnsweEi True (RETURI)) [SEP]
[RETURN] (882]
True (RETURK] [8EP] Answer: True (RETURN] <lendeftext
L.2. PENCIL
Prompt:
<lstartoftext|> & 4
41
3
42
3
V
3
V
1
F3
13v1) (- 3
+ 1 #5
( v
1
#6
(
4
v
3 #7 (
#8
V
<lendofprompt
Response:
Anawer:
True </endoftext:>>
41

---

PENCIL: Long Thoughts with Short Memory
L.3. Internal Thinking Process of PENCIL
Model Generation (1)
[CALL] question: prefix_from A 3 Izy False [CALL] Question: prefix_frem frrm Y Try 4 Falae [CALL]
Question: prefix_Irom from 3 Try Palse [CALL] Question: prefix_frem 4 2 Try 2 Palse [CALL]
Question: evaluate False False 3 False False Check #0 - True Check
#1
3 True Check
False [SE?] Answer: False [RETURN]
Reduction Rule (1)
[CAL]] Question: prefix_from V Try False [CALL] Question: prefix_from Try 4 False [CALL]
Question: prefix_from Try Palse [CALL) Queation: arefix_fram 4 2 Try 2 False Anawez False
Model Generation (2)
[CALL] Question: prefix_from v 3 Iry False [CALL] Queation: prefix_ frem V 4 Try 6 Falae [CALL]
Question: prefix_from 3 1 Try False [CALL] Question: prefix_from V 2 Try 2 False Answer
False [SEP] Answer: False [RETURN]
Reduction Rule (2)
[CALL] Question: prefix_from V 3 Try Palse [CATT] Question: prefix_from V 4 Try 4 Palse [CAL]]
Question: prefix_ from Try False Answer: Falae
Model Generation (3)
[CALL] Question: prefix_freee from 4 Try
[CALL] Question: prefix_fren frem Try Palse [CALL]
Question: prefix_froo from
Try False Answer: False Try 1 True [CALL] Question:
prefix_ V 2 Try 2 Fal se [CMIL Question: evaluate
True
Pai se 3 Fal se
False Check #0 ( 3 V - 3 True Check #1 ( 3 V 3 v
True Check #2 3 V 1 True Check
43 | - - - - 4 True check #4 ( V - 1 Irue Check 45 ( 4 4 V é V 3 True Check #6
( ( 4 Trme Check 47 ( (4V1) True Formula - True [SEP] Answer: True [RETURN)
Reduction Rule
[CALL] Question: prefix_from V 3 Try False [CALL] Question: prefix_fred Y 4 Try 4 Falae [CALL]
Question: on: prefix_from from F. Try False Answer: False Try 1 True [CAL]] Question:
prefix_from V Try 2 False Answer: True
Model Generation (4)
[CAL]] Question: prefix_freee V Try
[CALL] Question: prefix_frem from Try Palse [CALL]
Question: prefix_froo
Try False Answer: False Try 1 True [CALL] Question:
prefix_from V 2 Try 2 False Answer: True Try 2 True [CALL] Question: evaluate 1 True 2
True 3 = False
False Check #C ( V 7 True Check #1 ( V v 1 True Check #2
3 V 1 True Check #3 11 V - 4 True Check #4 - 111 True Check #5 ( (- 4 V
3 ) True Check $6 { - 4 True Check 47 (4V1) True Formula - True (SEP] Answer:
True [RETURN]
Reduction Rule (4)
[CALL] Question: prefix_from A 3 Iry False [CALL] Question: prefix_freee Y 4 Falae (CALL)
Question: arefix_from 3 Try False Answer: False Try 1 True [CALL] Question:
prefix_from V 2 Try 2 False Answer: True Try = True Answer: True
Model Generation (5)
[CALL]] Question: prefix_from V Try Question: prefix_from Try False Answer: Falae Try 1 True [CALL] Question:
[CALT]] Question: prefix_frem Try 4 Palse [CALT]]
prefix_from 2 Try 2 False Answer: True Try 2 True Answer: True (SEF) Answer: True
RETURN]
42

---

PENCIL: Long Thoughts with Short Memory
Reduction Rule (5)
[CALL] Question: prefix_free From V Try False [CADL] Question: frefix_frow Try 4 False [CALL]
Question: prefix_from Try False Answer: False Try True Answer: True
Model Generation (6)
[CALL] Question: prefix_free V Iry False [CALL] Question: prefix_from Try 4 False [CALL]
Question: prefix_freorr From Try Palse Answer: False Try True Answer: True [SEP] Answer:
True [RETURN]
Reduction Rule (6)
[CALL] Question: prefix_from V 3 Try Fa [CALL] Question: prefix_ From Try 4 False Answer:
True
Model Generation (7)
[CALL] Question: prefix_from V 3 Iry False [CALL] Question: prefix_ from V 4 Try 4 False Answer: True Try 4 - True [CALL] Question: prefix_from from Tzy 1 False [CALL] Question:
prefix_froo V 2. Try 2 Pal se [CALL] Question: evaluate 1 False 2 False 3 7alse
True Check #0 3 V
True Check #1 ( - v True Check #2 { 3 1 False [SEP)
Answer: False [RETURN]
Reduction Rule (7)
[CALL] Question: prefix_trom A 3 False [CALL] Question: prefix frem Y 4 Falae Answer: True Try 4 True [CXLL] Questien: prefix_free from Tzy False [CALL] Question:
from V Try False Answer: False
Model Generation (8)
[CALL] Question: prefix_fee from V Iry False [CALL] Question: prefix_frem Try Falae Answer: True Try True [CALL] Question: prefix_from from Tzy False [CALL] Question:
prefix_from 2 Try False Answer: False [SEP] Answer: False [RETURN]
Reduction Rule (8)
[CALL] Question: prefix from v Try True Try True [CALL] Question: prefix_from Tzy False Answer: False
(CALL) Question: prefix frem Try 4 False
Model Generation (9)
[CALL] Question: prefix_froo V Iry False [CALL] Question: prefix_fron Try 4 False Answer: True Try 4 True [CALL] Questions prefix_from from Tzy False Answer: False Tzy 1 True [CALL] Question: prefix_from V 2 Try
False [CALL] Questien: evaluate 1 True 2 = False
= False 4 True Check #0 ( 33V - 3 True Check #1 ( ( 3 V V 1 True Check #2 ( [ V
True Check #3 ( - 1 y 3 V wid 4 True Check 14 V 1-11 True Check 15 { 7 4 V V 3
True Check #6 { - 4 V True Check 17 ( True Formula True (SEF) Answes: True [
RETURN]
Reduction Rule (9)
[CALL] Question: prefix_from Y 3 Iry False [CALL] Question: prefix_frem Y Try 4 Falae Answer: True Try 4 = True [CALL] Question: prefix_free from E Tzy False Answer: False Try 1 True [CALL] Question: prefix_from V 2 Try False Answer: True
Model Generation (10)
(CALL) Question: prefix_ffeee from Y 3
False [CALL) Question: prefix_free Y 4 False Answer: True Try True [CALL] Question: crefix_from Try False
False Try 1 True Try True [CALL] Question: ( ( 3 1 True Check 42 1 True Check (-11 -iv- 3 4 True Check #4 ( ( V 1 Irue
(CMLL) question: prefix_ V Try False Answer:
avaluate True
False T-ue Check
True Check
Check 45
3 True Check #6 ( (- 4 True Check 47 4.4 V 1 True Formula
True [SEP]
Answer: True [RETURN]
43

---

PENCIL: Long Thoughts with Short Memory
Reduction Rule (10)
[CALL] Question: prefix_from A 3 Try Palse [CALL] Question: prefix_from from A 4 4 False Answer: True Try True [CALL] Queations prefix from Try False False Tzy
(CALD) Question: prefix_from A 2 rry ralse Answer: Try 2 Answer:
Model Generation (11)
[CALL] Question: prefix_from V 3 Iry = False [CALL] Question: prefix_ from V 4 Try 4 = False Answer: True Try 4 - True [CALL] Questien: prefix_ from Tzy 1 ralse Answer: Palse T=y 1 True (CMLL] Question: prefix_from A 2 Try Palse Answer: True Try 2 True Answer: True [SFP] Answer: True [RETURN]
Reduction Rule (11)
[CAL]] Question: prefix_fren V Try False [CALL] Question: prefix_from Try 4 False Answer: True Try True (CALL) Question: prefix_ from Tzy False Anawer: False Tzy 1 True Answer: True
Model Generation (12)
[CALL] Question: prefix_froo from A 3 Try False [CALL] Question: prefix_frem Y 4 Falae Answer: True Try 4 True [CALL] Question: prefix_from Try False Answer: Palse Try 1 True Answer: True [SEP] Answer: True [RETORN]
Reduction Rule (12)
[CALL] Question: prefix_ from A 3 Try False [CALL) Question: prefix_ frem Try 4 False Answer: True Try 4 = True Answer: True
Model Generation (13)
[CALL] Question: prefix_from V 3 Try False [CALL] Question: prefix_from V Try 4 False Answer: True Try True
[SEP]
[RETURN]
Reduction Rule (13)
[CALL] Question: prefix_from V 3 Try False Answer: True
Model Generation (14)
[CALL] Question: prefix_fre _rom V 3 Try False Answer: True Try 3 True [CALT]] Quest prefi From V 4 4 False [CALL] Question: prefix_from
Try False [CALL] Question:
prefix from. V Try False [CALL] Queation: evaluate
False
False
True
False Check ( 3 True Check (
True Check #1 ( (- V 3 V 1 True Check #2 V 11) True Check True Check +5 ( ( 4 4 V True Check #6
#3 (
( (-6V4) True Check #7 (4V1) False [SEP] Answer: Palse [RETURN]
Reduction Rule (14)
[CALL] Question: prefix_from from Y 3 Iry False Answer: True 3 True [CALL] Question: prefix_frem Y 4 Try 4 False [CALL] Question: prefix_froo from = Tzy False [CALL] Question: from V Try False Answer: False
Model Generation (15)
[CALL] Question: prefix_fret from V 3 Try False Answer: True Try 3 True [CALL] Quest prefix_from
Y 4 Try 4 False [CALL] Queation: prefix from Tzy 1 False [CALL] Question:
fromix_from V 2 Try 2 False Answer: False [SEP] Answer: False [RETURN]
Reduction Rule (15)
44

---

PENCIL: Long Thoughts with Short Memory
[CALT]] Question: prefix_from V 3 Try Palse Answer: True Try 3 True [CALT]] Quest prefix_ from
V 4 Try 4 False [CALL] Queation: prefix from rzy 1 False Anawer: False
Model Generation (16)
[CALL] Question: prefix_from V Try False Answer: True Try 3 True [CALL] Question: prefix_from
A 4 Try 4 Palse [CALL) Question: prefix_ from Tzy False Anawer: False Tzy 1 Irue
(CALL) Question: prefix_froo
v 2 rry
Zalse [CALL] Questien: evaluate 1 Irue 2 False
True 4 = False Check #0 ( 3 - 3 Trae Check #1 (- 3 V 3 V 1 True Check #2 [ 3 V 1
True Check #3 7 1 V 3 4 ) True check #4 V V-1 Irue Check $5 ( 7 V 4 V 3
True Check #6 - a V 4 True Check #7 (4V1) True Formula True [SRP] Answer: True [
RETURN]
Reduction Rule (16)
[CALL] Question: prefix_from V 3 Iry False Answer: True Try 3 True [CALL] Question: prefix_free
Y 4 Try 4 False [CALL] Questien: prefix_ from Tzy 1 False Anawer: False Tzy 1 - True
(CALL) Question: prefix_from A 2 Try False Answer: True
Model Generation (17)
[CML]] Question: prefix_from V 3 Try False Answer: True Try 3 True [CALL] Question: prefix @refix_from From
Y 4 Try 4 False [CALL] Queation: prefix_ from Tzy 1 False Anawer: False Tzy 1 True (CALL] Question: prefix_froo from A 2 Try
False Anawer: True Try 2 True [CALL] Question:
evaluate 1 True 2 = True 3 = True 4 = False Check #0 V
True Check #1 (
3
+ 1 True Check 42 3 V 1 True Check #3 (-VV- V 1 4 True Check #4 (1 - 1 True
Check 15
V True Check #6 (- 4 V True Check F7 (4V True Pormula
True [SEP] Answer: True [RETURN]
Reduction Rule (17)
[CALL] Question: prefix_from V 3 Try 3 False Answer: True Try 3 True [CAL]] Question: prefix_ x_rom Y 4 Try 4 ralse [CALL] Question: prefix_free from E Tzy False Anawer: False Tzy 1 True
(CALD) Question: frefix_from 4 2 Try False Answer: True 2 True Answer: True
Model Generation (18)
[CALL] question: prefix_fee from A 3 Iry False Answer: True Try 3 True (CALL) Question: prefix_fee from 4 4 Try 4 False [CALL] Questiens prefix_ from Tzy 1 False Answer: False T=y 1 True
[CALL] Question: prefix_from V 2 Try False Answer: True Try 2 True Answer: True [SEP]
Answer: True [RETURN]
Reduction Rule (18)
[CALL] question: prefix_from from V 3 Iry False Answer: True Try 3 True [CALL] Question: prefix_ from V 4 Try 4 False [CALL] Question: prefix_from E Try 1 = False Answer: False Try 1 = True
Answer: True
Model Generation (19)
[CALL] Question: prefix_from V 3 Iry False Answer: True Try 3 True [CALL] Question: prefix_from
V 4 Try 4 False [CALL] Queation: prefix_from Tzy 1 False Anawer: False Tzy 1 = True Answer: True [SRP] Answer: True [RETORN]
Reduction Rule (19)
[CALL] Question: prefix_fros from A Iry V 4 Try False Answer: True
False Answer: True Try True [CALL] Question: Prefix_from
Model Generation (20)
45

---

PENCIL: Long Thoughts with Short Memory
[CALL] Question: prefix_from V 3 Try sa Answer: True Try 3 True [CALT]] Quest prefix prefix_from From
Y 4 Try 4 False Answer: True Try 4 True [CALL] Question: prefix_irom 3 1 rry 1 Falae
CALL] Question: prefix_ from 2 Try 2 - False [CALL] Question: evaluate
Falae 2 False
= True 4 = True Check #0 { 3 V n 3 True Check #1 ( 3 v V True Check #2 3 V 1
True Check #3 (-11 - V - 4 True Check #4 V 111 True Check +5 ( V 4 3
True Check #6
True Check f7 ( True Formula True [SBP) Answes: True [
RETURN]
Reduction Rule (20)
[CALL] Question: prefix_fron V 3 Try False Answer: True Try 3 True [CALL] Question: prefix_ from from V 4 Try False Answer: True Try True [CALL] Question: prefix_from Try 1 False CALL] Question: prefix_from Try False
Model Generation (21)
[CALL) question: prefix from 4 Iry
[CALL] Question: prefix from 4 Try 4 False Answer: True Try True [CALL] Question: prefix_from Try 1 False
Answer: Try
CALL] Question: prefix_from from Try 2 False Answer: True Try True [CALL] Question: evaluate 1 - False
True True
True Check #e V True Check (
True Chack #2 V True Check #3 ( V - V 4 True Check F4 ( V V 1 True
Check #5 ( - v V True Check #6 (-4 (-VV4) True Check #7 ( (4VL True Formula
True [SEP] Anawer: True [RETURN]
Reduction Rule (21)
[CALL] Question: prefix_from V 3 Try 3 False Answer: True Try 3 True [CAL]] Quest prefix_from V 4 Try 4 False Answer: True Try 4 True [CALL] Question: prefix_ xrom E Try 1 False
CALL] Question: prefix_feet from & Try 2 False Answer: True Try True Answer: True
Model Generation (22)
[CALL] Question: prefix_from V 3 Try False Answer: True Try 3 True [CALL] Question: prefix_from Y 4 Try 4 False Answer: True Try 4 True [CALL] question: axefix_fren 3 Try 1 False
CALL] Question: prefix_from V Try 2 False Answer: True Try True Answer: True [SEP]
True [RETURN]
Reduction Rule (22)
[CALL] Question: prefix from V Iry False Y Try False Answer: True
Try [CALL] Question: prefix from Try [CALL] Question: prefix_frem Try Falae
Model Generation (23)
[CML] Question: prefix_fros From V Try Answer: Try 3 [CAL]] Quest prefix from Y 4 Try 4 False Answer: True Try 4 True [CALL] Question: prefix_from Try 1 False
Anawer: True [SEP] Answer: True [RETURN)
Reduction Rule (23)
[CALL] Question: prefix_free from V Iry False Answer: True Try 3 True [CALL] Question: prefix_from
V 4 Try Pai se Answer: True Try 4 True Answer: True
Model Generation (24)
[CALL] Question: prefix_freee from V 3 Try False Answer: True Try 3 True [CALL] Question: prefix_ from V 4 Try 4 False Anawer: True Try 4 = True Answer: True [SEP] Answer: True [RETURN)
Reduction Rule (24)
[CALL] Question: prefix_from V 3 Try False Answer: True Try 3 True Answer: True
46

---

PENCIL: Long Thoughts with Short Memory
Model Generation (25)
[CALL] Question: prefix_ from V 3 Iry True [RETURN]
Fallse Answer: True Try 3 True Anawer: True [SEP]
Answer:
Reduction Rule (25)
Answer: True
Model Generation (Final Response)
Answer:
True <lendoftex: |>
M. Example: Einstein's Puzzle
M.1. Chain-of-Thought
Prompt:
<Istertoftext Constraintal. the Green house is immedi ately the right of the who keeps Bi Birds Constraint42 the Brit is immedi ately to the right of the German 1onstraint43 who keeps Doga is the house as Red house Constraint the who keeps Birds is inmediately the rigat of Swede </enoofprmmpt]
Response:
[CALL] s=m.== Possible Assignments
Houset1
Color category have poasibllities Blue Red
Naticnality category have 3 possibilities Brit German Swede Pet: category have possibilities Birds Dogs Pish
Houset2
Color category have 3 poasibilities Blue Green Red Naticnality category have 3 possibilities Brit German Swede Pet category have possibilities Birds Dogs Fish Houset3
Color category have possibilities Blue Green Red Naticnality eategory have 3 possibilities Brit German Sxede category have possibilities Birds Dogs Fish Unsatisfied constraints are Constraint:) Constraint Constraint43 Constraint Puzzle not solved yet Propagation Applying Constraint:1 [CALL]
PHASE 1: Single-value logic for Green and Birds under RIGET constraint
PHASE 2: Handling relation Green RIGHT Birds
Green is immediately RIGHT of Rirds
Removing Green from Housed1 because Green can't be in the leftmost house if it 's to the RIGHT of
4 Birds
Removing Birds from House#3 can't be in the rightmost house it's the LEFT of Green [SEP] Houset1 Color category changed from possibilities Blue Green Red possibilities Blue Red
Houset3 category changed from. passibilities Birds Dogs Fish possibilities Dogs Fish
+ RETURN]
Applying Constraint#2 [CALL]
PHASE 1: Single-valve logic for Brit and German under RIGET constraint
PHASE 2: Handling relation Brit RIGHT German
Brit is immediately RIGHT of German
Removing Brit from Hlouse11 because Brit can't be in the leftmost house if it 's to the RIGHT of
S Gernan
Removing German from House#3 can't be in the rightmost house if it's to the LEFT of Brit [SEP] Houset1 Nationality category changed from 3 possibilitis lities Brit German Swade to 2 possibilities German Swede
Houset3 Nationality category changed from possibilities Brit German Swede pessibllities Brit
<) Swede [RETURN]
Applying Constraint#3 [CALL]
PHASE 1: Single-valve logic for Dogs and Red under SAME constraint.
47

---

must be right of House PENCIL: Long Thoughts with Short Memory
PRASE 2: Handling ing relation Dogs Dogs must be in the SAME house as Red [SEP] No changes from this constraint [RETURN] Applying Constraint#4 [CALL]
PEASE 1: Single-value logic for Birds and Swede under RIGET constraint.
PRASE 2: Handling relation Birds RIGHT Swede
Birds is immediately RIGHT of Swede
Removing Birds from Housedl because 3irds can't be in the leftmost house if it's 's to the RIGHT of Swede
Removing Swede Hlouse can't in the rightmost house it's s the LEFT Birds
[SEP]
Nationality category changed from 2 possibilities arit Swede passibilities Brit
Houset1 Pet category changed from possibilities Birds Dogs Fish possibilities Dogs Fish [
4 RETURN]
[SRP] [CALL] ==m_=m Possible Assignments After Propagation
House#1
Color category have 2 poasibllities Blue Red
Naticnality category have 2 possibilities German Swede Pet category have possibilities Dogs Fish
Houset2
Color category have possibilition 3lue Green Red Naticnality category
3 possibilities Brit
Swede
category have posaibllities Birds Dogs Fish House#3
Color category have possibilities Blue Green Red Naticnality category is Brit
Pet category have possibilities Dogs Fish Unsatisfied constraints are Constraint Constraint#2 Constrain:43 Constraintt4 [RETURN]
=> Puzzle not selved yet sesses Branch ==s_==
Branching on Boussetl Color categery with 2 possibilities Blue Red Trying possibility Blue in Houset1 Color category
[CALL] s*m_um Possible Assignments
#ouset1
Color category Blue
Naticnality category have 2 possibilities German Swede Pet category have possibilities Dogs Fish House#2
Color category have 3 possibilities Blue Green Red National lit category have 3 bitiiiiliiiss Brit German Swede Pet category have possibilities Birds Dogs Fish Houset3
Color category have possibilities Blue Green Red Naticnality category is Brit
category have possibilities Dogs Fish Unsatisfied constraints Puzzle not solved yet
Constraintt1 Constraint Constraintd3 Constraint
===_== Propagation Applying Constraint#1 [CALL]
FRASE 1: Single-value logic for Green and Birds under RIGHT constraint
Removing Blue from Hlouse22 Color category because Blue is pinned in another house
Removing Blue from House#3 Color category because Blue is pinned in another house Forcing Birds in House#2 2et category because it can only appear here PEASE 2: Handling relation Green RIGHT Birds
Green is immediately RIGHT of Birda Since Birds is pinned Jouse/2 zemoving
House|2 because
<>
Placing Green in House#3 because Birds is pinned to House#2
[SRP] Houset2 Color category changed from possibilities Blus Green Red to possibilities Red Houset3 Color category changed from possibilities Rlue Green Red to 1 possibilities Green #ouset2 Pet categozy changed from. 3 possibilities Birds Dogs Fish to pcasibilities Birds (RETURN) Remove Constraint:1 because it is aatisfied Applying Constraint#2 [CALL]
PIASE 1: single-value logic for Brit and German under RIGHT constzaint Removing Brit from Houser2 Nationality category because Brit is pinned in another house PEASE Handling relation Brit RIGHT German Brit is immediately RIGHT German must be exactly one
the LEFT removing from
48

---

PENCIL: Long Thoughts with Short Memory
Placing German Fousef2 because is pinned House#3
[SEP] Houset1 Nationality category changed from 2 possibilities German Swede to possibilities
Swede
#ouset2 Nationality categozy changed from 3 possibilities Brit German Swede to 1 possibilities
4 Sernan [RETURN]
Remove Constraint because it is satisfied
Applying Constraint#3 [CALL]
PEASE 1: single-value logic for Dega and Red under SAME constraint PEASE Handling relation Dogs SAME Red
Dogs be in the SAME house Red
Since is pinned Hooset2 removing Dogs from Housee1
Since Red is pinned to Hoaset2 removing Doga from House#3 House42 can't hold Doge since it can't hold Red
[SRP] Houset2 Color category changed from possibilities Red to J possibilities empty
House#1 Pet category changed from 2 possibilities Dogs Fish to 1 possibilities Fish
[oosse33 Pet category changed from. 2 possibilities Dogs Fish to 1 possibilities Fish [RETURN]
[SEP] No Solution [RETURN]
Trying possibility Red in House#1 Color category
[CALT]] ==s_=m Possible Assi insentt
Rouse#1
Color category Red
Naticnality category have possibilities
Pet category have possibilities Dogs Fish
House#2
Color category have possibilities Blue Green Red Naticnality category have 3 possibilities Brit German Swede Fet category have posaibilities Birds Dogs Fish House#3
Color category have 3 possibilities Blue Green Red Naticnality category is Brit
Pet. category have possibilsties Fish Unsatisfied constraints Puzzle not salved yet
Constraint41 Constraint+2 Constrainz43 Constraint
Propagation Applying Constraint#1 [CALL]
FRASE 1: single-value logic for Green and Birds under RIGUT constzaint
Removing Red from Eouse#2 Color category because Red is pinned in another house Removing Red from Rouse#3 Color category because Red is pinned in another house Forcing Rirds in Houset2 Pet category because it can only appear here PEASE 2: Handling relation Green RIGHT Birds
Green is immediately RIGHT of Birds Since Birds is pinned House#2 removing Green from House#2 because Green be right of House
Placing Green Houset3 because Birds pinned Bluuset2
category changed Houset3 Color category changed from possibilities Blue Green Red to 1 possibilities Green Houset2 Pet category changed from 3 possibilities Birds Dogs Fish to possibilities Birds [RETURN] Remove Constraint#] because it is satisfied Applying Constraint [CALL]
[SRP] Houset2
possibilities
Green Red possibilities Blue
PIASS 1: Single-value logic for Brit and German under RIGHT constraint.
Removing Brit from House#2 Nationality category because Brit is pinned in another house PEASE 2: Handling relation Brit RIGHT German Brit is immadiately RTGHT of German
German be exactly one house the LEFT removing Houset1
Flacing German In House#2 because Brit is pinned flouset3
[SEP] Houset1 Nationality category changed from 2 possibilities German Swede possibilities Swede
Houset2 Nationality category changed from possibilities Brit German Swede to poss icssibilities
4 Gernan [RFTURN]
Remove Constraint42 because it is aatisfied Applying Constraint [CALL]
PEASE 1: Single-value logic for Dogs and Red under SAME constraint
PIASE 2: Mandling relation Dogs SAME Red
Dogs must be in the SAME house Red
Flacing Dogs House#1 since Red is in this house
since Red is pinned Houset1 removing Dogs from Houset3
[SBP] Houset1 Pet category changed from possibilities Dogs Fish possibilities Dogs
49

---

PENCIL: Long Thoughts with Short Memory
House#3 cateqory changed from possibilities Dogs Fish to possibilities Fish [RETURN]
Remove Constraint because it satisfied Applying Constraint#4 [CALL]
PRASE 1: Single-value logic for Pirds and Swede under RIGET constraint
PEASE 2: Handling relation Birds RIGHT Swede
Birds is immediately RTSHT of Swede
[SEP] No changes Irom this constraint [RETURN]
Remove Constraint+4 because it is satistied
[SEP] [CALL] ==s==s Possible Assignments After Propagation
Ilouset1
Color category Red
Naticnality category is Swede
Pet category Dogs
House#2
Color cateqory is Blue
Naticnality category is German
Pet category is Birds House#3
Color category is Green Naticnality category is Brit category Fish Unsatisfied constraints
[RETURN]
Puzzle is solved
[SEP] Solution House#1 Color category is Red Naticnality category is Swede
Fet category is Dogs Houset2
Color category is Blue
Naticnality category is German
Pet. category is Birds House#3
Color category
Naticnality category is Brit Pet category Fish (RETURX)
[SEP] Solution Ilousef1
Color category is Red Naticnality category is Swede
Pet. category is Bogs
Houset2
Color category is Blue
Naticnality category is Gernan
Pet category Birds Hoouset3
Color category
Naticnality category is Brit
Pet category is Fish [RETURN]
=> House#3 owns the Fish
>> the Brit owns the Fish < <
M.2. PENCIL
Prompt:
<|startoftext| > Constrain:d1 the Green house is immediately to the right of the who keeps Birds Constraint42 the Brit is inmediately the right of the German Constraint#3 the who keeps Dogs is the house the Red house Constraint
keeps Birds is immediately
right of Swede </endofpremptl>
Response:
Solution Housed1
Color category Red Naticnality category is Swede
Pet category Dogs Houset2
50

---

PENCIL: Long Thoughts with Short Memory
Color cateqory Blue Nationality category is German Pet category is Birds House#3
Color category is Green Nationalite ity category is Brit Pet category is Fish Housed3 owns the Fish
the Brit the Fish <
endoftext
M.3. Internal Thinking Process of PENCIL
Model Generation (1)
[CALT]] Possible Assi gnments
Houset1
Color category have 3 poasibilities Blue Green Red
Naticnality category have 3 possibilities Brit German Swede
Pet category have possibilities Birds Dogs Fish Houset2
Color category have poasibilities Blue Green Red Natienality category have 3 possibilities Brit German Swede Pet category have possibílities Birds Dogs House#3
Color category have possibilities Blue Green Red Naticnality category have 3 possibilities Brit German Swede Pet category have possibilities Birds Dogs Fish Unsatisfied constraints are Constraintt) constraint Constraintd3 Constraintta
=> Puzzle not selved yet
=-*__- Propagation Applying Constraint/1 [CALL]
PEASE Single-value logic for Fish and Red under RIGHE constraint
PEASE Handling relation Fish RIGHT Red
Fish immediately RIGHT
Removing Fish from House#1 because Fish can't Removing Red from House#3 can't be in the rightmost house if it's to the LEFT of Fish
the leftmoat house if it's to the RIGHT Red
[SEP] Houset3 Color category changed from 3 possibilities Blue Green Red to 2 possibilities Blue () Green
Mousett Pet category changed from 3 possibilities Birds Dogs Fish to 2 pessibilities Birds Dogs
4 RETURN]
Reduction Rule (1)
[CALL]
Possible Assignments
Hoosee1
Color category have possibilities Blue Green Red Naticnality category have 3 possibilities Brit German Swede category have possibil Birds Dogs Fish House42
Color category have poasibilities Blue Green Red Naticnality category have 3 possibilities Brit German Swede Pet category have possibilities Birds Dogs Fish Mousett
Color category have 3 possibi lities Blue Green Red Naticnality category have 3 possibilities Brit German Swede Pet category have possibilities Birds Dogs Fish Unsatisfied constraints Puzzle selved yet Propagation
Constraintt] Constraint+2 Constraint43 Constraint*9
Applying Constraint#1 Houset3 Color category changed from possibilities Blue Green Red to 2
4 possibilities Blue Green
#ouset1 Pet category changed from 3 possibi ittes Birds Dogs Fish to possibi 1 ittes Birds Dogs
Model Generation (2)
51

---

PENCIL: Long Thoughts with Short Memory
[CALL] Possible Assiqnments
Houset1
Color category have 3 possibilities Blue Green Red
Naticnality category have 3 possibilities Brit German Swede
Pet. category have possibilities Birds Dogs Pish
Rouset2
Color category have 3 poasibilities Blue Green Red Nationality category have 3 possibillties Brit German Swede Pet category have possibilities Birds Dogs Fish Ilouset3
Red Naticnality category have 3 possibilities Brit German Swede Pet category have possibilities Birds Dogs Fish Unsatisfied constraints are Constraint41 Constraint#2 Constraint#3 Constraint:4
Color category
possibilities
=> Puzzle not solved yet
------ Propagation
Applying Constraint#l Houset3 Color category changed from possibilities Blue Green Red to 2
<) possibilities Blue Green
Rouset1 Pet category changed from possibi ieiiibiities Birds Fish possibilities Birds Applying Constraint#2 [CAL]]
PEASE single-value logic
and Red under constraint
PEASE Hladllin relation Green is immediately LEFT Red
LEFT Red
Removing Green from House#3 because Green can't be in the rightmost house if it's to the LEFT of Red Removing Red from Rouser1 because Red can't 't be in the leftmast house if it's to the RIGHT of Green [SEP] Houset1 Color categozy changed from 3 possibilities Blue Green Red to 2 possibilities Blue Green
#ouse#3 Color category changed from 2 possibilities Blue Green to possibilities Blue [RETURN]
Reduction Rule (2)
[CALL] Possible hasignments
House#1
Color category have possibilities Blue Green Red Naticnality category have 3 possibilities Brit German Swede Pet category have possibilities Birds Dogs Fish
Houset2
Color category have 3 possibilities Blue Green Red Naticnality cateqory have 3 possibilities Brit German Swede Pet category have possibilities Birds Dogs Fish House#3
Color category have possibilities Blue Green Red Naticnality category
3 possibilities Arit Pet category have possibilities Birds Dogs Unsatisfied constraints are Constraiat41 Constraint42 Constrainz43 Constraint44
Swede
Puzzle not salved yet
====== Propagation ======
Applying Constraint Nooseet Coler category changed from 3 possibilities Blue Green Red to 2
4 possibilities Blue Green
#ouset1 Pet category changed from. 3 possibilities Birds Dogs Fish possisilities Birds Dogs Applying Constraint#2 Houset1 Color category changed from posslbilities Blue Green Red to 2 9 possibilities Blue Green
Kouse#3 Color category changed from possibilities Blue Green possibilities Blue
Model Generation (3)
[CALL] s=s==s Possible Assignments
Houset1
Color category have 3 possibilities Blue Green Red Natienality category have 3 possibilities Brit German Swede Pet category have possibilities Birds Dogs Fish
Rouset2
Color category have poasibilities Blue Naticnality category have 3 possibilities Brit German Swede Pet category have possibilities Birds Dogs Fish
Red
Houset3
Color category have possibe bi lities Blue Green Red
52

---

PENCIL: Long Thoughts with Short Memory
Naticnality cateqory have 3 possibilities Brit German Swede Pet category have possibilities Birds Dogs Fish Unsatisfied constraints are Constraint41 Constraint#2 Constraint#3 Constraint*4
=> Puzzle not solved yet
------ Propagation Applying Constraint#l #ouset3 Color category changed From 3 possibl 1ities Blue Breen Red to 2
9 poasibilities Blue Green
Houset1 Pet category changed from. 3 possibilities Birds Fish pessibilities Birds Dogs Applying Constraint#2 Houset1 Color category changed from possibilities Blue Green Red to 2 + possibilities Blue
Hoouset Calor category changed from possibilities Applying Constraint43 [CALL]
to possibilities Blue
PEASE 1: single-value logic for Fish and Swede under RIGHT constraint
PEASE 2: Handling relation Fish RIGHT Swede
Fish is immediately RIGHT of Swede
Remaving Swede from 3luuse can't be in the rightmost house if it's to the LEFT of Fish
[SEP] #ouse#3 Nationality category changed from 3 possibilities Brit German Swede to 2 possibilities Brit German [RETURN]
Reduction Rule (3)
[CALL] Possible Assignments
House#1
Color category have 3 possibi lities Blue Green Red Naticnality category have 3 possibilities Brit German Swede Fet category have posaibilities Birds Dogs Fish
House#2
Color category have 3 possibilities Blue Green Red Naticnality category have 3 possibilities Brit German Sxede Pet. category have possibilities Birds Dogs Fish House#3
Red Naticnality category have 3 possibilities Brit German Swede Pet category have possibilities Birds Dogs Fish Unsatisfied constraints are Constraintt] Constraint:2 Constraint:3 Constrainttd
Color category have poasibilities
=> Puzzle not solved yet
--*___ Propagation Applying Constraint#1 Houset3 Color category changed from 3 possibilities Blue Green Red to 2
9 possibilities Blue Green
Houset1 Pet category changed from. 3 passibilities Birds Fish pessibilities Birds Dogs
Applying Constraint#2 Houset1 Color category changed from possibilities Blue Green Red to 2 possibilities Blue Green
Houset3 Color category changed from possibilities Green to possibil bitiiis Applying Constraint#5 Houset3 Nationality category changed possibil lities German Swede to possibilities Brit German
Model Generation (4)
[CALL]
Possible Assignments
Houset1
Color category have possibilities Blue Green Red
Naticnality category have 3 possibilities Brit German Swede category have possibilities Birds Dogs Fish
#ouset2
Color category have poasibilities Blue Green Red Naticnality category have 3 possibilities Brit German Swede Pet category have possibilities Birds Dogs Fish Moosee3
Color category have 3 possibilities Blue Green Red Naticnality category have 3 possibilities Brit German Swede Pet category have possibilities Birds Dogs Fish Unsatisfied constraints
1 constraint:2 Constraintd3 Constraint*a Puzzle solved yet
Propagation
Applying Constrainté1 Houset3 Color category changed from possibilities Blue Green Bed to 2
>) possibilities Blue Green
#ouset1 Pet category changed from 3 possibilities Birds Dogs Fish to possibil ittes Birds Dogs
53

---

PENCIL: Long Thoughts with Short Memory
Applying Constraint Houset1 Color category changed from possibilities Green to 4 possibilities Blue Green
House#3 Color category changed from 2 possibilities Blue Green to i possibilities Blue Applying Constraint#3 #ouset3 Nationality category changed from 3 possibilities Brit German Swede to
7 2 possibilities Brit German
Applying Constraint#d [CALL]]
PEASE 1: single-value logic for Brit and Birds under LEFT constraint
PEASE 2: Handling relation Brit LEFT Birds Brit is immediately LEFT of Birds
Removing Brit from Housee because Brit Removing Birds
the rightmost house if it to the leftmost house it's the RIGHT of
Birds
Housed1
3irds
() Brit
[SEP] House#3 Nationality category changed from 2 possibilities arit German to possibilities Gernan
House#1 Pet cateqory changed from 2 possibilities Birds Dogs to possibilities Dogs [RETURN]
Reduction Rule (4)
[CALL] Possible Assiqnments
Hoosee1
Color category have possibllities Blue Red
Natienality category have 3 possibilities Brit German Swede Pet category have possibilities Birds Dogs Fish Houset2
Color category have 3 poasibilities Blue Green Red Naticnality category have 3 possibilities Brit German Swede Pet category have possibilities Birds Dogs Fish House#3
Color category have possibilities Blue Green Red Naticnality category have 3 possibilities Brit German Sxede category have possibilities Birds Dogs Fish Unsatisfied constraints Puzzle not solved yet
4onstraiat41 Constraint42 Constraint43 Constraint44
Propagation Applying Constraint llouset3 Coler category changed from possibilities Blue Green Red to 2
() possibilities Blue Green
Houset1 Pet category changed from. 3 possibilities Birds Dogs Fish to 2 poaslbilities Birds Dogs Applying Constraint#2 Houset1 Color category changed from 3 possibilitie Blue Green Red to 2 9 possibilities Blue Green
Houset3 Color category changed frem possibilities Blue Green to possibilities Blue
Applying Constraint43 Houset3 Nationality category changed from possibilities Brit German Swede to
<> possibilities Brit German
Applying Constraint#d Houset3 Nationality category changed possibilities German
4 possibilities
Houset1 Pet category changed from. 2 possibilities Birds Dogs to possibilities Dogs
Model Generation (5)
[CALL]
Possible Assignments
Houset1
Color category have possibilities Blue Green Red Naticnality category have 3 possibilities Brit German Swede category have possibilities Birds Dogs Fish
#ouset2
Color category have poasibilities Blue Green Red Naticnality category have 3 possibilities Brit German Swede Pet category have possibilities Birds Dogs Fish Moosee3
Color category have 3 possibilities Blue Green Red Naticnality category have 3 possibilities Brit German Swede Pet category have possibilities Birds Dogs Fish Unsatisfied constraints
1 constraint:2 Constraintd3 Constraint*a Puzzle solved yet
Propagation
Applying Constrainté1 Houset3 Color category changed from possibilities Blue Green Bed to 2
>) possibilities Blue Green
#ouset1 Pet category changed from 3 possibilities Birds Dogs Fish to possibil ittes Birds Dogs
54

---

PENCIL: Long Thoughts with Short Memory
Applying Constraint Houset1 Color category changed from possibilities Green to 4 possibilities Blue Green
House#3 Color category changed from possibilities Blue Green to i possibilities Blue Applying Constraint#3 Houset3 Nationality category changed from possibilities Brit German Swede to 7 2 possibilities Brit German
Applying Constraint #ouset3 Nationality category changed from 2 possibil lisiess Brit German to
4. poasibilities German
Houset1 Pet category changed from. 2 possibilities Birds to possibilities Doga
[SEP] [CALL]
Possible Assignments After Propagation
[louset1
category
possibilities Green
Naticnality category have 3 possibilities Brit German Swede Pet category Dogs
House#2
Color cateqory have 3 possibilities Blue Green Red Naticnality category have 3 possibilities Brit German Swede Pet category have possibilities Birds Dogs Fish House#3
Color category is Blue
Nationality category is German
category have possibllities Birds Dogs Fish Unsatisfied constraints Constraint41 Constraint+2 Constraint:3 Constraint [RETURN]
Reduction Rule (5)
[CALL]
Possible hasignments After Propagation
Houset1
Color category have 2 possibilities Blue Green
Naticnality category have 3 possibilities Brit German Sxede Pet. category is Bogs
House42
Color category have poasibilities Blue Red Naticnality category have 3 possibilities Brit German Swede Pet category have possibilities Birds Dogs Fish Hooseet
Color category is Blue
Naticnality category is German
Pet category have possibilities Birds Dogs Pish Unsatisfied constraints are Constraintt] Constraint#2 Constraint#3 Constraint*4
Model Generation (6)
[CALL] Possible Assignments After Propaçation
Houset1
Color category have possibilities Blue Green
Naticnality category have 3 possibilitiee Brit German Swede Fet category is Dogs
Rouset2
Color category have 3 possibilities Blue Green Red Nationality category have 3 possibillties Brit German Swede Pet category have possibilities Birds Dogs Fish House#3
Color category Blue
Nationality category is
Pet category have possibilities Birds Dogs Fish Unsatisfied constraints are Constraintt] Constraint#2 Constraint#3 Constrainttà => Puzzle not solved yet
Branch
Branching on Houuse1 Color categery with 2 possibilities Blue Green Trying possibility Green in House#1 Color category
[CALL] s=m_== Possible Assignments
Rouset1
Color category
Naticnality category 3 possibilities Brit Swede
Pet category Bogs Houset2
Color category have possibi lities alue Green Red
55

---

PENCIL: Long Thoughts with Short Memory
Nationality cateqory have 3 possibilities Brit German
Pet category have possibilities Birds Dogs Fish
House#3
Color category is Blue
Nationality category is German
Pet. category have possibilities Birds Dogs Pish Constraint41 Constraint Constrainz43 Constraint
Unsatiafied constraints Puzzle not solved yes
Propagation Applying Constraint [CALL]
PEASE Single-value logic
Fish
RIGHE constraint
Removing Dogs from House#2 Pet category because Dogs pinned in another house Removing Doga from House#3 Pet category because Doga pinned in another house Removing Green from House#2 Color category because Sreen is pinned in ancther house Removing Blue from Rouset2 Color cateqory because Blue is pinned in another house PRASE 2: laadllin zelation Fish RIGIT Red Fish is immediately RIGHT of Red
Since Red is pinned to House*2 removing Fish from House#2 because Fish mast be right of Houset2 Placing Pish in Houset3 because Red is pinned to Houset2
[SEP] Houset2 Color category changed from postibilities Blue Green Red to possibilities Red Houset2 categozy changed from. possibilities Birds Dogs Fiah pcasibilities Birds [ooset3 category changed from. possibilities Birds Dogs Fish pcasibllities Fish (RETURN]
Reduction Rule (6)
[CALL] Possible Assignments After Propagation
House#1
Color category have possibi lities Blue Green
Nationality cateqory have 3 possibilities Brit German Swede category Dogs Ilouset2
Color category have possibilities Blue Green Red Natienality category have 3 possibilities Brit German Swede Pet. category have possibilit Birds Dogs Pish House#3
Color category is Blue
Naticnality cateqory is Gernar:
Pet category have possibilities Birds Dogs Fish Unsatisfied constraints Puzzle not salved yet Branch
Constrainti] Constrainti2 Constraintd3 Constraint
Branching on Houset1 Color category 2 poasibilities Blue Trying possibility Green Houset1 category [CALL)
Possible Assignments
Hloueetl
Color category is Green
Naticnality category have 3 possibilities Brit German Swede Pet. category is Bogs
House#2
Color category have 3 poasibilities Blue Green Red Naticnality category have 3 possibilities Brit German Sxede Pet category have possibilities Birds Dogs Fish Housett
Color category
Naticnality category is German
Pet category have possibilities Birds Dogs Fish Unsatisfied constraints are Constraintt] Constraint#2 Constraint#3 Constraint44 -> Puzzle not salved yet
Propagation
Applying Constraint#1 Houset2 Color category changed from possibilities Blue Green Bed to 1
4 possibilities Red
#ouset2 Pet cateqory changed from possibilities Birds Dogs Fish possibilities Birds
Rouse#3 Pet cateqory changed from possibilities Birds Dogs Fish possibilities Fish
Model Generation (7)
56

---

PENCIL: Long Thoughts with Short Memory
[CALL] Possible Assiqnments After Propaçation
Houset1
Color category have 2 possibilities Blue Green
Naticnality category have 3 possibilities Brit German Swede Pet. category is bogs
Rouset2
Color category have 3 possibilities Blue Green Red Nationality category have 3 possibillties Brit German Swede Pet category have possibilities Birds Dogs Fish Ilouset3
Color category Blue
Naticnality category is German
Pet category have possibilities Birds Dogs Fish Unsatisfied constraints are Constraint4] Constraint#2 Constraint#3 Constraint
=> Puzzle not solved yet
------ Branch
Branching on #ouse#1 Color categery with 2 possibilities Blue Green
Trying possibility Green in House#1 Color category
[CALL]] ==m_=m Possible Assignment
Rouse#1
Color category
Naticnality category
possibilities Brit Swede
Pet category Bogs
House#2
Color category have possibil litiess Blue Green Red Naticnality category have 3 possibilities Brit German Swede Fet category have possibilities Birds Dogs Fish Houset3
Color category is Blue
Naticnality category is German
Pet category have possibilsties Birds Fish Unsatisfied constraints Puzzle not salved yet
Constraint41 Constraint+2 Constrainz43 Constraint*:
Propagation
Applying Constraint#1 Houset2 Coler category changed from poasibilities Blue Green Red to 1
4 possibilities Red
House#2 Pet category changed from 3 possibilities Birds Dogs Fish to possibilities Birds #ouse43 Pet category changed from 3 possibilities Birds Dogs Fish to poasibilities Fish Remove Constraint:) because it is satisfied Applying #o [CALL]
PEASE 1: single-value logic for Green and Red under LEFT constraint
PEASE Handling relation Green LEFT Red Green is immediately LEFT of Red
[SEP] changes this constraint [RETURN]
Reduction Rule (7)
[CALT.] s=m=== Possible Assi Assi gnments After Propagation ====== Houset1
Color category have 2 poasibilities Blue Green
Naticnality category have 3 possibilities Brit German Swede Pet category Bogs
Houset2
possibi lities Green Red Naticnality category have 3 possibilities Brit German Swede Pet category have possibilities Birds Dogs Fish House#3
category
Color category is Blue
Naticnality category is German
Pet category have possibilities Birds Dogs Fish Unsatiafied constraints are Constraint41 Constraint#2 Constrainz43 Constraint44 Puzzle salved yat Branch
Branching on Boouset Color category with 2 possibilities Blue
Trying possibility Green in Houset1 Color category
[CALL] Possible Assignments
#ouset1
57

---

PENCIL: Long Thoughts with Short Memory
Color cateqory
Naticnality category have 3 possibilities Brit German Swede Pet category is Bogs House#2
Color category have 3 possibilities Blue Green Red Naticnality category have 3 possibil litiis Brit German Swede Pet category have possibilities Birds Dogs Fish House43
Color category Blue
Naticnality category is
category have possibilities Birds Dogs Pish Unsatisfied constraints are Constraint41 Constraint42 Constrainz43 Constraint44 Puzzle not solved ye:
====== Propagation ==se=s
Applying Constraint#1 Houset2 Color category changed from possibilities Blue Green Red to 1
4 possibilities Red
House#2 Pet category changed from possibilities Birds Dogs Fish to possibilities Birds #ouse#3 Pet category changed from possibilities Birds Dogs Fish to possibilities Fish Remove Constraint:) because it is satisfied
Applying Constraint No changes from this constraint
Model Generation (8)
[CALL] Possible Assignments After Propagation Ilouset1
Color category have 2 possibilities Blue Green
Naticnality category have 3 possibilities Brit German Swede Pet. category is Bogs
Rouse#2
Color category
poasibilities Blue Red
Naticnality category 3 possibilities Brit German Swede Pet category have possibilities Birds Dogs Fish Hooseet
Color category is Blue
Naticnality category is German
Fet category have posaibilities Birds Dogs Fish Unsatisfied constraints are Constraintt] Constraint#2 Constrain:#3 Constraint*:
=> Puzzle not solved
------ Branch
Branching on Rouset1 Color category with 2 possibilities Blue Green in House#l Color category
Trying possibility
[CA[T]]
Possible Assignments
Houset]
Color category is Green
Naticnality category have 3 possibilities Brit German Swede Pet category is Bogs
House42
Color category have 3 possibilitin lities Blue Green Red Naticnality category have 3 possibilities Brit German Swede Pet category have possibilities Birds Dogs Fish House#3
Color category Blue
Naticnality category is category have possibilities Birds Dogs Unsatiafied constraints are Constraint41 constraint42 Constrainz43 Constraint44 => Puzzle not solved yet
==s=== Propagation ===e_s
Applying Constraint/1 Hooese2 Color categozy changed from 3 poasibilities Blue Green Red to 1
4 possibilities Red
House42 Pet category changed from. possibilities Birds Dogs Fish to possisilities Birds House43 Pet category changed from. possibilities Birds Dogs Fish to possibilities Fish Remove Constraint:] because it is satisfied Applying Constraint#2 changes from this constraint
Remove Constraint42 because it satisfied Applying Constraint43 [CALL]
PHASE Single-value logic for Fish and Swede under RIGHT constraint
Remaving German from Houset: Nationalie oty category because German is pinned another house
58

---

PENCIL: Long Thoughts with Short Memory
Removing German from House#2 Nationality cateqory because German is pinned another house PEASE 2: Handling relation Fish RIGHT Swede
Fish is immediately RIGHT of Swede Swede must be exactly one house to the LEFT removing from House#1
Placing Swede in Houset2 because Fish is pinned to Rouset3
[SRP] Houset1 National ity category changed from 3 possibilitias bilities Rrit German Swade to 1 possibil iitess itees Brit
Rouset2 Nationality categozy changed from possibilities Brit Gezman Swede to possibilities Swede [RETURN]
Reduction Rule (8)
[CALL] s=m=== Possible Assiqnments After Propaçation ====== House#1
Color category have 2 possibilities Blue Green
Naticnality category have 3 possibilities Brit German Swede
Pet category is Dogs
Houset2
Color category have possibilities Blue Green Red Naticnality category 3 possibilities Brit German Swede category have possibilities Birds Dogs Pish
House#3
Color category Blue
Naticnality category is German
Fet category have posaibilities Birds Dogs Fish Unsatisfied constraints are Constraint Constraint Constraintd3 Constraint
Puzzle not solved
sesse= Branch ======
Branching on Bouset1 Color categery with 2 possibilities Blue Green
Trying possibility Grean in House#1 Color category
[CALL]
Possible Assignments
Houset1
Color category Green
Naticnality category have 3 possibilities Brit German Swede Pet: category is Bogs
House#2
Color category have 3 poasibilities Blue Green Red Naticnality cateqory have 3 possibilities Brit German Swede Pet category have possibilities Birds Dogs Fish Houset3
Color category Blue
Naticnality category is German
category have possibilsties Birds Dogs Unsatisfied constraints are Constraint Constraint Constraintd3 Constraint:4
Puzzle not solved ye:
Propagation Applying Constraint#1 Houset2 Color category changed from possibilities Blue Green Red to 1
4 possibilities Red
Houset2 Pet category changed from 3 possibilities Birds Dogs Fish to possibilities Birds Houset3 Pet category changed from. possibilities Birds Dogs Fish to possibilities Fish Remove Constraintt1 because it is satistied Applying Constraint#2 changes from this constraint
Remove Constraint42 because it satisfied
Applying Constraint llouse11 Nationality category changed possibilities Brit Swede possibilities Brit
Houset2 Nationality category changed from possibilities Brit German Swede to possibilities Swede
Model Generation (9)
[CALL] ==.__= Possible Assignments After Propagation ==ssss
Houset1
Color category have bossibilities Blue Green
Naticnality category 3 possibilities Brit Swede
category Dogs
Houset2
Color category have possibilities Blue Green Red
Nationality ity category have 3 possibilit.f Brit German Swede
59

---

PENCIL: Long Thoughts with Short Memory
category have possibilities Birds Dogs House43
Color category is Blue
Naticnality category is Gernan
Pet. category have possibilsties Birds Dogs Pish
Unsatisfied constraints are Constrainti) constraint::2 Constrainta3 Constraint:a
Puzzle not solved
-*._._ Branch
Branching on Rouse#1 Color categery with 2 possibilities Blue Green Hlouset1 Color category Pessible Assignments
Trying possibility
[CALL]
House#1
Color category Green
Naticnality cateqory have 3 possibilities Brit German Swede Pet category is Bogs
Ilouse22
Color category have 3 possibilities Blue Green Red Naticnality category have 3 possibilities Brit German Swede Pet. category have possibilities Birds Dogs Pish Rouse#3
Color category Blue
Naticnality categozy is German
Pet category have possibilities Birds Dogs Fish Unsatisfied constraints are Constraint41 Constraint42 Constrainz43 Constraint44
-> Puzzle not selved yet
==*_с- Propagation ==s__=
Applying Constraint#i Houset2 Color categozy changed from poaalbilities Blue Green Red to 1
+ possibilities Red
House#2 Pet category changed from 3 possibilities Birds Dogs Fish to possibilities Birds Ioouset3 Pet category changed from possibilities Birds Dogs Fish to pessibilities Pish Remove Constraint:] because it is satisfied
Applying Constraint#2 changes from this constraint Constraint4? because
satisfied
Applying Constraint#3 Houset1 Nationality category changed from possibilities German Swede to possibilities Brit
2losset2 Nationality categozy changed from possibilities Brit German Swede to possibllities Swede Remove Constraint43 because it is satisfied Applying Constraint#4 [CALL]
PRASE 1: Single-value logic for Brit and Birds under LEPT constraint
PEASE 2: Handling relation Brit LEFT Birds Brit is immediately LEFT of Birds
[SEP] No changes from this constraint [RETORN]
Reduction Rule (9)
[CALL] Possible Assignments After Propagation
House#1
Color category have 2 possibilities lities Blue Green
Naticnality category have 3 possibilities Brit German Swede Pet category is Dogs
Kouse#2
Color category have possibilities Blue Green Red Naticnality category
3 possibilities Brit Swede category have possibilities Birds Dogs Pish House43
Color category is Blue
Naticnality category is German
Pet category have possibilities Birds Dogs Fish Unsatisfied constraints are Constraint:] constraint Constraint Constraint
Puzzle not solved
==m___ Branch ==m_==
Branching Rouset1 Color category with 2 possibilities Blue Sreen
Trying possibility
Houset1 Color category
[CALL] Possible Aasignments
Houset1
Color category Green
Naticnality ity category have 3 bossibilitis Brit German Swede
60

---

PENCIL: Long Thoughts with Short Memory
category Bogs
Houset2
Color category have 3 possibilities Blue Green Red
Naticnality category have 3 possibilities Brit German Swede
Pet. category have possibilities Birds Dogs Pish Rouset3
Color category is Blue
Nationality category is German
Pet category have possibilities Birds Dogs Fish Unsatisfied constraints Puzzle not selved yet
Constraiat Constraint Constraint:3 Constraint
Propagation Applying Constraint41 Houset2 Coler categozy changed from poasibilities Blue Green Red to 1
4 possibilities Red
Houset2 Pet category changed from 3 possibilities Birds Dogs Fish to possibilities Birds Ioouse33 Pet category changed from. 3 possibilities Birds Dogs Fish to pessibilities Fish Remove Constraint+1 because it is satisfied
Applying Constraint#2 No changes from this constraint
Remove Constraint because it satisfied
Applying Constraint#3 Houset1 Nationality category changed from possibilitios Brit German Swede to possibilities Brit
Houset2 Nationality categozy changed
possibilities Brit German Swede pessibllities Svede
Remove Constraint43 because it satisfied
Applying Constraintéd changes from this constraint
Model Generation (10)
[CALL]] Possible Assi Assignnan gnments After Propagation #ouse#1
Color category
poasibilities Blue Green
Naticnality category have 3 possibilities Brit Swede
Pet category Bogs
Hoosee2
Color category have 3 possibil litiess Blue Green Red Naticnality category have 3 possibilities Brit German Swede Fet category have possibilities Birds Dogs Fish Houset3
Color category is Blue
Naticnality category is German
Pet. category have possibilsties Birds Fish Unsatisfied constraints Puzzle not
Constraint41 Constraint+2 Constrainz43 Constraint yet
Branch
Branching on Housetl Color category with 2 possibilities Blue Green Trying possibility Green in Nouset] Color category [CALL] s=s==s Possible Assignments
Houset1
Color category is Green
Naticnality category have 3 possibilities Brit German Swede Pet category is Dogs
Kouse#2
Color category have possibilities Blue Green Red Naticnality category
3 possibilities Brit Swede category have possibilities Birds Dogs House43
Color category is Blue
Naticnality category is German
Pet category have possibilities Birds Dogs Fish Unsatisfied constraints are Constraint:t constraint Constrainti3 Constrainttà
Puzzle not solved
==m_== Propagation ===_==
Applying Constraint#1 Houset2 Color category changed from possibilities Blue Green Red to possibilities Red
Houset2 category changed from. passibilities Birds Dogs Fish peasibilities Birds House#3 Pet category changed from. possibilities Birds Dogs Fish possibilities Fish Remove Constraintt] because it satisfied
Applying Constraine #2 No changes from this constraint.
61

---

PENCIL: Long Thoughts with Short Memory
Remove Constraint+2 because it satisfied
Applying Constraint43 Houset1 Nationality categozy changed from possibilities Brit German Swede to
? possibilities Brit
House42 Nationality categozy changed from 3 possibilities Brit German Swede to 1 possibilities Swede Possible Assignments After Propagation
Remove Constraintt3 because it is satisfied
Applying Constraint#d No changes from this constraint
Remove Constraintt4 because it is aatisfied
[SEP] [CALL]
House#1
Color category
Naticnality category is Brit
Pet category Dogs
House42
Color cateqory is Red Naticnality cateqory is Swede Fet category is Birds House#3
Color category is Blue Naticnality category is German Pet category is Fish Unsatiafied constraints [RETURN]
Reduction Rule (10)
[CALL] Possible Aasignments After Propaçation
Houset1
Color category have 2 possibilities Blue Green Naticnality category have 3 possibilities Brit German Swede Pet. category is Bogs
Rouset2
Color category have poasibilitiea Blue Red Naticnality category
3 possibilities Brit German Swede Pet category have possibilities Birds Dogs Hooset3
Color category is Blue
Naticnality category is Gernan
Fet category have possibilities Birds Dogs Fish Unsatisfied constraints are Constraint4] Constraint#2 Constraint#3 Constraint4a => Puzzle not solved yez
----_- Branch
Branching on Rouse#1 Color category with 2 poasibilities Blue Green Trying possibility Green House#1 Color category
[CM.L.]
Passible Assignments After Propagation
#ouset1
Color category is Green
Naticnality category is Brit Pet category is Bogs Mouset2
Color category is Red Naticnality category is Swede Pet category is Birds Rouse#3
Color category is Blue Naticnality category is Pet category Fish Unsatiafied constraints are
Model Generation (11)
[CALL] ==.__= Possible Assignments After Propagation =asees
Houset1
Color category have possibilities lities Blue Green
Naticnality category 3 possibilities Brit Swede
category Dogs
Houset2
Color category have possibilities Blue Green Red Nationality ity category have 3 possibilitsf Brit German Swede
62

---

PENCIL: Long Thoughts with Short Memory
category have possibilsties Dogs Houset3
Color category is Blue
Naticnality category is Gernan
Pet. category have possibilsties Birds Dogs Pish
Unsatisfied constraints are Constraint:) Constraint:: Constrainta3 Constraint:4
Puzzle not solved
-*..._ Branch
Branching Rouse#1 Color category with 2 possibilities Blue Green Hlouset1 Color category
Trying possibility
[CALL]
Pessible Assignments After Propaçation
House#1
Color category Green
Naticnality cateqory is Brit
Pet category is Bogs Ilouse22
Color category is Red Naticnality category is Swede Pet category is Birds Rouse#3
Color category Blue Naticnality categozy is German
Pet category Fish Unsatisfied constraints are
-> Puzzle is solved
[SEP] Solution House#1 color category is Green Naticnality cateqory is Brit
Pet category is Dogs Hoosse22
Color category is Red
Naticnality category is Swede category Birds House#3
Color category is Blue
Naticnality category is German
Bet category is Fish [RETURN)
Reduction Rule (11)
[CALL] Possible Assignments After Propaçation
#ouset1
Color category have possibilities Blue Green
Naticnality category have 3 possibilities Brit German Swede Pet category is Dogs
House#2
Color category have 3 possibilities Blue Green Red Naticnality category have 3 possibil lities Rrit German Swede Pet category have possibilities Birds Dogs Fish Houset3
Color category Blue
Naticnality category is German
category have possibilities Birds Dogs Unsatisfied
Constraint:) Constraint:? Constraintd3 Constraint Puzzle not solved ye:
==s_== Branch
Branching on Souset1 Color category with 2 possibilities Blue Green Trying possibility Green in Hooset1 Color category Solution Hooseet
Color category is Green Natienality category is Brit Pet category is Bogs Houset2
Color category is Red Naticnality category is Swede Pet category Birds
Houset3
63

---

PENCIL: Long Thoughts with Short Memory
Color cateqory Blue Naticnality category is German Pet category is Fish
Model Generation (12)
[CALL] Possible Assignments After Propaçation Ilouset1
Color category have 2 possibilit lities Blue Green
Naticnality category have 3 possibilities Brit German Swede Pet category is Bogs
Rouse#2
poasibllities Blue Red possibilities Brit German Swede Pet category have possibilities Birds Dogs Fish House#3
Color category
Naticnality category
Color category is Blue
Naticnality category is German
Fet category have posaibilities Birds Dogs Fish Unsatisfied constraints are Constraintt1 Constraint#2 Constrainz#3 Constraint*: => Puzzle not solved yet
------ Branch
Branching on Rouset1 Color category with 2 possibi lities Blue Sreen Trying possibility Green Housetl Color category
solution Housedl
Color category Green
Naticnality category is Brit Pet: category is Bogs House#2
Color category is Red Nationality cateqory is Swede Pet category is Birds Houset3
Color category is Blue
Naticnality category is German
category Pish
[SRP] Solution Housef1 Color category Green Naticnality category is Brit Pet category is Bogs Houset2
Color category is Red Naticnality category is Swede Pet category is Birds Rouse#3
Color category Blue
Naticnality category is Pet category Fish [RETURX]
Reduction Rule (12)
Solution House#1
Color category is Green Naticnalits itt category is Rrit Pet category is Dogs Houset2
Color category is Red
Naticnality category is Swede Pet category is Birds House#3
color category is Blue
Naticnality category is Gernan
category Fish
Model Generation (Final Response)
64

---

PENCIL: Long Thoughts with Short Memory
Solution Houset1
Color category is Green Naticnality category is Brit Pet category is Bogs Rouse#2
Color category is Red
Naticnality category is Swede
category Birds Houset3
Color cateqory Blue
Naticnality category is German
Pet category is Fish
=> House#3 owns the Fish
the German owns the Fish <lendoftext |>
65


Reviews:
[{"review_id": "GaBeGaO0Qr", "reviewer": "Reviewer_zuSb", "summary": "The paper proposes PENCIL, a next-token generation scheme that incorporates a reduction mechanism to control the length of the generated sequence. This mechanism removes redundant context, enabling more efficient generation while reducing memory usage. Experimentally, transformers trained on 3SAT, QBF, and Einstein’s puzzle demonstrate that PENCIL achieves higher accuracy compared to standard un-reduced Chain-of-Thought reasoning. Additionally, it converges faster during optimization when evaluated under the same FLOP constraints. Theoretically, PENCIL is capable of universal computation.", "questions": "", "limitations": "", "rating": 4, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "> **How PENCIL can be applied to standard LLMs**\n\nThe way we envision applying PENCIL to standard LLMs is to fine-tune LLMs on examples that include our special tokens, with the goal that model learns to reason in a structured manner that leverages memory efficiently and enables longer reasoning. Such datasets can be generated by domain experts (which is arduous but fairly common for LLM alignment), possibly using automatic anotation of common structures in structured mathematical or logical writting. One can also generate such datasets automatically by converting the running trace of *any algorithms* written in a pure functional programming language into a training set (see our response to Reviewer xx5n's Q2 for how this can be done for Einstein's puzzle); correspondingly, the maximal context length for PENCIL is proportional to the maximal stack memory (typically much smaller than the running time). We will discuss in detail how to generate such datasets for general algorithms in the next version of the paper.\n\nWhile we have not yet applied PENCIL to standard LLMs (this requires significant resources, both for data collection and training), we nonetheless have provided empirical evidence by showing even small language models can learn to generate structured CoT. We will more comprehensively discuss potential ways to apply PENCIL to real-world LLMs and leave this as future work.\n\n> **Q1: Effectiveness of Thought Reduction**\n\nIn principle, PENCIL can effectively reduce the reasoning trace for any problem whose space complexity is smaller than its time complexity, as we formally prove in Section 5. While the time and space gap is typically significant, there does exist cases where all computations are useful and should be preserved, as the reviewer suggested; it is true in this case the reduction is not necessarily useful. We appreciate the reviewer’s point and will include a discussion in the next version.\n\n\n> **Q2: Expressiveness of PENCIL in Relation to Finite-Precision Transformers**\n\nYes, Theorem 5.4 can be extended to cases where the base model is a transformer. Particularly, we can prove that PENCIL with a fixed finite-size decoder-only transformer can perform universal space-efficient computation, by simulating Turing machine running in $T$ steps and $S$ space with $\\mathcal O(T)$ generated tokens and maximal sequence length $\\mathcal O(S)$. This is a significant improvement over standard CoT, which requires context length to grow proportionally with $\\mathcal O(T)$ (i.e. results in [1]). An immediate implication is that PENCIL can solve all $\\mathrm{PSPACE}$ problems using polynomial context-length, whereas CoT can only solve problems in $\\mathrm{P}$.\n\nThe high-level idea of the proof is as follows: for any Turing machine $\\mathcal M$, we can construct a transformer (under some architectural specifications such as average-hard attention used in [1]) that can executed Algorithm 1 during its forward pass. Specifically, the transformer should be able to: (1) simulate the step-by-step execution of the Turing machine, (2) detect when to generate the $\\texttt{[SEP]}$ token indicating the start of summarization, and (3) summarize thoughts by computing a compressed state representation of the current token sequence. Although the construction is not straight-forward, we will include the proof in the paper once we can make updates.\n\n[1] W. Merrill and A. Sabharwal. \"The expresssive power of transformers with chain of thought.\" ICLR 2024.\n\n> **Minors**\n\n$t_i$ ($i>0$) always exists for Turing machines whose running time is at least twice of the maximal memory, otherwise we have $\\mathcal O(T(\\mathcal M,x)) = \\mathcal O(S(\\mathcal M, s, x))$ and reduction is unnecessary as space optimality is automatically achieved. We will also correct other typos the reviewer pointed out.", "claims_and_evidence": "The claims are generally supported.", "methods_and_evaluation_criteria": "The proposed method and the evaluation setup make sense.\n\nThe primary concern is the applicability of PENCIL to standard large language models. In the current setup, the model is trained to generate CoT reasoning that can be systematically reduced, stemming from the well-structured solutions in 3SAT, QBF, and Einstein’s puzzle. The training data explicitly follow this structured pattern, so that the model learn this pattern to be reduced. However, in practical settings where such structured CoT data are unavailable and the solution patterns are unknown, how can PENCIL be effectively applied?", "theoretical_claims": "Before Theorem 5.4, the paper constructs an efficient solution by defining $t^i$ as the smallest integer larger than $t_{i-1}$ such that the length of ... is no more than half of the sequence length of .... The proof for the existence of $t^i$ is missing.", "experimental_designs_or_analyses": "The experimental designs are sound.", "relation_to_broader_scientific_literature": "CoT is widely used for reasoning with LLMs, enabling them to solve problems by generating long reasoning chains. However, recent concerns have emerged regarding the efficiency of this approach, particularly given the minimum sequence length required to solve complex problems with finite-precision transformers.\n\nThis paper addresses this concern by proposing a reduction scheme that adaptively shortens the reasoning chain, reducing memory usage while preserving the model’s reasoning capabilities.", "essential_references_not_discussed": "To the reviewer's knowledge, all essential references are discussed.", "other_strengths_and_weaknesses": "### Strength:\n\n1. The problem addressed in the paper is important and relevant.\n2. The paper is well-written and clearly presented.", "other_comments_or_suggestions": "Line 365 (left): There is a duplicate \"since\".", "questions_for_authors": "Besides the concern regarding how PENCIL can be applied to standard LLMs, the reviewer has two additional questions:\n\n1. Effectiveness of Thought Reduction\n\nThe reviewer suggests that the authors include a discussion on the conditions under which PENCIL can effectively reduce the reasoning process to save memory. The examined problems in the paper exhibit a clear structured reasoning process, where intermediate steps can be meaningfully reduced without affecting the final solution. However, there exist other problem types where individual steps may not involve much computation, yet the reasoning process must retain or summarize all intermediate computational results.\n\nFor example, in longest increasing subsequence and subset sum problems, dynamic programming approaches must maintain all possible combinations' results (lengths or sums) and track these combinations to construct the final solution. In such cases, there may be limited potential for reduction, as the computation needs to be preserved throughout the process. The feasibility of reduction also depends on how solution patterns are designed. A discussion on this limitation would strengthen the paper.\n\n2. Expressiveness of PENCIL in Relation to Finite-Precision Transformers\n\nRecent work (e.g., Merrill et al. 2023, cited in the paper) has investigated the expressiveness of Chain-of-Thought (CoT) reasoning under finite-precision transformer constraints. Could the theoretical analysis be extended to demonstrate whether PENCIL expands the complexity class of problems that CoT can solve while maintaining the same rate of CoT length?\n\nThe reviewer is willing to increase the score if some of the concerns and questions raised in this review are adequately addressed.", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "Q3LLQQx95g", "reviewer": "Reviewer_xx5n", "summary": "The paper introduces PENCIL, an extension of the Chain-of-Thought (CoT) approach for language models. PENCIL addresses the \"write-only\" limitation of CoT, where intermediate reasoning steps accumulate indefinitely in the context, by incorporating a reduction mechanism. This mechanism uses special tokens ([CALL], [SEP], [RETURN]) to structure reasoning and discards unnecessary intermediate thoughts once a computation completes, reducing the maximal context length from exponential to polynomial for certain tasks. The main algorithmic idea is an iterative process alternating between CoT-style generation and a reduction rule (C [CALL] T [SEP] A [RETURN] ⇒ CA).\n\nThe paper evaluates PENCIL on SAT (Satisfiability), QBF (Quantified Boolean Formulas), and Einstein's puzzle, demonstrating significant context length reductions, high accuracy, and scalability to complex problems. Theoretically, PENCIL can simulate a Turing machine with O(T) tokens and O(S) maximal sequence length, where T is time and S is space.", "questions": "", "limitations": "", "rating": 4, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "> **Weakness 1: \"The data generation process requires knowing the reasoning structure. How reasoning problems without a clear structure (e.g., math problems) can beneﬁt from this approach remains a question.\"**\n\nIndeed, language models do not inherently reason in a way that allows for convenient space reduction. To extend PENCIL to general reasoning problems, one potential approach is to fine-tune LLMs on specialized datasets, either manually labeled or automatically generated, so that models learn to reason in a structured, memory-efficient manner (see our response to “How PENCIL can be applied to standard LLMs” for Reviewer zuSb).\n\nMoreover, we want to kindly point out that many math problems actually do exhibit PENCIL-like structures. For example, lemmas consist of statements which needs to be remembered, and proofs which do not. Similarly, many math problems involve intermediate computations with a complex derivation which can be forgotten, leaving only a concise final expression that needs to be retained. This natural separation in mathematical reasoning directly aligns with the PENCIL approach.\n\n> **Weakness 2: \"Models used in this study are too small compared to the current LLMs. This could disadvantage standard CoT approaches and limit the generalizability of the paper's conclusions to larger models.\"**\n\nWhile we have not yet conducted experiments on real-world LLMs (which we leave as future work), we believe using larger models with larger context window would further amplify the advantages of PENCIL. \n\nThis is because, in terms of theoretical expressiveness, CoT requires the maximal context length to grow with the running time of a problem, whereas PENCIL only requires it to grow with the needed memory; the gap between time and space is significant (e.g. exponential) for inherently hard reasoning problems. Although this gap is less pronounced for smaller models on tasks, it would become much more significant on larger-scale problems. \n\n> **Q1: \"How trace rate is calculated?\"**\n\nLet $x$ be the ground-truth reasoning trace, and $\\hat x$ be the reasoning trace generated by the model (as defined in Equation 8). The trace rate is defined as $$\\frac{1}{\\max\\{|x|, |\\hat x|\\}}\\sum_{i=1}^{\\min\\{|x|, |\\hat x|\\}} \\mathbf 1(x_i =\\hat x_i)$$, which quantifies the percentage of correctly predicted tokens. We choose this metric because it is both a direct measure of sequence similarity and tractable even for very long traces.\n\n> **Q2: \"How was the training data for Einstein's Puzzle generated? Additionally, how did you transform the algorithm's solutions into text? Did you use templates to verbalize the solutions?\"**\n\nWe implemented the Einstein’s Puzzle solver in Python, and as the code runs, it uses templates to verbalize the key steps. For example, when removing an entry from all possibilities, the code generates thoughts like:\n\n*Since green must be immediately to the right of Birds, we remove “green” from House \\#1 (it can’t be in the leftmost position if it’s supposed to be on the right of something else)\"*\n\nSpecial tokens are appended automatically. The general rule is as follows: when the code calls a new function, it appends the \"[CALL]\" token to the trace, and when the function finishes all computations and is ready to return, it appends \"[SEP] A [RETURN]\" where A is the returned value. (And if the returned value is from another function, we use the tail recursion in Equation 10 to further optimize the space.) \n\nIn fact, this method can be generalized to any algorithm written in a pure functional style; we will detail this further in the next version and open-source our code once published.\n\n\n> **Q3: \"What is the complexity of the problem in the training data? Are all test problems in-domain in terms of complexity, or are some of them OOD?\"**\n\nThe complexity of the problems in the training data matches that of the test problems (i.e., the same n). We plan to explore extensions to the OOD setting as future work.\n\n> **Q4: \"Could the model size and data generation process explain CoT's poor performance?\"**\n\nIt is possible that both the model size and the data generation format affect CoT’s performance. As shown in Figure 7, increasing the model size and context length improves CoT performance. And if we keep increasing the size, presumably CoT will eventually also solve $5\\times 5$ or more complicated puzzles, but PENCIL will be able to go even further. That is, regardless of the model size and context window, we have shown PENCIL can consistently solve larger-scale problems than the problems CoT can solve with that model size. We will add [1] in the next version.\n\n[1] Shah, Kulin, et al. “Causal language modeling can elicit search and reasoning capabilities on logic puzzles.” arXiv:2409.10502 (2024).\n\n> **Q5: \"Do you think this method can applied directly for fine-tuning LLMs?\"**\n\nYes, we believe that fine-tuning LLMs on structured datasets generated as described is a promising future direction.", "claims_and_evidence": "The paper makes three primary claims:\n\n1. **PENCIL reduces maximal context length from exponential to polynomial for certain tasks.**\n    - **Evidence**: Empirical results show dramatic reductions (e.g., SAT: 13,804 to 2,507 tokens; QBF: 151,661 to 649 tokens at n=10; Einstein’s puzzle: 151,192 to 3,335 tokens for 5x5). Figure 4 provide clear comparisons with standard CoT.\n2. **PENCIL achieves high accuracy on challenging reasoning tasks.**\n    - **Evidence**: Table 1 shows 100% accuracy and trace rate for SAT and QBF up to n=10, outperforming baseline CoT. Table 2 reports 97% accuracy on the 5x5 Einstein’s puzzle versus 25% for CoT.\n3. **PENCIL simulates a Turing machine with optimal time and space complexity.**\n    - **Evidence**: Section 5 shows theoretical justifications that PENCIL can simulate a Turing machine with O(T) tokens and O(S) maximal sequence length.\n\nThe results and evidence are strong, with empirical data and theoretical arguments aligning with the claims.", "methods_and_evaluation_criteria": "The methods and evaluation criteria are well-suited to the problem:\n\n- **Methods**: PENCIL combines a next-token predictor (transformer) with a reduction rule, applied iteratively. The rule’s design, inspired by function calls, is well-motivated and effectively addresses context overflow in CoT.\n- **Evaluation Criteria**: Tasks (SAT, QBF, Einstein’s puzzle) are compositional problems and computationally intensive, making them suitable for testing context efficiency and scalability.\n\nThe choice of benchmarks and metrics are appropriate for the problem.", "theoretical_claims": "I reviewed the theoretical results in Section 5 and Appendix B, and they appear valid to me. However, I'm not an expert in computational theory, so my judgment might be incorrect.", "experimental_designs_or_analyses": "Three tasks are used in the experiment: \n\n- **SAT and QBF**: Using a 6-layer 10M-parameter transformer, PENCIL achieves 100% accuracy up to n=10, with context length reductions validated by Figure 4.\n- **Einstein’s Puzzle**: An 8-layer 25M-parameter transformer achieves 97% accuracy on the 5x5 version.\n- The author also analyzes the convergence speed and conducts an ablation study on model size.\n\nThe designs are valid. My only concern is the model used in this study is too small compared to the current LLMs. This could disadvantage standard CoT approaches and limit the generalizability of the paper's conclusions to larger models.", "relation_to_broader_scientific_literature": "This work builds on the Chain-of-Thought (CoT) framework, addressing its scalability problem in context length. It might improve LLM performance in length generalization. It also connects to prior research on compressing model contexts.", "essential_references_not_discussed": "I can't notice any.", "other_strengths_and_weaknesses": "**Strengths:**\n\n- The proposed method is novel and well-motivated;\n- Empirical results are strong and comprehensive;\n- The paper is well-structured, with intuitive explanations and illustrative figures.\n\n**Weaknesses:**\n\n- The data generation process requires knowing the reasoning structure. How reasoning problems without a clear structure (e.g., math problems) can benefit from this approach remains a question.\n- Models used in this study are too small compared to the current LLMs. This could disadvantage standard CoT approaches and limit the generalizability of the paper's conclusions to larger models.", "other_comments_or_suggestions": "See Questions", "questions_for_authors": "- How trace rate is calculated?\n- How was the training data for Einstein's Puzzle generated? Additionally, how did you transform the algorithm's solutions into text? Did you use templates to verbalize the solutions?\n- What is the complexity of the problem in the training data? Are all test problems in-domain in terms of complexity, or are some of them OOD?\n- Could the model size and data generation process explain CoT's poor performance? Shah et al. (2024) trained transformers on Einstein puzzles with carefully constructed CoT and demonstrated that the model can achieve a high solve rate.\n- Do you think this method can applied directly for fine-tuning LLMs?\n\nShah, Kulin, et al. \"Causal language modeling can elicit search and reasoning capabilities on logic puzzles.\" arXiv preprint arXiv:2409.10502 (2024).", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "QYV8cXXT8Q", "reviewer": "Reviewer_TGaA", "summary": "The paper focused on the CoT reasoning, and proposed a PENCIL framework with reduction mechanism to exclude the unnecessary parts in the CoT. The authors conducted experiments on SAT, QBF and Einstein’s Puzzle to demonstrate the effectiveness of the framework. The authors also proved that the framework could simulate a Turing machine.\n## update after rebuttal\nThe responses have addressed most of my concerns. I raised my score to 3.", "questions": "", "limitations": "", "rating": 3, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "> **Weakness 1 & Q1: \"The three datasets used in the paper are all SAT-like ones, which lacks discussion on generalizability to more general reasoning. Besides, the reduced CoT growing from exponential to polynomial only works for the SAT-like tasks.\"**\n\nWe choose SAT and QBF because they are representative NP-complete and PSPACE-complete problems that no existing algorithm can solve efficiently, and thus they are ideal for stress-testing a model's capability in handling hard reasoning tasks. Moreover, PENCIL can be extended to arbitrary tasks provided the underlying algorithms can be written in a pure functional style. See our response to Reviewer xx5n's Q2 where we have briefly described the high-level idea. \n\nTo work on general reasoning tasks, one potential approach is to fine-tune existing LLMs on datasets with special tokens (generated either manually or automatically), enabling the model to learn to reason in a structured manner and think longer to solve more complicated tasks. See detailed discussion of how PENCIL can be applied to standard LLMs in our response to Reviewer zuSb. We will elaborate on this in the next version and leave further extensions as future work.\n\n> **Weakness 2 & Q2 & Concern 1 in Methods And Evaluation Criteria: \"How to ensure that the reduced parts are really no longer necessary especially for more general reasoning tasks.\"**\n\nFor our data generation process, the reduced parts are guaranteed to be unnecessary, because when generating the dataset, the special tokens are placed in the trace in strict accordance with how function calls are used in the (Python) codes that implement the algorithm for solving the task. \n\nFor general tasks whose structured reasoning trace is not explicitly included in the training set, there is no absolute guarantee that the model will always remove the unneeded parts. Nevertheless, this is a common limitation of all structured reasoning approaches (CoT, for example, does not always output useful intermediates steps that contribute to the final answer for general reasoning tasks, even models are trained to do so). Moreover, as we mentioned earlier, one potential way to mitigate this limitation is to fine-tune LLMs on appropriately formatted datasets, allowing them to learn to extract useful information from previous thoughts and use such a skill in general reasoning tasks.\n\n\n> **Weakness 2 & Concern 2 in Methods And Evaluation Criteria: \"The repeatedly LLM call may greatly increases computation complexity compared with generating CoT in one call.\"**\n\nIt is important to note that ***PENCIL does not repeatedly call LLMs, nor does it increase computation complexity; instead, it significantly improves the efficiency compared with one-pass CoT***. \n\nSpecifically, as has been discussed in the last paragraph of Section 2.2, for each application of reduction $$\\textbf{C} \\texttt{[CALL]} \\textbf{T} \\texttt{[SEP]} \\textbf{A} \\texttt{[RETURN]} \\Rightarrow\n\\textbf{C}\\textbf{A}$$ the same model is used to generate new tokens following the same sequence, rather than calling a new LLM and feeding the reduced sequence into it. The benefit of sticking to the same model and the sequence is that the KV cache of the context $\\textbf{C}$ can be preserved, and only the KV cache for \\textbf{A} should be recomputed, which incurs marginal cost, as reflected in Equation 8 that shows the minimal FLOPs (where KV cache usage is optimized) needed for PENCIL. Intuitively, PENCIL significantly saves computation because for each generated token the prefix length is significantly smaller than its CoT counterpart, while the total number of generated tokens is the same. Empirically, Figure 6 demonstrates that PENCIL is significantly more computationally efficient than direct CoT for each problem instance.\n\n> **Weakness 3: \"It would be better to simplify the introduction, such as adding some examples and explanations.\"**\n\nThanks for the suggestion. We will improve the clarity of introduction in the next revision.\n\n> **Weakness 4 & Q3: \"The context window of current LLMs could be extended to quite large, such as 1M. So I wonder whether it’s necessary to remove unnecessary parts from CoT.\"**\n\nIndeed, there are many existing efforts trying to extend the context window of LLMs, see our response to Reviewer yxYs's Q3 for a detailed discussion and how PENCIL fundamentally differs from them. Our contribution is orthogonal to their efforts contributions of aforementioned papers, i.e. one can always combine PENCIL with larger context window to potentially even achieve better performance. \n\nMoreover, it has been argued that enlarging the context window size can introduce issues such as diminished ability to retrieve relevant information from a very long context (see, e.g. [1]), whereas PENCIL is immune to such an issue by completely eliminating the unneeded thoughts.\n\n[1] Liu, Nelson F., et al. \"Lost in the middle: How language models use long contexts.\" ACL 2024.", "claims_and_evidence": "Overall the claims are supported by the experimental results and the theoretically analysis. But the claim, that the framework could reduce the exponential CoT growing to polynomial, seems to only work for the SAT-like reasoning task.", "methods_and_evaluation_criteria": "Some concerns are listed as follows.\n1. How to ensure that the reduced parts are really no longer necessary especially for more general reasoning tasks.\n2. The framework needs to repeatedly input the existing steps into the LLM to get the output. But initially the LLM could generate the CoT in one call, and the computation can be greatly reduced with KV cache.", "theoretical_claims": "There are one lemma and one theorem in the paper. I roughly go through the proof in the appendix, and have not found issues.", "experimental_designs_or_analyses": "The authors conduct experiments on three SAT-like tasks under different difficulties, and the experimental results demonstrated the effectiveness of the proposed framework. But the authors only conducted experiments on tasks similar to SAT, and lacked results on more general reasoning tasks to show its generalizability. Besides, the authors only compare the performances of the fine-tuned small LLMs. It would be better to provide results on larger LLMs and other CoT reasoning methods to further support the necessity of the reduction mechanism.", "relation_to_broader_scientific_literature": "The paper proposed a novel reduction mechanism to reduce the CoT lengths and improve reasoning efficiency and capability. The authors further theoretically proved that the proposed framework could simulate Turing machine.", "essential_references_not_discussed": "The related works are well cited.", "other_strengths_and_weaknesses": "In summary, the strengths of the paper are listed as follows.\n1. The paper proposed a novel reduction mechanism to reduce the CoT lengths and improve reasoning efficiency and capability.\n2. The authors conducted experiments to demonstrate the effectiveness of the framework, and theoretically proved that the proposed framework could simulate Turing machine.\n\nThe weaknesses are as follows.\n1. The three datasets used in the paper are all SAT-like ones, which lacks discussion on generalizability to more general reasoning. Besides, the reduced CoT growing from exponential to polynomial only works for the SAT-like tasks.\n2. It’s unclear how to determine whether the reduced parts are truly unnecessary. And the repeatedly LLM call may greatly increases computation complexity compared with generating CoT in one call.\n3. The proposed framework is easy to follow, but the authors introduced the method in a way quite hard to understand. It would be better to simplify the introduction, such as adding some examples and explanations.\n4. The context window of current LLMs could be extended to quite large, such as 1M. So I wonder whether it’s necessary to remove unnecessary parts from CoT.", "other_comments_or_suggestions": "None.", "questions_for_authors": "1. Can the proposed framework and findings work on more general reasoning tasks.\n2. How to determine whether the reduced parts are truly unnecessary.\n3. As the context window of LLMs could be quite large, is it necessary to remove unnecessary parts from the CoT.", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "5uUv8MUufU", "reviewer": "Reviewer_yxYs", "summary": "This paper introduces PENCIL, a novel method designed to overcome a fundamental limitation of standard chain‐of‐thought (CoT) reasoning in language models. The main idea is to interleave token generation with a reduction mechanism that “cleans up” intermediate reasoning steps—using specially defined tokens (e.g., [CALL], [SEP], [RETURN])—so that the context remains compact. This approach reduces the maximal context length from being proportional to the time complexity (often exponential) to being proportional to the actual space required (polynomial). The paper provides both theoretical results (showing that PENCIL can simulate Turing machines with optimal time and space efficiency) and extensive empirical evidence on challenging tasks such as SAT, QBF, and Einstein’s puzzle, where PENCIL achieves significantly higher accuracy and efficiency than standard CoT methods.\n\n## update after rebuttal\n\nI thank the authors for their detailed response. They provided helpful clarifications regarding the novelty and motivation for the proposed reduction rule, positioning it effectively against other context management techniques. The explanation of the training process and how the model learns to utilize the special tokens addressed my concerns about feasibility. Furthermore, the discussion on the theoretical claims regarding Turing machine simulation and the potential generality beyond the tested tasks was insightful. My assessment of the paper's contribution has been positively updated.", "questions": "", "limitations": "", "rating": 4, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "> **Weakness 1: \"Some proofs and technical details are deferred to the appendix; a more self-contained presentation could aid clarity.\"**\n\nThank you for the suggestion. We will incorporate key technical details from the Appendix into the main paper once we have an additional page in the final version.\n\n> **Weakness 2 & Q1: \"Could the authors provide further ablation studies to isolate the contribution of the reduction rule from other architectural modifications? How sensitive is the performance to the exact design of the special tokens and reduction triggers?\"**\n\nWe kindly note that in all our experiments, we have controlled for architectural and implementation choices by fixing the transformer architecture (including number of parameters, context window size, positional encoding, etc.) and the training algorithm (optimizer, batch size, learning rate, etc.). The only difference between CoT and PENCIL is in the data preprocessing (see the first three paragraphs of Section 4) and whether the reduction rule is applied during inference. This ensures the performance difference stems from the reduction rule.\n\nAs shown in Section 4, when all other factors are fixed, PENCIL consistently outperforms CoT, especially on larger problems. Moreover, the superior performance is insensitive to the specific choice of architectures. For example, in Figure 7, when we vary the model size (for both CoT and PENCIL) and context window size, our approach still achieves better performance. Empirically, the performance gap is also insensitive to the positional encoding (e.g. simple absolute PE works as well).\n\nWhile the precise design of the reduction rule might affect performance, we have not yet found an alternative rule that achieves better space and time efficiency than the one proposed (Equation 1). That being said, we conjecture if there does exist a better rule, PENCIL should achieve better performance and larger gap with CoT.\n\n\n> **Q2: \"While the paper shows impressive results on SAT, QBF, and Einstein’s puzzle, how does PENCIL perform on real-world tasks or benchmarks that involve natural language understanding beyond synthetic reasoning problems?\"**\n\nIt is indeed very promising to adapt PENCIL to general real-world tasks that involve natural language understanding. One potential way is to generate datasets with special tokens and fine-tune existing LLMs. See  However, this requires considerate engineering efforts, and thus we leave this as future work. Also see a discussion of \"how PENCIL can be applied to standard LLMs\" in our response to Reviewer zuSb.\n\n> **Weakness 3 & Q3: \"A more extensive discussion comparing with other memory efficient transformer techniques such as state space models could be beneﬁcial; Can the authors elaborate on how PENCIL compares with other recent memory compression or dynamic token pruning methods in terms of both efficiency and accuracy?\"**\n\nExisting memory-efficient architectures, such as those employing linear complexity attention (e.g., [1]), still require the context length to grow with the running time for problem solving, and thus do not address the fundamental limitation of CoT that PENCIL overcomes. While state-space models (e.g. [2]) avoid this issue by storing only the state, but this often comes at the cost of reduced expressiveness; for instance, SSMs have been shown (empirically and theoretical) to struggle with even simple tasks like copying [3]. \n\nOther memory compression and token pruning methods (e.g., [4–7]) typically combine base models with external heuristic algorithms (such as those relying on score functions and ranking). As a result, the models do not have the capability to reduce the space themselves whereas PENCIL explicit trains the model to do so. Moreover, these methods do not have theoretical benefits of solving arbitrary problems with optimal space complexity that PENCIL offers. \n\nPENCIL essentially differs from these lines of works by handling the limitation of the next-token generation (i.e. CoT) paradigm, and is orthogonal to the contributions of aforementioned papers. In other words, PENCIL is compatible with different base model choices and existing memory compression techniques. We will incorporate a more comprehensive discussion on related work in the next revision.\n\n[1] Rethinking attention with performers, ICLR 2021\n\n[2] Mamba: Linear-time sequence modeling with selective state spaces, 2023\n\n[3] Repeat After Me: Transformers are Better than State Space Models at Copying, ICML 2024\n\n[4] Efficient streaming language models with attention sinks, ICLR 2024\n\n[5] H2o: Heavy-hitter oracle for efficient generative inference of large language models, NeurIPS 2023\n\n[6] Model tells you what to discard: Adaptive kv cache compression for llms, ICLR 2024\n\n[7] Llmlingua: Compressing prompts for accelerated inference of large language models, EMNLP 2023", "claims_and_evidence": "The paper makes several claims:\n\n- That traditional CoT suffers from an unbounded accumulation of intermediate steps, leading to inefficient use of memory.\n- That a simple reduction rule can compress the reasoning trace, reducing memory requirements from exponential to polynomial in many cases.\n- That PENCIL, by interleaving generation and reduction, can simulate universal computation (i.e., a Turing machine) efficiently.\n- That empirical results on hard reasoning tasks (e.g., a 97% success rate on a 5×5 Einstein puzzle with a relatively small model) support these claims.\n\nThe authors support these claims with a combination of rigorous theoretical analysis (including formal definitions and proofs) and comprehensive experimental evaluations across multiple benchmarks. While some proofs are deferred to the appendix, the provided sketches and derivations appear convincing.", "methods_and_evaluation_criteria": "The proposed method is well motivated and builds on the core idea of managing memory via reduction—analogous to garbage collection or stack unwinding in classical computation. The evaluation is conducted on standard yet challenging benchmarks (SAT, QBF, Einstein’s puzzle) that are appropriate for testing reasoning and memory efficiency. Metrics such as accuracy, trace rate, maximal sequence length, and inference time are used to compare PENCIL with standard CoT, and the evaluation criteria are both rigorous and relevant to the claims made.", "theoretical_claims": "The paper includes several theoretical claims, notably that PENCIL (and its variant SCROLL) can simulate a Turing machine with time and space complexities that are optimal (i.e., time proportional to T(M, x) and space proportional to S(M, s, x)). I reviewed the sketch proofs in the main text and appendix (e.g., the formulation of the iterative next-token generator and the corresponding state function). While some details are deferred, the arguments are logically consistent and align with known theoretical frameworks. No major issues were found with the presented theoretical claims, although a more detailed step-by-step verification of the proofs would be beneficial in future revisions.", "experimental_designs_or_analyses": "The experiments are designed to test both the accuracy and efficiency of PENCIL relative to standard CoT approaches. The benchmarks chosen (SAT, QBF, and various sizes of Einstein’s puzzle) are well established in the literature. The analyses include both convergence speed and scalability (in terms of inference time and maximal context length). The experimental design appears sound, with clear comparisons across different problem sizes and model capacities. One suggestion might be to include additional ablations that isolate the effect of the reduction mechanism from other architectural choices.", "relation_to_broader_scientific_literature": "PENCIL is positioned at the intersection of chain-of-thought reasoning and memory-efficient computation. It builds upon previous works on CoT prompting (e.g., Wei et al., 2022) and extends the idea by introducing memory reduction techniques that are reminiscent of classical programming language strategies such as tail recursion and garbage collection. The paper effectively relates its contributions to prior work on external memory augmentation in LLMs as well as theoretical studies on the expressivity of transformers. It clearly advances the discussion by addressing the scalability limitations inherent in unbounded CoT approaches.", "essential_references_not_discussed": "While the paper cites a broad range of relevant literature, one potential gap is a deeper discussion of recent work on dynamic token pruning and memory compression in transformers (e.g., related to recent studies on efficient attention mechanisms). Including a comparison with methods that also aim to limit context length (even if via different techniques) could further strengthen the discussion.", "other_strengths_and_weaknesses": "### Strengths:\n\n1. The paper introduces a clear and intuitive mechanism for reducing memory footprint during reasoning.\n1. The theoretical analysis is rigorous and establishes strong claims regarding universal computation.\n1. Empirical results are compelling, demonstrating significant improvements on challenging tasks with modest model sizes.\n\n### Weaknesses:\n\n1. Some proofs and technical details are deferred to the appendix; a more self-contained presentation could aid clarity.\n2. Additional ablation studies might help to isolate the impact of the reduction mechanism versus other design choices.\n3. A more extensive discussion comparing with other memory-efficient transformer techniques such as state space models could be beneficial.", "other_comments_or_suggestions": "The paper is well written and the key ideas are communicated clearly. A few minor typographical errors and formatting inconsistencies were noted in the supplementary material. Future revisions might also consider a broader discussion on potential limitations or failure cases of the reduction mechanism, especially in tasks where intermediate reasoning steps are critical for later stages.", "questions_for_authors": "1. Could the authors provide further ablation studies to isolate the contribution of the reduction rule from other architectural modifications? How sensitive is the performance to the exact design of the special tokens and reduction triggers?\n\n2. While the paper shows impressive results on SAT, QBF, and Einstein’s puzzle, how does PENCIL perform on real-world tasks or benchmarks that involve natural language understanding beyond synthetic reasoning problems?\n\n3.  Can the authors elaborate on how PENCIL compares with other recent memory compression or dynamic token pruning methods in terms of both efficiency and accuracy?", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Meta-review: This paper introduces a novel approach that addresses CoT reasoning's context length limitations by incorporating a reduction mechanism that cleans up intermediate computations. The method uses special tokens to structure reasoning and discard unnecessary thoughts, reducing context length from exponential to polynomial for complex tasks. 

Its key strengths include: its strong theoretical foundation (ie, proving PENCIL can simulate Turing machines with optimal complexity), impressive empirical results (97% accuracy on Einstein's puzzle with a small 25M model), and clear potential to tackle problems intractable with standard CoT.

During rebuttal, the authors effectively addressed concerns about applicability to general reasoning and standard LLMs, computational efficiency, and necessity given growing context windows. While there are limitations in the current implementation's focus on structured reasoning tasks, the significant contribution to advancing language model reasoning capabilities merits acceptance.
Decision: Accept (poster)