The Predicate-Enumeration-Aggregation (PEA) framework (Wang et al., 2025) improves large-language-model performance on computational-reasoning tasks — Boolean satisfiability, the Game of 24, and planning — by having the LLM synthesize predicate/enumeration/aggregation programs whose execution decides a quantified formula; but it restricts variables to finite domains and predicates to efficient evaluability, so quantified statements over infinite domains, such as arithmetic over the integers, lie outside its scope (the paper's own illustrative number-theoretic example is not representable in its formalism). The primary source acknowledges this finite-domain restriction without addressing it. The open problem: define and realize a sound extension of PEA beyond finite domains — via richer (e.g., decidable arithmetic) logics or explicitly specified sound approximation of infinite-domain predicates — such that executing LLM-synthesized programs still yields trustworthy answers to the original quantified statements.

Background

Large language models (LLMs) are pretrained neural text models that can be prompted to solve reasoning tasks, and a prominent strategy for improving their reliability on problems with an exact answer is to have them write executable programs instead of reasoning in natural language. The Predicate-Enumeration-Aggregation (PEA) framework (Wang, Weng, Alhanahnah, Jha, and Reps, 2025) formalizes one such strategy. A computational-reasoning problem is written as a quantified first-order formula Q1x1,…,Qkxk.  P(x1,…,xk)Q_1 x_1, \ldots, Q_k x_k.\; P(x_1,\ldots,x_k), where each QiQ_i is an existential or universal quantifier and PP is a Boolean predicate. PEA deliberately restricts every variable to range over a finite domain and every predicate to be efficiently evaluable by a program. It then instructs an LLM to synthesize three code components — a predicate evaluator, an enumerator over the product of the finite domains, and an aggregation rule (for example, "does any candidate satisfy the predicate?") — and executes the synthesized program locally, deciding the formula by brute-force enumeration. On Boolean satisfiability (SAT, the problem of deciding whether an assignment making a Boolean formula true exists), the Game of 24 (a puzzle asking whether four given numbers can be combined by arithmetic operations to yield 24), and the Blocksworld and Logistics planning benchmarks (standard AI planning testbeds in which an agent rearranges blocks or routes packages between cities), PEA raised the accuracy of the underlying models (GPT-4o, OpenAI o1-mini, o1) by roughly 50% on average while cutting runtime, because a synthesized program is written once and reused across all instances of a task.

The finite-domain restriction is precisely what makes PEA terminating and sound: exhaustive enumeration plus aggregation over a finite space decides the quantified statement exactly. The paper itself acknowledges the cost of this design: propositions over infinite sets — its own motivating example is the number-theoretic statement "the sum of an odd number and an even number is odd", quantified over the integers Z\mathbb{Z} — cannot be represented, since naive enumeration over Z\mathbb{Z} never terminates. Extending this style of LLM-synthesized, execution-based reasoning to such domains must confront classical logic: the first-order theory of integer addition (Presburger arithmetic) is decidable, but the first-order theory of (Z,+,×)(\mathbb{Z}, +, \times) is undecidable, and the decidable arithmetic fragments that do exist — the ones decided by Satisfiability Modulo Theories (SMT) solvers, which check formulas against background theories such as linear integer arithmetic and can emit machine-checkable proofs — carry high worst-case complexity, so no brute-force analogue is available. Separately, several research lines couple LLMs with established solvers or synthesize solver-like software (LLMs translating problems into solver input languages, or coding agents building decision procedures), but these are alternatives to PEA's programmable enumeration paradigm rather than extensions of it. The open question is whether that paradigm itself can be extended — or soundly approximated — beyond finite domains while keeping its defining property: executing an LLM-synthesized program yields a trustworthy answer to the original quantified statement.

Problem Statement

Extend the Predicate-Enumeration-Aggregation (PEA) framework of Wang et al. (2025) — where a computational-reasoning problem is a quantified formula Q1x1,…,Qkxk.  P(x1,…,xk)Q_1 x_1, \ldots, Q_k x_k.\; P(x_1,\ldots,x_k) with variables restricted to finite domains and efficiently evaluable predicates, solved by an LLM synthesizing predicate/enumeration/aggregation programs that are executed locally — to problems over infinite or practically unbounded domains, such as quantified statements over the integers Z\mathbb{Z}.

A complete answer must: (i) define the extended problem class — the logic or fragment and its semantics — that strictly contains finite-domain PEA problems and genuinely includes quantified infinite-domain instances; (ii) provide a synthesis-plus-execution procedure in the PEA style whose accepted answers are sound for the original quantified statement, either provably correct or correct under an explicitly declared approximation semantics (for example, one-sided answers, certified bounds, or machine-checkable certificates), and which is nondegenerate — it returns certified verdicts, rather than abstaining throughout, on a stated non-trivial class of infinite-domain instances, and, when it claims provable correctness, halts with a verdict on every instance decidable in the declared fragment; and (iii) demonstrate the extension on at least two distinct quantified infinite-domain problem families outside the current finite-domain expressiveness, including arithmetic statements over Z\mathbb{Z}, with certified verdicts actually returned on at least five instances in each demonstrated family, with soundness established by proof or by verifiable certificates accompanying the answers, and with the executed predicate, enumeration, and aggregation programs produced by a large language model whose identity and synthesis setup are reported (the synthesis half of the paradigm must be exercised; the soundness argument itself may be formal and need not rest on unverified model behaviour).

References

  1. Zi Wang, Shiwei Weng, Mohannad Alhanahnah, Somesh Jha, Tom Reps. PEA: Enhancing LLM Performance on Computational-Reasoning Tasks. 2025. arXiv:2502.10938, DOI 10.48550/arXiv.2502.10938. https://arxiv.org/abs/2502.10938
  2. Derrick Goh Xin Deik, Quanyu Long, Zhengyuan Liu, Nancy F. Chen, Wenya Wang. Programming over Thinking: Efficient and Robust Multi-Constraint Planning. 2026. arXiv:2601.09097, DOI 10.48550/arXiv.2601.09097. https://arxiv.org/abs/2601.09097
  3. Daniel Cao, Michael Katz, Harsha Kokel, Kavitha Srinivas, Shirin Sohrabi. Automating Thought of Search: A Journey Towards Soundness and Completeness. 2024. arXiv:2408.11326, DOI 10.48550/arXiv.2408.11326. https://arxiv.org/abs/2408.11326
  4. Aaron Bembenek. Current Practices for Building LLM-Powered Reasoning Tools Are Ad Hoc – and We Can Do Better. 2025. arXiv:2507.05886, DOI 10.48550/arXiv.2507.05886. https://arxiv.org/abs/2507.05886
  5. Mikoláš Janota, Mirek Olšák. LLM2SMT: Building an SMT Solver with Zero Human-Written Code. 2026. arXiv:2603.06931, DOI 10.48550/arXiv.2603.06931. https://arxiv.org/abs/2603.06931
  6. Atharva Naik, Yash Mathur, Prakam, Carolyn Rose, David Mortensen. ReaComp: Compiling LLM Reasoning into Symbolic Solvers for Efficient Program Synthesis. 2026. arXiv:2605.05485, DOI 10.48550/arXiv.2605.05485. https://arxiv.org/abs/2605.05485