{"id":"1d9daeed-2539-4bf4-9407-8ed3b6cc96aa","arxiv_id":"2411.15898","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":2,"one_line_summary":"LLMs can draft Symboleo specifications from natural-language contracts, and adding example scenarios sharply reduces errors, but the evaluation relies on one small contract and manual scoring.","lead":"This paper reports early experiments using LLMs to turn plain-English legal contracts into formal Symboleo specifications, testing 38 prompt combinations on GPT-4o and a few other models. The results are promising but error-prone, with grammar adherence and environment-variable handling as the main weak spots.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Manual, author-assigned error weights are the sole quantitative evidence; without automated Symboleo validation or independent scoring, the case rankings in Tables I-II are not trustworthy.","rationale":"The reader's weakest assumption is accurate. I examined possible alternative concerns: single test contract, lack of repeated runs, no baseline, temperature variations, and the fact that non-GPT models were only tested on two cases. These are all real limitations, but each would weaken the generalizability claim; the manual scoring concern attacks the internal validity of every quantitative result in the paper. If the error weights are wrong, no amount of additional contracts or runs would fix the headline comparison. I therefore agree with the reader's identification. The paper is honest about the limitation, and the authors propose automated validation as future work; that is why the appropriate verdict remains CONDITIONAL rather than REJECT: the qualitative findings are plausible and reproducible artifacts are provided, but the quantitative claims should be treated as unverified until a parser-based check is performed. The concrete test above is feasible because the Symboleo grammar and SymboleoPC tool are referenced in the paper.","tokens_in":13778,"tokens_out":2551,"duration_ms":25242,"concrete_test":"Run all 38 GPT-4o outputs and the 8 other-LLM outputs through the publicly available Symboleo Xtext parser and the SymboleoPC validator, and compare automated parse/semantic errors against the manual error weights in Table I. If a substantial fraction of generated specifications fail to parse, or if automated error counts disagree with the manual totals by more than the paper's own 8-point equivalence margin, then the manual metric is the bottleneck and Tables I-II cannot support the rankings.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Section V-B explicitly concedes that the generated Symboleo specifications 'were not evaluated using automated tools or formal validation methods, instead relying on manual (and possibly biased) evaluation.' This is the load-bearing issue because the paper's central evidence consists entirely of weighted error totals in Table I and Table II: the 177-to-64 drop in case 2, Mistral scoring 31, and all 38-case comparisons are derived from these manually assigned weights. The taxonomy itself is fragile: several categories overlap ('Including Information from Outside the Query' vs. 'Including Unnecessary Information'; 'Missing All Attributes' vs. 'Missing Attributes'), and no annotation protocol, rubric examples, or inter-rater reliability measure is reported. Since the first three authors scored their own generated outputs, confirmation bias is plausible. If the error weights are miscalibrated—e.g., if grammar-inconsistency counts conflate syntactic and semantic defects, or if many generated specifications would not even parse under the actual Xtext grammar—then the quantitative rankings and the claimed advantage of few-shot prompting lose their evidentiary value. The qualitative observation that LLMs produce plausible-looking Symboleo fragments may survive, but the central claim of accelerated specification is not supported without a validated correctness measure.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":14175,"tokens_out":10197,"duration_ms":86321,"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":[{"comment":"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.","section":"Section V-B; Tables I-II"},{"comment":"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.","section":"Section IV-B (Variations in Output with Same Input)"},{"comment":"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.","section":"Section III-B; Section V-B"}],"minor_comments":[{"comment":"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).","section":"Section IV-C"},{"comment":"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.","section":"Table I"},{"comment":"Minor typos: 'building blocs' should be 'building blocks,' and the abstract's 'especial' should be 'especially.'","section":"Section III-A; Abstract"},{"comment":"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.","section":"Figure 1"},{"comment":"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.","section":"Section IV-A"},{"comment":"Reference [20] contains a typo: 'hhttps://gemini.google.com' should be 'https://gemini.google.com.'","section":"Reference [20]"},{"comment":"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.","section":"Section IV; Section IV-C"}],"recommendation":"major_revision","confidential_remarks":"This is essentially a workshop-grade empirical study, and the gap between its quantitative presentation and the reliability of its measurement is real; however, the gap is fixable within a revision by adding machine parse-checking (the grammar is public), independent scoring of a subset, and repetition of a few key configurations. I would not accept the current version because the advertised quantitative comparisons (177 vs. 64; the Table II rankings) depend on an unvalidated manual instrument, but I would not reject it either, given the transparent limitations and the public artifacts. The novelty is modest relative to recent DSL-generation work (e.g., DSL-Xpert, Leite et al.), but the Symboleo focus and the broad prompt sweep justify a revised version if the authors are willing to strengthen the evaluation."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Quick take: this is a small, honest exploratory study on LLM-generated Symboleo specs from English contracts. The promising signal—few-shot examples cut weighted errors from 177 to 64 on GPT-4o—is real, but the numbers rest entirely on the authors' manual scoring, so treat them as suggestive rather than definitive.\n\nWhat's new: first full LLM-generation experiment for Symboleo, with a systematic sweep of 38 prompt combinations (grammar, semantics, examples, emotional prompts), a cross-model check on four other LLMs, and a Symboleo-specific error taxonomy. The authors share prompts and data on Zenodo. The paper is refreshingly clear about its limitations: no automated validation, one test contract, no repeated runs, and manual assessment by the authors themselves.\n\nWhat it does well: the qualitative finding—that LLMs can produce plausible partial specifications and that examples help more than grammar alone—is credible and useful for anyone building DSL code generators. The discussion of context sensitivity (e.g., scenario C lacking environment variables causing the model to drop them) is insightful.\n\nSoft spots, in proportion: the biggest is the measurement. The error taxonomy has overlapping categories (e.g., 'Including Information from Outside the Query' vs. 'Including Unnecessary Information'; 'Missing All Attributes' vs. 'Missing Attributes'), no inter-rater reliability is reported, and the severity weights are author-defined. The stress-test note is right that the quantitative rankings in Table I/II should not be taken too seriously. However, the main claims (examples reduce errors, grammar alone can hurt) would likely hold under a different weighting—the raw error counts follow the same pattern. Also, the cross-LLM comparison is limited to two cases with web versions, and the 'better than ChatGPT' claim (especially Mistral) needs more evidence.\n\nWho it's for: people working on LLM-based DSL/code generation, requirements engineering, or legal contract formalization. It's a modest data point, not a breakthrough, but a legitimate one. A serious referee could help sharpen the evaluation realism (e.g., request independent annotations or a parse check) without rejecting the paper outright.\n\nRecommendation: send it to peer review at an SE/RE venue. It's an early-experiment paper with clearly stated limits; the field benefits from such reports. My own verdict would be 'revise and resubmit' with pressure to strengthen the evaluation.","headline":"Small, honest Symboleo-LLM experiment; the few-shot signal is real but the manual scoring makes the exact numbers provisional.","tokens_in":14527,"tokens_out":3208,"would_cite":false,"duration_ms":26486,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"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.","keywords":["Symboleo","legal contracts","domain-specific language","large language models","prompt engineering","few-shot learning","formal specification generation","error taxonomy"],"falsifier":"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.","tokens_in":13611,"feed_emoji":"⚖️","tokens_out":11409,"duration_ms":89703,"temperature":0.7,"pith_summary":"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.","feed_headline":"Three examples slash LLM contract errors from 177 to 64","feed_subtitle":"Across five models, example contracts in prompts cut specification errors sharply—a step toward faster legal contracts.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Defines Symboleo's ontology and grammar and supplies example scenarios B and C used in the prompts.","marker":"[2]"},{"why":"The GPT-4o chat interface used for the 38 prompt configurations.","marker":"[8]"},{"why":"Survey from which the prompt components (grammar context, few-shot, emotional prompting) are drawn.","marker":"[16]"},{"why":"Source of Scenario A, the medical supply contract used as a worked example, and of the Symboleo-to-smart-contract pipeline.","marker":"[15]"},{"why":"Source of the Computer Sale test contract and of SymboleoPC, the model-checking motivation for downstream verification.","marker":"[14]"},{"why":"Prior Symboleo generation via controlled natural-language templates, the baseline the authors contrast with LLM-based generation.","marker":"[6]"},{"why":"Related DSL code generation with grammar and few-shot learning for little-known DSLs, used as a comparison in the discussion.","marker":"[9]"},{"why":"Motivates LLM use for legal compliance tasks.","marker":"[13]"}],"fun_headline_variants":["Examples slash LLM contract formalization errors by nearly two-thirds","Three in-prompt examples cut LLM spec errors from 177 to 64","LLMs turn legal contracts into specs—but still need human oversight","Even smaller models beat GPT-4o's prompted contract spec errors"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Examples slash LLM contract formalization errors by nearly two-thirds","Three in-prompt examples cut LLM spec errors from 177 to 64","LLMs turn legal contracts into specs—but still need human oversight","Even smaller models beat GPT-4o's prompted contract spec errors"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001252,"raw_usage":{"total_tokens":5139,"prompt_tokens":957,"completion_tokens":4182,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":573,"completion_tokens_details":{"reasoning_tokens":4114}},"tokens_in":573,"tokens_out":4182,"duration_ms":26215,"temperature":1.0,"reasoning_tokens":4114,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-12T13:45:10.647191+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":"Specification and analysis of legal contracts with Symboleo,","cited_arxiv_id":null,"evidence_quote":"Defines Symboleo's ontology and grammar and supplies example scenarios B and C used in the prompts."},{"cited_title":"ChatGPT 4o,","cited_arxiv_id":null,"evidence_quote":"The GPT-4o chat interface used for the 38 prompt configurations."},{"cited_title":"DSL-Xpert: LLM- driven generic DSL code generation,","cited_arxiv_id":null,"evidence_quote":"Related DSL code generation with grammar and few-shot learning for little-known DSLs, used as a comparison in the discussion."}],"review_version":1}