-
zScore: A Universal Decentralised Reputation System for the Blockchain Economy
Authors:
Himanshu Udupi,
Ashutosh Sahoo,
Akshay S. P.,
Gurukiran S.,
Parag Paul,
Petrus C. Martens
Abstract:
Modern society functions on trust. The onchain economy, however, is built on the founding principles of trustless peer-to-peer interactions in an adversarial environment without a centralised body of trust and needs a verifiable system to quantify credibility to minimise bad economic activity. We provide a robust framework titled zScore, a core primitive for reputation derived from a wallet's onch…
▽ More
Modern society functions on trust. The onchain economy, however, is built on the founding principles of trustless peer-to-peer interactions in an adversarial environment without a centralised body of trust and needs a verifiable system to quantify credibility to minimise bad economic activity. We provide a robust framework titled zScore, a core primitive for reputation derived from a wallet's onchain behaviour using state-of-the-art AI neural network models combined with real-world credentials ported onchain through zkTLS. The initial results tested on retroactive data from lending protocols establish a strong correlation between a good zScore and healthy borrowing and repayment behaviour, making it a robust and decentralised alibi for creditworthiness; we highlight significant improvements from previous attempts by protocols like Cred showcasing its robustness. We also present a list of possible applications of our system in Section 5, thereby establishing its utility in rewarding actual value creation while filtering noise and suspicious activity and flagging malicious behaviour by bad actors.
△ Less
Submitted 17 February, 2025;
originally announced March 2025.
-
Substructural Parametricity
Authors:
C. B. Aberlé,
Chris Martens,
Frank Pfenning
Abstract:
Ordered, linear, and other substructural type systems allow us to expose deep properties of programs at the syntactic level of types. In this paper, we develop a family of unary logical relations that allow us to prove consequences of parametricity for a range of substructural type systems. A key idea is to parameterize the relation by an algebra, which we exemplify with a monoid and commutative m…
▽ More
Ordered, linear, and other substructural type systems allow us to expose deep properties of programs at the syntactic level of types. In this paper, we develop a family of unary logical relations that allow us to prove consequences of parametricity for a range of substructural type systems. A key idea is to parameterize the relation by an algebra, which we exemplify with a monoid and commutative monoid to interpret ordered and linear type systems, respectively. We prove the fundamental theorem of logical relations and apply it to deduce extensional properties of inhabitants of certain types. Examples include demonstrating that the ordered types for list append and reversal are inhabited by exactly one function, as are types of some tree traversals. Similarly, the linear type of the identity function on lists is inhabited only by permutations of the input. Our most advanced example shows that the ordered type of the list fold function is inhabited only by the fold function.
△ Less
Submitted 4 March, 2025;
originally announced March 2025.
-
Reasoning about Study Regulations in Answer Set Programming
Authors:
Susana Hahn,
Cedric Martens,
Amade Nemes,
Henry Otunuya,
Javier Romero,
Torsten Schaub,
Sebastian Schellhorn
Abstract:
We are interested in automating reasoning with and about study regulations, catering to various stakeholders, ranging from administrators, over faculty, to students at different stages. Our work builds on an extensive analysis of various study programs at the University of Potsdam. The conceptualization of the underlying principles provides us with a formal account of study regulations. In particu…
▽ More
We are interested in automating reasoning with and about study regulations, catering to various stakeholders, ranging from administrators, over faculty, to students at different stages. Our work builds on an extensive analysis of various study programs at the University of Potsdam. The conceptualization of the underlying principles provides us with a formal account of study regulations. In particular, the formalization reveals the properties of admissible study plans. With these at end, we propose an encoding of study regulations in Answer Set Programming that produces corresponding study plans. Finally, we show how this approach can be extended to a generic user interface for exploring study plans.
△ Less
Submitted 8 August, 2024;
originally announced August 2024.
-
One-Shot Method for Computing Generalized Winding Numbers
Authors:
Cedric Martens,
Mikhail Bessmeltsev
Abstract:
The generalized winding number is an essential part of the geometry processing toolkit, allowing to quantify how much a given point is inside a surface, often represented by a mesh or a point cloud, even when the surface is open, noisy, or non-manifold. Parameterized surfaces, which often contain intentional and unintentional gaps and imprecisions, would also benefit from a generalized winding num…
▽ More
The generalized winding number is an essential part of the geometry processing toolkit, allowing to quantify how much a given point is inside a surface, often represented by a mesh or a point cloud, even when the surface is open, noisy, or non-manifold. Parameterized surfaces, which often contain intentional and unintentional gaps and imprecisions, would also benefit from a generalized winding number. Standard methods to compute it, however, rely on a surface integral, challenging to compute without surface discretization, leading to loss of precision characteristic of parametric surfaces.
We propose an alternative method to compute a generalized winding number, based only on the surface boundary and the intersections of a single ray with the surface. For parametric surfaces, we show that all the necessary operations can be done via a Sum-of-Squares (SOS) formulation, thus computing generalized winding numbers without surface discretization with machine precision. We show that by discretizing only the boundary of the surface, this becomes an efficient method.
We demonstrate an application of our method to the problem of computing a generalized winding number of a surface represented by a curve network, where each curve loop is surfaced via Laplace equation. We use the Boundary Element Method to express the solution as a parametric surface, allowing us to apply our method without meshing the surfaces. As a bonus, we also demonstrate that for meshes with many triangles and a simple boundary, our method is faster than the hierarchical evaluation of the generalized winding number while still being precise.
We validate our algorithms theoretically, numerically, and by demonstrating a gallery of results \new{on a variety of parametric surfaces and meshes}, as well uses in a variety of applications, including voxelizations and boolean operations.
△ Less
Submitted 8 August, 2024;
originally announced August 2024.
-
InaGVAD : a Challenging French TV and Radio Corpus Annotated for Speech Activity Detection and Speaker Gender Segmentation
Authors:
David Doukhan,
Christine Maertens,
William Le Personnic,
Ludovic Speroni,
Reda Dehak
Abstract:
InaGVAD is an audio corpus collected from 10 French radio and 18 TV channels categorized into 4 groups: generalist radio, music radio, news TV, and generalist TV. It contains 277 1-minute-long annotated recordings aimed at representing the acoustic diversity of French audiovisual programs and was primarily designed to build systems able to monitor men's and women's speaking time in media. inaGVAD…
▽ More
InaGVAD is an audio corpus collected from 10 French radio and 18 TV channels categorized into 4 groups: generalist radio, music radio, news TV, and generalist TV. It contains 277 1-minute-long annotated recordings aimed at representing the acoustic diversity of French audiovisual programs and was primarily designed to build systems able to monitor men's and women's speaking time in media. inaGVAD is provided with Voice Activity Detection (VAD) and Speaker Gender Segmentation (SGS) annotations extended with overlap, speaker traits (gender, age, voice quality), and 10 non-speech event categories. Annotation distributions are detailed for each channel category. This dataset is partitioned into a 1h development and a 3h37 test subset, allowing fair and reproducible system evaluation. A benchmark of 6 freely available VAD software is presented, showing diverse abilities based on channel and non-speech event categories. Two existing SGS systems are evaluated on the corpus and compared against a baseline X-vector transfer learning strategy, trained on the development subset. Results demonstrate that our proposal, trained on a single - but diverse - hour of data, achieved competitive SGS results. The entire inaGVAD package; including corpus, annotations, evaluation scripts, and baseline training code; is made freely accessible, fostering future advancement in the domain.
△ Less
Submitted 6 June, 2024;
originally announced June 2024.
-
Finite-Choice Logic Programming
Authors:
Chris Martens,
Robert J. Simmons,
Michael Arntzenius
Abstract:
Logic programming, as exemplified by datalog, defines the meaning of a program as its unique smallest model: the deductive closure of its inference rules. However, many problems call for an enumeration of models that vary along some set of choices while maintaining structural and logical constraints -- there is no single canonical model. The notion of stable models for logic programs with negation…
▽ More
Logic programming, as exemplified by datalog, defines the meaning of a program as its unique smallest model: the deductive closure of its inference rules. However, many problems call for an enumeration of models that vary along some set of choices while maintaining structural and logical constraints -- there is no single canonical model. The notion of stable models for logic programs with negation has successfully captured programmer intuition about the set of valid solutions for such problems, giving rise to a family of programming languages and associated solvers known as answer set programming. Unfortunately, the definition of a stable model is frustratingly indirect, especially in the presence of rules containing free variables.
We propose a new formalism, finite-choice logic programming, that uses choice, not negation, to admit multiple solutions. Finite-choice logic programming contains all the expressive power of the stable model semantics, gives meaning to a new and useful class of programs, and enjoys a least-fixed-point interpretation over a novel domain. We present an algorithm for exploring the solution space and prove it correct with respect to our semantics. Our implementation, the Dusa logic programming language, has performance that compares favorably with state-of-the-art answer set solvers and exhibits more predictable scaling with problem size.
△ Less
Submitted 21 November, 2024; v1 submitted 29 May, 2024;
originally announced May 2024.
-
Exploring Consequences of Privacy Policies with Narrative Generation via Answer Set Programming
Authors:
Chinmaya Dabral,
Emma Tosch,
Chris Martens
Abstract:
Informed consent has become increasingly salient for data privacy and its regulation. Entities from governments to for-profit companies have addressed concerns about data privacy with policies that enumerate the conditions for personal data storage and transfer. However, increased enumeration of and transparency in data privacy policies has not improved end-users' comprehension of how their data m…
▽ More
Informed consent has become increasingly salient for data privacy and its regulation. Entities from governments to for-profit companies have addressed concerns about data privacy with policies that enumerate the conditions for personal data storage and transfer. However, increased enumeration of and transparency in data privacy policies has not improved end-users' comprehension of how their data might be used: not only are privacy policies written in legal language that users may struggle to understand, but elements of these policies may compose in such a way that the consequences of the policy are not immediately apparent.
We present a framework that uses Answer Set Programming (ASP) -- a type of logic programming -- to formalize privacy policies. Privacy policies thus become constraints on a narrative planning space, allowing end-users to forward-simulate possible consequences of the policy in terms of actors having roles and taking actions in a domain. We demonstrate through the example of the Health Insurance Portability and Accountability Act (HIPAA) how to use the system in various ways, including asking questions about possibilities and identifying which clauses of the law are broken by a given sequence of events.
△ Less
Submitted 13 December, 2022;
originally announced December 2022.
-
Deep Learning for Reaction-Diffusion Glioma Growth Modelling: Towards a Fully Personalised Model?
Authors:
Corentin Martens,
Antonin Rovai,
Daniele Bonatto,
Thierry Metens,
Olivier Debeir,
Christine Decaestecker,
Serge Goldman,
Gaetan Van Simaeys
Abstract:
Reaction-diffusion models have been proposed for decades to capture the growth of gliomas, the most common primary brain tumours. However, severe limitations regarding the estimation of the initial conditions and parameter values of such models have restrained their clinical use as a personalised tool. In this work, we investigate the ability of deep convolutional neural networks (DCNNs) to addres…
▽ More
Reaction-diffusion models have been proposed for decades to capture the growth of gliomas, the most common primary brain tumours. However, severe limitations regarding the estimation of the initial conditions and parameter values of such models have restrained their clinical use as a personalised tool. In this work, we investigate the ability of deep convolutional neural networks (DCNNs) to address the pitfalls commonly encountered in the field. Based on 1,200 synthetic tumours grown over real brain geometries derived from magnetic resonance (MR) data of 6 healthy subjects, we demonstrate the ability of DCNNs to reconstruct a whole tumour cell density distribution from only two imaging contours at a single time point. With an additional imaging contour extracted at a prior time point, we also demonstrate the ability of DCNNs to accurately estimate the individual diffusivity and proliferation parameters of the model. From this knowledge, the spatio-temporal evolution of the tumour cell density distribution at later time points can ultimately be precisely captured using the model. We finally show the applicability of our approach to MR data of a real glioblastoma patient. This approach may open the perspective of a clinical application of reaction-diffusion growth models for tumour prognosis and treatment planning.
△ Less
Submitted 26 November, 2021;
originally announced November 2021.
-
Novices' Learning Barriers When Using Code Examples in Open-Ended Programming
Authors:
Wengran Wang,
Archit Kwatra,
James Skripchuk,
Neeloy Gomes,
Alexandra Milliken,
Chris Martens,
Tiffany Barnes,
Thomas Price
Abstract:
Open-ended programming increases students' motivation by allowing them to solve authentic problems and connect programming to their own interests. However, such open-ended projects are also challenging, as they often encourage students to explore new programming features and attempt tasks that they have not learned before. Code examples are effective learning materials for students and are well-su…
▽ More
Open-ended programming increases students' motivation by allowing them to solve authentic problems and connect programming to their own interests. However, such open-ended projects are also challenging, as they often encourage students to explore new programming features and attempt tasks that they have not learned before. Code examples are effective learning materials for students and are well-suited to supporting open-ended programming. However, there is little work to understand how novices learn with examples during open-ended programming, and few real-world deployments of such tools. In this paper, we explore novices' learning barriers when interacting with code examples during open-ended programming. We deployed Example Helper, a tool that offers galleries of code examples to search and use, with 44 novice students in an introductory programming classroom, working on an open-ended project in Snap. We found three high-level barriers that novices encountered when using examples: decision, search and integration barriers. We discuss how these barriers arise and design opportunities to address them.
△ Less
Submitted 23 April, 2021;
originally announced April 2021.
-
Towards Action Model Learning for Player Modeling
Authors:
Abhijeet Krishnan,
Aaron Williams,
Chris Martens
Abstract:
Player modeling attempts to create a computational model which accurately approximates a player's behavior in a game. Most player modeling techniques rely on domain knowledge and are not transferable across games. Additionally, player models do not currently yield any explanatory insight about a player's cognitive processes, such as the creation and refinement of mental models. In this paper, we p…
▽ More
Player modeling attempts to create a computational model which accurately approximates a player's behavior in a game. Most player modeling techniques rely on domain knowledge and are not transferable across games. Additionally, player models do not currently yield any explanatory insight about a player's cognitive processes, such as the creation and refinement of mental models. In this paper, we present our findings with using action model learning (AML), in which an action model is learned given data in the form of a play trace, to learn a player model in a domain-agnostic manner. We demonstrate the utility of this model by introducing a technique to quantitatively estimate how well a player understands the mechanics of a game. We evaluate an existing AML algorithm (FAMA) for player modeling and develop a novel algorithm called Blackout that is inspired by player cognition. We compare Blackout with FAMA using the puzzle game Sokoban and show that Blackout generates better player models.
△ Less
Submitted 9 March, 2021;
originally announced March 2021.
-
Initial condition assessment for reaction-diffusion glioma growth models: A translational MRI/histology (in)validation study
Authors:
Corentin Martens,
Laetitia Lebrun,
Christine Decaestecker,
Thomas Vandamme,
Yves-Rémi Van Eycke,
Antonin Rovai,
Thierry Metens,
Olivier Debeir,
Serge Goldman,
Isabelle Salmon,
Gaetan Van Simaeys
Abstract:
Diffuse gliomas are highly infiltrative tumors whose early diagnosis and follow-up usually rely on magnetic resonance imaging (MRI). However, the limited sensitivity of this technique makes it impossible to directly assess the extent of the glioma cell invasion, leading to sub-optimal treatment planing. Reaction-diffusion growth models have been proposed for decades to extrapolate glioma cell infi…
▽ More
Diffuse gliomas are highly infiltrative tumors whose early diagnosis and follow-up usually rely on magnetic resonance imaging (MRI). However, the limited sensitivity of this technique makes it impossible to directly assess the extent of the glioma cell invasion, leading to sub-optimal treatment planing. Reaction-diffusion growth models have been proposed for decades to extrapolate glioma cell infiltration beyond margins visible on MRI and predict its spatial-temporal evolution. These models nevertheless require an initial condition, that is the tumor cell density values at every location of the brain at diagnosis time. Several works have proposed to relate the tumor cell density function to abnormality outlines visible on MRI but the underlying assumptions have never been verified so far. In this work we propose to verify these assumptions by stereotactic histological analysis of a non-operated brain with glioblastoma using a tailored 3D-printed slicer. Cell density maps are computed from histological slides using a deep learning approach. The density maps are then registered to a postmortem MR image and related to an MR-derived geodesic distance map to the tumor core. The relation between the edema outlines visible on T2 FLAIR MRI and the distance to the core is also investigated. Our results suggest that (i) the previously suggested exponential decrease of the tumor cell density with the distance to the tumor core is not unreasonable but (ii) the edema outlines may in general not correspond to a cell density iso-contour and (iii) the commonly adopted tumor cell density value at these outlines is likely overestimated. These findings highlight the limitations of using conventional MRI to derive glioma cell density maps and point out the need of validating other methods to initialize reaction-diffusion growth models and make them usable in clinical practice.
△ Less
Submitted 2 February, 2021;
originally announced February 2021.
-
An Object-Oriented Library for Heat Transfer Modelling and Simulation in Open Cell Foams
Authors:
Tobias M. Scheuermann,
Paul Kotyczka,
Christian Martens,
Haithem Louati,
Bernhard Maschke,
Marie-Line Zanota,
Isabelle Pitault
Abstract:
Metallic open cell foams have multiple applications in industry, e. g. as catalyst supports in chemical processes. Their regular or heterogeneous microscopic structure determines the macroscopic thermodynamic and chemical properties. We present an object-oriented python library that generates state space models for simulation and control from the microscopic foam data, which can be imported from t…
▽ More
Metallic open cell foams have multiple applications in industry, e. g. as catalyst supports in chemical processes. Their regular or heterogeneous microscopic structure determines the macroscopic thermodynamic and chemical properties. We present an object-oriented python library that generates state space models for simulation and control from the microscopic foam data, which can be imported from the image processing tool iMorph. The foam topology and the 3D geometric data are the basis for discrete modeling of the balance laws using the cell method. While the material structure imposes a primal chain complex to define discrete thermodynamic driving forces, the internal energy balance is evaluated on a second chain complex, which is constructed by topological duality. The heat exchange between the solid and the fluid phase is described based on the available surface data. We illustrate in detail the construction of the dual chain complexes, and we show how the structured discrete model directly maps to the software objects of the python code. As a test case, we present simulation results for a foam with a Kelvin cell structure, and compare them to a surrogate finite element model with homogeneous parameters.
△ Less
Submitted 6 February, 2020;
originally announced February 2020.
-
A Resourceful Reframing of Behavior Trees
Authors:
Chris Martens,
Eric Butler,
Joseph C. Osborn
Abstract:
Designers of autonomous agents, whether in physical or virtual environments, need to express nondeterminisim, failure, and parallelism in behaviors, as well as accounting for synchronous coordination between agents. Behavior Trees are a semi-formalism deployed widely for this purpose in the games industry, but with challenges to scalability, reasoning, and reuse of common sub-behaviors.
We prese…
▽ More
Designers of autonomous agents, whether in physical or virtual environments, need to express nondeterminisim, failure, and parallelism in behaviors, as well as accounting for synchronous coordination between agents. Behavior Trees are a semi-formalism deployed widely for this purpose in the games industry, but with challenges to scalability, reasoning, and reuse of common sub-behaviors.
We present an alternative formulation of behavior trees through a language design perspective, giving a formal operational semantics, type system, and corresponding implementation. We express specifications for atomic behaviors as linear logic formulas describing how they transform the environment, and our type system uses linear sequent calculus to derive a compositional type assignment to behavior tree expressions. These types expose the conditions required for behaviors to succeed and allow abstraction over parameters to behaviors, enabling the development of behavior "building blocks" amenable to compositional reasoning and reuse.
△ Less
Submitted 24 March, 2018;
originally announced March 2018.
-
"How Was Your Weekend?" A Generative Model of Phatic Conversation
Authors:
Hannah Morrison,
Chris Martens
Abstract:
Unspoken social rules, such as those that govern choosing a proper discussion topic and when to change discussion topics, guide conversational behaviors. We propose a computational model of conversation that can follow or break such rules, with participant agents that respond accordingly. Additionally, we demonstrate an application of the model: the Experimental Social Tutor (EST), a first step to…
▽ More
Unspoken social rules, such as those that govern choosing a proper discussion topic and when to change discussion topics, guide conversational behaviors. We propose a computational model of conversation that can follow or break such rules, with participant agents that respond accordingly. Additionally, we demonstrate an application of the model: the Experimental Social Tutor (EST), a first step toward a social skills training tool that generates human-readable conversation and a conversational guideline at each point in the dialogue. Finally, we discuss the design and results of a pilot study evaluating the EST. Results show that our model is capable of producing conversations that follow social norms.
△ Less
Submitted 12 February, 2018;
originally announced February 2018.
-
A Common Framework for Audience Interactivity
Authors:
Alina Striner,
Sasha Azad,
Chris Martens
Abstract:
Audience interactivity is interpreted differently across domains. This research develops a framework to describe audience interactivity across a broad range of experiences. We build on early work characterizing child audience interactivity experiences, expanding on these findings with an extensive review of literature in theater, games, and theme parks, paired with expert interviews in those domai…
▽ More
Audience interactivity is interpreted differently across domains. This research develops a framework to describe audience interactivity across a broad range of experiences. We build on early work characterizing child audience interactivity experiences, expanding on these findings with an extensive review of literature in theater, games, and theme parks, paired with expert interviews in those domains. The framework scaffolds interactivity as nested spheres of audience influence, and comprises a series of dimensions of audience interactivity including a Spectrum of Audience Interactivity. This framework aims to develop a common taxonomy for researchers and practitioners working with audience interactivity experiences.
△ Less
Submitted 27 March, 2018; v1 submitted 9 October, 2017;
originally announced October 2017.
-
A Generative Model of Group Conversation
Authors:
Hannah Morrison,
Chris Martens
Abstract:
Conversations with non-player characters (NPCs) in games are typically confined to dialogue between a human player and a virtual agent, where the conversation is initiated and controlled by the player. To create richer, more believable environments for players, we need conversational behavior to reflect initiative on the part of the NPCs, including conversations that include multiple NPCs who inte…
▽ More
Conversations with non-player characters (NPCs) in games are typically confined to dialogue between a human player and a virtual agent, where the conversation is initiated and controlled by the player. To create richer, more believable environments for players, we need conversational behavior to reflect initiative on the part of the NPCs, including conversations that include multiple NPCs who interact with one another as well as the player. We describe a generative computational model of group conversation between agents, an abstract simulation of discussion in a small group setting. We define conversational interactions in terms of rules for turn taking and interruption, as well as belief change, sentiment change, and emotional response, all of which are dependent on agent personality, context, and relationships. We evaluate our model using a parameterized expressive range analysis, observing correlations between simulation parameters and features of the resulting conversations. This analysis confirms, for example, that character personalities will predict how often they speak, and that heterogeneous groups of characters will generate more belief change.
△ Less
Submitted 21 June, 2017;
originally announced June 2017.
-
Deriving Quests from Open World Mechanics
Authors:
Ryan Alexander,
Chris Martens
Abstract:
Open world games present players with more freedom than games with linear progression structures. However, without clearly-defined objectives, they often leave players without a sense of purpose. Most of the time, quests and objectives are hand-authored and overlaid atop an open world's mechanics. But what if they could be generated organically from the gameplay itself? The goal of our project was…
▽ More
Open world games present players with more freedom than games with linear progression structures. However, without clearly-defined objectives, they often leave players without a sense of purpose. Most of the time, quests and objectives are hand-authored and overlaid atop an open world's mechanics. But what if they could be generated organically from the gameplay itself? The goal of our project was to develop a model of the mechanics in Minecraft that could be used to determine the ideal placement of objectives in an open world setting. We formalized the game logic of Minecraft in terms of logical rules that can be manipulated in two ways: they may be executed to generate graphs representative of the player experience when playing an open world game with little developer direction; and they may be statically analyzed to determine dependency orderings, feedback loops, and bottlenecks. These analyses may then be used to place achievements on gameplay actions algorithmically.
△ Less
Submitted 30 April, 2017;
originally announced May 2017.
-
Languages of Play: Towards semantic foundations for game interfaces
Authors:
Chris Martens,
Matthew A. Hammer
Abstract:
Formal models of games help us account for and predict behavior, leading to more robust and innovative designs. While the games research community has proposed many formalisms for both the "game half" (game models, game description languages) and the "human half" (player modeling) of a game experience, little attention has been paid to the interface between the two, particularly where it concerns…
▽ More
Formal models of games help us account for and predict behavior, leading to more robust and innovative designs. While the games research community has proposed many formalisms for both the "game half" (game models, game description languages) and the "human half" (player modeling) of a game experience, little attention has been paid to the interface between the two, particularly where it concerns the player expressing her intent toward the game. We describe an analytical and computational toolbox based on programming language theory to examine the phenomenon sitting between control schemes and game rules, which we identify as a distinct player intent language for each game.
△ Less
Submitted 15 March, 2017;
originally announced March 2017.
