ABSTRACT. This paper presents the SMT solver primo, which is fully vibe-coded and then parameter-tuned, achieving state-of-the-art results on linear real arithmetic (QF-LRA). The performance of primo is achieved by a systematic literature survey, repeated profiling, and parameter tuning. The resulting solver outperforms the winner of the QF-LRA track of SMT-COMP 2026. This confirms that vibe-coding of automated reasoning tools will enable us to make great strides in the future.

ABSTRACT. We describe the knowledge representation and proof search choices behind llmpipe, an English-to-logic question-answering pipeline. The system maps English assertions and questions to a controlled-predicate first-order representation, compiles it into prover-ready clauses, and uses GK, a saturation-based first-order prover extended for commonsense reasoning, to derive answers and render proofs back into English.

We distinguish between machinery that requires dedicated prover support, such as contradiction-tolerant search, numeric confidence handling, and defeasible reasoning with prioritized default blocks, and first-order encodings, such as context terms, Davidsonian events, modal classifiers, biconditional answer definitions, and canonicalized measurements. These choices affect clause shape, term depth, proof search branching, axiom selection, and other proof search strategies. We evaluate the pipeline on nlformtasks, a 1600-case English question-answering test set, across four LLM backends. The goal is to identify which representations are useful for different classes of English questions and how they affect automated reasoning performance.

ABSTRACT. Large language models (LLMs) have achieved remarkable progress in formal mathematical reasoning. Mathematical competition problems fall into two broad types: theorem-proving problems ask for a proof of a fully specified statement, whereas answer-construction problems ask the solver to construct an answer object and prove that it satisfies the stated specification. Existing mathematical reasoning engines mainly target theorem-proving problems, yet answer-construction problems remain less studied. This setting is challenging because model capabilities are misaligned, with general LLMs better suited to answer construction and prover LLMs better suited to proof generation, and because Lean proof checking alone does not rule out inadmissible circular witnesses. To close this gap, we introduce Enumerate-Conjecture-Prove (ECP), a neuro-symbolic framework for solving answer-construction problems in Lean. ECP uses general LLMs to perform bounded enumeration and construct candidate answers, and invokes prover LLMs to produce machine-checked proofs. ECP introduces admissibility checking to ensure that each answer is canonical and does not involve a circular argument. On PutnamBench and autoformalized MathArena answer-construction problems, ECP formally solves 17/346 and 18/75 answer-construction problem instances with admissible answers and proofs, respectively, outperforming LLM baselines at aligned inference budgets. Our code is available at https://github.com/sunjia72/ecp-lpar.

ABSTRACT. Invertibility conditions are properties used by the cvc5 Satisfiability Modulo Theories (SMT) solver to reason about quantified bit-vector formulas. Previous work has proven 122 of 160 invertibility conditions for arbitrary bit-width. We prove the remaining 38 properties in the Rocq interactive theorem prover (ITP) with the help of Google Gemini and Claude Code. This paper presents our efforts in completing this set of proof goals and a case study for using AI assistants in proof projects.

ABSTRACT. Roel de Vrijer's assignment maps a simply typed \(\lambda\)-term to a measure whose numerical component drops after every \(\beta\)-contraction. We present that assignment as a compact Haskell program, which uses host-language functions for the functional component of the measure. We prove that the returned integer is in fact a decreasing bound on all subsequent reduction sequences.

ABSTRACT. We study the cycle-detection problem for affine single-path linear-constrained loops over the integers. A cycle is a finite execution that returns to its initial state. Cycle detection is a natural relaxation of termination: every cycle witnesses non-termination, while an infinite execution need not contain a cycle.

We prove that cycle detection for affine integer loops belongs to $\Sigma_2^P$. The proof relies on the algebraic structure of periodic vectors of the update matrix. Using the cyclotomic factors of its characteristic polynomial, we obtain a polynomial representation of the periodic subspace and of exponentially distant states along a periodic orbit. We then apply a small-integer-solution theorem to show that, whenever a cyclic state exists, one exists with polynomial bit-length. Consequently, cycle existence can be expressed by existentially guessing such a state and universally quantifying over a polynomial-size binary encoding of a position in its orbit, with the resulting predicate decidable in polynomial time.

ABSTRACT. We present a PSPACE-complete fragment of first order logic we call QEALM (QBF-like EPR by Alternating Level-ordered Miniscoping). Unlike other well-known fragments it is more analogous to QBF (Quantified Boolean Formulas) because it has game-like alternations and can be restricted to complete problems for the polynomial hierarchy. QEALM is a natural first order analogue to QBF just as EPR (Effectively Propositional logic) is a first analogue to Dependency QBF.

In this paper we prove the PSPACE and Polynomial Hierarchy completeness theorems of QEALM among other nice properties such as closure under Robinson's resolution and retained hardness after intersection with Schaefer fragments. We use our new definition to identify problems in the TPTP library that fall into this fragment and their level in the polynomial hierarchy.

ABSTRACT. Maslov's class K is a decidable fragment of equality-free first-order logic. It subsumes numerous classical decidable fragments, including the equality-free monadic fragment, the equality-free two-variable fragment, and the Gödel class. It also captures the more recently introduced equality-free uniform one-dimensional fragment. Introduced over 50 years ago, the class K has been studied in automated deduction, primarily through resolution-based methods. Despite this long history, basic properties of K remained poorly understood until recently, when NExpTime-completeness of satisfiability and the finite model property were finally established. However, the proofs are highly non-trivial and technically sophisticated.

We present considerably simpler proofs of NExpTime-completeness and the finite model property for K. Our approach is based on a novel Skolemization procedure tailored to K. Moreover, we extend the class K by allowing a distinguished binary predicate interpreted as an equivalence relation, and prove that the resulting fragment has a 2-NExpTime-complete satisfiability problem. Finally, we discuss the possible addition of equality to the class K.

ABSTRACT. Boolos’ Curious Inference (BCI) is a well-known example of a class of first-order reasoning problems that require infeasibly many proof steps in a first-order proof calculus but exhibit short and elegant proofs in second-order (or higher-order) logic. Consequently, BCI remains intractable for contemporary first-order automated theorem provers. Although the original problem formulation is also beyond the capabilities of current higher-order provers, previous work by Benzmüller et al. demonstrates that augmenting the problem statement with suitable higher-order formulas allows these provers to succeed. Building on this work, we introduce a procedure for identifying and generating such candidate augmentations. This procedure is implemented in the new ciao tool. Using ciao as a pre-processing tool makes BCI fully automatically solvable for the very first time.

ABSTRACT. We present a system for generating intermediate lemmas, used as cut formulas, that restructure first-order proof search in saturation-based theorem provers. Given a CNF problem, a heterogeneous graph neural network encodes clauses, literals, terms, variables and symbols. An autoregressive decoder then samples candidate lemmas by pointing to symbols in the input and by obeying arity constraints during decoding. Candidate lemmas are accepted when an ATP proves both sides of the cut, i.e. the problem extended with the lemma and with its negation. Together with adjustable criteria for proof-search speedup this gives a supervised learning signal and a learning-proving feedback loop.

We train and evaluate the methods on ATP datasets built from the Mizar Mathematical Library with both E and Vampire. On the E test set, the best single configuration helps 96 of 187 baseline-proved problems, while an ensemble helps 127 67.9%, with speedups up to 196x. We also show that a cut generator trained on the E data transfers to Vampire: when the cuts are delivered as AVATAR claims, Vampire proves 501 hard Mizar problems unsolved by Vampire or E before, and speeds up 2236 further problems. In combination with trained Deepire and Vampire's CASC mode, the learning/conjecturing/portfolio methods discussed here prove 1228 Mizar problems unsolved by Vampire or E before.

ABSTRACT. The calculus ALASCA extends superposition-based saturation proving with reasoning in Uninterpreted Functions and Linear Real Arithmetic (UFLRA). As efficiency of saturation algorithms depend on literal selection, simplification, and redundancy elimination, this paper improves reasoning in Uflra by introducing theory-specific notions and methods for all of these techniques. The implementation of these methods in the first-order theorem prover Vampire shows substantial gains in every tested benchmark category, solving a number of problems previously unsolved by any system.

ABSTRACT. A neural clause-selection guidance approach in the Vampire theorem prover was recently shown to substantially improve the success rate of the prover's default strategy on the TPTP benchmark. We experimentally study the impact of the approach across several ITP-derived benchmark sets and its interaction with theorem proving strategies.

We find that while the neural guidance consistently improves performance within individual benchmark domains, cross-benchmark application of guiding models underperforms the plain default strategy. The picture when considering combined strategies is less clear-cut, indicating persisting value of neural guidance but under diminishing returns.