Pith. sign in

REVIEW 4 major objections 5 minor 16 references

Scaling Up Formal Representation of Clinical Trial Protocols in Ensemble Logic Using LLMs: A Preliminary Study

T0 review · 4 major / 5 minor · reviewed 2026-08-01 · deepseek-v4-flash

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

Pith's one-line read LLM-driven workflow translates narrative clinical trial protocols into Temporal Ensemble Logic formulas, using back-translation to show the formal versions retain meaning.

desk verdict CT-TEL is a useful preliminary pipeline for getting clinical trial text into TEL, but the round-trip similarity metric doesn't validate the formulas, and the paper's own §5.3 concession makes that clear. read the letter →

arxiv 2607.21307 v1 pith:HOU5FTS2 submitted 2026-07-23 cs.LO cs.AIcs.ET

Yan Huang , Xubing Hao , Xiaojin Li , Rashmie Abeysinghe , Xiaoqian Jiang , Licong Cui , Guo-Qiang Zhang This is my paper · ORCID
classification cs.LOcs.AIcs.ET MSC 03B4468Q6068T50
keywords clinicaltrialprotocolsTemporalEnsembleLogiclargelanguagemodelsback-translationsemanticsimilarityformalrepresentationcohortsimulationmodelchecking
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

This paper tries to establish that large language models can convert narrative clinical trial protocols from a public trial registry into Temporal Ensemble Logic (TEL) formulas at scale, and that the conversion is faithful. The authors build CT-TEL, a pipeline that formalizes 23 Alzheimer's-disease medication trials into TEL and then uses a separate LLM pass to translate the formulas back into natural language. The back-translated protocols are compared to the source texts using human expert ratings, LLM ratings, and lexical/semantic similarity metrics. The scores suggest the formalized versions retain the temporal meaning of the original protocols. If this holds, it would remove the manual-encoding bottleneck that has prevented logic-based reasoning from being applied to large collections of trial records.

What carries the argument

The central mechanism is Temporal Ensemble Logic (TEL), a temporal logic whose formulas combine atomic propositions with shift operators (p at offset t), box operators (condition holds continuously for duration t), diamond operators (event occurs within window t), Boolean connectives, and quantifiers over time anchors. The workflow uses TEL as an intermediate representation: an LLM compiles narrative protocol text into TEL formulas, a second LLM reconstructs trial-protocol modules from the formulas, and fidelity is scored by comparing the reconstruction to the original. The bidirectionality of TEL is what makes the back-translation check possible.

What would settle it

Run a model-checking engine on the generated TEL formulas and compare satisfaction sets against the intended clinical events from the original protocol timelines; if a formula admits or excludes a patient cohort that the original narrative would not, the fidelity claim for that trial is falsified.

Watch

Extended reading notes

Core claim

The paper's central discovery is that a round-trip LLM pipeline can produce TEL formulas from real clinical trial text with measurable semantic fidelity. Across 23 trials, semantic similarity between original and reverse-translated module text averaged 0.622 for conditions and 0.860 for eligibility, with diagonal entries in cross-trial similarity matrices clearly exceeding off-diagonal baselines. The authors interpret these results as evidence that the intermediate TEL formulas are faithful logical models, enabling downstream model-checking and cohort simulation.

Load-bearing premise

The paper's central assumption is that high semantic similarity between the original text and the LLM's back-translation of the TEL formula proves the formula itself is logically faithful; but embedding-based similarity cannot detect wrong temporal anchors, collapsed duration states, or hallucinated fields, as the paper itself concedes.

Editorial extensions

If this is right

  • Automated generation of TEL formulas removes the manual encoding bottleneck, making logic-based trial representation practical for large registries.
  • TEL formulas can be fed into model-checking engines to simulate eligibility cohorts and test recruitment strategies against real-world data.
  • Self-controlled case series could use these formulas to construct synthetic control arms from real-world patient timelines.
  • The workflow could extend beyond Alzheimer's disease trials to other therapeutic areas sharing the same protocol schema.
  • Cross-LLM results suggest the pipeline is not tied to a single model, though not all models can execute the formal-synthesis prompts.

Reading between the lines

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

  • The semantic-similarity proxy is text-to-text; it does not verify the TEL formula's logical structure. A model-checking comparison of satisfaction sets would be a stricter test, as the paper itself notes.
  • The masking experiment suggests that ontology labels contribute to surface similarity but may not be needed for logical correctness, implying the fidelity metric conflates terminology grounding with temporal accuracy.
  • If scaled, this approach could make trial protocols directly queryable, but the 'implicit assumption injection' failure mode means hallucinated fields may propagate into formal models even when semantic scores look high.
  • A natural extension would be to test the pipeline on trials with more complex nested temporal constraints, where the paper reports temporal distortion occurs.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

4 major / 5 minor

Summary. The paper proposes CT-TEL, a workflow that uses large language models (LLMs) to translate narrative clinical trial protocols from ClinicalTrials.gov into Temporal Ensemble Logic (TEL) formulas. The pipeline includes ontology mapping, temporal event extraction, four-step TEL formalization, and a back-translation evaluation in which an LLM reconverts the TEL formulas into natural-language protocol text. Fidelity is assessed by human/LLM rating and by lexical/semantic similarity between the original and reconstructed text. The authors report results on 23 Alzheimer's-disease medication trials, including sensitivity ablations and a cross-trial similarity baseline, and claim that the workflow 'rigorously validates' semantic fidelity and scales formal protocol representation.

Significance. If the central claim were supported, CT-TEL would be a valuable contribution: it offers a concrete, reproducible pipeline for turning free-text protocols into executable temporal-logic formulas, with potential downstream use in cohort simulation and model checking. The paper has real strengths: it uses genuine ClinicalTrials.gov data, makes prompts and structured outputs publicly available, includes a cross-trial baseline to contextualize similarity scores, and candidly discusses known failure modes. However, the validation strategy measures text-to-text similarity between original and back-translated protocols, not the correctness of the intermediate TEL formulas. The authors themselves state that embedding-based metrics cannot detect logic errors. As a result, the paper's load-bearing assertion of faithful formalization is not yet established by the reported evidence.

major comments (4)
  1. [Section 3 / Section 4.1 (after Table 1)] The fidelity evaluation measures lexical and semantic similarity between the original protocol text and the LLM-back-translated protocol text, not between the source and the TEL formula. The paper's own sentence in Section 4.1 concedes: 'Embedding-based metrics cannot detect logic errors such as collapsed duration states, hallucinated fields, or incorrect temporal anchors.' This is precisely the gap that matters for the claim that CT-TEL maps protocols to 'computable logical structures.' High text-reconstruction similarity can be achieved even when the intermediate formula is wrong, because the reverse-translating LLM can draw on clinical priors to fill in or alter content. Table 1's scores (e.g., 0.622–0.860) are therefore an upper bound on formula fidelity, not evidence of it.
  2. [Section 4.1, 'Human and LLM-Based Review'] The human expert review also evaluated the reconstructed protocols against the original source, not the TEL formulas themselves. The consensus mean scores (1.89 human, 1.85 LLM) thus speak to the quality of the natural-language reconstruction, not to whether the formalization correctly encodes the trial's temporal requirements. To support the central claim, the authors need at least a direct sample-based review of formulas (e.g., experts checking that each formula's operators, anchors, and durations match the source), or a logic-level comparison such as model checking the original and reconstructed formulas against the same temporal event structure.
  3. [Section 5.1, 'Concept-term masking experiment'] The masking experiment illustrates the same problem. When ontological labels are replaced with opaque placeholders, back-translation similarity drops, as expected, because the reverse-translating LLM loses clinical context. But the authors correctly note that the underlying logical structure might still be accurate. This is exactly the point: the reported semantic scores respond to surface vocabulary, not to the correctness of temporal operators, Boolean structure, or quantifier scoping. The experiment therefore does not validate the formulas; it demonstrates the metric's sensitivity to surface form. The paper needs a separate, logic-level evaluation to substantiate the claim that the formulas are faithful.
  4. [Section 4, 'Example: From Canonical Formula to Protocol Narrative' (Eq. 1)] The worked example for NCT04179721 asserts that the back-translation 'confirms the semantic fidelity of the automated formalization.' This is circular: the back-translation is generated from the very formula it is supposed to validate, and the text is then compared to the source. Without an independent check that the TEL formula's temporal structure (e.g., the 3-month box operator, the 1-month diamond windows, the existential anchor x) matches the protocol's actual requirements, the example is illustrative but not evidential.
minor comments (5)
  1. [Abstract / Section 1] The abstract and introduction describe the validation as 'rigorous,' but Section 4.1 and Section 5.3 acknowledge that the current metrics cannot detect logic-level errors. Consider softening the wording to 'preliminary' or 'text-level' fidelity to align the claims with the evidence.
  2. [Section 2, 'Ensemble Logic'] The phrase 'represented as anatomic proposition p' appears to be a typo for 'atomic proposition p.' Please correct.
  3. [Section 3, 'Evaluation of Translation Fidelity'] The description of the cross-trial similarity matrix is clear, but the text would benefit from stating explicitly that the off-diagonal baseline is computed on text reconstructions and therefore shares the same limitation of not reflecting formula correctness.
  4. [Table 1 / Table 2] The tables are informative, but the captions should note that the similarity scores are text-level measures, not formula-level validations, to prevent readers from interpreting them as direct evidence of logical fidelity.
  5. [Section 5.3, 'Temporal distortion of nested constraints'] The discussion of collapsed duration states is a useful failure analysis, but it would be stronger with a concrete example showing the original text, the generated formula fragment, and the incorrect collapsed form. As written, the reader cannot assess the severity or frequency of this failure mode.

Circularity Check

1 steps flagged · score 4.0 of 10

The 'fidelity' validation is partly circular: the paper assumes formula-to-text bidirectionality and then uses an LLM round-trip as rigorous validation, even though the metric cannot test formula semantics.

  1. self definitional [Section 2 (Logical Representation of Clinical Trials, final paragraph)]
    "Because every formula is built from these five mechanisms, the mapping between free-text protocol statements and logic is bidirectional: a protocol sentence can be compiled into a TEL formula, and a TEL formula can be read back as an unambiguous clinical narrative. This property is exploited by the CT-TEL workflow (Section 3) for both automated formalization and rigorous reverse-translation evaluation."

    The paper asserts as a fact the property that the evaluation must prove: reverse-translating a TEL formula yields a faithful clinical narrative. This assumed bidirectionality is used to justify reverse-translation as 'rigorous' validation of forward-translation fidelity. Forward translation, reverse translation, and LLM-based review are all performed by the same model class (Gemini 3.1 Pro), so the round-trip semantic score measures self-consistency rather than formula correctness. The paper concedes (§5.3) that embedding metrics cannot detect logic errors like collapsed durations, hallucinated fields, or wrong anchors, so the validation reduces to that assumption rather than checking whether formulas match source temporal semantics.

full rationale

The non-circular parts of the pipeline - ontology mapping, library provenance, and off-diagonal baseline controls - are meaningful, and the paper is transparent about limitations. However, the central claim of 'rigorously validating the semantic fidelity' of the TEL formulas relies on a round-trip through the same LLM family and a text-to-text similarity score. This is not an independent ground truth for formula correctness. The human review also targets reconstructed protocol text, not the formulas' logical semantics. Because the conclusion 'Round-trip semantic evaluation ... confirmed that complex clinical timelines can be faithfully rendered into computable logical structures' goes beyond what the metric can establish, the core fidelity argument has a partial self-definitional circularity. Score 4 reflects the presence of independent workflow content and the paper's explicit acknowledgment of the limitation, while still flagging that the validation of the main fidelity claim is not fully independent.

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

No new physical or formal entities are postulated; TEL and QEL are cited from prior work. The main unexamined input is the assumed validity of the LLM-generated formulas and the text-similarity proxy used to measure fidelity.

assumptions (4)
  • domain assumption Temporal Ensemble Logic (TEL) is expressive enough to capture the temporal semantics of clinical trial protocols
    The paper relies on TEL as defined in prior work by the same authors (refs 1, 2, 4) without providing an independent formalization or comparing to other logics beyond a brief background.
  • domain assumption Semantic similarity between original and back-translated text is a valid proxy for TEL formula fidelity
    This is the central evaluation assumption; the paper partially concedes its weakness in §5.3.
  • ad hoc to paper LLM-generated TEL formulas are syntactically valid and well-scoped
    There is no parser or type-checker; the paper only enforces JSON schema on intermediate outputs (Section 3, 'structured output constraints').
  • domain assumption Ontology mapping via UMLS/AD-CDO with human correction ensures variable grounding
    The authors assume the corrected mappings are complete and correct for all 23 trials; no inter-annotator agreement on these corrections is reported.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Scaling Up Formal Representation of Clinical Trial Protocols in Ensemble Logic Using LLMs: A Preliminary Study." pith.science (2026). https://pith.science/paper/HOU5FTS2

@misc{pith2026260721307,
  author       = {Pith},
  title        = {Pith review of: Scaling Up Formal Representation of Clinical Trial Protocols in Ensemble Logic Using LLMs: A Preliminary Study},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/HOU5FTS2}},
  note         = {Machine review of arXiv:2607.21307}
}
read the original abstract

The reliance on unstructured free text for documenting clinical trial protocols creates a significant barrier to automated reasoning, cohort discovery, and trial simulation. The lack of formal structure obscures critical temporal phenotypes, such as dynamic eligibility criteria and event timing constraints. Although Temporal Ensemble Logic (TEL) offers an expressive framework for modeling these elements, manual encoding remains a prohibitive bottleneck. We introduce the CT-TEL workflow: a scalable pipeline leveraging Large Language Models (LLMs) to translate narrative clinical protocols into TEL formulas. We applied CT-TEL to generate logical models for 23 real-world trials from ClinicalTrials.gov. We evaluated translation fidelity via a back-translation approach, using LLMs to convert TEL formulas back into natural language and measuring semantic similarity against source texts. The resulting semantic retention suggests that LLMs may offer a pathway for mapping informal protocols to computable logic, providing preliminary evidence toward scalable clinical trial emulation within the emerging "Symbolic Biomedicine" paradigm championed by the corresponding author.

Figures

Figures reproduced from arXiv: 2607.21307 by the authors.

Figure 1
Figure 1. LLM-driven paradigm: forward translation to TEL, reverse translation, and evaluation. A central challenge for such observational modeling stems from clinical trial protocols. These protocols define eligibility criteria, treatment regimens, follow￾up schedules, and outcome assessments. Each module is inherently temporal, unfolding across specific intervals and involving complex logical dependencies. Because these con… view at source ↗
Figure 2
Figure 2. The CT-TEL Workflow comprises three structural components. Data Sources and Protocol Download. The CT-TEL workflow begins by retrieving trial protocol records directly from ClinicalTrials.gov. Each record is ingested in its native JSON format and includes six modules relevant to clinical events and temporal logic: descriptionModule, conditionsModule, designModule, armsInterventionsModule, outcomesModule, and eligibi… view at source ↗
Figure 3
Figure 3. Hierarchical data schema of the CT-TEL Library with aggregate counts (left) and two worked examples traced through all six levels (right). Arrows denote backward traceability. These blocks are unified into a single canonical TEL formula: Φ = ∃x h φelig ∧ φbase ∧ φtx ∧ φout i (1) Reading this formula as natural language: “There exists a baseline time-point x at which permanently based nursing staff who have not decli… view at source ↗
Figures from the paper (1 more)
Figure 4
Figure 4. Figure 4: Cross-trial semantic similarity per module. Rows correspond to original records and columns to transla￾tions. Axis labels show the last two digits of each NCT identifier, e.g., 90 corresponds to NCT06630390; CL denotes NCT06630390Claude and MS denotes NCT06630390masked…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

16 extracted references · 1 linked inside Pith

  1. [1]

    QEL: Rational Ensemble Logic for Model-Checking-Based Cohort Discovery with Real-World Electrophysiology Data.Under review, 2026

    Zhang, G.-Q., Hao, X., Huang, Y ., Li, X., and Cui, L. QEL: Rational Ensemble Logic for Model-Checking-Based Cohort Discovery with Real-World Electrophysiology Data.Under review, 2026

    2026

  2. [2]

    Temporal ensemble logic for integrative representation of the entirety of clinical trials.32nd International Symposium on Temporal Representation and Reasoning (TIME 2025)

    Li X, Huang Y , Abeysinghe R, et al. Temporal ensemble logic for integrative representation of the entirety of clinical trials.32nd International Symposium on Temporal Representation and Reasoning (TIME 2025). LIPIcs; 2025

    2025

  3. [3]

    Formal representation of eligibility criteria: A literature review.Journal of the American Medical Informatics Association

    Weng C, Tu SW, Sim I, Richesson R. Formal representation of eligibility criteria: A literature review.Journal of the American Medical Informatics Association. 2010;17(1):10-22

    2010

  4. [4]

    Temporal ensemble logic.arXiv preprint arXiv:2408.14443

    Zhang GQ. Temporal ensemble logic.arXiv preprint arXiv:2408.14443. 2024

    arXiv 2024

  5. [5]

    Study Data Tabulation Model (SDTM) [Internet]

    CDISC. Study Data Tabulation Model (SDTM) [Internet]. Austin (TX): Clinical Data Interchange Standards Con- sortium. [accessed 2026 Mar]. Available from: https://www.cdisc.org/standards/foundational/sdtm

    2026

  6. [6]

    Ontology for Biomedical Investigations (OBI) [Internet]

    OBO Foundry. Ontology for Biomedical Investigations (OBI) [Internet]. [accessed 2026 Mar]. Available from: http://obi-ontology.org

    2026

  7. [7]

    The temporal logic of programs

    Pnueli A. The temporal logic of programs. In:18th Annual Symposium on Foundations of Computer Science (SFCS 1977). IEEE; 1977:46-57

    1977

  8. [8]

    Temporal data representation, normalization, extraction, and reasoning: A review from clinical domain

    Madkour M, Benhaddou D, Tao C. Temporal data representation, normalization, extraction, and reasoning: A review from clinical domain. Computer methods and programs in biomedicine. 2016 May 1;128:52-68

    2016

Show all 16 references
  1. [9]

    Using features of Arden Syntax with object-oriented medical data models for guideline modeling

    Peleg M, Ogunyemi O, Tu S, Boxwala AA, Zeng Q, Greenes RA, Shortliffe EH. Using features of Arden Syntax with object-oriented medical data models for guideline modeling. Proc AMIA Annu Symp. 2001:523

    2001

  2. [10]

    BFO: Basic formal ontology

    Otte JN, Beverley J, Ruttenberg A. BFO: Basic formal ontology. Applied ontology. 2022 Mar 15;17(1):17-43

    2022

  3. [11]

    Maintaining knowledge about temporal intervals.Communications of the ACM

    Allen JF. Maintaining knowledge about temporal intervals.Communications of the ACM. 1983;26(11):832-843

    1983

  4. [12]

    A propositional modal logic of time intervals.Journal of the ACM

    Halpern JY , Shoham Y . A propositional modal logic of time intervals.Journal of the ACM. 1991;38(4):935-962

    1991

  5. [13]

    CT-TEL-scaleup: Scaling Up Formal Representation of Clinical Trial Proto- cols in Ensemble Logic Using LLMs [Internet]

    Huang Y , Hao X, et al. CT-TEL-scaleup: Scaling Up Formal Representation of Clinical Trial Proto- cols in Ensemble Logic Using LLMs [Internet]. GitHub; 2026 [accessed 2026 June]. Available from: https://github.com/yhc29/CT-TEL-scaleup

    2026

  6. [14]

    The unified medical language system (UMLS): integrating biomedical terminology

    Bodenreider O. The unified medical language system (UMLS): integrating biomedical terminology. Nucleic acids research. 2004 Jan 1;32(suppl 1):D267-70

    2004

  7. [15]

    AD-CDO: A Lightweight Ontology for Representing Eligibility Criteria in Alzheimer’s Disease Clinical Trials

    Sun Z, Abeysinghe R, Li X, Hu X, Cui L, Zhang GQ, Bian J, Tao C. AD-CDO: A Lightweight Ontology for Representing Eligibility Criteria in Alzheimer’s Disease Clinical Trials. arXiv preprint arXiv:2511.21724. 2025 Nov 20

    2025

  8. [16]

    Bethesda (MD): National Library of Medicine (US)

    ClinicalTrials.gov [Internet]. Bethesda (MD): National Library of Medicine (US). 2000- [accessed 2026 Feb]. Available from: https://clinicaltrials.gov

    2000

Pith tools

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