Adrianistán

Scryer Prolog Meetup 2023 Notes (day 2)

14/11/2023

This is a continuation of the previous post. In this post, we'll see the talks that happened on day 2.

Verifying safety properties in dose escalation trial design with Prolog - David C. Norris

David Norris works in medical research. In particular, he works on finding the right amount of a new drug for patients. This was a joint work with Markus Triska.

When new drugs are introduced in oncology a dose-finding trial is needed with humans. They need to be done with unhealthy patients because they're too toxic. Also, we can't repeat the experiments with the same patients as the use of the drug modifies the condition of the patient itself.

Both purposes: therapeutic for patients where actual drugs are not working, and scientifically to learn about the correct doses. After 4 weeks, a binary decision. Have we reached Dose-Limiting Toxicity? (DLT)

Only the dose makes the poison - Paracelsus

Scientists like to use the 3+3 method. A simple but underspecified method for dose escalation. Difficult to find a precise description. We can find papers with errors implementing the method.

He implemented a trial workflow with DCGs. Also using constraints. It can generate all possible paths for a trial. With all paths, we can calculate exact properties without Monte Carlo statistical errors... EscRisk app. precautionary package (available for R)

Problems with this first version: not generalizable, lacks depth (doesn't explain previous trials)

Rewrote it to be more general and start from the point of view of making decisions incrementally and how many patients regret taking that dose

Use of reified predicates for decision making. Are they infeasible? Are they regrettable?

After we have this, and a DCG for running and generating paths. We can verify the safety properties of (all) trials and their recommended dose. Backward and forward reasoning thanks to monotonic constraints enables in clpz.

There's a problem with trial design in 3+3. Patients need to wait for other patients to reach the same status to proceed. Wasting time is not optimal. They added extra predicates to allow cohorts of size less than 3.

Current studies show a lot of fine print when doing 3+3 trials. But David can trust his results without needing fine print thanks to LP and the abstractions available in Scryer.

Q&A: A main concern was to model every possible case and not lose any correct solution. So we used clpz, reif, ... But reviewers complained that it (proving there are no mistakes) was slow. Different priorities :)

When declaring reified predicates, it's recommended to add _t to mark it's a reified predicate

Meta-predicates for the answer constraint semantics and constraint-based modelling in Prolog - Dr. François Fage

He started doing Prolog with an internship about unification in equational theories by Term Rewriting Systems in Prolog I.

Later worked on unification of finite and infinite terms (meet Prolog II team!)

Reactive programming with condition-action rules: ASP and semantics of Prolog with negation

Developed Meta(F) finite domain constraint library using freeze/frozen/setarg

Polymorphic subtyping with Prolog using CHR

Developed at INRIA a biological system with 2 languages and 4 semantics at the same time

But he talks about teaching Prolog. Several courses on CLP at École Polytechnique some years ago. But now resumed teaching Prolog. For the subject Constraint-Based Modeling & Algorithms for Decision-Making

They first used MiniZinc for modeling + Python for toy solvers

So, they moved to Prolog in 2023.

Some abstractions are not as nice: lots of focus on recursion and list-oriented constructs, no indexed mathematical variables.

Some Prolog metapredicates were defined before constraints and they have bugs or the way the work is not specified.

Some terminology is inherited and may not be the best one today

Some examples cited:

Bug in frozen/2 in SWI so they had to implement constraints using attr var

Abstractions like foreach loops lose constraints! Maybe add an error if you try to use it with attr var to signal it is not intended to work with it.

Predicates like bagof/3 duplicate constraints (both SWI and Scryer). Should we fix bagof/3, fix clpz or create a correct list_of predicate? Some systems like CHR and SMT simplify their constraints but clpz does not.

So, he developed a for_all library to express loops in a more declarative way using a DSL.

Introduces also a let predicate to allow functional expressions inside but it would be nice to have a mechanism to define functions in Prolog without needing an aux predicate.

He also developed an array library compatible with the for_all library.

He also developed a MiniZinc library which is a MiniZinc parser but solves the problem in Prolog -> useful for debugging.

In the Q&A section, it was debated that maybe the missing key abstraction in Prolog are List Comprehensions.

Prolog for Verification, Analysis and Transformation tools - Prof. Dr. Michael Leuschel

He didn't like Prolog at the beginning. However now we uses Prolog in ProB, a validation tool for high level specs. Like B, Z, Event-B, TLA+, Alloy, CSP, XTL (Prolog). Used in the industry.

B is a language based on set theory. You can execute ProB in a Jupyter notebook.

B uses Unicode symbols. Problems like Send More Money and N-Queens can be solved in B with intersections, set comprehensions, existential operators, etc

There's also a UI and models can run in real-time

Lots of industrial users in train systems.

He uses different ways of interfacing with other languages: C FFI API for Z3, ZeroMQ and sockets for Java UI, Java B code parser, ... Linda (SICSstus) was much slower than ZeroMQ.

They use coroutines extensively: freeze/2, when/2 and block declarations (SICStus). Blocks are less expressive than when but faster and less intrusive.

They're important to implement determinism first propagation (first solve deterministic stuff to reduce search space). Solvers combined via reification.

Process Algebras CSP (Tony Hoare) can be applied to Prolog very closely to formal language.

B requires Type Inference and it's easily encoded in Prolog.

B requires classical negation, not negation as failure. He implements constructive negation by having two interpreters, one for finding solutions, other for finding counter examples.

He showed a comparison between Java and Prolog in TLA+ Translators. Prolog code is much shorter and readable than the equivalent Java code.

Why not Prolog?

Why Prolog?

  • Nondeterminism and unification for encoding semantic/translation rules
  • Coroutines
  • Constraints
  • Tabling (although it doesn't work well with constraints)

    • Q&A: Trains don't run B when they're in production. There's a code generator from B to B0 and later to Ada, C, ... But as we can't prove the code generation is fine, trains run more than 1 system generated differently and they work in tandem.

    Prolog and algebra - Dr. David Stewart

    David Stewart is a mathematician from Manchester. He has been working together with David Cushing and George Stagg on several math papers where they use Prolog to help with the proofs.

    Thanks to CLP they could explore extremely big math objects. While other systems are just brute forcing, their use of CLP makes it work faster.

    The most famous paper they published with this strategy was: You need 27 tickets to guarantee a win on the UK National Lottery.It reached pop science websites and even appeared on the news. NBC television, for example, showed this "interesting" title while discussing the paper and their use of Prolog.

    In the National Lottery you have to guess 6 numbers of 59. To win something you need to guess at least 2. With 27 you can do it. But with 26 not. The difficult thing is trying to prove that wth 26 it was not possible and they used Prolog for that.

    He also discussed the paper: A Prolog assisted search for new simple Lie algebras. He then started to explain what a Lie algebra is and what is a simple Lie algebra

    He later shared his wishes about Prolog

    First, he wanted to have a matrix multiplication constraint. Right now, there's no matrix multiplication constraint. There's a scalar product constraint but it's not usable for their use case. It was discussed whether a specialized constraint in the library would yield more performance or not than than a naive custom one.

    David also said that better term rewriting would be useful as Some equations can be simplified a lot by doing the right variable substitution but CLP doesn't apply it.

    On the Q&A it was said that the lottery ticket scheme is perfect for money laundering

    Grants4Companies: A logic-based AI application in the public sector - Dr. Markus Triska

    Markus Triska is the author of The Power of Prolog book and YouTube channel. He also works for the Austrian government in a department for digital government. They don't develop directly software, however.

    He presents a project developed by the Austrian government that checks which grants apply to each company.

    First, he starts recommending two books:

    The Collapse of Complex Societies by Joseph Tainter. TL;DR societies collapse because of bureaucracy. At some point they reach a level of diminishing benefits

    Le Règne de la Quantité et les Signes des Temps. René Guénon. We're always oscillating between quantity and quality. And now we're in a quantity system.

    The use of AI in the administration must satisfy the three following properties.

    They cannot guess patterns (like statistical AI) since everything we do must be backed by some explanation according to the law.

    They also try to use the minimum needed data and publicly available data (to prevent misuse). They ask for permission before doing any calculation.

    Grants are translated from natural language to a machine-interpretable language. They mix company data and the AI shows applicable grants (and why not to other grants). They use Scryer Prolog although the format of the grants is similar to Lisp.

    As it was contracted work they could not choose everything by themselves./p>

    Current work: adding more grants, more data sources, explaining results, analysis of grants, UX improvements,...

    Grants are not applied automatically since they depend on other entities.

    They're very interested in ISO conforming systems since it's important for the government. We're also using Scryer to explore relations between grants (find contradictions, find subsets/supersets, ...)

    They're very interested in how the system explains why a grant could be applicable or not. He hopes in the future explainability could be more important and even required if a catastrophe in IT happens. The system right now is able to do it, marking in different colors the exact reason why a grant may be rejected

    They use Three Valued Logic (an unknown value) because they might not have the data (Strong Kleene Logic K3)

    Law as Code: Applying logic programming to formalize and analyze laws and regulations - Dr. Björn Lellmann

    Björn also works in the Austrian government like Markus, but his project is more general. He repeats the same stuff about what a public administration needs for its AI.

    A law in itself could be a publicly available logic program, with clearly defined semantics, and follows a formalized, logic-based, executable rule representation.

    >Right now, lots of laws are translated into IT systems by IT persons that are not experts and they can introduce mistakes. Ideally, both versions should be defined in parallel to reduce translation bugs. We can use the help of LLM to help translate the current legal texts into logic programs. But always verifying the output.

    Possible applications: Business grants (G4C), checking evidence requirements (Single Digital Gateway), HR processes, ...

    The aim of the project is to create a basis for technical implementation of laws based on Logical Programming.

    In the showcase they used a Rules Engine provided by Unisys. He shows the UI, it's like a table, very flat difficult to see the hierarchy and the relations of the rules.

    But they have another UI that shows the rules compared to the text. It allows working in parallel with the legal text and the logic program. Also allows exporting to RuleML and Prolog.

    The project is not about having a precise representation of the laws yet. It's more about a proof of concept and the technical environment.

    Using Law as Code while drafting the laws could enable:

    The end goal is not about removing judges and making everything automatic. The human factor needs to stay. Also, some laws are ambiguous as a feature and they do not intend to change that.

    Why Prolog?

    In the Q&A people asked about Catala, a language with similar goals. However, in their (small) experience, Catala was not as easy as Prolog to reason about the laws and rules (and not just executing something).

    End words

    Additionally, Dr. Tomas Veloz could not attend the meeting but he left a recording of his talk, so everyone can see it.

    And that's it! Those were my notes from the Scryer Prolog Meetup. Later we had more offline conversations and we tried the delicious Altbier from Düsseldorf. I hope you find them interesting and I hope there will be more meetups in the future.

    Tags: scryer prolog meetup notes