Showing 1–16 of 16 results for author: Nishida, N

Recent Trends in Personalized Dialogue Generation: A Review of Datasets, Methodologies, and Evaluations

Authors: Yi-Pei Chen, Noriki Nishida, Hideki Nakayama, Yuji Matsumoto

Abstract: Enhancing user engagement through personalization in conversational agents has gained significance, especially with the advent of large language models that generate fluent responses. Personalized dialogue generation, however, is multifaceted and varies in its definition -- ranging from instilling a persona in the agent to capturing users' explicit and implicit cues. This paper seeks to systemical… ▽ More Enhancing user engagement through personalization in conversational agents has gained significance, especially with the advent of large language models that generate fluent responses. Personalized dialogue generation, however, is multifaceted and varies in its definition -- ranging from instilling a persona in the agent to capturing users' explicit and implicit cues. This paper seeks to systemically survey the recent landscape of personalized dialogue generation, including the datasets employed, methodologies developed, and evaluation metrics applied. Covering 22 datasets, we highlight benchmark datasets and newer ones enriched with additional features. We further analyze 17 seminal works from top conferences between 2021-2023 and identify five distinct types of problems. We also shed light on recent progress by LLMs in personalized dialogue generation. Our evaluation section offers a comprehensive summary of assessment facets and metrics utilized in these works. In conclusion, we discuss prevailing challenges and envision prospect directions for future research in personalized dialogue generation. △ Less

Submitted 28 May, 2024; originally announced May 2024.

Comments: Presented in LREC-COLING 2024

Equational Theories and Validity for Logically Constrained Term Rewriting (Full Version)

Authors: Takahito Aoto, Naoki Nishida, Jonas Schöpf

Abstract: Logically constrained term rewriting is a relatively new formalism where rules are equipped with constraints over some arbitrary theory. Although there are many recent advances with respect to rewriting induction, completion, complexity analysis and confluence analysis for logically constrained term rewriting, these works solely focus on the syntactic side of the formalism lacking detailed investi… ▽ More Logically constrained term rewriting is a relatively new formalism where rules are equipped with constraints over some arbitrary theory. Although there are many recent advances with respect to rewriting induction, completion, complexity analysis and confluence analysis for logically constrained term rewriting, these works solely focus on the syntactic side of the formalism lacking detailed investigations on semantics. In this paper, we investigate a semantic side of logically constrained term rewriting. To this end, we first define constrained equations, constrained equational theories and validity of the former based on the latter. After presenting the relationship of validity and conversion of rewriting, we then construct a sound inference system to prove validity of constrained equations in constrained equational theories. Finally, we give an algebraic semantics, which enables one to establish invalidity of constrained equations in constrained equational theories. This algebraic semantics derive a new notion of consistency for constrained equational theories. △ Less

Submitted 5 July, 2024; v1 submitted 2 May, 2024; originally announced May 2024.

Comments: Accepted at the 9th International Conference on Formal Structures for Computation and Deduction 2024

On Singleton Self-Loop Removal for Termination of LCTRSs with Bit-Vector Arithmetic

Authors: Ayuka Matsumi, Naoki Nishida, Misaki Kojima, Donghoon Shin

Abstract: As for term rewrite systems, the dependency pair (DP, for short) framework with several kinds of DP processors is useful for proving termination of logically constrained term rewrite systems (LCTRSs, for short). However, the polynomial interpretation processor is not so effective against LCTRSs with bit-vector arithmetic (BV-LCTRSs, for short). In this paper, we propose a novel DP processor for BV… ▽ More As for term rewrite systems, the dependency pair (DP, for short) framework with several kinds of DP processors is useful for proving termination of logically constrained term rewrite systems (LCTRSs, for short). However, the polynomial interpretation processor is not so effective against LCTRSs with bit-vector arithmetic (BV-LCTRSs, for short). In this paper, we propose a novel DP processor for BV-LCTRSs to solve a singleton DP problem consisting of a dependency pair forming a self-loop. The processor is based on an acyclic directed graph such that the nodes are bit-vectors and any dependency chain of the problem is projected to a path of the graph. We show a sufficient condition for the existence of such an acyclic graph, and simplify it for a specific case. △ Less

Submitted 26 July, 2023; originally announced July 2023.

Comments: Presented at WST 2023

On Transforming Narrowing Trees into Regular Tree Grammars Generating Ranges of Substitutions

Authors: Naoki Nishida, Yuya Maeda

Abstract: The grammar representation of a narrowing tree for a syntactically deterministic conditional term rewriting system and a pair of terms is a regular tree grammar that generates expressions for substitutions obtained by all possible innermost-narrowing derivations that start with the pair and end with particular non-narrowable terms. In this paper, under a certain syntactic condition, we show a tran… ▽ More The grammar representation of a narrowing tree for a syntactically deterministic conditional term rewriting system and a pair of terms is a regular tree grammar that generates expressions for substitutions obtained by all possible innermost-narrowing derivations that start with the pair and end with particular non-narrowable terms. In this paper, under a certain syntactic condition, we show a transformation of the grammar representation of a narrowing tree into another regular tree grammar that overapproximately generates the ranges of ground substitutions generated by the grammar representation. In our previous work, such a transformation is restricted to the ranges w.r.t. a given single variable, and thus, the usefulness is limited. We extend the previous transformation by representing the range of a ground substitution as a tuple of terms, which is obtained by the coding for finite trees. We show a precise definition of the transformation and prove that the language of the transformed regular tree grammar is an overapproximation of the ranges of ground substitutions generated by the grammar representation. We leave an experiment to evaluate the usefulness of the transformation as future work. △ Less

Submitted 22 February, 2019; originally announced February 2019.

Comments: In Proceedings WPTE 2018, arXiv:1902.07818

ACM Class: F.4.2

Journal ref: EPTCS 289, 2019, pp. 68-87

On Transforming Functions Accessing Global Variables into Logically Constrained Term Rewriting Systems

Authors: Yoshiaki Kanazawa, Naoki Nishida

Abstract: In this paper, we show a new approach to transformations of an imperative program with function calls and global variables into a logically constrained term rewriting system. The resulting system represents transitions of the whole execution environment with a call stack. More precisely, we prepare a function symbol for the whole environment, which stores values for global variables and a call sta… ▽ More In this paper, we show a new approach to transformations of an imperative program with function calls and global variables into a logically constrained term rewriting system. The resulting system represents transitions of the whole execution environment with a call stack. More precisely, we prepare a function symbol for the whole environment, which stores values for global variables and a call stack as its arguments. For a function call, we prepare rewrite rules to push the frame to the stack and to pop it after the execution. Any running frame is located at the top of the stack, and statements accessing global variables are represented by rewrite rules for the environment symbol. We show a precise transformation based on the approach and prove its correctness. △ Less

Submitted 22 February, 2019; originally announced February 2019.

Comments: In Proceedings WPTE 2018, arXiv:1902.07818

ACM Class: F.4.2; F.1.1

Journal ref: EPTCS 289, 2019, pp. 34-52

MOBIUS: Model-Oblivious Binarized Neural Networks

Authors: Hiromasa Kitai, Jason Paul Cruz, Naoto Yanai, Naohisa Nishida, Tatsumi Oba, Yuji Unagami, Tadanori Teruya, Nuttapong Attrapadung, Takahiro Matsuda, Goichiro Hanaoka

Abstract: A privacy-preserving framework in which a computational resource provider receives encrypted data from a client and returns prediction results without decrypting the data, i.e., oblivious neural network or encrypted prediction, has been studied in machine learning that provides prediction services. In this work, we present MOBIUS (Model-Oblivious BInary neUral networkS), a new system that combines… ▽ More A privacy-preserving framework in which a computational resource provider receives encrypted data from a client and returns prediction results without decrypting the data, i.e., oblivious neural network or encrypted prediction, has been studied in machine learning that provides prediction services. In this work, we present MOBIUS (Model-Oblivious BInary neUral networkS), a new system that combines Binarized Neural Networks (BNNs) and secure computation based on secret sharing as tools for scalable and fast privacy-preserving machine learning. BNNs improve computational performance by binarizing values in training to $-1$ and $+1$, while secure computation based on secret sharing provides fast and various computations under encrypted forms via modulo operations with a short bit length. However, combining these tools is not trivial because their operations have different algebraic structures and the use of BNNs downgrades prediction accuracy in general. MOBIUS uses improved procedures of BNNs and secure computation that have compatible algebraic structures without downgrading prediction accuracy. We created an implementation of MOBIUS in C++ using the ABY library (NDSS 2015). We then conducted experiments using the MNIST dataset, and the results show that MOBIUS can return a prediction within 0.76 seconds, which is six times faster than SecureML (IEEE S\&P 2017). MOBIUS allows a client to request for encrypted prediction and allows a trainer to obliviously publish an encrypted model to a cloud provided by a computational resource provider, i.e., without revealing the original model itself to the provider. △ Less

Submitted 29 November, 2018; originally announced November 2018.

Journal ref: IEEE Access (Volume: 7, Issue:1. 04 September 2019)

A Theory of Reversibility for Erlang

Authors: Ivan Lanese, Naoki Nishida, Adrián Palacios, Germán Vidal

Abstract: In a reversible language, any forward computation can be undone by a finite sequence of backward steps. Reversible computing has been studied in the context of different programming languages and formalisms, where it has been used for testing and verification, among others. In this paper, we consider a subset of Erlang, a functional and concurrent programming language based on the actor model. We… ▽ More In a reversible language, any forward computation can be undone by a finite sequence of backward steps. Reversible computing has been studied in the context of different programming languages and formalisms, where it has been used for testing and verification, among others. In this paper, we consider a subset of Erlang, a functional and concurrent programming language based on the actor model. We present a formal semantics for reversible computation in this language and prove its main properties, including its causal consistency. We also build on top of it a rollback operator that can be used to undo the actions of a process up to a given checkpoint. △ Less

Submitted 19 June, 2018; originally announced June 2018.

Comments: To appear in the Journal of Logical and Algebraic Methods in Programming (Elsevier)

Transforming Dependency Chains of Constrained TRSs into Bounded Monotone Sequences of Integers

Authors: Tomohiro Sasano, Naoki Nishida, Masahiko Sakai, Tomoya Ueyama

Abstract: In the dependency pair framework for proving termination of rewriting systems, polynomial interpretations are used to transform dependency chains into bounded decreasing sequences of integers, and they play an important role for the success of proving termination, especially for constrained rewriting systems. In this paper, we show sufficient conditions of linear polynomial interpretations for tra… ▽ More In the dependency pair framework for proving termination of rewriting systems, polynomial interpretations are used to transform dependency chains into bounded decreasing sequences of integers, and they play an important role for the success of proving termination, especially for constrained rewriting systems. In this paper, we show sufficient conditions of linear polynomial interpretations for transforming dependency chains into bounded monotone (i.e., decreasing or increasing) sequences of integers. Such polynomial interpretations transform rewrite sequences of the original system into decreasing or increasing sequences independently of the transformation of dependency chains. When we transform rewrite sequences into increasing sequences, polynomial interpretations have non-positive coefficients for reducible positions of marked function symbols. We propose four DP processors parameterized by transforming dependency chains and rewrite sequences into either decreasing or increasing sequences of integers, respectively. We show that such polynomial interpretations make us succeed in proving termination of the McCarthy 91 function over the integers. △ Less

Submitted 18 February, 2018; originally announced February 2018.

Comments: In Proceedings WPTE 2017, arXiv:1802.05862

ACM Class: F.4.2

Journal ref: EPTCS 265, 2018, pp. 82-97

Transforming Proof Tableaux of Hoare Logic into Inference Sequences of Rewriting Induction

Authors: Shinnosuke Mizutani, Naoki Nishida

Abstract: A proof tableau of Hoare logic is an annotated program with pre- and post-conditions, which corresponds to an inference tree of Hoare logic. In this paper, we show that a proof tableau for partial correctness can be transformed into an inference sequence of rewriting induction for constrained rewriting. We also show that the resulting sequence is a valid proof for an inductive theorem correspondin… ▽ More A proof tableau of Hoare logic is an annotated program with pre- and post-conditions, which corresponds to an inference tree of Hoare logic. In this paper, we show that a proof tableau for partial correctness can be transformed into an inference sequence of rewriting induction for constrained rewriting. We also show that the resulting sequence is a valid proof for an inductive theorem corresponding to the Hoare triple if the constrained rewriting system obtained from the program is terminating. Such a valid proof with termination of the constrained rewriting system implies total correctness of the program w.r.t. the Hoare triple. The transformation enables us to apply techniques for proving termination of constrained rewriting to proving total correctness of programs together with proof tableaux for partial correctness. △ Less

Submitted 18 February, 2018; originally announced February 2018.

Comments: In Proceedings WPTE 2017, arXiv:1802.05862

ACM Class: F.4.2

Journal ref: EPTCS 265, 2018, pp. 35-51

Reversible Computation in Term Rewriting

Authors: Naoki Nishida, Adrián Palacios, Germán Vidal

Abstract: Essentially, in a reversible programming language, for each forward computation from state $S$ to state $S'$, there exists a constructive method to go backwards from state $S'$ to state $S$. Besides its theoretical interest, reversible computation is a fundamental concept which is relevant in many different areas like cellular automata, bidirectional program transformation, or quantum computing, t… ▽ More Essentially, in a reversible programming language, for each forward computation from state $S$ to state $S'$, there exists a constructive method to go backwards from state $S'$ to state $S$. Besides its theoretical interest, reversible computation is a fundamental concept which is relevant in many different areas like cellular automata, bidirectional program transformation, or quantum computing, to name a few. In this work, we focus on term rewriting, a computation model that underlies most rule-based programming languages. In general, term rewriting is not reversible, even for injective functions; namely, given a rewrite step $t_1 \rightarrow t_2$, we do not always have a decidable method to get $t_1$ from $t_2$. Here, we introduce a conservative extension of term rewriting that becomes reversible. Furthermore, we also define two transformations, injectivization and inversion, to make a rewrite system reversible using standard term rewriting. We illustrate the usefulness of our transformations in the context of bidirectional program transformation. △ Less

Submitted 8 October, 2017; originally announced October 2017.

Comments: To appear in the Journal of Logical and Algebraic Methods in Programming

Sound Structure-Preserving Transformation for Weakly-Left-Linear Deterministic Conditional Term Rewriting Systems

Authors: Ryota Nakayama, Naoki Nishida, Masahiko Sakai

Abstract: In this paper, we show that the SR transformation, a computationally equivalent transformation proposed by Serbanuta and Rosu, is a sound structure-preserving transformation for weakly-left-linear deterministic conditional term rewriting systems. More precisely, we show that every weakly-left-linear deterministic conditional term rewriting system can be converted to an equivalent weakly-left-linea… ▽ More In this paper, we show that the SR transformation, a computationally equivalent transformation proposed by Serbanuta and Rosu, is a sound structure-preserving transformation for weakly-left-linear deterministic conditional term rewriting systems. More precisely, we show that every weakly-left-linear deterministic conditional term rewriting system can be converted to an equivalent weakly-left-linear and ultra-weakly-left-linear deterministic conditional term rewriting system and prove that the SR transformation is sound for weakly-left-linear and ultra-weakly-left-linear deterministic conditional term rewriting systems. Here, soundness for a conditional term rewriting system means that reduction of the transformed unconditional term rewriting system creates no undesired reduction sequence for the conditional system. △ Less

Submitted 3 January, 2017; originally announced January 2017.

Comments: In Proceedings WPTE 2016, arXiv:1701.00233

ACM Class: F.4.2 Grammars and Other Rewriting Systems

Journal ref: EPTCS 235, 2017, pp. 62-77

Zero-resource Machine Translation by Multimodal Encoder-decoder Network with Multimedia Pivot

Authors: Hideki Nakayama, Noriki Nishida

Abstract: We propose an approach to build a neural machine translation system with no supervised resources (i.e., no parallel corpora) using multimodal embedded representation over texts and images. Based on the assumption that text documents are often likely to be described with other multimedia information (e.g., images) somewhat related to the content, we try to indirectly estimate the relevance between… ▽ More We propose an approach to build a neural machine translation system with no supervised resources (i.e., no parallel corpora) using multimodal embedded representation over texts and images. Based on the assumption that text documents are often likely to be described with other multimedia information (e.g., images) somewhat related to the content, we try to indirectly estimate the relevance between two languages. Using multimedia as the "pivot", we project all modalities into one common hidden space where samples belonging to similar semantic concepts should come close to each other, whatever the observed space of each sample is. This modality-agnostic representation is the key to bridging the gap between different modalities. Putting a decoder on top of it, our network can flexibly draw the outputs from any input modality. Notably, in the testing phase, we need only source language texts as the input for translation. In experiments, we tested our method on two benchmarks to show that it can achieve reasonable translation performance. We compared and investigated several possible implementations and found that an end-to-end model that simultaneously optimized both rank loss in multimodal encoders and cross-entropy loss in decoders performed the best. △ Less

Submitted 23 July, 2017; v1 submitted 14 November, 2016; originally announced November 2016.

Comments: Some error corrections in Sect.2.2 and Table 5, Machine Translation, 2017

Towards Reversible Computation in Erlang

Authors: Naoki Nishida, Adrián Palacios, Germán Vidal

Abstract: In a reversible language, any forward computation can be undone by a finite sequence of backward steps. Reversible computing has been studied in the context of different programming languages and formalisms, where it has been used for debugging and for enforcing fault-tolerance, among others. In this paper, we consider a subset of Erlang, a concurrent language based on the actor model. We formally… ▽ More In a reversible language, any forward computation can be undone by a finite sequence of backward steps. Reversible computing has been studied in the context of different programming languages and formalisms, where it has been used for debugging and for enforcing fault-tolerance, among others. In this paper, we consider a subset of Erlang, a concurrent language based on the actor model. We formally introduce a reversible semantics for this language. To the best of our knowledge, this is the first attempt to define a reversible semantics for Erlang. △ Less

Submitted 19 August, 2016; originally announced August 2016.

Comments: Pre-proceedings paper presented at the 26th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2016), Edinburgh, Scotland UK, 6-8 September 2016 (arXiv:1608.02534)

Report number: LOPSTR/2016/20

Verifying Procedural Programs via Constrained Rewriting Induction

Authors: Carsten Fuhs, Cynthia Kop, Naoki Nishida

Abstract: This paper aims to develop a verification method for procedural programs via a transformation into Logically Constrained Term Rewriting Systems (LCTRSs). To this end, we extend transformation methods based on integer TRSs to handle arbitrary data types, global variables, function calls and arrays, as well as encode safety checks. Then we adapt existing rewriting induction methods to LCTRSs and pro… ▽ More This paper aims to develop a verification method for procedural programs via a transformation into Logically Constrained Term Rewriting Systems (LCTRSs). To this end, we extend transformation methods based on integer TRSs to handle arbitrary data types, global variables, function calls and arrays, as well as encode safety checks. Then we adapt existing rewriting induction methods to LCTRSs and propose a simple yet effective method to generalize equations. We show that we can automatically verify memory safety and prove correctness of realistic functions. Our approach proves equivalence between two implementations, so in contrast to other works, we do not require an explicit specification in a separate specification language. △ Less

Submitted 25 February, 2017; v1 submitted 30 August, 2014; originally announced September 2014.

ACM Class: D.2.4; I.2.3

On Constructing Constrained Tree Automata Recognizing Ground Instances of Constrained Terms

Authors: Naoki Nishida, Masahiko Sakai, Yasuhiro Nakano

Abstract: An inductive theorem proving method for constrained term rewriting systems, which is based on rewriting induction, needs a decision procedure for reduction-completeness of constrained terms. In addition, the sufficient complete property of constrained term rewriting systems enables us to relax the side conditions of some inference rules in the proving method. These two properties can be reduced to… ▽ More An inductive theorem proving method for constrained term rewriting systems, which is based on rewriting induction, needs a decision procedure for reduction-completeness of constrained terms. In addition, the sufficient complete property of constrained term rewriting systems enables us to relax the side conditions of some inference rules in the proving method. These two properties can be reduced to intersection emptiness problems related to sets of ground instances for constrained terms. This paper proposes a method to construct deterministic, complete, and constraint-complete constrained tree automata recognizing ground instances of constrained terms. △ Less

Submitted 21 November, 2013; originally announced November 2013.

Comments: In Proceedings TTATT 2013, arXiv:1311.5058

ACM Class: F.1.1 Automata

Journal ref: EPTCS 134, 2013, pp. 1-10

Soundness of Unravelings for Conditional Term Rewriting Systems via Ultra-Properties Related to Linearity

Authors: Naoki Nishida, Masahiko Sakai, Toshiki Sakabe

Abstract: Unravelings are transformations from a conditional term rewriting system (CTRS, for short) over an original signature into an unconditional term rewriting systems (TRS, for short) over an extended signature. They are not sound w.r.t. reduction for every CTRS, while they are complete w.r.t. reduction. Here, soundness w.r.t. reduction means that every reduction sequence of the corresponding unravel… ▽ More Unravelings are transformations from a conditional term rewriting system (CTRS, for short) over an original signature into an unconditional term rewriting systems (TRS, for short) over an extended signature. They are not sound w.r.t. reduction for every CTRS, while they are complete w.r.t. reduction. Here, soundness w.r.t. reduction means that every reduction sequence of the corresponding unraveled TRS, of which the initial and end terms are over the original signature, can be simulated by the reduction of the original CTRS. In this paper, we show that an optimized variant of Ohlebusch's unraveling for a deterministic CTRS is sound w.r.t. reduction if the corresponding unraveled TRS is left-linear or both right-linear and non-erasing. We also show that soundness of the variant implies that of Ohlebusch's unraveling. Finally, we show that soundness of Ohlebusch's unraveling is the weakest in soundness of the other unravelings and a transformation, proposed by Serbanuta and Rosu, for (normal) deterministic CTRSs, i.e., soundness of them respectively implies that of Ohlebusch's unraveling. △ Less

Submitted 9 August, 2012; v1 submitted 25 June, 2012; originally announced June 2012.

Comments: 49 pages, 1 table, publication in Special Issue: Selected papers of the "22nd International Conference on Rewriting Techniques and Applications (RTA'11)"

ACM Class: F.4.2

Journal ref: Logical Methods in Computer Science, Volume 8, Issue 3 (August 10, 2012) lmcs:669