arXiv subjects

Christopher Hahn

Publications and source records attributed to Christopher Hahn.

At least 19 recordsLinked to original sources

arXiv2024

Scaled-up prediction of steady Navier-Stokes equation with component reduced order modeling

Scaling up new scientific technologies from laboratory to industry often involves demonstrating performance on a larger scale. Computer simulations can accelerate design and predictions in the deployment process, though traditional numerical methods are computationally intractable even for intermediate pilot plant scales. Recently, component reduced order modeling method is developed to tackle this challenge by combining projection reduced order modeling and discontinuous Galerkin domain decomposition. However, while many scientific or engineering applications involve nonlinear physics, this method has been only demonstrated for various linear systems. In this work, the component reduced order modeling method is extended to steady Navier-Stokes flow, with application to general nonlinear physics in view. Large-scale, global domain is decomposed into combination of small-scale unit component. Linear subspaces for flow velocity and pressure are identified via proper orthogonal decomposition over sample snapshots collected at small scale unit component. Velocity bases are augmented with pressure supremizer, in order to satisfy inf-sup condition for stable pressure prediction. Two different nonlinear reduced order modeling methods are employed and compared for efficient evaluation of nonlinear advection: 3rd-order tensor projection operator and empirical quadrature procedure. The proposed method is demonstrated on flow over arrays of five different unit objects, achieving $23$ times faster prediction with less than $4\%$ relative error up to $256$ times larger scale domain than unit components. Furthermore, a numerical experiment with pressure supremizer strongly indicates the need of supremizer for stable pressure prediction. A comparison between tensorial approach and empirical quadrature procedure is performed, which suggests a slight advantage for empirical quadrature procedure.

math.NA↗

arXiv2024

Scalable physics-guided data-driven component model reduction for steady Navier-Stokes flow

Computational physics simulation can be a powerful tool to accelerate industry deployment of new scientific technologies. However, it must address the challenge of computationally tractable, moderately accurate prediction at large industry scales, and training a model without data at such large scales. A recently proposed component reduced order modeling (CROM) tackles this challenge by combining reduced order modeling (ROM) with discontinuous Galerkin domain decomposition (DG-DD). While it can build a component ROM at small scales that can be assembled into a large scale system, its application is limited to linear physics equations. In this work, we extend CROM to nonlinear steady Navier-Stokes flow equation. Nonlinear advection term is evaluated via tensorial approach or empirical quadrature procedure. Application to flow past an array of objects at moderate Reynolds number demonstrates $\sim23.7$ times faster solutions with a relative error of $\sim 2.3\%$, even at scales $256$ times larger than the original problem.

math.NA↗

arXiv2024

Symmetry Preservation in Swarms of Oblivious Robots with Limited Visibility

In the general pattern formation (GPF) problem, a swarm of simple autonomous, disoriented robots must form a given pattern. The robots' simplicity imply a strong limitation: When the initial configuration is rotationally symmetric, only patterns with a similar symmetry can be formed [Yamashita, Suzyuki; TCS 2010]. The only known algorithm to form large patterns with limited visibility and without memory requires the robots to start in a near-gathering (a swarm of constant diameter) [Hahn et al.; SAND 2024]. However, not only do we not know any near-gathering algorithm guaranteed to preserve symmetry but most natural gathering strategies trivially increase symmetries [Castenow et al.; OPODIS 2022]. Thus, we study near-gathering without changing the swarm's rotational symmetry for disoriented, oblivious robots with limited visibility (the OBLOT-model, see [Flocchini et al.; 2019]). We introduce a technique based on the theory of dynamical systems to analyze how a given algorithm affects symmetry and provide sufficient conditions for symmetry preservation. Until now, it was unknown whether the considered OBLOT-model allows for any non-trivial algorithm that always preserves symmetry. Our first result shows that a variant of Go-to-the-Average always preserves symmetry but may sometimes lead to multiple, unconnected near-gathering clusters. Our second result is a symmetry-preserving near-gathering algorithm that works on swarms with a convex boundary (the outer boundary of the unit disc graph) and without holes (circles of diameter 1 inside the boundary without any robots).

cs.RO↗

arXiv2024

TCAD Simulations of Radiation Damage in 4H-SiC

To increase the scientific output of particle physics experiments, upgrades are underway at all major accelerator facilities to significantly improve the luminosity. Consequently, the solid-state detectors used in the experiments will exhibit more severe radiation-induced damage. To ensure sufficiently long sensor lifetimes, alternative materials to the established silicon sensors, with improved resilience to radiation, are investigated. For one of the promising candidate materials, silicon carbide, only recently a model describing the radiation damage in technology aided computer design (TCAD) simulations has been proposed. In this paper we present our latest achievements towards modeling radiation damage of 4H-SiC in TCAD tools. We first verify the utilized TCAD framework against published silicon data and then use it to approximate measurements of neutron-irradiated 4H-SiC particle detectors. We are able to confirm in simulations the measurement results, i.e., an almost flat capacitance as a function of bias voltage and a decreasing forward current with increasing particle fluence. Based on our simulations we are able to explain the latter by trapped charge carriers that create a space charge region within the device.

physics.ins-det↗

arXiv2024

Undecided State Dynamics with Stubborn Agents

In the classical Approximate Majority problem with two opinions there are agents with Opinion 1 and with Opinion 2. The goal is to reach consensus and to agree on the majority opinion if the bias is sufficiently large. It is well known that the problem can be solved efficiently using the Undecided State Dynamics (USD) where an agent interacting with an agent of the opposite opinion becomes undecided. In this paper, we consider a variant of the USD with a preferred Opinion 1. That is, agents with Opinion 1 behave stubbornly -- they preserve their opinion with probability $p$ whenever they interact with an agent having Opinion 2. Our main result shows a phase transition around the stubbornness parameter $p \approx 1-x_1/x_2$. If $x_1 = \Theta(n)$ and $p \geq 1-x_1/x_2 + o(1)$, then all agents agree on Opinion 1 after $O(n\cdot \log n)$ interactions. On the other hand, for $p \leq 1-x_1/x_2 - o(1)$, all agents agree on Opinion 2, again after $O(n\cdot \log n)$ interactions. Finally, if $p \approx 1-x_1/x_2$, then all agents do agree on one opinion after $O(n\cdot \log^2 n)$ interactions, but either of the two opinions can survive. All our results hold with high probability.

cs.DC↗

arXiv2024

Autoformalizing Natural Language to First-Order Logic: A Case Study in Logical Fallacy Detection

Translating natural language into formal language such as First-Order Logic (FOL) is a foundational challenge in NLP with wide-ranging applications in automated reasoning, misinformation tracking, and knowledge validation. In this paper, we introduce Natural Language to First-Order Logic (NL2FOL), a framework to autoformalize natural language to FOL step by step using Large Language Models (LLMs). Our approach addresses key challenges in this translation process, including the integration of implicit background knowledge. By leveraging structured representations generated by NL2FOL, we use Satisfiability Modulo Theory (SMT) solvers to reason about the logical validity of natural language statements. We present logical fallacy detection as a case study to evaluate the efficacy of NL2FOL. Being neurosymbolic, our approach also provides interpretable insights into the reasoning process and demonstrates robustness without requiring model fine-tuning or labeled training data. Our framework achieves strong performance on multiple datasets. On the LOGIC dataset, NL2FOL achieves an F1-score of 78%, while generalizing effectively to the LOGICCLIMATE dataset with an F1-score of 80%.

cs.CL↗

arXiv2024

Forming Large Patterns with Local Robots in the OBLOT Model

In the arbitrary pattern formation problem, $n$ autonomous, mobile robots must form an arbitrary pattern $P \subseteq \mathbb{R}^2$. The (deterministic) robots are typically assumed to be indistinguishable, disoriented, and unable to communicate. An important distinction is whether robots have memory and/or a limited viewing range. Previous work managed to form $P$ under a natural symmetry condition if robots have no memory but an unlimited viewing range [22] or if robots have a limited viewing range but memory [25]. In the latter case, $P$ is only formed in a shrunk version that has constant diameter. Without memory and with limited viewing range, forming arbitrary patterns remains an open problem. We provide a partial solution by showing that $P$ can be formed under the same symmetry condition if the robots' initial diameter is $\leq 1$. Our protocol partitions $P$ into rotation-symmetric components and exploits the initial mutual visibility to form one cluster per component. Using a careful placement of the clusters and their robots, we show that a cluster can move in a coordinated way through its component while drawing $P$ by dropping one robot per pattern coordinate.

cs.RO↗

arXiv2024

LawInstruct: A Resource for Studying Language Model Adaptation to the Legal Domain

Instruction tuning is an important step in making language models useful for direct user interaction. However, the legal domain is underrepresented in typical instruction datasets (e.g., only 10 out of 1600+ tasks in Super-NaturalInstructions). To study whether instruction tuning on legal datasets is necessary for strong legal reasoning, we aggregate 58 annotated legal datasets and write instructions for each, creating LawInstruct. LawInstruct covers 17 global jurisdictions, 24 languages and a total of 12M examples across diverse tasks such as legal QA, summarization of court cases, and legal argument mining. We evaluate our models on LegalBench, measuring legal reasoning across five categories in 162 challenging and realistic legal tasks, and MMLU, to measure potential drops in general reasoning capabilities. We find that legal-specific instruction tuning on Flan-T5 - yielding FLawN-T5 - improves performance on LegalBench across all model sizes, with an aggregate increase of 15 points or 50% over Flan-T5 for the base size. No model size shows performance drops in MMLU. We publish LawInstruct as a resource for further study of instruction tuning in the legal domain.

cs.CL↗

arXiv2024

NeuroSynt: A Neuro-symbolic Portfolio Solver for Reactive Synthesis

We introduce NeuroSynt, a neuro-symbolic portfolio solver framework for reactive synthesis. At the core of the solver lies a seamless integration of neural and symbolic approaches to solving the reactive synthesis problem. To ensure soundness, the neural engine is coupled with model checkers verifying the predictions of the underlying neural models. The open-source implementation of NeuroSynt provides an integration framework for reactive synthesis in which new neural and state-of-the-art symbolic approaches can be seamlessly integrated. Extensive experiments demonstrate its efficacy in handling challenging specifications, enhancing the state-of-the-art reactive synthesis solvers, with NeuroSynt contributing novel solves in the current SYNTCOMP benchmarks.

cs.LO↗

arXiv2023

Train Small, Model Big: Scalable Physics Simulators via Reduced Order Modeling and Domain Decomposition

Numerous cutting-edge scientific technologies originate at the laboratory scale, but transitioning them to practical industry applications is a formidable challenge. Traditional pilot projects at intermediate scales are costly and time-consuming. An alternative, the E-pilot, relies on high-fidelity numerical simulations, but even these simulations can be computationally prohibitive at larger scales. To overcome these limitations, we propose a scalable, physics-constrained reduced order model (ROM) method. ROM identifies critical physics modes from small-scale unit components, projecting governing equations onto these modes to create a reduced model that retains essential physics details. We also employ Discontinuous Galerkin Domain Decomposition (DG-DD) to apply ROM to unit components and interfaces, enabling the construction of large-scale global systems without data at such large scales. This method is demonstrated on the Poisson and Stokes flow equations, showing that it can solve equations about $15 - 40$ times faster with only $\sim$ $1\%$ relative error. Furthermore, ROM takes one order of magnitude less memory than the full order model, enabling larger scale predictions at a given memory limitation.

cs.CE↗

arXiv2023

Lightweight Online Learning for Sets of Related Problems in Automated Reasoning

We present Self-Driven Strategy Learning ($\textit{sdsl}$), a lightweight online learning methodology for automated reasoning tasks that involve solving a set of related problems. $\textit{sdsl}$ does not require offline training, but instead automatically constructs a dataset while solving earlier problems. It fits a machine learning model to this data which is then used to adjust the solving strategy for later problems. We formally define the approach as a set of abstract transition rules. We describe a concrete instance of the sdsl calculus which uses conditional sampling for generating data and random forests as the underlying machine learning model. We implement the approach on top of the Kissat solver and show that the combination of Kissat+$\textit{sdsl}$ certifies larger bounds and finds more counter-examples than other state-of-the-art bounded model checking approaches on benchmarks obtained from the latest Hardware Model Checking Competition.

cs.AI↗

arXiv2023

nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models

A rigorous formalization of desired system requirements is indispensable when performing any verification task. This often limits the application of verification techniques, as writing formal specifications is an error-prone and time-consuming manual task. To facilitate this, we present nl2spec, a framework for applying Large Language Models (LLMs) to derive formal specifications (in temporal logics) from unstructured natural language. In particular, we introduce a new methodology to detect and resolve the inherent ambiguity of system requirements in natural language: we utilize LLMs to map subformulas of the formalization back to the corresponding natural language fragments of the input. Users iteratively add, delete, and edit these sub-translations to amend erroneous formalizations, which is easier than manually redrafting the entire formalization. The framework is agnostic to specific application domains and can be extended to similar specification languages and new neural models. We perform a user study to obtain a challenging dataset, which we use to run experiments on the quality of translations. We provide an open-source implementation, including a web-based frontend.

cs.LO↗

arXiv2023

Iterative Circuit Repair Against Formal Specifications

We present a deep learning approach for repairing sequential circuits against formal specifications given in linear-time temporal logic (LTL). Given a defective circuit and its formal specification, we train Transformer models to output circuits that satisfy the corresponding specification. We propose a separated hierarchical Transformer for multimodal representation learning of the formal specification and the circuit. We introduce a data generation algorithm that enables generalization to more complex specifications and out-of-distribution datasets. In addition, our proposed repair mechanism significantly improves the automated synthesis of circuits from LTL specifications with Transformers. It improves the state-of-the-art by $6.8$ percentage points on held-out instances and $11.8$ percentage points on an out-of-distribution dataset from the annual reactive synthesis competition.

cs.LG↗

arXiv2023

Fast Convergence of $k$-Opinion Undecided State Dynamics in the Population Protocol Model

We analyze the convergence of the $k$-opinion Undecided State Dynamics (USD) in the population protocol model. For $k$=2 opinions it is well known that the USD reaches consensus with high probability within $O(n \log n)$ interactions. Proving that the process also quickly solves the consensus problem for $k>2$ opinions has remained open, despite analogous results for larger $k$ in the related parallel gossip model. In this paper we prove such convergence: under mild assumptions on $k$ and on the initial number of undecided agents we prove that the USD achieves plurality consensus within $O(k n \log n)$ interactions with high probability, regardless of the initial bias. Moreover, if there is an initial additive bias of at least $\Omega(\sqrt{n} \log n)$ we prove that the initial plurality opinion wins with high probability, and if there is a multiplicative bias the convergence time is further improved. Note that this is the first result for $k > 2$ for the USD in the population protocol model. Furthermore, it is the first result for the unsynchronized variant of the USD with $k>2$ which does not need any initial bias.

cs.DC↗

arXiv2022

Formal Specifications from Natural Language

We study the generalization abilities of language models when translating natural language into formal specifications with complex semantics. In particular, we fine-tune language models on three datasets consisting of English sentences and their corresponding formal representation: 1) regular expressions (regex), frequently used in programming and search; 2) First-order logic (FOL), commonly used in software verification and theorem proving; and 3) linear-time temporal logic (LTL), which forms the basis for industrial hardware specification languages. Our experiments show that, in these diverse domains, the language models maintain their generalization capabilities from pre-trained knowledge of natural language to generalize, e.g., to new variable names or operator descriptions. Additionally, they achieve competitive performance, and even outperform the state-of-the-art for translating into regular expressions, with the benefits of being easy to access, efficient to fine-tune, and without a particular need for domain-specific reasoning.

cs.SE↗

arXiv2022

Explaining Hyperproperty Violations

Hyperproperties relate multiple computation traces to each other. Model checkers for hyperproperties thus return, in case a system model violates the specification, a set of traces as a counterexample. Fixing the erroneous relations between traces in the system that led to the counterexample is a difficult manual effort that highly benefits from additional explanations. In this paper, we present an explanation method for counterexamples to hyperproperties described in the specification logic HyperLTL. We extend Halpern and Pearl's definition of actual causality to sets of traces witnessing the violation of a HyperLTL formula, which allows us to identify the events that caused the violation. We report on the implementation of our method and show that it significantly improves on previous approaches for analyzing counterexamples returned by HyperLTL model checkers.

cs.LO↗

arXiv2022

Attention Flows for General Transformers

In this paper, we study the computation of how much an input token in a Transformer model influences its prediction. We formalize a method to construct a flow network out of the attention values of encoder-only Transformer models and extend it to general Transformer architectures including an auto-regressive decoder. We show that running a maxflow algorithm on the flow network construction yields Shapley values, which determine the impact of a player in cooperative game theory. By interpreting the input tokens in the flow network as players, we can compute their influence on the total attention flow leading to the decoder's decision. Additionally, we provide a library that computes and visualizes the attention flow of arbitrary Transformer models. We show the usefulness of our implementation on various models trained on natural language processing and reasoning tasks.

cs.LG↗

arXiv2022

Runtime Enforcement of Hyperproperties

An enforcement mechanism monitors a reactive system for undesired behavior at runtime and corrects the system's output in case it violates the given specification. In this paper, we study the enforcement problem for hyperproperties, i.e., properties that relate multiple computation traces to each other. We elaborate the notion of sound and transparent enforcement mechanisms for hyperproperties in two trace input models: 1) the parallel trace input model, where the number of traces is known a-priori and all traces are produced and processed in parallel and 2) the sequential trace input model, where traces are processed sequentially and no a-priori bound on the number of traces is known. For both models, we study enforcement algorithms for specifications given as formulas in universally quantified HyperLTL, a temporal logic for hyperproperties. For the parallel model, we describe an enforcement mechanism based on parity games. For the sequential model, we show that enforcement is in general undecidable and present algorithms for reasonable simplifications of the problem (partial guarantees or the restriction to safety properties). Furthermore, we report on experimental results of our prototype implementation for the parallel model.

cs.LO↗