Pith. sign in

REVIEW 3 major objections 7 minor 30 references

Towards the LLM-Based Generation of Formal Specifications from Natural-Language Contracts: Early Experiments with Symboleo

T0 review · 3 major / 7 minor · reviewed 2026-08-12 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read This paper reports that out-of-the-box LLMs can draft Symboleo specifications from English contract clauses, with three worked examples cutting GPT-4o's weighted error score from 177 to 64 and the other four models scoring lower.

desk verdict Small, honest Symboleo-LLM experiment; the few-shot signal is real but the manual scoring makes the exact numbers provisional. read the letter →

arxiv 2411.15898 v1 pith:EUPP33WU submitted 2024-11-24 cs.SE

Mounira Nihad Zitouni , Amal Ahmed Anda , Sahil Rajpal , Daniel Amyot , John Mylopoulos This is my paper · ORCID
classification cs.SE
keywords Symboleolegalcontractsdomain-specificlanguagelargemodelspromptengineeringfew-shotlearningformalspecificationgenerationerrortaxonomy
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Large language models have never been trained on Symboleo, a domain-specific language for formally specifying legal contracts, yet the paper asks whether they can translate a short English contract into a Symboleo draft. The authors test 38 prompt combinations on GPT-4o and two of those configurations on four other models, scoring each output with a hand-built taxonomy of 16 error types. Their central result is that worked examples are the strongest lever: GPT-4o's weighted error score fell from 177 with no guidance to 64 with three examples, and the four other models scored between 27 and 54 on the same two cases. They conclude that LLM drafts are close enough that a human expert can repair them rather than write specifications from scratch, and that the main remaining weaknesses are grammar adherence and the identification of environment variables.

What carries the argument

The mechanism that carries the experiment is a prompt-assembly grid over four components: the Symboleo Xtext grammar, a prose explanation of Symboleo's modalities and event functions (e.g., Happens, HappensBefore, HappensWithin), zero to three worked legal-contract examples (medical supply, energy supply, meat sale), and an emotional nudge line. The 38 combinations were run on GPT-4o in ephemeral mode, and two extreme combinations were rerun on four other LLMs. Output quality is measured through a hand-built error taxonomy: 16 error types in three severity classes (weights 4, 3, and 2), summed across the seven components of a Symboleo specification (domain, declarations, pre/postconditions, signature, obligations/powers, constraints) to yield a total error weight per case.

What would settle it

Re-run the same 38 prompt configurations on GPT-4o (and the two cross-model cases on the other four models) multiple times, parse every output with the Symboleo Xtext grammar, and check semantic validity with SymboleoPC; if the automated failure rates do not reproduce the reported ordering, especially the 177-to-64 drop from adding examples and Mistral's 31, then the manual error weights do not measure real specification correctness.

Watch

Extended reading notes

Core claim

The paper's claim, stated in its own terms, is that out-of-the-box LLMs can generate sufficiently plausible Symboleo specifications from natural-language contracts to accelerate the work of a human formalizer. The evidence is a prompt-combination grid: grammar, semantic explanations, zero-to-three worked examples, and an emotional directive, assembled into 38 GPT-4o prompts plus two extreme cases on Claude 3.5 Haiku, Gemini 1.5 Pro 002, Llama 3.2, and Mistral 7B. The authors report that adding three examples lowered GPT-4o's weighted error score from 177 to 64, that the full guidance combination lowered it to 39, and that all four other models produced lower weighted errors than 64 on the three-example case, with Mistral at 31 and even the weakest of them at 54. They attribute the largest share of remaining violations, 49 percent, to grammar adherence, environment-variable identification, and syntax issues, and they explicitly frame expert oversight as necessary.

Load-bearing premise

The load-bearing premise is that the manual scoring by the first three authors, using a self-defined Symboleo-specific taxonomy with severity weights, accurately measures the correctness of the generated specifications; the authors state that no automated tool or formal validation was applied to the outputs.

Editorial extensions

If this is right

  • Prompt engineers targeting little-known DSLs should treat few-shot examples as the primary lever; in this experiment GPT-4o's weighted error score dropped from 177 to 64 when three worked Symboleo examples were added to the prompt.
  • Grammar alone is not helpful and can backfire: giving GPT-4o the grammar without examples and without theory (case 21) produced a weighted error score of 199, worse than giving no guidance at all.
  • The approach transfers across models: on the same two test cases, Claude 3.5 Haiku, Gemini 1.5 Pro 002, Llama 3.2, and Mistral 7B all scored lower weighted errors than GPT-4o's 64 on the minimally guided three-example case.
  • Example content shapes what the model copies: when one worked example lacked environment variables, the model tended to omit environment variables even in responses to a contract that needed them.
  • Run-to-run variability of up to 8 weighted error points means small differences between configurations should not be over-interpreted; the authors treat cases within this margin as equivalent.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The paper's manual scoring could be replaced by a fully automated harness: pipe each generated specification through the Symboleo Xtext parser and then through a semantic checker such as SymboleoPC, which would make the 38-case comparison reproducible and remove the author-bias risk the paper acknowledges.
  • Because environment-variable errors are both frequent and sensitive to example content, a small prompt dataset in which every example explicitly includes at least one environment variable may fix a large share of the observed failures without fine-tuning.
  • If the cross-model result generalizes, confidential legal contracts could be processed locally on open-weight models like Mistral 7B rather than sent to hosted APIs; the paper does not test privacy or data-governance aspects of this workflow.
  • A natural next experiment the authors do not run is iterative repair: instead of one-shot generation, feed parser error messages back to the LLM and regenerate, which could reduce the grammar/syntax component of the 49 percent error share.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 7 minor

Summary. Zitouni et al. report an exploratory experiment on generating formal Symboleo specifications from a short natural-language legal contract using out-of-the-box web-based LLMs. They systematically vary four prompt components (Xtext grammar inclusion, semantic explanations of obligations/powers/events, zero-to-three few-shot examples, and emotional prompting) across 38 configurations on GPT-4o, and run two selected configurations on Claude 3.5 Haiku, Gemini 1.5 Pro 002, Llama 3.2, and Mistral 7B. The generated specifications are manually scored against 16 error types grouped into three severity levels, producing weighted error totals per contract section (Tables I and II). The main reported outcomes are that few-shot examples reduce weighted errors (case 1: 177 to case 2: 64 on GPT-4o), grammar without examples can increase errors (case 21: 199), and all four other LLMs scored at or below GPT-4o on the two shared configurations, with Mistral scoring 31 and 30. The authors conclude that LLM-based generation of plausible Symboleo fragments could accelerate human formalization, and they identify grammar/syntax adherence and environment-variable identification as the major error sources; they explicitly list as limitations the lack of automated validation, the single target contract, the absence of repeated runs, and the unvalidated evaluation metrics.

Significance. This is a clearly scoped exploratory study whose main value, if the results hold, is as an early signal that few-shot prompting materially improves LLM output quality for an obscure DSL and that grammar-only guidance can backfire, with 49% of observed errors concentrated in grammar/syntax adherence and environment-variable identification. The paper ships valuable artifacts: prompts, generated specifications, and the analysis are on Zenodo, the target Computer Sale contract is held out from the example set (so the task is not circular), and the exploration of 38 prompt configurations is systematic for a first study. The authors also disclose their main threats to validity unusually explicitly. The central weakness is that every quantitative ranking rests on unvalidated self-scoring by three of the authors, so the magnitudes (e.g., 177 vs. 64) and rankings should be regarded as provisional; the qualitative demonstration that LLMs produce partially correct, fixable specifications is credible and worth publishing after the evaluation is hardened.

major comments (3)
  1. [Section V-B; Tables I-II] The load-bearing evidence for all quantitative claims in Tables I and II is the manually assigned error weights, and Section V-B concedes that the generated SYMBOLEO specifications 'were not evaluated using automated tools or formal validation methods, instead relying on manual (and possibly biased) evaluation.' The first three authors scored their own outputs, and no inter-rater reliability measure, annotation protocol, or worked rubric examples are reported; several taxonomy categories overlap ('Including Information from Outside the Query' vs. 'Including Unnecessary Information'; 'Missing All Attributes' vs. 'Missing Attributes'), and the severity weights (4/3/2) are asserted without justification or sensitivity analysis. I request three concrete additions: (1) run the 38 generated specifications through the public SYMBOLEO Xtext grammar/parser to obtain a machine-checkable parse-validity signal, (2) have an independent annotator score a random subset and report agreement (e.g., Cohen's kappa), and (3) report how the totals and rankings in Tables I and II change under alternative severity weightings. Without these, the headline 177-to-64 reduction and the cross-model rankings should be presented as exploratory measurements of unknown reliability rather than as results.
  2. [Section IV-B (Variations in Output with Same Input)] The authors set an equivalence margin of 8 error points based on informally observed variations when the same input was run 'multiple times,' but they do not report the number of repetitions, which cases were repeated, or the distribution of the observed differences; the margin is then used to conclude that example order had 'minimal impact' (cases 5 and 9, 8 and 10, 23 and 27). Because each of the 38 configurations was run once (Section IV), every pairwise comparison conflates prompt effects with run-to-run noise and annotation noise, and the single-run qualitative discussion of cases 21 vs. 30 and 3 vs. 12 in the 'Impact of the Prompt' paragraph is vulnerable to the same variability. Please report the repeat-run data and its distribution, justify the 8-point margin statistically, or rephrase the equivalence and ordering conclusions as hypotheses rather than findings.
  3. [Section III-B; Section V-B] All 38 GPT-4o test cases and the two-configuration cross-model comparison (Table II) target the same four-clause Computer Sale contract, so the abstract's claim that the results 'will likely accelerate the specification of legal contracts' extrapolates beyond the evidence, even though Section V-B explicitly acknowledges the single-contract design. The authors should either restrict the conclusion to the studied contract (and note its small size and simple structure), or add at least one additional held-out contract of different structure to the evaluation; the existing example scenarios A, B, and C could be re-used as targets for a small number of the most interesting prompt configurations.
minor comments (7)
  1. [Section IV-C] The sentence 'Llama showed high error rates with minimal input but excelled in case 2 with detailed guidance' appears to mislabel the configurations; the detailed-guidance configuration is case 33, while case 2 is the minimal one (no grammar, theory, or prompt).
  2. [Table I] The header legend defines CAS, CON, DOM, PRE, POS, SIG, and COS but does not define the Declarations (Dec) and Obligations/Powers (OP) columns, and the 'Cont' column takes unexplained nonzero values (case 1 = 1, case 30 = 4) that are never discussed in the text.
  3. [Section III-A; Abstract] Minor typos: 'building blocs' should be 'building blocks,' and the abstract's 'especial' should be 'especially.'
  4. [Figure 1] Figure 1 is referenced in Section IV-B but not included in the manuscript text; please include it and state whether the reported frequencies count violations across all 38 generated specifications.
  5. [Section IV-A] The illustrative example for 'Missing Attributes' is 'who := cust,' which reads as a missing assignment rather than a missing attribute; please replace it with an example that matches the category definition.
  6. [Reference [20]] Reference [20] contains a typo: 'hhttps://gemini.google.com' should be 'https://gemini.google.com.'
  7. [Section IV; Section IV-C] The term 'test case 2' is used ambiguously: in Section IV it denotes the configuration with scenarios A, B, and C but no grammar/theory/prompt, while Section IV-C also describes it as 'minimal guidance'; please clarify the naming convention at first use.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the central empirical claim is independently evaluable, and the paper's acknowledged manual evaluation is a validity limitation, not a reduction of the result to its inputs.

full rationale

The paper's derivation chain is an empirical experiment, not a formal derivation, and no step reduces the reported result to its own inputs by construction. The target Computer Sale contract is held out from all few-shot examples, so the generation task is not engineered to make success definitional. The error-weight taxonomy and severity weights in Section IV-A are author-defined measurement instruments, but the paper does not claim these weights are derived from the data or that the rankings are true by definition; they are explicit evaluation criteria applied to LLM outputs. The 8-point equivalence margin is presented as a comparison convention derived from observed repeated-run variation, not as a fitted parameter used to predict itself. The only self-citations (e.g., [2], [6], [13]) supply the Symboleo language, example contracts, and a motivation for emotional prompting; none of these citations defines the quantitative outcome or forces the reported case rankings. Section V-B explicitly concedes that the generated specifications 'were not evaluated using automated tools or formal validation methods, instead relying on manual (and possibly biased) evaluation,' which is an honest and load-bearing validity threat to the quantitative claims, but a threat to correctness rather than circularity. Since the paper does not claim a derived theorem and its measures are not equivalent to the predicted outcome, no circular step can be exhibited, and the appropriate finding is no significant circularity.

Assumptions & free parameters 2 free parameters · 4 assumptions · 0 invented entities

The central results rest on the correctness of hand-crafted example specifications and a self-defined scoring rubric. The paper makes no mathematical claims and introduces no new entities.

free parameters (2)
  • Severity weights (High=4, Medium=3, Low=2) = 4 / 3 / 2
    Chosen by hand in Section IV-A to compute total error weights; changes to these weights would change which prompt configurations appear best.
  • Equivalent-output error margin = 8
    Set in Section IV-B 'Variations in Output with Same Input' to declare specifications equivalent; directly affects comparisons between test cases.
assumptions (4)
  • domain assumption Symboleo grammar and semantics as described in [2] are correct and complete specifications of the DSL.
    The paper uses these definitions to construct prompts and to evaluate whether generated output is grammatically and semantically valid (Sections II and IV).
  • domain assumption The three example contracts and their Symboleo specifications are correct reference translations.
    These examples are taken from prior papers by the same group and are used as few-shot prompts, so any errors in them would propagate into LLM outputs and the evaluation assumptions.
  • ad hoc to paper The Computer Sale contract is representative enough of business contracts for drawing general conclusions about prompt impact.
    All 38 test cases generate a specification for this single small contract; the paper acknowledges this limitation in Section V-B.
  • ad hoc to paper The error taxonomy and its severity weights are a valid measure of specification quality.
    The metrics are created by the authors, not validated by others or by automated tools, as acknowledged in Section V-B.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Towards the LLM-Based Generation of Formal Specifications from Natural-Language Contracts: Early Experiments with Symboleo." pith.science (2026). https://pith.science/paper/EUPP33WU

@misc{pith2026241115898,
  author       = {Pith},
  title        = {Pith review of: Towards the LLM-Based Generation of Formal Specifications from Natural-Language Contracts: Early Experiments with Symboleo},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/EUPP33WU}},
  note         = {Machine review of arXiv:2411.15898}
}
read the original abstract

Over the past decade, different domain-specific languages (DSLs) were proposed to formally specify requirements stated in legal contracts, mainly for analysis but also for code generation. Symboleo is a promising language in that area. However, writing formal specifications from natural-language contracts is a complex task, especial for legal experts who do not have formal language expertise. This paper reports on an exploratory experiment targeting the automated generation of Symboleo specifications from business contracts in English using Large Language Models (LLMs). Combinations (38) of prompt components are investigated (with/without the grammar, semantics explanations, 0 to 3 examples, and emotional prompts), mainly on GPT-4o but also to a lesser extent on 4 other LLMs. The generated specifications are manually assessed against 16 error types grouped into 3 severity levels. Early results on all LLMs show promising outcomes (even for a little-known DSL) that will likely accelerate the specification of legal contracts. However, several observed issues, especially around grammar/syntax adherence and environment variable identification (49%), suggest many areas where potential improvements should be investigated.

Figures

Figures reproduced from arXiv: 2411.15898 by the authors.

Figure 1
Figure 1. Frequencies of errors across all generated S [PITH_FULL_IMAGE:figures/full_fig_p005_1.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

30 extracted references · 12 canonical work pages

  1. [1]

    From legal contracts to formal specifications: A systematic literature review,

    M. Soavi, N. Zeni, J. Mylopoulos, and L. Mich, “From legal contracts to formal specifications: A systematic literature review,” SN Computer Science , vol. 3, no. 5, Jun 2022. [Online]. Available: https://doi.org/10.1007/s42979-022-01228-4

    doi:10.1007/s42979-022-01228-4 2022

  2. [2]

    Specification and analysis of legal contracts with Symboleo,

    A. Parvizimosaed, S. Sharifi, D. Amyot, L. Logrippo, M. Roveri, A. Rasti, A. Roudak, and J. Mylopoulos, “Specification and analysis of legal contracts with Symboleo,” Software and Systems Modeling, vol. 21, no. 6, pp. 2395–2427, 2022. [Online]. Available: https://doi.org/10.1007/s10270-022-01053-6

    work page doi:10.1007/s10270-022-01053-6 2022

  3. [3]

    AutoMTLSpec: Learning to generate MTL specifications from natural language contracts,

    N. Ge, J. Yang, T. Yu, and W. Liu, “AutoMTLSpec: Learning to generate MTL specifications from natural language contracts,” in 2023 27th International Conference on Engineering of Complex Computer Systems (ICECCS) . IEEE CS, 2023, pp. 71–80. [Online]. Available: https://doi.org/10.1109/ICECCS59891.2023.00018

    arXiv 2023

  4. [4]

    Text mining tool for translating terms of contract into technical specifications: Development and application in the railway sector,

    G. Fantoni, E. Coli, F. Chiarello, R. Apreda, F. Dell’Orletta, and G. Pratelli, “Text mining tool for translating terms of contract into technical specifications: Development and application in the railway sector,” Computers in Industry , vol. 124, p. 103357, 2021. [Online]. Available: https://doi.org/10.1016/j.compind.2020.103357

    arXiv 2021

  5. [5]

    Semantic annotation of legal contracts with ContrattoA,

    M. Soavi, N. Zeni, J. Mylopoulos, and L. Mich, “Semantic annotation of legal contracts with ContrattoA,” Informatics, vol. 9, no. 4, 2022. [Online]. Available: https://doi.org/10.3390/informatics9040072

    doi:10.3390/informatics9040072 2022

  6. [6]

    Towards legal contract formalization with controlled natural language templates,

    R. Meloche, D. Amyot, and J. Mylopoulos, “Towards legal contract formalization with controlled natural language templates,” in 2023 IEEE 31st International Requirements Engineering Conference (RE) . IEEE CS, 2023, pp. 317–322. [Online]. Available: https://doi.org/10. 1109/RE57278.2023.00042

    arXiv 2023

  7. [7]

    A web-based environment for the specification and generation of smart legal contracts,

    R. Meloche, D. Sivakumar, A. A. Anda, S. Alfuhaid, D. Amyot, L. Logrippo, and J. Mylopoulos, “A web-based environment for the specification and generation of smart legal contracts,” in International Symposium on Compliance for Algorithmic Law (SCALGO), post-event proceedings, ser. Lecture Notes in Computer Science. Springer (to appear), 2024

    work page 2024

  8. [8]

    ChatGPT 4o,

    Open AI, “ChatGPT 4o,” https://openai.com/index/chatgpt/ [Last ac- cessed: Nov. 2024]

    work page 2024

Show all 30 references
  1. [9]

    DSL-Xpert: LLM- driven generic DSL code generation,

    V . Lamas, M. R. Luaces, and D. Garcia-Gonzalez, “DSL-Xpert: LLM- driven generic DSL code generation,” in Proceedings of the ACM/IEEE 27th International Conference on Model Driven Engineering Languages and Systems, ser. MODELS Companion ’24. ACM, 2024, pp. 16–20. [Online]. Ava...

    2024

  2. [10]

    A comparative study of DSL code generation: Fine-tuning vs. optimized retrieval augmentation,

    N. Bassamzadeh and C. Methani, “A comparative study of DSL code generation: Fine-tuning vs. optimized retrieval augmentation,” 2024. [Online]. Available: https://arxiv.org/abs/2407.02742

    2024 arXiv

  3. [12]

    On the use of GPT-4 for creating goal models: An exploratory study,

    B. Chen, K. Chen, S. Hassani, Y . Yang, D. Amyot, L. Lessard, G. Mussbacher, M. Sabetzadeh, and D. Varró, “On the use of GPT-4 for creating goal models: An exploratory study,” in 2023 IEEE 31st International Requirements Engineering Conference Workshops (REW). IEEE CS, 2023, p...

    2023

  4. [14]

    SymboleoPC: checking properties of legal contracts,

    A. Parvizimosaed, M. Roveri, A. Rasti, A. A. Anda, S. Alfuhaid, D. Amyot, L. Logrippo, and J. Mylopoulos, “SymboleoPC: checking properties of legal contracts,” Software and Systems Modeling , 2024. [Online]. Available: https://doi.org/10.1007/s10270-024-01180-2

    2024 doi

  5. [15]

    Automated generation of smart contract code from legal contract specifications with Symboleo2SC,

    A. Rasti, A. A. Anda, S. Alfuhaid, A. Parvizimosaed, D. Amyot, M. Roveri, L. Logrippo, and J. Mylopoulos, “Automated generation of smart contract code from legal contract specifications with Symboleo2SC,” Software and Systems Modeling , 2024. [Online]. Available: https://doi.o...

    2024 doi

  6. [16]

    A systematic survey of prompt engineering in large language models: Techniques and applications,

    P. Sahoo, A. K. Singh, S. Saha, V . Jain, S. Mondal, and A. Chadha, “A systematic survey of prompt engineering in large language models: Techniques and applications,” 2024. [Online]. Available: https://arxiv.org/abs/2402.07927

    2024 arXiv

  7. [17]

    Llama 3.2,

    Meta, “Llama 3.2,” 2024, https://www.llama.com/ [Last accessed: Nov. 2024]

    2024

  8. [18]

    Claude 3.5 haiku,

    Anthropic, “Claude 3.5 haiku,” 2024, https://claude.ai/ [Last accessed: Nov. 2024]

    2024

  9. [19]

    Mistral 7b,

    Mistral AI, “Mistral 7b,” 2024, https://mistral.ai/ [Last accessed: Nov. 2024]

    2024

  10. [20]

    Gemini 1.5 pro 002,

    Google, “Gemini 1.5 pro 002,” 2024, hhttps://gemini.google.com/ [Last accessed: Nov. 2024]

    2024

  11. [21]

    Towards ontological foundations for conceptual modeling: The unified foundational ontology (UFO) story,

    G. Guizzardi, G. Wagner, J. P. A. Almeida, and R. S. Guizzardi, “Towards ontological foundations for conceptual modeling: The unified foundational ontology (UFO) story,” Applied Ontology , vol. 10, no. 3-4, pp. 259–271, 2015. [Online]. Available: https: //doi.org/10.3233/AO-150157

    2015 doi

  12. [22]

    Symboleo: Towards a specification language for legal contracts,

    S. Sharifi, A. Parvizimosaed, D. Amyot, L. Logrippo, and J. Mylopoulos, “Symboleo: Towards a specification language for legal contracts,” in 2020 IEEE 28th International Requirements Engineering Conference (RE). IEEE CS, 2020, pp. 364–369. [Online]. Available: https: //doi.org...

    2020

  13. [23]

    Bettini, Implementing domain-specific languages with Xtext and Xtend

    L. Bettini, Implementing domain-specific languages with Xtext and Xtend. Packt Publishing Ltd, 2016

    2016

  14. [24]

    Supplementary Material, Towards the LLM-Based Generation of Formal Specifications from Natural-Language Contracts: Early Experiments with Symboleo,

    M. N. Zitouni, A. A. Anda, S. Rajpal, D. Amyot, and J. Mylopoulos, “Supplementary Material, Towards the LLM-Based Generation of Formal Specifications from Natural-Language Contracts: Early Experiments with Symboleo,” Nov. 2024. [Online]. Available: https://doi.org/10.5281/zeno...

    2024 doi

  15. [25]

    A survey on RAG meeting LLMs: Towards retrieval- augmented large language models,

    W. Fan, Y . Ding, L. Ning, S. Wang, H. Li, D. Yin, T.-S. Chua, and Q. Li, “A survey on RAG meeting LLMs: Towards retrieval- augmented large language models,” in Proceedings of the 30th ACM SIGKDD Conference on Knowledge Discovery and Data Mining , ser. KDD ’24. ACM, 2024, pp. ...

    2024

  16. [26]

    Model generation with LLMs: From requirements to UML sequence diagrams,

    A. Ferrari, S. Abualhaija, and C. Arora, “Model generation with LLMs: From requirements to UML sequence diagrams,” in 2024 IEEE 32nd International Requirements Engineering Conference Workshops (REW). IEEE CS, 2024, pp. 291–300. [Online]. Available: https: //doi.org/10.1109/REW...

    2024

  17. [27]

    Multi-step iterative automated domain modeling with large language models,

    Y . Yang, B. Chen, K. Chen, G. Mussbacher, and D. Varró, “Multi-step iterative automated domain modeling with large language models,” in Proceedings of the ACM/IEEE 27th International Conference on Model Driven Engineering Languages and Systems , ser. MODELS Companion ’24. ACM...

    2024

  18. [28]

    SpecGen: Automated generation of formal program specifications via large language models,

    L. Ma, S. Liu, Y . Li, X. Xie, and L. Bu, “SpecGen: Automated generation of formal program specifications via large language models,”

  19. [29]

    Leveraging large language models for automatic smart contract generation,

    E. A. Napoli, F. Barbàra, V . Gatteschi, and C. Schifanella, “Leveraging large language models for automatic smart contract generation,” in 2024 IEEE 48th Annual Computers, Software, and Applications Conference (COMPSAC) , 2024, pp. 701–710. [Online]. Available: https://doi.or...

    2024 arXiv

  20. [30]

    Extracting formal smart-contract specifications from natural language with LLMs,

    G. Leite, F. Arruda, P. Antonino, A. Sampaio, and A. W. Roscoe, “Extracting formal smart-contract specifications from natural language with LLMs,” in Formal Aspects of Component Software , D. Marmsoler and M. Sun, Eds. Springer, 2024, pp. 109–126. [Online]. Available: https://...

    2024 doi

  21. [31]

    SymboleoNLP: A tool for generating formal specifications from legal contract templates,

    R. Meloche, D. Amyot, and J. Mylopoulos, “SymboleoNLP: A tool for generating formal specifications from legal contract templates,” in 2024 IEEE 32nd International Requirements Engineering Conference (RE). IEEE CS, 2024, pp. 498–499. [Online]. Available: https: //doi.org/10.110...

    2024

  22. [2024]

    Available: https://arxiv.org/abs/2401.08807

    [Online]. Available: https://arxiv.org/abs/2401.08807

    arXiv

Pith tools

Reviewed August 12, 2026 · model on record in the stance chip above.