Informes técnicos de investigación DSIC-ELP

Colección de documentos de trabajo, informes técnicos y otro material de investigación realizado por los investigadores del Departamento de Sistemas Informáticos y Computación (DSIC). Grupo ELP: Extensiones de la Programación Lógica (Extensions of Logic Programming) de la Universitat Politècnica de València en el desarrollo de sus investigaciones.

URI permanente para esta colecciónhttps://riunet.upv.es/handle/10251/8351

Examinar

Mostrando 1 - 16 de 16

Access status: Abierto ,
Contamination Budget: Trade-offs between Breadth, Depth and Difficulty
(2025-05-22) Mehrbakhsh, Behzad; Hernández-Orallo, José; Martínez-Plumed, Fernando; Departamento de Sistemas Informáticos y Computación; Escuela Técnica Superior de Ingeniería Informática; Instituto Universitario Valenciano de Investigación en Inteligencia Artificial; European Commission; European Regional Development Fund; Generalitat Valenciana; Agencia Estatal de Investigación
Contamination in large language models (LLMs), and machine learning more broadly, refers to the inclusion of equal –or very similar– examples in both training and test sets. This phenomenon usually translates into better test performance. Here we explore when this contamination is performed intentionally, for purposes that can be malicious (e.g., get better scores in evaluations) or benevolent (e.g., fix some mistakes). These interventions, usually in the form of fine-tuning memorisations, come with a budget in the size of the fine-tuning dataset. Several trade-offs appear between the breadth of the intervention (how many examples to be memorised), its depth (how many repetitions of each example) and the difficulty of the examples. By studying several LLMs and datasets, we observe some monotonic behaviour (more difficult items require more depth to be ‘fixed’) but also some non-monotonic phenomena (very high depth levels have negative effects on non-contaminated examples). This suggests that trade-offs should be found not only in terms of the budget but also according to model specifics, the task and the item difficulty at hand.
Access status: Abierto ,
A Probabilistic Framework for Non-Cheating Machine Teaching
(2022-05-03) Ferri Ramírez, César; Hernández-Orallo, José; Telle, Jan Arne; Departamento de Sistemas Informáticos y Computación; Escuela Técnica Superior de Ingeniería Informática; Instituto Universitario Valenciano de Investigación en Inteligencia Artificial
Over the past decades in the field of machine teaching, several restrictions have been introduced to avoid ‘cheating’, such as collusion-free or non-clashing teaching. However, these restrictions forbid several teaching situations that we intuitively consider natural and fair, especially those ‘changes of mind’ of the learner as more evidence is given, affecting the likelihood of concepts and ultimately their posteriors. Under a new generalised probabilistic teaching, not only do these non-cheating constraints look too narrow but we also show that the most relevant machine teaching models are particular cases of this framework: the consistency graph between concepts and elements simply becomes a joint probability distribution. We show a simple procedure that builds the witness joint distribution from the ground joint distribution. We prove a chain of relations, also with a theoretical lower bound, on the teaching dimension of the old and new models. Overall, this new setting is more general than the traditional machine teaching models, yet at the same time more intuitively capturing a less abrupt notion of non-cheating teaching.
Access status: Abierto ,
Narrowing-based Optimization of Rewrite Theories
(Universitat Politècnica de València, 2020-06-08) Alpuente Frasnedo, María; Ballis, Demis; Escobar Román, Santiago; Sapiña-Sanchis, Julia; Departamento de Sistemas Informáticos y Computación; Escuela Técnica Superior de Ingeniería Informática; Instituto Universitario Valenciano de Investigación en Inteligencia Artificial; Agencia Estatal de Investigación; Generalitat Valenciana
Partial evaluation has been never investigated in the context of rewrite theories that allow concurrent systems to be specified by means of rules, with an underlying equational theory being used to model system states as terms of an algebraic data type. In this paper, we develop a symbolic, narrowing-driven partial evaluation framework for rewrite theories that supports sorts, subsort overloading, rules, equations, and algebraic axioms. Our partial evaluation scheme allows a rewrite theory to be optimized by specializing the plugged equational theory with respect to the rewrite rules that define the system dynamics. This can be particularly useful for automatically optimizing rewrite theories that contain overly general equational theories which perform unnecessary computations involving matching modulo axioms, because some of the axioms may be blown away after the transformation. The specialization is done by using appropriate unfolding and abstraction algorithms that achieve significant specialization while ensuring the correctness and termination of the specialization. Our preliminary results demonstrate that our transformation can speed up a number of benchmarks that are difficult to optimize otherwise.
Access status: Abierto ,
Abstract Contract Synthesis and Verification in the Symbolic K Framework
(Universitat Politècnica de València, 2018-04-12) Alpuente Frasnedo, María; Pardo Pont, Daniel; Villanueva, Alicia; Departamento de Sistemas Informáticos y Computación; Escuela Técnica Superior de Ingeniería Informática; Instituto Universitario Valenciano de Investigación en Inteligencia Artificial; European Regional Development Fund; Ministerio de Economía y Competitividad; Ministerio de Educación, Cultura y Deporte; Generalitat Valenciana
[EN] In this article, we propose a symbolic technique that can be used for automatically inferring software contracts from programs that are written in a non-trivial fragment of C, called KernelC, that supports pointer-based structures and heap manipulation. Starting from the semantic definition of KernelC in the K semantic framework, we enrich the symbolic execution facilities recently provided by K with novel capabilities for contract synthesis that are based on abstract subsumption. Roughly speaking, we define an abstract symbolic technique that axiomatically explains the execution of any (modifier) C function by using other (observer) routines in the same program. We implemented our technique in the automated tool KindSpec 2.1, which generates logical axioms that express pre- and postcondition assertions which define the precise input/output behavior of the C routines. Thanks to the integrated support for symbolic execution and deductive verification provided by K, some synthesized axioms that cannot be guaranteed to be correct by construction due to abstraction can finally be verified in our framework with little effort.
Access status: Abierto ,
Static Correction of Maude Programs with Assertions
(Universitat Politècnica de València, 2018-04-12) Alpuente Frasnedo, María; Ballis, D.; Sapiña-Sanchis, Julia; Departamento de Sistemas Informáticos y Computación; Escuela Técnica Superior de Ingeniería Informática; Instituto Universitario Valenciano de Investigación en Inteligencia Artificial; Generalitat Valenciana
In this paper, we present a novel transformation method for Maude programs featuring both automatic program diagnosis and correction. The input of our method is a reference specification A of the program behavior that is given in the form of assertions together with an overly general program R whose execution might violate the assertions. Our technique translates R into a refined program R' in which every computation is a computation in R that satisfies the assertions of A. Our correction technique is first formalized for topmost rewrite theories, and then we generalize it to larger rewrite theories that support nested structured configurations. Our technique copes with infinite space states and does not require the knowledge of any failing run. We report experiments that assess the effectiveness of assertion-driven correction.
Access status: Abierto ,
I.G
(Universitat Politècnica de València, 2018-04-12) Hernández-Orallo, José; Departamento de Sistemas Informáticos y Computación; Escuela Técnica Superior de Ingeniería Informática; Instituto Universitario Valenciano de Investigación en Inteligencia Artificial
This report summarises the key ideas for a simple concept of I.G. and its explanatory value for several areas.
Access status: Abierto ,
Function Calls at Frozen Positions in Termination of Context-Sensitive Rewriting
(Universitat Politècnica de València, 2015-05-26) Gutiérrez Gil, Raúl; Lucas Alba, Salvador; Departamento de Sistemas Informáticos y Computación; Escuela Politécnica Superior de Alcoy; Escuela Técnica Superior de Ingeniería Informática; Instituto Universitario Valenciano de Investigación en Inteligencia Artificial
Context-sensitive rewriting (CSR) is a variant of rewriting where only selected arguments of function symbols can be rewritten. Consequently, the subterm positions of a term are classified as either active, i.e., positions of subterms that can be rewritten; or frozen, i.e., positions that cannot. Frozen positions can be used to denote subexpressions whose evaluation is delayed or just forbidden. A typical example is the if-then-else operator whose second and third arguments are not evaluated until the evaluation of the first argument yields either true or false. Imposing replacement restrictions can improve the termination behavior of rewriting-based computational systems. Termination of CSR has been investigated by several authors and a number of automatic tools are able to prove it. In this paper, we analyze how frozen subterms affect termination of CSR. This analysis helps us to improve our context-sensitive dependency pair (CS-DP) framework for automatically proving termination of CSR. We have implemented these improvements in our tool MU-TERM. The experiments show the power of the improvements in practice.
Access status: Abierto ,
ACUOS: A System for Modular ACU Generalization with Subtyping and Inheritance (extended version)
(Universitat Politècnica de València, 2014-07-16) Alpuente, María; Escobar, Santiago; Espert, Javier; Meseguer, José
Computing generalizers is relevant in a wide spectrum of automated reasoning areas where analogical reasoning and inductive inference are needed. The ACUOS system computes a complete and minimal set of semantic generalizers (also called \anti-uni ers") of two structures in a typed language modulo a set of equational axioms. By supporting types and any combination of associativity (A), commutativity (C), and unity (U) algebraic axioms for function symbols, ACUOS allows reasoning about typed data structures, e.g. lists, trees, and (multi-)sets, and typical hierarchical/structural relations such as is a and part of. This paper discusses the modular ACU generalization tool ACUOS and illustrates its use in a classical arti ficial intelligence problem.
Access status: Abierto ,
Abstract Diagnosis for tccp using a Linear Temporal Logic
(Universitat Politècnica de València, 2014-02-15) Comini, Marco; Titolo, Laura; Villanueva, Alicia; Departamento de Sistemas Informáticos y Computación; Escuela Técnica Superior de Ingeniería Informática; Instituto Universitario Valenciano de Investigación en Inteligencia Artificial; Ministerio de Ciencia e Innovación; Generalitat Valenciana
Automatic techniques for program verification usually suffer the well-known state explosion problem. Most of the classical approaches are based on browsing the structure of some form of model (which rep- resents the behavior of the program) to check if a given specification is valid. This implies that a part of the model has to be built, and some- times the needed fragment is quite huge. In this work, we provide an alternative automatic decision method to check whether a given property, specified in a linear temporal logic, is valid w.r.t. a tccp program. Our proposal (based on abstract interpreta- tion techniques) does not require to build any model at all. Our results guarantee correctness but, as usual when using an abstract semantics, completeness is lost.
Access status: Abierto ,
A Condensed Goal-Independent Bottom-Up Fixpoint Semantics Modeling the Behavior of tccp
(Universitat Politècnica de València, 2013) Comini, Marco; Titolo, Laura; Villanueva, Alicia; Departamento de Sistemas Informáticos y Computación; Escuela Técnica Superior de Ingeniería Informática; Instituto Universitario Valenciano de Investigación en Inteligencia Artificial; Ministerio de Ciencia e Innovación; Generalitat Valenciana
In this paper, we present a new compositional bottom-up semantics for the Timed Concurrent Constraint Language (tccp in short) which is defined for the full language. In particular, is able to deal with the non- monotonic characteristic of tccp, which constitutes a substantial addi- tional technical difficulty w.r.t. other compositional denotational seman- tics present in literature (which do not tackle the full language). The semantics is proved to be (correct and) fully abstract w.r.t. the full behavior of tccp, including infinite computations. This is particularly important since tccp has been defined to model reactive systems and they may not terminate with a purpose. The overall of these features makes our proposal particularly suitable as the basis for the definition of semantic-based program manipulation tools (like analyzers, debuggers or verifiers), especially in the context of reactive systems.
Access status: Abierto ,
A Condensed Goal-Independent Bottom-Up Fixpoint Semantics Modeling the Behavior of tccp
(Universitat Politècnica de València, 2013-04-13) Comini, Marco; Titolo, Laura; Villanueva, Alicia; Departamento de Sistemas Informáticos y Computación; Escuela Técnica Superior de Ingeniería Informática; Instituto Universitario Valenciano de Investigación en Inteligencia Artificial
In this paper, we present a new compositional bottom-up semantics for the Timed Concurrent Constraint Language (tccp in short). Such semantics is defined for the full language. In particular, is able to deal with the non-monotonic characteristic of the language, which constitutes a substantial additional technical difficulty w.r.t. other compositional denotational semantics present in literature (which do not tackle the full language). The semantics is proved to be (correct and) fully abstract w.r.t. the full behavior of tccp, including infinite computations. This is particularly important since tccp has been defined to model reactive systems. The overall of these features makes our proposal particularly suitable as the basis for the definition of semantic-based program manipulation tools (like analyzers, debuggers or verifiers), especially in the context of reactive systems.
Access status: Abierto ,
A Dependency Pair Framework for AvC-Termination
(Universitat Politècnica de València, 2011-05-04) Alarcón Jiménez, Beatriz; Gutiérrez Gil, Raúl; Lucas, Salvador; Meseguer, José
The development of powerful techniques for proving termination of rewriting modulo a set of equational axioms is essential when dealing with rewriting logic-based programming languages like CafeOBJ, Maude, ELAN, OBJ, etc. One of the most important techniques for proving termination over a wide range of variants of rewriting (strategies) is the dependency pair approach. Several works have tried to adapt it to rewriting modulo associative and commutative (AC) equational theories, and even to more general theories. However, as we discuss in this paper, no appropriate notion of minimality (and minimal chain of dependency pairs) which is well-suited to develop a dependency pair framework has been proposed to date. In this paper we carefully analyze the structure of in nite rewrite sequences for rewrite theories whose equational part is any combination of associativity and/or commutativity axioms, which we call AvC-rewrite theories. Our analysis leads to a more accurate and optimized notion of dependency pairs through the new notion of stably minimal term. We then develop a suitable dependency pair framework for proving termination of AvC-rewrite theories.
Access status: Abierto ,
Innermost Termination of Context-Sensitive Rewriting
(Universitat Politècnica de València, 2011-05-04) Alarcón Jiménez, Beatriz; Lucas, Salvador
Innermost context-sensitive rewriting (CSR) has been proved useful for modeling the computational behavior of programs of algebraic languages like Maude, OBJ, etc, which incorporate an innermost strategy which is used to break down the nondeterminism which is inherent to reduction relations. Furthermore, innermost termination of rewriting is often easier to prove than termination. Thus, under appropriate conditions, a useful strategy for proving termination of rewriting is trying to prove termination of innermost rewriting. This phenomenon has also been investigated for context-sensitive rewriting. Up to now, only few transformation-based methods have been proposed and used to (specifically) prove termination of innermost CSR. Powerful and e cient techniques for proving (innermost) termination of (unrestricted) rewriting like the dependency pair framework have not been considered yet. In this work, we investigate the adaptation of the dependency pair framework to innermost CSR. We provide a suitable notion of innermost context-sensitive dependency pair and show how to extend and adapt the main notions which conform the framework (chain, termination problem, processor, etc.). Thanks to the innermost context-sensitive dependency pairs, we can now use powerful techniques for proving termination of innermost CSR. This is made clear by means of some benchmarks showing that our techniques dramatically improve over previously existing transformational techniques, thus establishing the new state-of-the-art in the area. We have implemented them as part of the termination tool MU-TERM.
Access status: Abierto ,
Backward Trace Slicing for Rewriting Logic Theories -Technical report -
(Universitat Politècnica de València, 2011-04-19) Alpuente Frasnedo, María; Ballis, Demis; Espert, Javier; Romero, Daniel
Trace slicing is a widely used technique for execution trace analysis that is effectively used in program debugging, analysis and comprehension. In this paper, we present a backward trace slicing technique that can be used for the analysis of Rewriting Logic theories. Our trace slicing technique allows us to systematically trace back rewrite sequences modulo equational axioms (such as associativity and commutativity) by means of an algorithm that dynamically simplifies the traces by detecting control and data dependencies, and dropping useless data that do not influence the final result. Our methodology is particularly suitable for analyzing complex, textually-large system computations such as those delivered as counter-example traces by Maude model-checkers.
Access status: Abierto ,
Backward Trace Slicing for Rewriting Logic Theories -Technical report -
(Universitat Politècnica de València, 2011-04-19) Alpuente Frasnedo, María; Ballis, D.; Espert, J.; Romero, D.
Trace slicing is a widely used technique for execution trace analysis that is effectively used in program debugging, analysis and comprehension. In this paper, we present a backward trace slicing technique that can be used for the analysis of Rewriting Logic theories. Our trace slicing technique allows us to systematically trace back rewrite sequences modulo equational axioms (such as associativity and commutativity) by means of an algorithm that dynamically simplifies the traces by detecting control and data dependencies, and dropping useless data that do not influence the final result. Our methodology is particularly suitable for analyzing complex, textually-large system computations such as those delivered as counter-example traces by Maude model-checkers.
Access status: Abierto ,
On Unfolding Completeness for Rewriting Logic Theories
(Universitat Politècnica de València, 2010-10-04) Alpuente Frasnedo, María; Baggi, Michele; Ballis, Demis; Falaschi, Moreno
Many transformation systems for program optimization, program synthesis, and program specialization are based on fold/unfold transformations. In this paper, we investigate the semantic properties of a narrowing-based unfolding transformation that is useful to transform rewriting logic theories. We also present a transformation methodology that is able to determine whether an unfolding transformation step would cause incompleteness and avoid this problem by completing the transformed rewrite theory with suitable extra rules. More precisely, our methodology identifies the sources of incompleteness and derives a set of rules that are added to the transformed rewrite theory in order to preserve the semantics of the original theory.

Examinar

Envíos recientes