arXiv Science⌕ Search
Home/Archive/arXiv

arXiv · 2504.04942

Lemmanaid: Neuro-Symbolic Lemma Conjecturing

Yousef Alhessi·Sólrún Halla Einarsdóttir·George Granberry·Emily First·Moa Johansson·Sorin Lerner·Nicholas Smallbone
View original source ↗Read source document ↗Export metadata ↓

Abstract

Mathematicians and computer scientists are increasingly leveraging proof assistants to formalize and check complex proofs, a task that demands substantial expertise. Can we lower the bar by automating the conjecturing of helpful, interesting and novel lemmas? We present the first neuro-symbolic lemma conjecturing tool, LEMMANAID, designed to discover conjectures by drawing analogies between mathematical theories. LEMMANAID uses a fine-tuned LLM to generate lemma templates that describe the shape of a lemma, and symbolic methods to fill in the details. We compare LEMMANAID against the same LLM fine-tuned to generate lemmas directly, as well as a fully symbolic conjecturing method. On test sets from Isabelle's HOL library and Archive of Formal Proofs (AFP), LEMMANAID consistently outperforms both neural and symbolic methods. Using DeepSeek-coder-6.7B as a backend, LEMMANAID discovers 50% (HOL) and 29% (AFP) of the gold standard lemmas, increasing to 55% and 35% when ensembling prompting strategies. In a case study on Octonions, LEMMANAID discovers 79% of the gold standard lemmas, compared to 62% for neural-only and 23% for the state of the art symbolic tool. Furthermore, in a targeted comparison, LEMMANAID discovers more gold standard lemmas than both Claude Opus 4.5 and GPT-5.2. Our results show that LEMMANAID can conjecture a significant number of interesting lemmas across complex formalizations in mathematics and computer science.

Explore related subjects

cs.AIcs.LO

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Yousef Alhessi, Sólrún Halla Einarsdóttir, George Granberry, Emily First, Moa Johansson, Sorin Lerner, Nicholas Smallbone. 2026-06-02. Lemmanaid: Neuro-Symbolic Lemma Conjecturing. https://arxiv.org/abs/2504.04942

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Towards a Mechanistic Understanding of Propositional Logical Reasoning in Large Language Models

Understanding how Large Language Models (LLMs) perform logical reasoning internally remains a fundamental challenge. While prior mechanistic studies focus on identifying task specific circuits, they leave open the question of what computational strategies LLMs employ for propositional reasoning. We address this gap with a causal mechanistic analysis on PropLogic-MI, a controlled benchmark of 11 propositional rules across one- and two-hop tasks, applied to three model families (Qwen3, Llama-3.1, Mistral). Rather than asking which components are necessary, we ask how the reasoning process is organized, and identify four interlocking mechanisms: Staged Computation, where early, middle, and late layers take on distinct functional roles; Information Transmission, where semantic content aggregates at boundary tokens; Fact Retrospection, where fact tokens stay causally active as binding lookup in middle layers and as sustained access in late layers under hard reasoning loads; and Specialized Attention Heads that structurally implement these patterns. A prompt-order control that places the query before the facts confirms that this organization is model-internal rather than input-layout-induced. These findings show that pretrained LLMs solve propositional reasoning through a structured, layer-organized process that recurs across models, rule categories, and reasoning hops.

cs.AI↗
arXiv2026

TimeWarp: Evaluating Web Agents by Revisiting the Past

As web agents close the gap with humans on benchmarks, one question arises: Do today's agents perform just as well on tomorrow's web? We introduce TimeWarp, a benchmark that emulates the evolving web. TimeWarp consists of three web environments, each with six UI versions spanning UI design, frontend code, and workflows from different eras of the internet. We pair TimeWarp with a set of complex, realistic tasks covering different forms of web navigation. Our experiments reveal that vision-based agents are vulnerable to changes, while text-based agents become brittle once fine-tuned on a single version. To address this, we propose TimeTraj, a new annotation method that uses plan distillation to collect trajectories across multiple versions. By training agents on teacher rollouts using our BC-variant, we achieve substantial performance gains: 20.4% to 37.7% for Qwen-3 4B and 0% to 27.0% for Llama-3.1 8B models. Our work helps study generalization across web designs and opens a new paradigm for collecting plans rather than trajectories to improve the robustness of web agents.

cs.AI↗
arXiv2026

Playing Devil's Advocate: Off-the-Shelf Persona Vectors Rival Targeted Steering for Sycophancy

Sycophancy is the tendency of language models to agree with users irrespective of correctness. Prior work has extracted sycophancy persona vectors and causally controlled this trait through activation steering (Chen et al., 2025; arXiv:2507.21509). We ask whether existing vectors for general roles, extracted without targeting sycophancy, transfer to this mitigation task. We compare critical and conformist role vectors with a sycophancy-targeted Contrastive Activation Addition (CAA) baseline on a held-out, counterbalanced PhilPapers benchmark, using task-specific coefficient tuning. On Gemma 2 27B and Qwen 3 32B, the selected critical-role vectors achieve mean sycophancy-logit reductions approximately 68% and 98% as large as CAA's, respectively. Conformist-role effects are weak and heterogeneous. Role vectors have low absolute cosine similarity with the measured CAA direction, establishing geometric separation at the intervention layer without identifying distinct downstream mechanisms. These results show that general persona vectors can help mitigate sycophancy in LLMs, even when extracted without sycophancy-specific labels. Code: https://anonymous.4open.science/#!/r/Sycophancy-Steering-9DF0/.

cs.AI↗