Large Language Models (LLMs) often struggle with rigorous logical reasoning, suffering from hallucinations and inconsistent deduction. Chain-of-Thought (CoT) prompting relies heavily on the frozen model’s inherent capabilities, while neuro-symbolic approaches face a "translation reliability" bottleneck in which semantic parsing errors mislead external solvers. Recent work attempts to infuse symbolic capabilities via fine-tuning, but typically mimics forward reasoning, suffering from search-space explosion and irrelevant intermediate facts that dilute attention. We propose SOLID (Symbolic Oriented Logic Infusion via Dual-verification), a framework that synthesizes high-quality supervision through a Dual-Verification Mechanism: bidirectional consistency checks filter out hallucinated translations. Crucially, instead of forward chaining, we execute validated translations to generate backward reasoning traces—verifying necessary premises from the goal. By fine-tuning on these focused, goal-oriented paths, SOLID infuses the model with the efficient deduction process of a symbolic engine. Experiments on ProntoQA, LogicNLI, and ProofWriter demonstrate state-of-the-art accuracy, significantly outperforming CoT baselines, solver-based methods, and forward-chaining variants. Code and data are available at: https://github.com/ejie22/SOLID.

Geometry Problem Solving (GPS) is a fundamental task in mathematical reasoning, with applications in intelligent education and automated theorem proving. Existing neuro-symbolic solvers often rely on two restrictive assumptions: textual conditions are expressed as atomic geometric statements, and target derivation can be reduced to eager elimination of intermediate variables. These assumptions break down in realistic problems, where coupled geometric descriptions lead to combinatorial growth in parsing patterns, and nonlinear constraints make explicit elimination inefficient or even intractable. We propose RIGOR, a neuro-symbolic GPS framework based on Atomic Semantic Normalization and Declarative Constraint Reasoning. RIGOR uses a Geometric Semantic Normalizer trained on our newly constructed GSN-15K dataset to normalize geometric texts into atomic statements for reliable formalization. It then adopts a Declarative Symbolic Engine that globally accumulates derived geometric constraints and determines target values through constraint entailment, while also reconstructing proof-grounded reasoning traces. Experiments on multiple standard GPS benchmarks show that RIGOR outperforms state-of-the-art methods while producing interpretable derivations. Our project is available at https://github.com/dongyuhang22/RIGOR.

Constraint programming (CP) is a crucial technology for solving real-world constraint optimization problems (COPs), with the advantages of rich modeling semantics and high solving efficiency. Using large language models (LLMs) to generate formal modeling automatically for COPs is becoming a promising approach, which aims to build trustworthy neuro-symbolic AI with the help of symbolic solvers. However, CP has received less attention compared to works based on operations research (OR) models. We introduce ConstraintLLM, the first LLM specifically designed for CP modeling, which is trained on an open-source LLM with multi-instruction supervised fine-tuning. We propose the Constraint-Aware Retrieval Module (CARM) to increase the in-context learning capabilities, which is integrated in a Tree-of-Thoughts (ToT) framework with guided self-correction mechanism. Moreover, we construct and release IndusCP, the first industrial-level benchmark for CP modeling, which contains 140 challenging tasks from various domains. Our experiments demonstrate that ConstraintLLM achieves state-of-the-art solving accuracy across multiple benchmarks and outperforms the baselines by 2x on the new IndusCP benchmark. Code and data are available at: https://github.com/william4s/ConstraintLLM.

Deep neural networks can be vulnerable to adversarial attacks, even for the mainstream Transformer-based models. Although several robustness enhancement approaches have been proposed, they usually focus on some certain type of perturbation. As the types of attack can be various and unpredictable in practical scenarios, a general and strong defense method is urgently in require. We notice that most well-trained models can be weakly robust in the perturbation space, i.e., only a small ratio of adversarial examples exist. Inspired by the weak robust property, this paper presents a novel ensemble method for enhancing robustness. We propose a lightweight framework PAD to save computational resources in realizing an ensemble. Instead of training multiple models, a plugin module is designed to perturb the parameters of a base model which can achieve the effect of multiple models. Then, to diversify adversarial example distributions among different models, we promote each model to have different attention patterns via optimizing a diversity measure we defined. Experiments on various widely-used datasets and target models show that PAD can consistently improve the defense ability against many types of adversarial attacks while maintaining accuracy on clean data. Besides, PAD also presents good interpretability via visualizing diverse attention patterns.