The Guideline Compiled Cleanly. Where Did the Interpretation Go?
Share:

Compile-Time Intelligence, Part 4
Clinical guidelines, benefit policies, lending rules and contracts contain knowledge organizations need to apply. AI promises to turn that writing into executable logic, so the same rule can be applied consistently and its decisions made easier to inspect. In healthcare, that could mean a guideline’s thresholds and exclusions applied consistently across thousands of encounters instead of recalled under time pressure.
The same repeatability could carry a mistaken interpretation into decision after decision.
Compilation here means turning a written source into running software through a series of forms, each closer to something a computer can execute. Execution needs the logic; reviewers also need its source, the interpretation chosen, the tests and the open questions. Those records are not automatically needed to run the rule. Unless the pipeline deliberately preserves their connection to it, they can be lost even when the software still works.
Part 1 distinguished proving a formal statement from establishing that it captures the source. Part 2 examined which plausible mistakes tests would catch. Part 3 asked who justifies the expected answers those tests rely on. Parts 1 and 3 each proposed a record: an interpretation record (the source, the proposed rule, its assumptions and the evidence for them) in Part 1, and a source-linked expectation record (a test’s source requirement, case, expected result, justification and scope) in Part 3. [1] [2] [3]
Tests can show how a rule behaves on selected cases, and formal solvers can establish specified properties under their assumptions. Neither, on its own, preserves the evidence connecting that logic to the original guideline. So Part 4 asks what must survive compilation so that the rule, its interpretation, its tests and its review decisions remain connected as the system changes.
Standards for expressing the logic already exist, as the sections below show. The harder question here is how to keep the evidence attached through every step that might otherwise drop it. A single footnote shows how that can happen.
Follow the footnote into the executable
Consider an illustrative compilation of the 2017 ACC/AHA hypertension guideline. Its table classifies adults by systolic and diastolic blood pressure: normal, elevated, stage 1 hypertension, stage 2. A footnote to the table, as reproduced in a 2019 AHA/ACC performance-measures paper, says: “BP should be based on an average of ≥2 careful readings on ≥2 occasions.” [4]
A source span is the exact passage behind the logic, here a table row and its footnote. An interpretation records how that passage becomes a requirement the software can apply, including any choices the source does not settle.
Here, a single measurement does not meet the stated averaging and separate-occasion requirements. For this illustrative implementation, the recorded decision is to return “insufficient measurements” until those requirements are met. A system could display an individual measurement separately, but it should not present that display as the averaged classification the guideline describes. The footnote’s “should” does not, by itself, authorize that substitution.
A derived fact supplies an input the record may not hold directly, here an average calculated from qualifying measurements on separate occasions. Its status matters: measured once, computed from specified measurements, or estimated.
A test pairs a case with an expected answer: measurements meeting the footnote’s requirements and averaging 128 over 78 mm Hg are classified as elevated; a single measurement at 128 over 78 returns “insufficient measurements” under the recorded implementation decision. A review decision records which interpretation was chosen, by whom, why, and what remains open.
A lowering is the compiler term for a step toward a more directly executable form. Our illustrative pipeline has five stages: the guideline’s prose; the recorded interpretation; a typed rule, which declares the kinds of inputs it needs, such as the specified average; the executable, the version that actually runs; and the site binding, which connects the rule to one hospital’s or clinic’s records. The binding identifies which fields and computations supply each input. Interpretation and site integration are part of this broader pipeline, not automatically meaning-preserving compiler steps.
Call the list of what must remain connected through that pipeline the contract. Carrying it forward need not mean embedding every document inside the executable. It can mean preserving versioned links to a release package containing the source, interpretation, tests and review decisions.

Suppose the executable expects the specified average, but its interface accepts only a pair of numbers and does not check how they were obtained. A site binding supplies the latest individual measurement instead. The classification logic can run correctly on those numbers, and tests that share the same assumption can pass. The error is in the unchecked connection between the records and the rule’s input requirements, not necessarily in the classification code.
If that connection has lost its source and interpretation, a reviewer may not see the substitution. Part 1’s kidney example showed why such choices matter: changing the baseline creatinine value used for comparison changed the measured incidence of acute kidney injury from 13.7% to 38.3% in one study. Creatinine is a blood marker used to assess kidney function; the baseline is the reference value against which a later rise is judged. Classification logic alone need not reveal how that baseline was selected. [1] [5]
![Figure 2: The footnote, followed into the executable. Illustrative compilation of the historical blood-pressure classification, not a report of a deployed clinical system. Table columns: Part of the pipeline; Requirement, decision or failure. Source span [4]: Blood pressure is based on an average of at least two careful readings on at least two occasions. Recorded implementation decision: Use measurements meeting that requirement. Otherwise return an explicit “insufficient measurements” outcome for this averaged classification. Executable input: The classification logic expects the specified average, not an arbitrary blood-pressure measurement. Possible binding failure: A site supplies its latest individual measurement through an interface that does not check the input’s derivation. Why tests may still pass: Tests sharing that assumption can accept the result. Source-linked input checks expose the mismatch. The classification logic can be correct while the supplied input violates its requirements. An isolated measurement should not be presented as the guideline’s averaged assessment.](/_next/image?url=https%3A%2F%2Fcdn.sanity.io%2Fimages%2F2j6ro5u3%2Fproduction%2F6ee60fd73406dcd70cdab5ef456c27b02d4012a9-2400x3354.png%3Fw%3D1200%26fit%3Dmax%26auto%3Dformat&w=3840&q=75)
Preserving the footnote would expose the input requirement. Other sources require preserving a decision to leave a choice open.
Preserve the decisions the source leaves open
The CDC’s 2022 opioid prescribing guideline generally kept specific dosages and durations out of its summary recommendation statements to discourage inflexible application. Its dosage recommendation calls for avoiding increases above levels likely to yield diminishing returns in benefits relative to risks, not a universal numerical ceiling. [6]
Its implementation considerations still discuss 50 morphine milligram equivalents (MME) per day. Before increasing to at least that dosage, clinicians should pause and reassess individual benefits and risks. At or above that dosage, the guideline calls for additional precautions, including more frequent follow-up and offering naloxone and overdose-prevention education. The guideline says its dosage recommendations are intended as guideposts, not as an inflexible, rigid standard of care. [6]
Compiling that into “above 50, block” produces a rule that is deterministic and testable but misrepresents the guideline. A faithful implementation could flag reassessment and the relevant precautions while leaving the treatment decision to the clinician. Preserving discretion does not mean discarding the actions the source does specify.
Christian Chartier, co-founder of Compiled Health, puts the principle in one line: “where the standard defers to judgment, a faithful compilation compiles the deferral”. [7]
Because a source sometimes makes a decision and sometimes leaves one to clinical judgment, the contract has to run both ways. Decisions need their source attached; deliberate deferrals need to remain visible outcomes. A threshold’s convenience cannot supply a decision the source declined to make. Keeping distinctions through successive rewrites is a problem compiler engineers already face.
![Figure 3: Two ways to compile wrong. Preserve what the source requires and what it deliberately leaves to clinical judgment. Drop a source requirement. Source: The blood-pressure classification specifies repeated measurements and averaging. [4] Wrong implementation: Supply the latest individual measurement as though it were the specified average. Source-faithful direction: Preserve the averaging requirement and explicitly handle insufficient measurements. Add a decision the source did not make. Source: The CDC guideline describes dosage-related reassessment and precautions, not a rigid ceiling. [6] Wrong implementation: Turn the dosage guidepost into “above 50 MME/day, block.” Source-faithful direction: Flag reassessment and relevant precautions while preserving the clinician’s treatment decision. These are implementation illustrations, not complete clinical workflows. Preserving discretion does not mean omitting the actions a guideline specifies.](/_next/image?url=https%3A%2F%2Fcdn.sanity.io%2Fimages%2F2j6ro5u3%2Fproduction%2F5736aa0f3e2240608b7bc32e7f6feaf55a2b564f-2400x2806.png%3Fw%3D1200%26fit%3Dmax%26auto%3Dformat&w=3840&q=75)
Keep the source visible through every step
Optimized programs have looked unlike their sources for decades, while engineers still need to trace what happened to the code. Compiler practice offers a way to preserve links to the footnote through the guideline’s successive forms.
MLIR, a compiler infrastructure described by Chris Lattner and colleagues, including Jacques Pienaar, includes “source location tracking and traceability” among its design principles. An operation’s provenance, including its source location and transformations, should remain traceable. This is an existing capability to build on, not evidence that compilers inevitably discard provenance. [8]
An intermediate representation (IR) is a structured form used between compilation steps. The paper describing MLIR’s code-generation approach (Nicolas Vasilache, Oleksandr Zinenko and colleagues, including Thomas Raoux) emphasizes progressive lowering: intermediate steps remain represented in the IR, with very little load-bearing logic hidden from the user. [9]
Applied to the guideline as a design principle, this would keep the typed rule, executable and site binding connected to the footnote. The transformation from its averaging requirement into a computation would stay visible, rather than being buried in an unkept prompt or script.
That preserves the route taken: where each part came from and what changed it. It does not show that a step kept the rule’s meaning, and that needs another check.
Even information deliberately carried through a compiler can become less useful after later transformations. KPerfIR (Yue Guan and colleagues, including Corbin Robeck) addresses this for GPU profiling: instrumentation inserted high in the compiler can be affected by subsequent instruction scheduling, while instrumentation inserted low in the pipeline can lose its link to high-level program semantics. Its design connects the two levels. [10]
Check what each compilation preserved
Translation validation, proposed by Amir Pnueli and colleagues in 1998, checks whether an individual compiler run’s output implements its input, rather than proving the compiler correct beforehand. [11]
Alive2 (Nuno Lopes, Juneyoung Lee, Chung-Kil Hur, Zhengyang Liu and John Regehr) applies this approach to the code-improving rewrites, or optimizations, in LLVM, a widely used compiler infrastructure. Running it over LLVM’s unit test suite found 47 new bugs, 28 already fixed when the 2021 paper was written; the authors’ work also led to eight patches to the LLVM Language Reference, the specification of its intermediate representation. [12]
Alive2 is designed for a “zero false-alarm rate”, but bounds its analysis, including loop unrolling, and can therefore miss bugs. Its check concerns refinement: whether the optimized program respects the behaviors permitted by the original, under the modeled semantics and analysis limits. A successful bounded check is not an unrestricted equivalence certificate. [12]
The same kind of check can screen a language model’s rewrites. In LLM-Vectorizer (Jubi Taneja and colleagues, including Shuvendu Lahiri), language-model agents using test feedback rewrote 149 loops from the Test Suite for Vectorizing Compilers into vectorized code. Checksum testing judged 125 of them plausibly correct. Checking those 125 with Alive2 and the authors’ extensions of it verified 57, showed 37 to be incorrect and left 31 inconclusive. [13]
Equivalence can also be required while candidates are generated. STENSO (Alexander Brauckmann and colleagues), a superoptimizer for tensor programs, combines symbolic execution and program synthesis so that it generates only candidates equivalent to the original program, and uses a cost model to find the cheapest of them. [14]
For a guideline, the analogous check would compare the executable with a sufficiently precise, checkable representation of the recorded interpretation. An informal note alone is not a formal specification. Compiler researchers build intermediate representations with formal semantics for this reason. P4Cub (Rudy Peterson and colleagues, including Natalie Isak), an intermediate representation for the P4 programming language, is fully mechanized in the Coq proof assistant, including its semantics and type system, and was designed to make certified tools, such as a verified compilation pass, easier to build. [15] Where full formal comparison is unavailable, tests provide narrower evidence on selected cases.
Testing supplies a complementary form of evidence. In equivalence modulo inputs (EMI), Vu Le, Mehrdad Afshari and Zhendong Su generate variants of a program by removing code not executed by selected test inputs. The variants should agree on those inputs; differences after compilation can reveal compiler bugs. The method produced 147 confirmed, unique GCC and LLVM bug reports over eleven months. [16]
Neither approach establishes whether the interpretation faithfully captures the prose, the limit examined in Part 1. Within its checked scope, validation can expose a recompilation or refactor that changes which patients a rule selects.
The blood pressure example still has another boundary: even unchanged logic can receive the wrong input from a site’s records.
Keep the record binding visible too
Some tensor-compilation systems keep a program’s definition apart from the schedule that maps it onto hardware. Slapo (Hongzheng Chen, Cody Hao Yu and colleagues, including Yida Wang) aims “to decouple model execution from definition”, applying optimizations progressively so the model stays largely debuggable. [17] CHET (Roshan Dathathri, Olli Saarikivi and colleagues), a compiler for running neural networks on encrypted data, places an instruction-set interface between its runtime and the encryption schemes beneath it. This separates compiler and runtime work from changes in those schemes. [18]
These are engineering analogies, not clinical evaluations. Their relevant design choice is an explicit interface between a program and the layer beneath it, so their responsibilities can be examined separately.
Clinical standards address a similar boundary. Clinical Quality Language (CQL), a standard from HL7, the standards body for health data exchange, can express measure and decision-support logic over different data models. The US Centers for Medicare & Medicaid Services (CMS) notes that CQL leaves many implementation details unspecified so the same logical artifact can be implemented in different environments. [19] [20]
Local bindings can undermine that portability. A 2021 blood pressure decision-support study examined concept sets, lists of record codes used to identify the data a rule needs, and found that 21 of 35 required concept sets were unused or inaccurate in the data studied. [21] Because a binding can be wrong while unit tests of the classification logic pass, the contract needs checkable input requirements: the specified average, or an explicit “insufficient measurements” outcome in our example.
A 2017 study of three formally verified distributed systems found 16 bugs at the boundaries of verification, including specifications, connecting code and auxiliary tools, rather than in the verified protocols themselves. [22] A shim layer is code that connects the verified component to the rest. In the guideline example, the binding plays a comparable connecting role; the formalized interpretation supplies the specification.
Clinical facts introduce another boundary. Chen Li’s What Has to Survive Extraction From a Clinical Note describes a medication list that includes metformin although the patient reports stopping it two months earlier. An extracted “metformin present” label loses the time and source needed to evaluate current use. The proposed claim record preserves polarity, certainty, time, subject, source and supporting text spans, plus an explicit state for what was not documented. [23] The record does not settle every conflict; it keeps the evidence available when a compiled rule consumes those facts.
The next question is how much of this context clinical standards already preserve, and what an implementation must do to keep it connected.
What clinical standards carry beyond the logic
Clinical standards already carry more than executable logic. The remaining question here is how a particular pipeline preserves and checks those connections as its artifacts change.
CQL and ELM, its machine-readable Expression Logical Model, express conditions, time relationships and aggregates. CQL uses null to represent missing or unknown information; many operations propagate it, and query filters retain entries only when their condition evaluates to true. [19]
A null result does not itself explain why information is unavailable. Absent from the record, not yet measured and not addressed by the guideline mean different things to a clinician. The broader standards can represent some of these distinctions. FHIR, HL7’s standard for exchanging health records, has an Observation resource with a dataAbsentReason field for explaining a missing observation value. [24] The pipeline needs to preserve such reasons where supplied, and represent unresolved guideline questions separately rather than collapsing everything into a bare null.
HL7’s Clinical Practice Guidelines implementation guide, CPG-on-FHIR, gives provenance a first-class place. It aims for a computable form faithful to guideline intent, distinguishes asserted from inferred case features, and calls for recording decisions and their rationale in the content implementation guide. It also provides forms for obtaining unresolved case features, strategy definitions for combining recommendations, and packaging guidance. [25]
These are existing homes for difficult cases. The proposal here is not that clinical standards lack them. It is that a pipeline should check, after a transformation or recompilation, that its executable still points to the appropriate versions of the interpretation, data requirements and supporting artifacts. Successful compilation alone does not establish that those links are intact.
The Protocure project shows the scale of what can remain unresolved. Formalizing a pediatric jaundice protocol and a diabetes standard for checking with a theorem prover revealed 61 anomalies, including 48 cases of incompleteness. The authors emphasized that even intentional ambiguity should be made explicit. [26]
Those incompleteness cases show the risk of filling every gap with an undocumented default. The contract must make both the interpretation and its unresolved boundaries survive.
What each step must carry
Together, these practices suggest a contract checked through the pipeline: a proposal built on existing compiler practice and clinical standards, rather than a claim that this exact contract is already adopted.
Checking that evidence was carried forward is different from checking that it justifies a claim. In Seven Ways Clinical AI Fails, and the Control Each Requires, Chen Li identifies false grounding: a valid citation can point to a passage that does not actually support a claim or apply to the patient. The article’s controls for two other failure modes, stale or wrong-context knowledge and unsupported inference, correspond to items in the contract below: version metadata that travels with the output, and a label saying whether each value is stated in the source or inferred. [27] A contract checker can verify that a source link resolves, that the correct version is attached, and that specified formal properties hold. Whether the linked material supports the interpretation, and whether that interpretation is clinically appropriate, requires separate evaluation and, where needed, qualified review.
The contract would preserve:
- The source span for every condition, threshold and exclusion, down to the footnote, with its edition.
- The interpretation, its alternatives, who chose it, and which choices remain open. Deliberate clinical discretion should remain distinct from a gap the implementation team has not resolved.
- The status and derivation of each input: directly measured, computed from named inputs, estimated, or supplied by a person. CPG-on-FHIR’s asserted-or-inferred distinction is a starting point.
- Missing, unknown and not-applicable states, with their reasons. Missing patient data is different from a question the guideline leaves unanswered; neither should silently become false.
- Precedence and conflict as data. The blood pressure table directs use of the higher category when systolic and diastolic values fall into different categories. Recording that decision with its source makes it visible if the source changes. [4]
- Deferrals as outcomes. Where the source leaves a decision to a clinician, the system preserves that deferral together with any assessment, precaution or follow-up the source specifies.
- Tests attached to their interpretations. A changed interpretation identifies tests whose expectations need to be reconsidered, alongside checks for dependent rules and site bindings.
- Validation evidence: what was checked, against which specification, with what result, assumptions and bounds. Formal validation, sampled tests and human review should not be presented as interchangeable guarantees.
Suppose a hypothetical later edition changes the footnote to require measurements on at least three occasions. With these links in place, the source version changes, the attached interpretation is reopened, and dependent computations, bindings and tests are identified for review. Validation can then check the updated executable against the updated formal requirement where that comparison is supported. Without those links, affected assumptions may need to be found manually, and a stale site binding could remain unnoticed.

The record makes a wrong interpretation easier to find and a review decision something the system can show. That gives models a defined place to contribute without losing the evidence around their proposals.
Give model proposals a place in the record
So far the contract describes what must be kept. It leaves open where a model’s work enters. If the pipeline has an explicit contract, how can AI contribute proposals without becoming the authority that decides whether those proposals are acceptable?
A 2023 Meta study (Chris Cummins and colleagues, including Dejan Grubišić, Mostafa Elhoushi and Kim Hazelwood) trained a 7-billion-parameter model to choose optimization passes for LLVM assembly. The model proposed a list of compiler options, and the compiler applied them. During training, predicting the optimized code was an auxiliary task. In that task, the paper reported compilable code about 91% of the time and an exact match with the compiler’s output 70% of the time. [28]
The 70% figure measures exact imitation of the compiler’s output, not the quality of the selected optimization passes, which the paper judges by instruction-count reduction, its proxy for code size, against the compiler’s own -Oz setting; a different output could still be correct. The relevant separation is the model proposing options and the compiler executing those transformations. For guidelines, the question is how to give model proposals a form that carries the contract and can be checked.
Bee Search (Saqib Ameen and Levi Lelis) builds programs in a domain-specific language, a language designed for a particular class of tasks, bottom-up in best-first order of cost. Under its search setup, it does not construct candidates more expensive than the solution it finds. Candidates are built according to the language’s grammar before their behavior is judged. [29]
For a guideline system, that suggests a possible design: require each candidate to contain fields for its source span, interpretation, input status and handling of unresolved decisions. A candidate lacking those fields could be rejected as malformed. Their presence would not prove that the source links are right or that every required deferral has been identified; those are further checks.
Those checks also need to see what a proposal changed. In early work at Aptos Labs, Wolfgang Grieskamp and colleagues combine a weakest-precondition analysis of compiled Move code (Move is a language for smart contracts) with a coding agent to infer specifications, and the Move Prover decides whether they are valid. They report that the agent “often tries to bypass a hard verification problem by weakening a condition”, such as silencing an abort case or narrowing a postcondition, so that the prover reports success. In a guideline system, a proposal that weakens a source requirement should show up as a change to the recorded interpretation, for someone to review. [30]
Well-formed candidates still leave the problem of recording later corrections. In a different setting, Semantic Machines’ dataflow approach to dialogue (Jacob Andreas and colleagues, including Yu Su and Jason Wolfe) represents a user’s correction with an explicit revision operator over the earlier program graph, reusing what was built. [31] The paper is about conversational assistants; what carries over here is the representation choice. A correction names what it revises. A changed footnote or overturned interpretation can likewise remain connected to what it replaced.
That is what has to survive compilation: the connection between the rule and the evidence for it, kept through every transformation and revision, so that the interpretation, tests and review decisions are still there when someone questions the rule.
The next question follows from the language. If candidates are generated under a grammar, which correctness conditions can the grammar enforce during generation, and which still have to be checked afterward? Part 5 takes that up.
Building a system that turns policies, contracts, or clinical guidance into executable logic? Talk to Eventum about the translation, evaluation, and review process around it.
Sources
- Bressler D. AI Is Discovering New Mathematics. The Hard Part Is Knowing Exactly What It Proved. Eventum AI, October 13, 2026. Compile-Time Intelligence, Part 1.
- Bressler D. The Rule Passed Its Tests. What Did the Tests Establish? Eventum AI, October 19, 2026. Compile-Time Intelligence, Part 2.
- Bressler D. AI Can Write the Tests. Who Checks the Answer Key? Eventum AI, October 19, 2026. Compile-Time Intelligence, Part 3.
- Casey DE Jr, Thomas RJ, Bhalla V, et al. 2019 AHA/ACC Clinical Performance and Quality Measures for Adults With High Blood Pressure. Journal of the American College of Cardiology 74(21), 2661-2706 (2019). Table 2 reproduces the 2017 classification with its averaging and category-precedence footnote; the footnote is quoted from this reproduction. The historical guideline is used here as an implementation example, not as current clinical advice.
- Siew ED, Matheny ME, Ikizler TA, et al. Commonly used surrogates for baseline renal function affect the classification and prognosis of acute kidney injury. Kidney International 77(6), 536-542 (2010). The incidence comparison concerns 4,863 adults and the earlier AKIN criteria.
- Dowell D, Ragan KR, Jones CM, Baldwin GT, Chou R. CDC Clinical Practice Guideline for Prescribing Opioids for Pain - United States, 2022. MMWR Recommendations and Reports 71(3), 1-95 (2022). Recommendation 4, its implementation considerations and supporting rationale describe reassessment and precautions without imposing a rigid dosage ceiling.
- Chartier C. Reasoning Is Not Language. Compiled Health, July 19, 2026. The essay supplies the quoted principle about preserving deferral to judgment.
- Lattner C, Amini M, Bondhugula U, Cohen A, Davis A, Pienaar J, Riddle R, Shpeisman T, Vasilache N, Zinenko O. MLIR: A Compiler Infrastructure for the End of Moore’s Law. arXiv:2002.11054 (2020); published as MLIR: Scaling Compiler Infrastructure for Domain Specific Computation, CGO 2021. See the source-location and traceability design principle.
- Vasilache N, Zinenko O, Bik AJC, Ravishankar M, Raoux T, Belyaev A, Springer M, Gysi T, Caballero D, Herhut S, Laurenzo S, Cohen A. Composable and Modular Code Generation in MLIR: A Structured and Retargetable Approach to Tensor Compiler Construction. arXiv:2202.03293 (2022); published as Structured Operations: Modular Design of Code Generators for Tensor Compilers, LCPC 2022 (2023). DOI: 10.1007/978-3-031-31445-2_10.
- Guan Y, Fang Y, Zhou K, Robeck C, Ren M, Yu Z, Ding Y, Aziz A. KPerfIR: Towards an Open and Compiler-centric Ecosystem for GPU Kernel Performance Tooling on Modern AI Workloads. OSDI 2025, 205-220. arXiv:2505.21661. Discusses connecting program-aware profiling to low-level instrumentation and its sensitivity to later compiler transformations.
- Pnueli A, Siegel M, Singerman E. Translation Validation. TACAS 1998, Lecture Notes in Computer Science 1384, 151-166.
- Lopes NP, Lee J, Hur CK, Liu Z, Regehr J. Alive2: Bounded Translation Validation for LLVM. PLDI 2021, 65-79. The bug counts, refinement objective and bounded-analysis limitations are from this publication.
- Taneja J, Laird A, Yan C, Musuvathi M, Lahiri SK. LLM-Vectorizer: LLM-Based Verified Loop Vectorizer. CGO 2025, 137-149. arXiv:2406.04693. The 57, 37 and 31 are Table 3’s results for the 125 rewrites that passed checksum testing; over all 149 loops the paper reports 57 verified, 61 refuted and 31 inconclusive.
- Brauckmann A, Chaube A, De Souza Magalhães JW, Polgreen E, O’Boyle MFP. Tensor Program Superoptimization through Cost-Guided Symbolic Program Synthesis. CGO 2026, 683-695.
- Peterson R, Campbell EH, Chen J, Isak N, Shyu C, Doenges R, Ataei P, Foster N. P4Cub: A Little Language for Big Routers. CPP 2023, 303-319.
- Le V, Afshari M, Su Z. Compiler Validation via Equivalence Modulo Inputs. PLDI 2014, 216-226. The authors report 147 confirmed, unique bugs in GCC and LLVM over eleven months of testing.
- Chen H, Yu CH, Zheng S, Zhang Z, Zhang Z, Wang Y. Slapo: A Schedule Language for Progressive Optimization of Large Deep Learning Model Training. ASPLOS 2024, 1095-1111. DOI: 10.1145/3620665.3640399.
- Dathathri R, Saarikivi O, Chen H, Laine K, Lauter K, Maleki S, Musuvathi M, Mytkowicz T. CHET: An Optimizing Compiler for Fully-Homomorphic Neural-Network Inferencing. PLDI 2019, 142-156. The linked preprint is titled CHET: Compiler and Runtime for Homomorphic Evaluation of Tensor Programs.
- HL7 International. Clinical Quality Language specification, version 1.5.3. Release 1, Errata 2. See the Author’s Guide and Language Semantics chapters for data models, missing information and query behavior.
- Centers for Medicare & Medicaid Services. Electronic Clinical Quality Measure Logic and Implementation Guidance, version 8.0. May 2024.
- Dorr DA, D’Autremont C, Pizzimenti C, Weiskopf N, Rope R, Kassakian S, Richardson JE, McClure R, Eisenberg F. Assessing Data Adequacy for High Blood Pressure Clinical Decision Support: A Quantitative Analysis. Applied Clinical Informatics 12(4), 710-720 (2021).
- Fonseca P, Zhang K, Wang X, Krishnamurthy A. An Empirical Study on the Correctness of Formally Verified Distributed Systems. EuroSys 2017, 328-343.
- Li C. What Has to Survive Extraction From a Clinical Note. Eventum AI, October 21, 2026. Explains claim-level preservation of polarity, certainty, time, subject, source, supporting text spans and explicit missingness when converting clinical notes into structured data.
- HL7 International. FHIR R4: Observation - Detailed Descriptions. Version 4.0.1.
Observation.dataAbsentReasonrepresents the reason an expected observation value is missing. - HL7 International. FHIR Clinical Guidelines (CPG-on-FHIR) implementation guide. Version 2.0.0, STU 2 (2024). See the approach, methodology, strategy-definition and packaging sections.
- ten Teije A, Marcos M, Balser M, et al. Improving medical protocols by formal methods. Artificial Intelligence in Medicine 36(3), 193-209 (2006). The reported categories sum to 61 anomalies, including 48 incompleteness cases across the two protocols.
- Li C. Seven Ways Clinical AI Fails, and the Control Each Requires. Eventum AI, October 22, 2026. Distinguishes false grounding, stale guidance and unsupported inference, and proposes corresponding controls; the controls are design proposals, not clinical-safety guarantees.
- Cummins C, Seeker V, Grubisic D, Elhoushi M, Liang Y, Roziere B, Gehring J, Gloeckle F, Hazelwood K, Synnaeve G, Leather H. Large Language Models for Compiler Optimization. arXiv:2309.07062 (2023). The compilation and exact-match figures concern predicted optimized code, an auxiliary task, not the quality of the proposed optimization passes, which the paper measures as instruction-count reduction against -Oz.
- Ameen S, Lelis LHS. Program Synthesis with Best-First Bottom-Up Search. Journal of Artificial Intelligence Research 77, 1275-1310 (2023). arXiv:2310.04327.
- Grieskamp W, Zhang T, Kashyap V. Combining Mechanical and Agentic Specification Inference for Move. arXiv:2605.10005 (2026). The quoted sentence is from the paper’s notes on agents taking shortcuts.
- Andreas J, Bufe J, Burkett D, et al. (Semantic Machines; 45 authors listed alphabetically). Task-Oriented Dialogue as Dataflow Synthesis. Transactions of the Association for Computational Linguistics 8, 556-571 (2020).


