Details of a Researcher - Okada, Mitsuhiro

Papers - Okada, Mitsuhiro

Division display 1 - 20 of about 132 ／ All the affair displays >>

Assessing Large Language Models with NeuBAROCO: Syllogistic Reasoning Ability and Biases,

Risako Ando, Hirohiko Abe, Takanobu Morishita, Koji Mineshima, Mitsuhiro Okada

ric. NAPTURAL LOGIC MEETS MACHINE LEARNING, June, 2023 (IWCS, LOGIC MEETS MACHINE LEARNING,) 4 2023.06

Last author, Accepted

Wittgenstein’s Struggle with Intuitionism, in Wittgenstein’s Philosophy in 1929

Mathieu Marion and Mitsuhir Okada

Studies in Twentieth-Century Philosophy) H 230 (Routledge) 230 1 - 16 2023.02

Part of collection (book), Joint Work, Corresponding author

Abductive Reasoning with Syllogistic Forms in Large Language Models

Abe H., Ando R., Morishita T., Ozeki K., Mineshima K., Okada M.

Lecture Notes in Computer Science 15504 LNCS 3 - 17 2025

ISSN 03029743

Research in AI using Large-Language Models (LLMs) is rapidly evolving, and the comparison of their performance with human reasoning has become a key concern. Prior studies have indicated that LLMs and humans share similar biases, such as dismissing logically valid inferences that contradict common beliefs. However, criticizing LLMs for these biases might be unfair, considering our reasoning not only involves formal deduction but also abduction, which draws tentative conclusions from limited information. Abduction can be regarded as the inverse form of syllogism in its basic structure, that is, a process of drawing a minor premise from a major premise and conclusion. This paper explores the accuracy of LLMs in abductive reasoning by converting a syllogistic dataset into one suitable for abduction. It aims to investigate whether the state-of-the-art LLMs exhibit biases in abduction and to identify potential areas for improvement, emphasizing the importance of contextualized reasoning beyond formal deduction. This investigation is vital for advancing the understanding and application of LLMs in complex reasoning tasks, offering insights into bridging the gap between machine and human cognition.

Access to Document (DOI)

An Eye-Tracking Study on the Effects of Using Highlighted Multi-attribute Tables: A Preliminary Report

Morii M., Ideno T., Tamari Y., Takemura K., Okada M.

Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics 14981 LNAI 467 - 471 2024

ISSN 03029743

Our previous research, aimed at improving the design of multi-attribute tables (such as product catalogs), found that black-and-white graphics aided decision-making more than numerical or textual formats (Ideno et al., Diagrams 2020). We extended these findings by examining how combining graphic and numerical presentation (highlighting the cells with superior values) influences decision-making. Twenty-one participants chose the most desirable digital cameras from five alternatives. Results showed faster decision-making with highlighted cells compared to non-highlighted ones. A two-stage decision strategy emerged, with more attribute-based gaze shifts initially and equal vertical and horizontal shifts later. We discussed the implications and prospects of highlighted multi-attribute tables.

Access to Document (DOI)

Can Euler Diagrams Improve Syllogistic Reasoning in Large Language Models?

Ando R., Ozeki K., Morishita T., Abe H., Mineshima K., Okada M.

Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics 14981 LNAI 232 - 248 2024

ISSN 03029743

In recent years, research on large language models (LLMs) has been advancing rapidly, making the evaluation of their reasoning abilities a crucial issue. Within cognitive science, there has been extensive research on human reasoning biases. It is widely observed that humans often use graphical representations as auxiliary tools during inference processes to avoid reasoning biases. However, currently, the evaluation of LLMs’ reasoning abilities has largely focused on linguistic inferences, with insufficient attention given to inferences using diagrams. In this study, we concentrate on syllogisms, a basic form of logical reasoning, and evaluate the reasoning abilities of LLMs supplemented by Euler diagrams. We systematically investigate how accurately LLMs can perform logical reasoning when using diagrams as auxiliary input and whether they exhibit similar reasoning biases to those of humans. Our findings indicate that, overall, providing diagrams as auxiliary input tends to improve models’ performance, including in problems that show reasoning biases, but the effect varies depending on the conditions, and the improvement in accuracy is not as high as that seen in humans. We present results from experiments conducted under multiple conditions, including a Chain-of-Thought setting, to highlight where there is room to improve logical diagrammatic reasoning abilities of LLMs.

Access to Document (DOI)

Exploring Reasoning Biases in Large Language Models Through Syllogism: Insights from the NeuBAROCO Dataset

Ozeki K., Ando R., Morishita T., Abe H., Mineshima K., Okada M.

Proceedings of the Annual Meeting of the Association for Computational Linguistics 16063 - 16077 2024

ISSN 0736587X

This paper explores the question of how accurately current large language models can perform logical reasoning in natural language, with an emphasis on whether these models exhibit reasoning biases similar to humans. Specifically, our study focuses on syllogistic reasoning, a form of deductive reasoning extensively studied in cognitive science as a natural form of human reasoning. We present a syllogism dataset called NeuBAROCO, which consists of syllogistic reasoning problems in English and Japanese. This dataset was originally designed for psychological experiments to assess human reasoning capabilities using various forms of syllogisms. Our experiments with leading large language models indicate that these models exhibit reasoning biases similar to humans, along with other error tendencies. Notably, there is significant room for improvement in reasoning problems where the relationship between premises and hypotheses is neither entailment nor contradiction. We also present experimental results and in-depth analysis using a new Chain-of-Thought prompting method, which asks LLMs to translate syllogisms into abstract logical expressions and then explain their reasoning process. Our analysis using this method suggests that the primary limitations of LLMs lie in the reasoning process itself rather than the interpretation of syllogisms.

Access to Document (DOI)

Evaluating Large Language Models with NeuBAROCO: Syllogistic Reasoning Ability and Human-like Biases

Ando R., Morishita T., Abe H., Mineshima K., Okada M.

Iwcs2023 Proceedings of the 4th Natural Logic Meets Machine Learning Workshop Naloma 2023 1 - 11 2023

This paper investigates whether current large language models exhibit biases in logical reasoning, similar to humans. Specifically, we focus on syllogistic reasoning, a well-studied form of inference in the cognitive science of human deduction. To facilitate our analysis, we introduce a dataset called NeuBAROCO, originally designed for psychological experiments that assess human logical abilities in syllogistic reasoning. The dataset consists of syllogistic inferences in both English and Japanese. We examine three types of biases observed in human syllogistic reasoning: belief biases, conversion errors, and atmosphere effects. Our findings demonstrate that current large language models struggle more with problems involving these three types of biases.

A Semantics for “Typically” in First-Order Default Reasoning

Bana G., Okada M.

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)) 12758 LNAI 3 - 20 2021

ISSN 03029743

We present a new semantics for first-order conditional logic, which is a generalization of that of Friedman, Halpern and Koller [7]. We utilize Fitting’s embedding of first-order classical logic in first-order S4 to define our semantics. We explain our semantics by showing how it works on the connective expressing “typically implies”. We argue that it has a number of good properties, in particular, it is more adjustable to special situations than that of [7]. For example, we can make sense of nested conditional implications even when a conditional implication does not necessarily hold on the entire set of possible worlds, but where-ever it is satisfied, the conclusion is typically satisfied.

Access to Document (DOI)

A Simplified Application of Howard’s Vector Notation System to Termination Proofs for Typed Lambda-Calculus Systems

Okada M., Takahashi Y.

ISSN 9783030635947

There have been some important methods of combining a recursive path ordering and Tait-Girard’s computability argument to provide an ordering for termination proofs of higher-order rewrite systems. The higher-order recursive path ordering HORPO by Jouannaud and Rubio and the computability path ordering CPO by Blanqui, Jouannaud and Rubio are examples of such an ordering. In this paper, we give a case study of yet another direction of such extension of recursive path ordering, avoiding Tait-Girard’s computability method plugged in the above mentioned works. This motivation comes from Lévy’s question in the RTA open problem 19, which asks for a reasonably straightforward interpretation of simply typed λ -calculus λ in a certain well founded ordering. As in the cases of HORPO and CPO, the addition of λ -abstraction and application into path orderings might be considered as one solution, but the following question still remains; can the termination of λ be proved by an interpretation in a first-order well founded ordering in the sense that λ -abstraction/application are not directly built in the ordering? Reconsidering one of Howard’s works on proof-theoretic studies, we introduce the path ordering with Howard algebra as a case study towards further studies on Lévy’s question. → →

Access to Document (DOI)

On Effects of Changing Multi-attribute Table Design on Decision Making: An Eye-Tracking Study

Ideno T., Morii M., Takemura K., Okada M.

ISSN 9783030542481

Information tables are often used for decision making. This study considers multi-attribute table designs from a diagrammatic perspective. We used two experiments to show how the decision-making strategies and performance are changed based on table design changes, using the eye-tracking method. We employed a multi-attribute catalog table with alternatives presented along the horizontal axis and attributes along the vertical axis in Experiment 1 and the opposite layout in Experiment 2. In each experiment, we used four different types of representations of the attribute values, and these values were restricted to two levels for comparison with previous works. The four types used were: (i) numerical representations, (ii) textual representations, (iii) black-and-white representations with black representing better values, and (iv) black-and-while representations with white representing better values. Our results suggest, among others, that (1) placing the alternatives along the vertical axis makes the table easier to decide in comparison to the opposite layout, and that (2) the two-stage decision strategy is taken with numerical representations and textual representations, while a single stage strategy is taken with the black-and-white representations. We also showed how the graphic black-and-white representations made decision-making easier, and how the order changes of alternatives and of attributes of a table influenced decision makers’ decision.

Access to Document (DOI)

A Small Remark on Hilbert’s Finitist View of Divisibility and Kanovich-Okada-Scedrov’s Logical Analysis of Real-Time Systems

Okada M.

ISSN 03029743

Hilbert remarked in the introductory part of his most famous finitism address (1925 [1]) that “[t]he infinite divisibility of a continuum is an operation that is present only in our thought”, which means that no natural event or matter is infinitely divisible in reality. We recall that Scedrov’s group including the author started logical analysis of real time systems with the principle similar to Hilbert’s no-infinite divisibility claim, in [2]. The author would like to note some early history of the group’s work on logical analysis of real time system as well as some remark related to Hilbert’s claim of no-infinite divisibility.

Access to Document (DOI)

Verification Methods for the Computationally Complete Symbolic Attacker Based on Indistinguishability

GERGEI BANA, ROHIT CHADHA, AJAY KUMAR EERALLA, MITSUHIRO OKADA

ACM Trans. Comput. Logic (Association for Computing Machinery) to appear ( 1 ) 2019.12

Research paper (scientific journal), Accepted, ISSN 15293785

© 2019 Copyright held by the owner/author(s). In recent years, a new approach has been developed for verifying security protocols with the aim of combining the benefits of symbolic attackers and the benefits of unconditional soundness: the technique of the computationally complete symbolic attacker of Bana and Comon (BC) [8]. In this article, we argue that the real breakthrough of this technique is the recent introduction of its version for indistinguishability [9], because, with the extensions we introduce here, for the first time, there is a computationally sound symbolic technique that is syntactically strikingly simple, to which translating standard computational security notions is a straightforward matter, and that can be effectively used for verification of not only equivalence properties but trace properties of protocols as well. We first fully develop the core elements of this newer version by introducing several new axioms. We illustrate the power and the diverse use of the introduced axioms on simple examples first. We introduce an axiom expressing the Decisional Diffie-Hellman property. We analyze the Diffie-Hellman key exchange, both in its simplest form and an authenticated version as well. We provide computationally sound verification of real-or-random secrecy of the Diffie-Hellman key exchange protocol formultiple sessions, without any restrictions on the computational implementation other than the DDH assumption. We also show authentication for a simplified version of the station-to-station protocol using UF-CMA assumption for digital signatures. Finally, we axiomatize IND-CPA, IND-CCA1, and IND-CCA2 security properties and illustrate their usage. We have formalized the axiomatic system in an interactive theorem prover, Coq, and have machine-checked the proofs of various auxiliary theorems and security properties of Diffie-Hellman and station-to-station protocol.

Access to Document (DOI)

Psychosocial Twin Cohort Studies in Japan: The Keio Twin Research Center (KoTReC)

Ando J., Fujisawa K.K., Hiraishi K., Shikishima C., Kawamoto T., Nozaki M., Yamagata S., Takahashi Y., Suzuki K., Someya Y., Ozaki K., Deno M., Tanaka M., Sasaki S., Toda T., Kobayashi K., Sakagami M., Okada M., Kijima N., Takizawa R., Murayama K.

Twin Research and Human Genetics (Twin Research and Human Genetics) 22 ( 6 ) 591 - 596 2019.12

ISSN 18324274

© The Author(s) 2020. The Keio Twin Research Center (KoTReC) was established in 2009 at Keio University to combine two longitudinal cohort projects - the Keio Twin Study (KTS) for adolescence and adulthood and the Tokyo Twin Cohort Project (ToTCoP) for infancy and childhood. KoTReC also conducted a two-time panel study of self-control and psychopathology in twin adolescence in 2012 and 2013 and three independent anonymous cross-sectional twin surveys (ToTcross) before 2012 - the ToTCross, the Junior and Senior High School Survey and the High School Survey. This article introduces the recent research designs of KoTReC and its publications.

Access to Document (DOI)

On quasi-ordinal diagrams

Mitsuhiro Okada and Yuta Takahashi

38-49, EPTCS 288, Post-Workshop Proceedings of the 10th EOTCS Post-Proceedings of Workshop on Computation with Terms and Graphs (TermGraph 2018) (FEPTCS) 38 - 49 2019.03

Research paper (international conference proceedings), Joint Work, Accepted

Following a Rule: Waismann's Version

<UMarion Mathieu and Okada, Mitsuhiro(/)-#HR

Publications of the Austrian Ludwig Wittgenstein Society – New Series (Austrian Ludwig Wittgenstein Society) 2019

Research paper (international conference proceedings), Joint Work

On quasi ordinal diagram systems

Okada M., Takahashi Y.

Electronic Proceedings in Theoretical Computer Science, EPTCS (Electronic Proceedings in Theoretical Computer Science, EPTCS) 288 38 - 49 2019

ISSN 20752180

© M. Okada & Y. Takahashi. The purposes of this note are the following two; we first generalize Okada-Takeuti’s well quasi ordinal diagram theory, utilizing the recent result of Dershowitz-Tzameret’s version of tree embedding theorem with gap conditions. Second, we discuss possible use of such strong ordinal notation systems for the purpose of a typical traditional termination proof method for term rewriting systems, especially for second-order (pattern-matching-based) rewriting systems including a rewrite-theoretic version of Buchholz’s hydra game.

Access to Document (DOI)

Qualitatively coherent representation makes decision-making easier with binary-colored multi-attribute tables: An eye-tracking study

Okada, M., Morii, M., Ideno, T., Takemura, K. & Okada, M

Frontiers in Psychology (Frontiers) 8(AUG), [1388]. 2017.08

Research paper (scientific journal), Joint Work, Accepted

Access to Document (DOI)

What is logic?

Mitsuhiro Okada

Proceedings of "Beyond Logic" cericy Meeting May 21-May 26, 2017 (Cersy) 2017.07

Research paper (international conference proceedings), Single Work

Semantics for “Enough-Certainty" and Fitting’s Embedding of Classical Logic in S4

Gergei Bana and Mitsuhiro Okada

LIPIcs, Leibniz International Proceeding Series (LIPIcs, Leibniz International Proceeding Series) 34(2016) ( article 23 ) 1 - 17 2016.08

Research paper (international conference proceedings), Accepted

Access to Document (DOI)

Syntactic Reduction in Husserl's early Phenomenology of Arithmetic

Mirja Hartimo and Mitsuhiro Okada

Synthese (Springer) 193 ( 3 ) 937 - 969 2016.03

Research paper (scientific journal), Joint Work, Accepted

Access to Document (DOI)

　 Previous page - Next page 　