arXiv subjects

Guangyu Hu

Publications and source records attributed to Guangyu Hu.

18 recordsLinked to original sources

arXiv2026

APEX-RBD: Mixed-Precision Exploration Framework for Hardware-Efficient Robot Dynamics Accelerator Design

Rigid Body Dynamics (RBD) forms the computational core of real-time robotic control, but its immense computational complexity creates a performance bottleneck that necessitates dedicated hardware accelerators. However, the substantial hardware resource and power costs of these accelerators make their deployment on resource-constrained edge platforms highly challenging. While quantization offers a promising path to optimize RBD hardware for edge computing, existing uniform-precision approaches remain inefficient by ignoring the diverse quantization sensitivities of different variables. Although mixed-precision offers a superior alternative, its exploration is intractable due to a vast search space and the prohibitive cost of closed-loop simulation for motion accuracy evaluation. To address these challenges, we introduce APEX-RBD, an automated framework that makes mixed-precision exploration computationally tractable while effectively identifying hardware-efficient configurations. Specifically, it performs physics-driven search space pruning via variable grouping and sensitivity analysis, and employs a data-efficient, prior-informed surrogate model to enable rapid trajectory error prediction. This formulation guides a hybrid optimizer to identify area- and power-efficient designs under user-defined accuracy and performance constraints. Experimental results demonstrate that APEX-RBD discovers designs achieving up to 1.9$\times$ area reduction and 1.8$\times$ power savings compared to uniform-precision baselines across diverse robotic platforms.

cs.AR↗

arXiv2026

Personalized Communication Skills for Agentic Recommender Systems

Agentic recommender systems increasingly employ large language model-based UserAgents to evaluate candidate items through simulated feedback before recommendations are delivered. However, existing UserAgents typically reason in isolation based on limited personal histories, which may lead to perspective narrowing: the agent evaluates candidates from a local and incomplete view, overlooks relevant preference facets, and consequently produces inaccurate judgments. A natural way to alleviate this problem is to introduce other users as advisor agents, whose diverse histories provide complementary evidence that helps the target user reconsider overlooked preference signals. Nevertheless, a generic user-advisor communication process is insufficient, as different user decision states require different forms of external advice. Based on this insight, we propose AgentCom, a personalized communication skill framework for agentic recommender systems. AgentCom organizes reusable communication skills into a shared why--what--how--who skill bank: why identifies the decision deficiency that necessitates communication, what specifies the information task, how determines the advisor interaction protocol, and who retrieves advisors capable of executing that protocol. To make the shared skill bank personalized at use time and adaptive over time, AgentCom introduces two complementary mechanisms: personalized skill routing and failure-driven skill evolution. Personalized skill routing constructs a communication path by sequentially selecting suitable skills for each user and recommendation context. Failure-driven skill evolution learns from unsuccessful communication cases and enriches the shared bank with reusable skills that address previously uncovered communication needs. Experiments show that AgentCom consistently improves recommendation performance across traditional, social, and agentic recommenders.

cs.IR↗

arXiv2026

Forbench: Symbolic Simulation Helps Make Your Testbench More Formal

Simulation remains the dominant approach in pre-silicon verification due to its ease of deployment and intuitive workflow. However, as simulation only explores a limited subset of possible execution traces within feasible time budgets, it often fails to explore rare corner cases, leaving latent bugs undetected. In contrast, formal verification offers mathematically rigorous guarantees of correctness. However, its practical adoption is constrained, not only by the scalability challenges over large-scale designs, but also by the change of mindset from stimulus-driven operations to the sequence-centric axiomatic view of design behaviors, introducing extra difficulty of writing precise properties to capture the exact verification intent. This paper aims to lower the barrier of applying formal methods in verification, by making simulation "more formal." It introduces Forbench, a word-level symbolic simulation framework that retains the familiar execution semantics of simulation but augments it with solver-backed symbolic signals and state transitions, enabling systematic exploration of RTL behaviors under symbolic inputs and conditions. It offers a Python interface, similar to the existing simulation-based frameworks, for defining constraints, coordinating symbolic (co-)simulations, and performing property checks. In additional to this more accessible interface, experiments also show that Forbench achieves notably speed-up over prior symbolic methods without the loss of coverage.

cs.AR↗

arXiv2026

Inverter Redistribution through Self-Dual and Self-Anti-Dual Function Transformation

And-Inverter Graph (AIG)-based logic synthesis has been a cornerstone of digital design automation for several decades. While numerous optimization techniques have been developed for both technology-independent and technology-dependent synthesis stages, existing technology mapping approaches predominantly employ graph-covering strategies directly on AIG representations without adequately addressing complemented edge distribution. Neglecting inverters creates a significant disconnect: complemented edges are systematically overlooked in technology-independent cost functions, yet they abruptly become critical during technology-dependent mapping. In this work, we introduce a delay-driven pre-processing stage that operates prior to technology mapping, designed to strategically redistribute complemented edges and mitigate the inverter-induced costs on critical paths. Experimental validation demonstrates that our delay-targeted methodology not only preserves original delay characteristics but also enables performance improvements. Notably, arithmetic logic in the EPFL combinational benchmark exhibits particular sensitivity to this approach, with our method achieving an average delay reduction of 0.49% and a maximum improvement of 3.86% on the case sqrt.

cs.LO↗

arXiv2026

AutoINV: Automated Invariant Generation Framework for Formal Verification on High-Level Synthesis Designs

High-level synthesis (HLS) transforms an algorithmic description of hardware from a higher abstraction (e.g., C/C++) into a register-transfer level (RTL) design, offering reduced development time and greater flexibility in design space exploration. However, such machine-generated RTL designs may contain major functional bugs or security vulnerabilities due to limitations or errors in the HLS tools. One of the most reliable methods to identify these vulnerabilities is formal verification, particularly model checking. Nevertheless, the large size of the generated RTL often causes model checking to struggle to conclude within reasonable time or resource limits. In this study, we propose utilizing the high-level design features from the HLS flow to construct a set of helper assertions aimed at guiding the model checker and accelerating the verification process. To identify the most effective set of helpers to assist the model checker, we develop a proving mechanism that iteratively reuses proving information to select the potentially most useful set of helpers. We evaluate the proposed framework on a set of HLS design benchmarks. Experimental results demonstrate that, when compared to vanilla model checking, our approach achieves a speedup of up to 6.05x, and 2.23x on average.

cs.AR↗

arXiv2026

A-IC3: Learning-Guided Adaptive Inductive Generalization for Hardware Model Checking

The IC3 algorithm represents the state-of-the-art (SOTA) hardware model checking technique, owing to its robust performance and scalability. A significant body of research has focused on enhancing the solving efficiency of the IC3 algorithm, with particular attention to the inductive generalization process: a critical phase wherein the algorithm seeks to generalize a counterexample to inductiveness (CTI), which typically is a state leading to a bad state, into a broader set of states. This inductive generalization is a primary source of clauses in IC3 and thus plays a pivotal role in determining the overall effectiveness of the algorithm. Despite its importance, existing approaches often rely on fixed inductive generalization strategies, overlooking the dynamic and context-sensitive nature of the verification environment in which spurious counterexamples arise. This rigidity can limit the quality of generated clauses and, consequently, the performance of IC3. To address this limitation, we propose a lightweight machine-learning-based framework that dynamically selects appropriate inductive generalization strategies in response to the evolving verification context. Specifically, we employ a multi-armed bandit (MAB) algorithm to adaptively choose inductive generalization strategies based on real-time feedback from the verification process. The agent is updated by evaluating the quality of generalization outcomes, thereby refining its strategy selection over time. Empirical evaluation on a benchmark suite comprising 914 instances, primarily drawn from the latest HWMCC collection, demonstrates the efficacy of our approach. When implemented on the state-of-the-art model checker rIC3, our method solves 26 to 50 more cases than the baselines and improves the PAR-2 score by 194.72 to 389.29.

cs.LO↗

arXiv2026

Beyond Overlap Metrics: Rewarding Reasoning and Preferences for Faithful Multi-Role Dialogue Summarization

Multi-role dialogue summarization requires modeling complex interactions among multiple speakers while preserving role-specific information and factual consistency. However, most existing methods optimize for automatic metrics such as ROUGE and BERTScore, which favor surface-level imitation of references rather than genuine gains in faithfulness or alignment with human preferences. We propose a novel framework that couples explicit cognitive-style reasoning with reward-based optimization for multi-role dialogue summarization. Our method first distills structured reasoning traces (e.g., step-by-step inferences and intermediate reflections) from a large teacher model and uses them as auxiliary supervision to initialize a reasoning-aware summarizer via staged supervised fine-tuning. It then applies GRPO with a dual-principle reward that blends metric-based signals with human-aligned criteria targeting key information coverage, implicit inference, factual faithfulness, and conciseness. Experiments on multilingual multi-role dialogue benchmarks show that our method matches strong baselines on ROUGE and BERTScore. Specifically, results on CSDS confirm the framework's stability in semantic consistency, while in-depth analysis on SAMSum demonstrates clear gains in factual faithfulness and model-based preference alignment. These findings underscore the value of reasoning-aware and preference-aware training for reliable dialogue summarization. Checkpoints and datasets are available at https://huggingface.co/collections/NebulaPixel/summorchestra-multirole-summary.

cs.CL↗

arXiv2026

AutoPDR: Circuit-Aware Solver Configuration Prediction for Hardware Model Checking

Property Directed Reachability (PDR) is a powerful algorithm for formal verification of hardware and software systems, but its performance is highly sensitive to parameter configurations. Manual parameter tuning is time-consuming and requires domain expertise, while traditional automated parameter tuning frameworks are not well-suited for time-sensitive verification tasks like PDR. This paper presents a circuit-aware solver configuration framework that employs graph learning for intelligent heuristic selection in PDR-based verification. Our approach combines graph representations with static circuit features to predict optimal PDR solving configurations for specific circuits. We incorporate expert prior knowledge through constraint-based parameter filtering to eliminate invalid and inefficient configurations and reduce 78% search space. Our feature extraction pipeline captures structural, functional, and connectivity characteristics of circuit topology and component patterns. Experimental evaluation on a comprehensive benchmark suite demonstrates significant performance improvements compared to default configurations and commonly-used settings. The system successfully identifies circuit-specific parameter patterns and automatically selects the most suitable solving strategies based on circuit characteristics, making it a practical tool for automated formal verification workflows.

cs.AR↗

arXiv2026

LeGend: A Data-Driven Framework for Lemma Generation in Hardware Model Checking

Property checking of RTL designs is a central task in formal verification. Among available engines, IC3/PDR is a widely used backbone whose performance critically depends on inductive generalization, the step that generalizes a concrete counterexample-to-induction (CTI) cube into a lemma. Prior work has explored machine learning to guide this step and achieved encouraging results, yet most methods adopt a per-clause graph analysis paradigm: for each clause they repeatedly build and analyze graphs, incurring heavy overhead and creating a scalability bottleneck. We introduce LeGend, which replaces this paradigm with one-time global representation learning. LeGend pre-trains a domain-adapted self-supervised model to produce latch embeddings that capture global circuit properties. These precomputed embeddings allow a lightweight model to predict high-quality lemmas with negligible overhead, effectively decoupling expensive learning from fast inference. Experiments show LeGend accelerates two state-of-the-art IC3/PDR engines across a diverse set of benchmarks, presenting a promising path to scale up formal verification.

cs.AR↗

arXiv2026

EvolveGen: Algorithmic Level Hardware Model Checking Benchmark Generation through Reinforcement Learning

Progress in hardware model checking depends critically on high-quality benchmarks. However, the community faces a significant benchmark gap: existing suites are limited in number, often distributed only in representations such as BTOR2 without access to the originating register-transfer-level (RTL) designs, and biased toward extreme difficulty where instances are either trivial or intractable. These limitations hinder rigorous evaluation of new verification techniques and encourage overfitting of solver heuristics to a narrow set of problems. To address this, we introduce EvolveGen, a framework for generating hardware model checking benchmarks by combining reinforcement learning (RL) with high-level synthesis (HLS). Our approach operates at an algorithmic level of abstraction in which an RL agent learns to construct computation graphs. By compiling these graphs under different synthesis directives, we produce pairs of functionally equivalent but structurally distinct hardware designs, inducing challenging model checking instances. Solver runtime is used as the reward signal, enabling the agent to autonomously discover and generate small-but-hard instances that expose solver-specific weaknesses. Experiments show that EvolveGen efficiently creates a diverse benchmark set in standard formats (e.g., AIGER and BTOR2) and effectively reveals performance bottlenecks in state-of-the-art model checkers.

cs.AR↗

arXiv2026

SegSEM: Enabling and Enhancing SAM2 for SEM Contour Extraction

Extracting high-fidelity 2D contours from Scanning Electron Microscope (SEM) images is critical for calibrating Optical Proximity Correction (OPC) models. While foundation models like Segment Anything 2 (SAM2) are promising, adapting them to specialized domains with scarce annotated data is a major challenge. This paper presents a case study on adapting SAM2 for SEM contour extraction in a few-shot setting. We propose SegSEM, a framework built on two principles: a data-efficient fine-tuning strategy that adapts by selectively training only the model's encoders, and a robust hybrid architecture integrating a traditional algorithm as a confidence-aware fallback. Using a small dataset of 60 production images, our experiments demonstrate this methodology's viability. The primary contribution is a methodology for leveraging foundation models in data-constrained industrial applications.

cs.AR↗

arXiv2026

IC3-Evolve: Proof-/Witness-Gated Offline LLM-Driven Heuristic Evolution for IC3 Hardware Model Checking

IC3, also known as property-directed reachability (PDR), is a commonly-used algorithm for hardware safety model checking. It checks if a state transition system complies with a given safety property. IC3 either returns UNSAFE (indicating property violation) with a counterexample trace, or SAFE with a checkable inductive invariant as the proof to safety. In practice, the performance of IC3 is dominated by a large web of interacting heuristics and implementation choices, making manual tuning costly, brittle, and hard to reproduce. This paper presents IC3-Evolve, an automated offline code-evolution framework that utilizes an LLM to propose small, slot-restricted and auditable patches to an IC3 implementation. Crucially, every candidate patch is admitted only through proof- /witness-gated validation: SAFE runs must emit a certificate that is independently checked, and UNSAFE runs must emit a replayable counterexample trace, preventing unsound edits from being deployed. Since the LLM is used only offline, the deployed artifact is a standalone evolved checker with zero ML/LLM inference overhead and no runtime model dependency. We evolve on the public hardware model checking competition (HWMCC) benchmark and evaluate the generalizability on unseen public and industrial model checking benchmarks, showing that IC3-Evolve can reliably discover practical heuristic improvements under strict correctness gates.

cs.AI↗

arXiv2026

Thermodynamic assessment of the Ba-La-S and Ga-La-S systems

This paper presents the first thermodynamic assessment of binary and pseudo-binary phase diagrams in the Ba--La--S and Ga--La--S systems by means of the CALPHAD method. Experimental phase diagram equilibrium data and thermodynamic properties available from the literature were critically reviewed and assessed using thermodynamic models for the Gibbs energies of individual phases. The associated solution model was used to describe the short-range ordering behavior of the liquid phases. To supplement the limited experimental data reported in the literature, ab initio molecular dynamics calculations were employed to derive mixing enthalpies of the liquid phases in the binary subsystems. The resulting phase diagrams and calculated thermodynamic properties show good agreement with available literature within the investigated compositional ranges of binary and pseudo-binary systems.

cond-mat.mtrl-sci↗

arXiv2025

BDD2Seq: Enabling Scalable Reversible-Circuit Synthesis via Graph-to-Sequence Learning

Binary Decision Diagrams (BDDs) are instrumental in many electronic design automation (EDA) tasks thanks to their compact representation of Boolean functions. In BDD-based reversible-circuit synthesis, which is critical for quantum computing, the chosen variable ordering governs the number of BDD nodes and thus the key metrics of resource consumption, such as Quantum Cost. Because finding an optimal variable ordering for BDDs is an NP-complete problem, existing heuristics often degrade as circuit complexity grows. We introduce BDD2Seq, a graph-to-sequence framework that couples a Graph Neural Network encoder with a Pointer-Network decoder and Diverse Beam Search to predict high-quality orderings. By treating the circuit netlist as a graph, BDD2Seq learns structural dependencies that conventional heuristics overlooked, yielding smaller BDDs and faster synthesis. Extensive experiments on three public benchmarks show that BDD2Seq achieves around 1.4 times lower Quantum Cost and 3.7 times faster synthesis than modern heuristic algorithms. To the best of our knowledge, this is the first work to tackle the variable-ordering problem in BDD-based reversible-circuit synthesis with a graph-based generative model and diversity-promoting decoding.

cs.AR↗

arXiv2025

FORWORD: Accelerating Formal Datapath Verification via Word-Level Sweeping

Modern circuit design process increasingly adopts high-level hardware construction languages and parameterized design methodologies to shorten development cycles and maintain high reusability, in contrast to traditional hardware description languages. Such designs often involve complex datapath with arithmetic operations, wide bit-vectors, and on-chip memories, whose scale and level of modeling often pose significant challenges to formal datapath verification. Traditional bit-level SAT sweeping techniques lack the necessary abstraction and adaptability that are required to establish equivalence at a higher level. In this paper, we propose FORWORD, a novel word-level sweeping verification engine tailored explicitly to formal datapath verification. FORWORD integrates randomized and constraint-driven word-level simulations, leveraging adaptive optimization to dynamically refine equivalent candidates identified during simulation. Experimental results demonstrate that FORWORD significantly outperforms state-of-the-art bit-level SAT sweeping engines and the monolithic SMT solving method, thanks to its enhanced capability in effectively identifying equivalent pairs. To the best of our knowledge, FORWORD is the first word-level sweeping engine explicitly designed for datapath verification, offering improved efficiency and adaptability to modern circuit designs.

cs.LO↗

arXiv2024

E-Syn: E-Graph Rewriting with Technology-Aware Cost Functions for Logic Synthesis

Logic synthesis plays a crucial role in the digital design flow. It has a decisive influence on the final Quality of Results (QoR) of the circuit implementations. However, existing multi-level logic optimization algorithms often employ greedy approaches with a series of local optimization steps. Each step breaks the circuit into small pieces (e.g., k-feasible cuts) and applies incremental changes to individual pieces separately. These local optimization steps could limit the exploration space and may miss opportunities for significant improvements. To address the limitation, this paper proposes using e-graph in logic synthesis. The new workflow, named Esyn, makes use of the well-established e-graph infrastructure to efficiently perform logic rewriting. It explores a diverse set of equivalent Boolean representations while allowing technology-aware cost functions to better support delay-oriented and area-oriented logic synthesis. Experiments over a wide range of benchmark designs show our proposed logic optimization approach reaches a wider design space compared to the commonly used AIG-based logic synthesis flow. It achieves on average 15.29% delay saving in delay-oriented synthesis and 6.42% area saving for area-oriented synthesis.

cs.AR↗

arXiv2024

AnisoGNN: graph neural networks generalizing to anisotropic properties of polycrystals

We present AnisoGNNs -- graph neural networks (GNNs) that generalize predictions of anisotropic properties of polycrystals in arbitrary testing directions without the need in excessive training data. To this end, we develop GNNs with a physics-inspired combination of node attributes and aggregation function. We demonstrate the excellent generalization capabilities of AnisoGNNs in predicting anisotropic elastic and inelastic properties of two alloys.

cond-mat.mtrl-sci↗

arXiv2023

Learning from 2D: machine learning of 3D effective properties of heterogeneous materials based on 2D microstructure sections

Microstructure--property relationships are key to effective design of structural materials for advanced applications. Advances in computational methods enabled modeling microstructure-sensitive properties using 3D models (e.g., finite elements) based on microstructure representative volumes. 3D microstructure data required as input to these models are typically obtained from either 3D characterization experiments or digital reconstruction based on statistics from 2D microstructure images. In this work, we present machine learning (ML) approaches to modeling effective properties of heterogeneous materials directly from 2D microstructure sections. To this end, we consider statistical learning models based on spatial correlations and convolutional neural networks as two distinct ML strategies. In both strategies, models are trained on a dataset of synthetically generated 3D microstructures and their properties obtained from micromechanical 3D simulations. Upon training, the models predict properties from 2D microstructure sections. The advantage of the presented models is that they only need 2D sections, whose experimental acquisition is more accessible compared to 3D characterization. Furthermore, the present models do not require digital reconstruction of 3D microstructures.

cond-mat.mtrl-sci↗