Reproduce “Towards the LLM-Based Generation of Formal Specifications from Natural-Language Contracts: Early Experiments with Symboleo” on OpenResearch
Turn your favorite coding agents into research agents that review literature, develop hypotheses, and run experiments.
Universal app for Apple silicon and Intel. Requires macOS 11 or later.
About this paper
Mounira Nihad Zitouni, Amal Ahmed Anda, Sahil Rajpal, Daniel Amyot, John Mylopoulos
Researchers from the University of Ottawa investigated the effectiveness of Large Language Models (LLMs), particularly GPT-4o, in automatically translating natural-language legal contracts into formal SYMBOLEO specifications, identifying crucial prompt engineering strategies and common error patterns. This work contributes to accelerating the formalization of legal agreements for applications like smart contracts.
Key insights
- Providing few-shot examples and SYMBOLEO's grammar significantly reduced LLM errors, but grammar provided in isolation could be detrimental by encouraging overly complex and incorrect code.
- LLMs demonstrated high sensitivity to contextual information, with the characteristics of recent examples (e.g., presence of environment variables) heavily influencing subsequent generations.
- Emotional prompts had negligible or counterproductive effects on specification quality, indicating their limited utility for precise technical generation tasks.
Summary by alphaXiv.
Tip: change arxiv.org to autoarxiv.org in any arXiv abstract link to open the paper here.