-
Laurel: Generating Dafny Assertions Using Large Language Models
Authors:
Eric Mugnier,
Emmanuel Anaya Gonzalez,
Ranjit Jhala,
Nadia Polikarpova,
Yuanyuan Zhou
Abstract:
Dafny is a popular verification language, which automates proofs by outsourcing them to an SMT solver. This automation is not perfect, however, and the solver often requires guidance in the form of helper assertions creating a burden for the proof engineer. In this paper, we propose Laurel, a tool that uses large language models (LLMs) to automatically generate helper assertions for Dafny programs…
▽ More
Dafny is a popular verification language, which automates proofs by outsourcing them to an SMT solver. This automation is not perfect, however, and the solver often requires guidance in the form of helper assertions creating a burden for the proof engineer. In this paper, we propose Laurel, a tool that uses large language models (LLMs) to automatically generate helper assertions for Dafny programs. To improve the success rate of LLMs in this task, we design two domain-specific prompting techniques. First, we help the LLM determine the location of the missing assertion by analyzing the verifier's error message and inserting an assertion placeholder at that location. Second, we provide the LLM with example assertions from the same codebase, which we select based on a new lemma similarity metric. We evaluate our techniques on a dataset of helper assertions we extracted from three real-world Dafny codebases. Our evaluation shows that Laurel is able to generate over 50% of the required helper assertions given only a few attempts, making LLMs a usable and affordable tool to further automate practical program verification.
△ Less
Submitted 26 May, 2024;
originally announced May 2024.
-
HYSYNTH: Context-Free LLM Approximation for Guiding Program Synthesis
Authors:
Shraddha Barke,
Emmanuel Anaya Gonzalez,
Saketh Ram Kasibatla,
Taylor Berg-Kirkpatrick,
Nadia Polikarpova
Abstract:
Many structured prediction and reasoning tasks can be framed as program synthesis problems, where the goal is to generate a program in a domain-specific language (DSL) that transforms input data into the desired output. Unfortunately, purely neural approaches, such as large language models (LLMs), often fail to produce fully correct programs in unfamiliar DSLs, while purely symbolic methods based…
▽ More
Many structured prediction and reasoning tasks can be framed as program synthesis problems, where the goal is to generate a program in a domain-specific language (DSL) that transforms input data into the desired output. Unfortunately, purely neural approaches, such as large language models (LLMs), often fail to produce fully correct programs in unfamiliar DSLs, while purely symbolic methods based on combinatorial search scale poorly to complex problems. Motivated by these limitations, we introduce a hybrid approach, where LLM completions for a given task are used to learn a task-specific, context-free surrogate model, which is then used to guide program synthesis. We evaluate this hybrid approach on three domains, and show that it outperforms both unguided search and direct sampling from LLMs, as well as existing program synthesizers.
△ Less
Submitted 24 May, 2024;
originally announced May 2024.
-
Complex variables for fractional-order systems
Authors:
Emmanuel A. Gonzalez
Abstract:
This paper discusses and summarizes some results on complex variables that are very useful in fractional-order systems analysis and design, specifically when the system is analyzed in the frequency domain. The author hopes that this document will serve as a handy reference when performing computations with complex variables, especially when working within the Laplace and Fourier domains. The reade…
▽ More
This paper discusses and summarizes some results on complex variables that are very useful in fractional-order systems analysis and design, specifically when the system is analyzed in the frequency domain. The author hopes that this document will serve as a handy reference when performing computations with complex variables, especially when working within the Laplace and Fourier domains. The reader can refer to Table I for the summary of these formulas.
△ Less
Submitted 5 November, 2018;
originally announced November 2018.
-
Continuous variables triple-photon states quantum entanglement
Authors:
E. A. Rojas Gonzalez,
A. Borne,
B. Boulanger,
J. A. Levenson,
K. Bencheikh
Abstract:
We investigate the quantum entanglement of the three modes associated with the three-photon states obtained by triple-photon generation in a phase-matched third-order nonlinear optical interaction. Although the second order processes have been extensively dealt with, there is no direct analogy between the second and third-order mechanisms. We show for example the absence of quantum entanglement be…
▽ More
We investigate the quantum entanglement of the three modes associated with the three-photon states obtained by triple-photon generation in a phase-matched third-order nonlinear optical interaction. Although the second order processes have been extensively dealt with, there is no direct analogy between the second and third-order mechanisms. We show for example the absence of quantum entanglement between the quadratures of the three modes in the case of spontaneous parametric triple-photon generation. However, we show that genuine triple-photon entanglement is obtained in the fully seeded case, and its efficiency increases with the seeding level.
△ Less
Submitted 11 September, 2017;
originally announced September 2017.
-
User-driven Intelligent Interface on the Basis of Multimodal Augmented Reality and Brain-Computer Interaction for People with Functional Disabilities
Authors:
S. Stirenko,
Yu. Gordienko,
T. Shemsedinov,
O. Alienin,
Yu. Kochura,
N. Gordienko,
A. Rojbi,
J. R. López Benito,
E. Artetxe González
Abstract:
The analysis of the current integration attempts of some modes and use cases of user-machine interaction is presented. The new concept of the user-driven intelligent interface is proposed on the basis of multimodal augmented reality and brain-computer interaction for various applications: in disabilities studies, education, home care, health care, etc. The several use cases of multimodal augmentat…
▽ More
The analysis of the current integration attempts of some modes and use cases of user-machine interaction is presented. The new concept of the user-driven intelligent interface is proposed on the basis of multimodal augmented reality and brain-computer interaction for various applications: in disabilities studies, education, home care, health care, etc. The several use cases of multimodal augmentation are presented. The perspectives of the better human comprehension by the immediate feedback through neurophysical channels by means of brain-computer interaction are outlined. It is shown that brain-computer interface (BCI) technology provides new strategies to overcome limits of the currently available user interfaces, especially for people with functional disabilities. The results of the previous studies of the low end consumer and open-source BCI-devices allow us to conclude that combination of machine learning (ML), multimodal interactions (visual, sound, tactile) with BCI will profit from the immediate feedback from the actual neurophysical reactions classified by ML methods. In general, BCI in combination with other modes of AR interaction can deliver much more information than these types of interaction themselves. Even in the current state the combined AR-BCI interfaces could provide the highly adaptable and personal services, especially for people with functional disabilities.
△ Less
Submitted 15 August, 2017; v1 submitted 12 April, 2017;
originally announced April 2017.
-
Augmented Coaching Ecosystem for Non-obtrusive Adaptive Personalized Elderly Care on the Basis of Cloud-Fog-Dew Computing Paradigm
Authors:
Yu. Gordienko,
S. Stirenko,
O. Alienin,
K. Skala,
Z. Soyat,
A. Rojbi,
J. R. López Benito,
E. Artetxe González,
U. Lushchyk,
L. Sajn,
A. Llorente Coto,
G. Jervan
Abstract:
The concept of the augmented coaching ecosystem for non-obtrusive adaptive personalized elderly care is proposed on the basis of the integration of new and available ICT approaches. They include the multimodal user interface (MMUI), augmented reality (AR), machine learning (ML), Internet of Things (IoT), and machine-to-machine (M2M) interactions. The ecosystem is based on the Cloud-Fog-Dew computi…
▽ More
The concept of the augmented coaching ecosystem for non-obtrusive adaptive personalized elderly care is proposed on the basis of the integration of new and available ICT approaches. They include the multimodal user interface (MMUI), augmented reality (AR), machine learning (ML), Internet of Things (IoT), and machine-to-machine (M2M) interactions. The ecosystem is based on the Cloud-Fog-Dew computing paradigm services, providing a full symbiosis by integrating the whole range from low-level sensors up to high-level services using integration efficiency inherent in synergistic use of applied technologies. Inside of this ecosystem, all of them are encapsulated in the following network layers: Dew, Fog, and Cloud computing layer. Instead of the "spaghetti connections", "mosaic of buttons", "puzzles of output data", etc., the proposed ecosystem provides the strict division in the following dataflow channels: consumer interaction channel, machine interaction channel, and caregiver interaction channel. This concept allows to decrease the physical, cognitive, and mental load on elderly care stakeholders by decreasing the secondary human-to-human (H2H), human-to-machine (H2M), and machine-to-human (M2H) interactions in favor of M2M interactions and distributed Dew Computing services environment. It allows to apply this non-obtrusive augmented reality ecosystem for effective personalized elderly care to preserve their physical, cognitive, mental and social well-being.
△ Less
Submitted 13 April, 2017;
originally announced April 2017.
