Tuesday, December 19, 2023

LLM that includes the concept of inference rules

Question: What's the difference between a plain old search engine and an LLM+RAG?
Answer: LLM+RAG provides an experience like semantic search capability plus synthesis but without the need for semantic tagging on the front-end or the back-end. 
[https://www.sbert.net/examples/applications/semantic-search/README.html#semantic-search]

Relevance to the Physics Derivation Graph: add the following to an existing large language model (LLM)

  • the list of inference rules for the Physics Derivation Graph
  • examples of Latex-to-Sage conversion
  • example Lean4 proofs
"fine tuning" versus "context provision"

How is "context provision" different from RAG?

What's the difference between a transformer and a model?

specifically



output of help for llama.cpp

docker run -it --rm  -v `pwd`:/scratch llama-cpp-with-mistral-7b-v0.1.q6_k:2023-12-22 /bin/bash 
root@dc98ac4a23d5:/opt/llama.cpp# ./main -h

usage: ./main [options]

options:
  -h, --help            show this help message and exit
      --version         show version and build info
  -i, --interactive     run in interactive mode
  --interactive-first   run in interactive mode and wait for input right away
  -ins, --instruct      run in instruction mode (use with Alpaca models)
  -cml, --chatml        run in chatml mode (use with ChatML-compatible models)
  --multiline-input     allows you to write or paste multiple lines without ending each in '\'
  -r PROMPT, --reverse-prompt PROMPT
                        halt generation at PROMPT, return control in interactive mode
                        (can be specified more than once for multiple prompts).
  --color               colorise output to distinguish prompt and user input from generations
  -s SEED, --seed SEED  RNG seed (default: -1, use random seed for < 0)
  -t N, --threads N     number of threads to use during generation (default: 20)
  -tb N, --threads-batch N
                        number of threads to use during batch and prompt processing (default: same as --threads)
  -p PROMPT, --prompt PROMPT
                        prompt to start generation with (default: empty)
  -e, --escape          process prompt escapes sequences (\n, \r, \t, \', \", \\)
  --prompt-cache FNAME  file to cache prompt state for faster startup (default: none)
  --prompt-cache-all    if specified, saves user input and generations to cache as well.
                        not supported with --interactive or other interactive options
  --prompt-cache-ro     if specified, uses the prompt cache but does not update it.
  --random-prompt       start with a randomized prompt.
  --in-prefix-bos       prefix BOS to user inputs, preceding the `--in-prefix` string
  --in-prefix STRING    string to prefix user inputs with (default: empty)
  --in-suffix STRING    string to suffix after user inputs with (default: empty)
  -f FNAME, --file FNAME
                        prompt file to start generation.
  -n N, --n-predict N   number of tokens to predict (default: -1, -1 = infinity, -2 = until context filled)
  -c N, --ctx-size N    size of the prompt context (default: 512, 0 = loaded from model)
  -b N, --batch-size N  batch size for prompt processing (default: 512)
  --samplers            samplers that will be used for generation in the order, separated by ';', for example: "top_k;tfs;typical;top_p;min_p;temp"
  --sampling-seq        simplified sequence for samplers that will be used (default: kfypmt)
  --top-k N             top-k sampling (default: 40, 0 = disabled)
  --top-p N             top-p sampling (default: 0.9, 1.0 = disabled)
  --min-p N             min-p sampling (default: 0.1, 0.0 = disabled)
  --tfs N               tail free sampling, parameter z (default: 1.0, 1.0 = disabled)
  --typical N           locally typical sampling, parameter p (default: 1.0, 1.0 = disabled)
  --repeat-last-n N     last n tokens to consider for penalize (default: 64, 0 = disabled, -1 = ctx_size)
  --repeat-penalty N    penalize repeat sequence of tokens (default: 1.1, 1.0 = disabled)
  --presence-penalty N  repeat alpha presence penalty (default: 0.0, 0.0 = disabled)
  --frequency-penalty N repeat alpha frequency penalty (default: 0.0, 0.0 = disabled)
  --mirostat N          use Mirostat sampling.
                        Top K, Nucleus, Tail Free and Locally Typical samplers are ignored if used.
                        (default: 0, 0 = disabled, 1 = Mirostat, 2 = Mirostat 2.0)
  --mirostat-lr N       Mirostat learning rate, parameter eta (default: 0.1)
  --mirostat-ent N      Mirostat target entropy, parameter tau (default: 5.0)
  -l TOKEN_ID(+/-)BIAS, --logit-bias TOKEN_ID(+/-)BIAS
                        modifies the likelihood of token appearing in the completion,
                        i.e. `--logit-bias 15043+1` to increase likelihood of token ' Hello',
                        or `--logit-bias 15043-1` to decrease likelihood of token ' Hello'
  --grammar GRAMMAR     BNF-like grammar to constrain generations (see samples in grammars/ dir)
  --grammar-file FNAME  file to read grammar from
  --cfg-negative-prompt PROMPT
                        negative prompt to use for guidance. (default: empty)
  --cfg-negative-prompt-file FNAME
                        negative prompt file to use for guidance. (default: empty)
  --cfg-scale N         strength of guidance (default: 1.000000, 1.0 = disable)
  --rope-scaling {none,linear,yarn}
                        RoPE frequency scaling method, defaults to linear unless specified by the model
  --rope-scale N        RoPE context scaling factor, expands context by a factor of N
  --rope-freq-base N    RoPE base frequency, used by NTK-aware scaling (default: loaded from model)
  --rope-freq-scale N   RoPE frequency scaling factor, expands context by a factor of 1/N
  --yarn-orig-ctx N     YaRN: original context size of model (default: 0 = model training context size)
  --yarn-ext-factor N   YaRN: extrapolation mix factor (default: 1.0, 0.0 = full interpolation)
  --yarn-attn-factor N  YaRN: scale sqrt(t) or attention magnitude (default: 1.0)
  --yarn-beta-slow N    YaRN: high correction dim or alpha (default: 1.0)
  --yarn-beta-fast N    YaRN: low correction dim or beta (default: 32.0)
  --ignore-eos          ignore end of stream token and continue generating (implies --logit-bias 2-inf)
  --no-penalize-nl      do not penalize newline token
  --temp N              temperature (default: 0.8)
  --logits-all          return logits for all tokens in the batch (default: disabled)
  --hellaswag           compute HellaSwag score over random tasks from datafile supplied with -f
  --hellaswag-tasks N   number of tasks to use when computing the HellaSwag score (default: 400)
  --keep N              number of tokens to keep from the initial prompt (default: 0, -1 = all)
  --draft N             number of tokens to draft for speculative decoding (default: 8)
  --chunks N            max number of chunks to process (default: -1, -1 = all)
  -np N, --parallel N   number of parallel sequences to decode (default: 1)
  -ns N, --sequences N  number of sequences to decode (default: 1)
  -pa N, --p-accept N   speculative decoding accept probability (default: 0.5)
  -ps N, --p-split N    speculative decoding split probability (default: 0.1)
  -cb, --cont-batching  enable continuous batching (a.k.a dynamic batching) (default: disabled)
  --mmproj MMPROJ_FILE  path to a multimodal projector file for LLaVA. see examples/llava/README.md
  --image IMAGE_FILE    path to an image file. use with multimodal models
  --mlock               force system to keep model in RAM rather than swapping or compressing
  --no-mmap             do not memory-map model (slower load but may reduce pageouts if not using mlock)
  --numa                attempt optimizations that help on some NUMA systems
                        if run without this previously, it is recommended to drop the system page cache before using this
                        see https://github.com/ggerganov/llama.cpp/issues/1437
  --verbose-prompt      print prompt before generation
  -dkvc, --dump-kv-cache
                        verbose print of the KV cache
  -nkvo, --no-kv-offload
                        disable KV offload
  -ctk TYPE, --cache-type-k TYPE
                        KV cache data type for K (default: f16)
  -ctv TYPE, --cache-type-v TYPE
                        KV cache data type for V (default: f16)
  --simple-io           use basic IO for better compatibility in subprocesses and limited consoles
  --lora FNAME          apply LoRA adapter (implies --no-mmap)
  --lora-scaled FNAME S apply LoRA adapter with user defined scaling S (implies --no-mmap)
  --lora-base FNAME     optional model to use as a base for the layers modified by the LoRA adapter
  -m FNAME, --model FNAME
                        model path (default: models/7B/ggml-model-f16.gguf)
  -md FNAME, --model-draft FNAME
                        draft model for speculative decoding
  -ld LOGDIR, --logdir LOGDIR
                        path under which to save YAML logs (no logging if unset)
  --override-kv KEY=TYPE:VALUE
                        advanced option to override model metadata by key. may be specified multiple times.
                        types: int, float, bool. example: --override-kv tokenizer.ggml.add_bos_token=bool:false

log options:
  --log-test            Run simple logging test
  --log-disable         Disable trace logs
  --log-enable          Enable trace logs
  --log-file            Specify a log filename (without extension)
  --log-new             Create a separate new log file on start. Each log file will have unique name: "<name>.<ID>.log"
  --log-append          Don't truncate the old log file.

Saturday, December 16, 2023

example interaction with ChatGPT 3.5 to produce a Lean proof

In a new conversation I provided the following prompt:
prompt

Answer the question based on the context below. Let's work this out in a step by step way to be sure we have the right answer.

Context: Lean is a proof assistant and programming language. Lean is based on the calculus of constructions with inductive types.

Context: There are multiple versions of Lean. This question is about Lean 4

`a=b` is a proposition. The variable `a` is Real valued and `b` is Real valued. Prove in version 4 of Lean that `(a=b) -> (a+2=b+2)`

ChatGTP 3.5 wrote in response
ChatGPT 3.5 response

Certainly! To prove the statement `(a = b) -> (a + 2 = b + 2)` in version 4 of Lean, you can follow these steps:

1. **Introduction of Variables**: Begin by introducing the variables and assumptions using the `variables` keyword. In this case, you have the variables `a` and `b` both being Real valued.

```lean
variables {a b : ℝ}
```

2. **Assumption**: State the assumption that `(a = b)`.

```lean
example (h : a = b) : a + 2 = b + 2 :=
```

3. **Transformation**: Use the assumption to transform the left-hand side of the conclusion `(a + 2)` to `(b + 2)` using the property of equality.

```lean
calc
   a + 2 = b + 2 : by rw h
```

Here, `calc` is used to chain together a sequence of expressions, and `rw h` applies the assumption `h`.

4. **QED (Quod Erat Demonstrandum)**: Conclude the proof.

```lean
   example (h : a = b) : a + 2 = b + 2 :=
   begin
     calc
       a + 2 = b + 2 : by rw h
   end
```

This step-by-step approach uses the Lean proof style to demonstrate the validity of the given proposition. The `calc` tactic is particularly useful for chaining together equalities.

On my computer I created a file "second_chatGPT_attempt.lean" and wrote
variables {a b : ℝ}

example (h : a = b) : a + 2 = b + 2 :=
begin
  calc
    a + 2 = b + 2 : by rw h
end
and then ran
docker run -it --rm -v `pwd`:/scratch --workdir /scratch lean3onubuntu lean --run second_chatGPT_attempt.lean
second_chatGPT_attempt.lean:2:0: error: unexpected identifier; expected command
second_chatGPT_attempt.lean:5:0: error: unknown identifier 'begin'
second_chatGPT_attempt.lean:6:2: error: unexpected token 'calc'; expected command
second_chatGPT_attempt.lean:8:0: error: invalid 'end', insufficient scopes
I then told ChatGPT
prompt

When I run the script

```lean
variables {a b : ℝ}

example (h : a = b) : a + 2 = b + 2 :=
begin
  calc
    a + 2 = b + 2 : by rw h
end
```

Lean 4 returns an error message: `error: unexpected identifier; expected command`

What should I do to fix the error?

ChatGPT 3.5 response

Apologies for the oversight. It seems I made an error in my previous responses. In Lean, you should use `theorem` or `example` as part of the proof declaration. Here's the corrected version:

```lean
variables {a b : ℝ}

theorem add_two_eq_add_two (h : a = b) : a + 2 = b + 2 :=
begin
  calc
    a + 2 = b + 2 : by rw h
end
```

In this corrected version, I replaced `example` with `theorem`. You can use `example` as well, but `theorem` is more appropriate when proving statements. This should resolve the error you encountered.

I then created a second Lean script, third_chatGPT_attempt.lean, and wrote
variables {a b : ℝ}

theorem add_two_eq_add_two (h : a = b) : a + 2 = b + 2 :=
begin
  calc
    a + 2 = b + 2 : by rw h
end
which got the same error as before when I attempted to run the script using Lean 4:
docker run -it --rm -v `pwd`:/scratch --workdir /scratch lean3onubuntu lean --run third_chatGPT_attempt.lean 
third_chatGPT_attempt.lean:1:0: error: unexpected identifier; expected command
third_chatGPT_attempt.lean:4:0: error: unknown identifier 'begin'
third_chatGPT_attempt.lean:5:2: error: unexpected token 'calc'; expected command
third_chatGPT_attempt.lean:7:0: error: invalid 'end', insufficient scopes
  

LLM prompts for the Physics Derivation Graph

Posing a prompt that gets a useful result currently requires some consideration. Below are some possible tasks for LLMs, along with additional context for the LLM.

Convert Latex to SymPy

TODO:

Answer the question based on the context below. Keep the answer short and concise. Respond "Unsure about answer" if not sure about the answer.

Context: Latex is software for document preparation to generate PDF files. Mathematical equations can be expressed in Latex using markup syntax. 

Context: SymPy is an open-source Python library for symbolic computation. SymPy provides a computer algebra system. SymPy can convert Latex math to SymPy, and SymPy can render a mathematical expression as Latex.

Question: What is the SymPy representation for the Latex expression $x^2 + y^2 = 1$ ?

Answer:

Right response:

Answer the question based on the context below. Keep the answer short and concise. Respond "Unsure about answer" if not sure about the answer.

Context: Latex is software for document preparation to generate PDF files. Mathematical equations can be expressed in Latex using markup syntax. 

Context: SymPy is an open-source Python library for symbolic computation. SymPy provides a computer algebra system. SymPy can convert Latex math to SymPy, and SymPy can render a mathematical expression as Latex.

Question: What is the SymPy representation for the Latex expression $\vec{p}_{electron} = \vec{p}_{1}-\vec{p}_{2}$ ?

Answer:

Right response:

Answer the question based on the context below. Keep the answer short and concise. Respond "Unsure about answer" if not sure about the answer.

Context: Latex is software for document preparation to generate PDF files. Mathematical equations can be expressed in Latex using markup syntax. 

Context: SymPy is an open-source Python library for symbolic computation. SymPy provides a computer algebra system. SymPy can convert Latex math to SymPy, and SymPy can render a mathematical expression as Latex.

Question: What is the SymPy representation for the Latex expression $x = \langle\psi_{\alpha}| \hat{A} |\psi_{\beta}\rangle$ ?

Answer:

Right response:

Specify the mathematical relation between period and frequency as an equation in Latex

TODO:

Caveat: the page https://en.wikipedia.org/wiki/Frequency includes the statement that

"period is the reciprocal of the frequency: f = 1/T."

Use the context below to produce a result. Keep the response short and concise. Respond "Unsure about answer" if not sure about the answer.

Context: Latex is software for document preparation to generate PDF files. Mathematical equations can be expressed in Latex using markup syntax. 

Context: Period (symbol T) is the interval of time between events. Frequency (symbol f) is the number of occurrences of a repeating event per unit of time

Specify the mathematical relation between period and frequency as an equation in Latex.

Find arxiv papers with derivations

TODO:

  • Explain arxiv
  • define what I mean by a derivation
  • Provide example citations

Provide citations based on the context below. 

Context: arxiv is an open-access repository of electronic preprints

Context: a derivation in mathematical Physics consists of a sequence of steps. Each step relates mathematical expressions to an inference rule. An expression is comprised of symbols and operators. An inference rule typically transforms input expressions into output expressions.

Cite three papers from arxiv that contain mathematical derivations with more than four steps.

Identify derivation steps between physics equations

TODO:

  • define what I mean by a derivation
  • Provide example steps

Answer the question based on the context below. Keep the answer short and concise. Respond "Unsure about answer" if not sure about the answer. Let's work this out in a step by step way to be sure we have the right answer.

Context: Latex is software for document preparation to generate PDF files. Mathematical equations can be expressed in Latex using markup syntax. 

Context: a derivation in mathematical Physics consists of a sequence of steps. Each step relates mathematical expressions to an inference rule. An expression is comprised of symbols and operators. An inference rule typically transforms input expressions into output expressions.

Question: What mathematical steps relate the Latex math expression $i x = log(y)$ and $\exp(i x) = y$ ?

Answer:

Right answer: Raise both sides as the power of $\exp$

Answer the question based on the context below. Keep the answer short and concise. Respond "Unsure about answer" if not sure about the answer. Let's work this out in a step by step way to be sure we have the right answer.

Context: Latex is software for document preparation to generate PDF files. Mathematical equations can be expressed in Latex using markup syntax. 

Context: a derivation in mathematical Physics consists of a sequence of steps. Each step relates mathematical expressions to an inference rule. An expression is comprised of symbols and operators. An inference rule typically transforms input expressions into output expressions.

Question: What is the derivative of $y = \cos(x) + i \sin(x)$ with respect to $x$ ?

Answer:

Right answer: $\frac{d}{dx} y = -\sin(x) + i\cos(x)$

Derive the wave function for a quantum particle in a 1D box

Answer the question based on the context below. Keep the answer short and concise. Respond "Unsure about answer" if not sure about the answer. Let's work this out in a step by step way to be sure we have the right answer.

Context: Latex is software for document preparation to generate PDF files. Mathematical equations can be expressed in Latex using markup syntax. 

Context: a derivation in mathematical Physics consists of a sequence of steps. Each step relates mathematical expressions to an inference rule. An expression is comprised of symbols and operators. An inference rule typically transforms input expressions into output expressions.

Question: derive the wave function for a quantum particle in a 1D box

Answer:

Right answer: see https://derivationmap.net/review_derivation/000010/

Derive Newton's Law of Universal Gravitation

Answer the question based on the context below. Keep the answer short and concise. Respond "Unsure about answer" if not sure about the answer. Let's work this out in a step by step way to be sure we have the right answer.

Context: a derivation in mathematical Physics consists of a sequence of steps. Each step relates mathematical expressions to an inference rule. An expression is comprised of symbols and operators. An inference rule typically transforms input expressions into output expressions.

provide a derivation of Newton's Law of Universal Gravitation

See https://physicsderivationgraph.blogspot.com/2023/06/finding-derivations-of-newtons-law-of.html

Convert derivation steps to a proof in Lean

TODO:

  • define what I mean by a derivation
  • Explain lean
  • Provide example
  • Emphasize correctness and precision

Answer the question based on the context below. Keep the answer short and concise. Respond "Unsure about answer" if not sure about the answer. Let's work this out in a step by step way to be sure we have the right answer.

Context: Lean is a proof assistant and programming language. Lean is based on the calculus of constructions with inductive types.

`a=b` is a proposition. The variable `a` is Real valued and `b` is Real valued. Prove in Lean that `(a=b) -> (a+2=b+2)`

Identify symbols in latex arxiv papers

TODO:

  • Provide example
  • Emphasize correctness and precision

Answer the question based on the context below. Keep the answer short and concise. Respond "Unsure about answer" if not sure about the answer.

Context: Latex is software for document preparation to generate PDF files. Mathematical equations can be expressed in Latex using markup syntax. 

Question: What mathematical expressions are present in the following Latex?

```
\begin{equation}
a = b + c
\end{equation}
Assuming you know $b$, then
\begin{equation}
b*c = f
\end{equation}
```

Answer:

Answer the question based on the context below. Keep the answer short and concise. Respond "Unsure about answer" if not sure about the answer.

Context: Latex is software for document preparation to generate PDF files. Mathematical equations can be expressed in Latex using markup syntax. 

Question: What variables are present in the following Latex?

```
\begin{equation}
a = b + c
\end{equation}
Assuming you know $b$, then
\begin{equation}
b*c = f
\end{equation}
```

Answer:

best practices for prompts for large language models - LLMs

ChatGPT was made available by OpenAI on 2022-11-30. As of 2023-12-16 I hadn't used ChatGPT (Generative Pre-trained Transformer) or other large language models (LLMs). In this post I document best practices other folks have come up with. My intent is to identify whether ChatGPT could be useful for tasks relevant to the Physics Derivation Graph. 

Sites I reviewed for best practices for prompts:

General text response

Prompt

Answer the question based on the context below. Keep the answer short and concise. Respond "Unsure about answer" if not sure about the answer.

Context: <context>

Question: <question>

Answer:

Prompt

Before providing the answer, state what you know and what you assume. Then state the steps that led you to your answer. Finally, provide the answer.

Prompt

Let's think step by step.

Prompt

Let's work this out in a step by step way to be sure we have the right answer.

Prompt

Imagine three different experts are answering this question.
All experts will write down 1 step of their thinking, then share it with the group.
Then all experts will go on to the next step, etc.
If any expert realizes they are wrong at any point then they leave.
The question is...


What to use an LLM for

The following table is from https://www.philschmid.de/instruction-tune-llama-2
Capability Example Instruction
Brainstorming Provide a diverse set of creative ideas for new flavors of ice cream.
Classification Categorize these movies as either comedy, drama, or horror based on the plot summary.
Closed QA Answer the question 'What is the capital of France?' with a single word.
Generation Write a poem in the style of Robert Frost about nature and the changing seasons.
Information Extraction Extract the names of the main characters from this short story.
Open QA Why do leaves change color in autumn? Explain the scientific reasons.
Summarization Summarize this article on recent advancements in renewable energy in 2-3 sentences.


Software generation

You are an expert programmer that writes simple, concise code and explanations. Write a python function to generate the nth fibonacci number.
 
A simple python function to remove whitespace from a string
  Code Llama supports a special prompt called infill
<PRE> def compute_gcd(x, y): <SUF>return result <MID>

Code review

Where is the bug in this code?
```
def fib(n):
    if n <= 0:
        return n
    else:
        return fib(n-1) + fib(n-2)
```

Tests of Software

write a unit test for this function:

Prompts for Retrieval Augmented Generation (RAG)

RAG = https://www.promptingguide.ai/techniques/rag 

    You are an expert Q&A system that is trusted around the world.\n"
        "Always answer the query only using the provided context information, "
        "and not prior knowledge."
        
 
      "Context information is below.\n"
            "---------------------\n"
            "{context_str}\n"
            "---------------------\n"
            "Given the context information and not prior knowledge, "
            "answer the query.\n"
            "Query: {query_str}\n"
            "Answer: "
      

 

From https://docs.llamaindex.ai/en/stable/examples/prompts/prompts_rag.html

Context information is below.
---------------------
{context_str}
---------------------
Given the context information and not prior knowledge, 
answer the query asking about citations over different topics.
Some examples are given below.

{few_shot_examples}

Query: {query_str}
Answer: 
  

Sunday, September 3, 2023

notes from Preposterous Universe podcast episode 245

Notes from the podcast https://www.preposterousuniverse.com/podcast/2023/07/31/245-solo-the-crisis-in-physics/

Definitions of Understanding

  • Strong understanding = unique, well-tested theory that accounts for all the data we have within the domain of applicability (defined by SMC at 14:00). 
    • Consequences: There are no competing theories. Modifications or extensions are feasible, but the domain is "solved." The theory won't be displaced.
    • Examples: general relativity, Newtonian dynamics, Newtonian gravity.
  • Weak understanding = more than one theory can account for the data. Unable to discriminate which is relevant since theories make the same predictions. (defined by SMC at 15:44)
    • Consequences: Not clear theory which is right. Right theory may not have been invented yet.
    • Examples
      • Foundations of quantum mechanics (e.g., Copenhagen interpretation, Bohemian, many worlds, jaggets platz)
      • dark matter and dark energy in cosmology. Properties are known, but multiple theories
        • dark matter: WIMPS, axions, 
        • dark energy: vacuum energy, dynamical quintesense-like fields
  • No understanding = have data but no theory (defined by SMC at 18:20)
    • Examples: what happens at or before the big bang
SMC's claim: We have either a strong or weak understanding of everything that is accessible through measurement. (at 21:40) There's nothing that's experimentally accessible and not understood. That's new!


Survey of domains and relations

What is it that we know?

Newtonian dynamics. Space is separate from time. Deterministic Laplacian evolution.

Theory of relativity (1905, Einstein) explains space-time (as per Minkowski, 1907).  (SMC: 29:22)
Special Relativity: how space-time is when gravity is not important; when space-time is flat. (SMC 30:20)
General Relativity: space-time can be curved and that curvature is gravity. Predicts big bang, black holes. SMC 30:10)

Quantum Mechanics (1920, Heisenberg).
Replaces classical mechanics -- SMC 32:10
QM is about continuous wave function defined by Schrodinger Equation. 
Solving Schrodinger's Equation results in discrete solutions -- SMC 35:55

Quantum Field Theory
Under the umbrella of Quantum Mechanics -- SMC 32:33.
QFT is compatible with Special Relativity -- SMC 32:42
The world is made of fields, not particles. -- SMC 34:40
Fields resolve into particles when the fields are observed.

Relativistic QFT includes Special Relativity

Quantum Electrodynamics (QED) is the theory of interactions of electrons, positrons, photons.
Initial theory had infinities. Resolved infinities using renormalization by taking limit in a specific way.

Ken Wilson simulated QED using discretized space-time (rather than a continuous PDEs).
--> Lattice Quantum Field Theory eliminates the infinities. 
Infinities (represented as loops of Feynman diagrams) are reduced to (non-infinite) tree diagrams in Feynman diagrams. 
Rather than arbitrarily large momentum (small space), discretization constraints the infinities.
Limitation on the domain of applicability is the Planck scale. -- SMC 45:20
This is the ultraviolet cut-off. There's an energy above which we don't know what's going on. -- SMC 46:05


stopped at 53:30

Saturday, August 26, 2023

HTML arxiv papers, semantic tagging, and formal verification

arxiv recently started experimenting with converting .tex files to HTML: https://info.arxiv.org/about/accessible_HTML.html

The first official announcement was in February 2022:
https://blog.arxiv.org/2022/02/21/arxiv-articles-as-responsive-web-pages/

The HTML from .tex effort is a collaboration between Deyan Ginev (a student of Dr. Kohlhase) and Bruce Miller (at NIST - https://www.nist.gov/people/bruce-r-miller). Kohlhase's group (https://kwarc.info/research/) focuses on semantic enrichment of Latex. Bruce provided the software to convert Latex.

The reason for this Latex to HTML conversion is because it's the first step for enabling semantic enrichment of content on the arxiv. There's immediate benefit for arxiv being able to support HTML, which I suspect is why arxiv cooperated with Kohlhase's group.

In the long term I see a need to connect semantic tagging (the focus of Kohlhase's group) with formal verification (e.g., derivations-as-proofs using Lean). The formally verified math expressions need to be tied to use in narrative text (e.g., arxiv papers). For example, if I'm referring to "x" in a publication, is that the same "x" specified in a Lean-based proof? One way of answering is to use tags like

<unique_variable_id=42>x</unique_variable_id>
 
in the narrative text document, and then have Lean reference the ID 42 in derivations. There are more conventional uses of tags like
<properties name_of_variable="distance" dimension_of_variable="length">x</properties>
but those tags don't address the question of whether two variables refer to the same concept.

Summary

I predict that the conversion of arxiv .tex files to HTML will enable semantic tagging. This will intersect with the challenge of "how do I relate the use of variables and expressions across multiple proofs in Lean?"

Saturday, August 12, 2023

a chain of custody for papers in arxiv to formal proofs in Lean

Papers published in arxiv using Latex contain narrative text and mathematical expressions. How could we have confidence that the content of a published paper is related to a formal proof?

The narrative text would refer to symbols, expressions, units, and quantities. The expressions and symbols could be embedded in the Latex source using a package that provides macros.

The author's .tex would include loading a package like

\usepackage{pdg}[server_address=http://serveraddressforpdg.net]

Then when the author references an expression they would use

\begin{equation}
\pdgexp{192839}
\end{equation}

When compiled to PDF, the macro \pdgexp calls to the server address http://serveraddressforpdg.net to return the Latex expression. The same could be done for an inline reference to a symbol, like \pdgsymbol{93831911}

In this approach there wouldn't need to be an appendix for the derivation because the derivation steps are hosted on the PDG server.

The chain of custody would be

arxiv PDF -- arxiv .tex -- .tex contains references to PDG expression and symbol IDs -- PDG server contains derivation steps -- steps are validated using Lean


The macro might need to cache the PDG database locally so the server doesn't get called every time the .tex is compiled PDF. 
Also, allow the author to force a refresh of the cache.

Sunday, June 18, 2023

software for numerical calculations of derived expressions versus implementation of an algorithm

Suppose I have a Python program that takes "angle" and "initial speed" as arguments and calculates where a ball shot from a cannon lands. The program could be described using the function

f(\theta, s) = d

where \theta is the angle, s is the speed, and d is the distance from the cannon where the ball lands. The function could be expressed using a variety of languages like Python, C, Lean, etc.

If f(\theta, s) = d is derived from the equations of motion (like https://derivationmap.net/review_derivation/201726/) and each step is verified using Lean (as described in this post), then we can use Lean to calculate d from \theta and s. The difference would be that there's more explanation of where the result came from. Rather than just "here the equation to use," including the derivation step and proof of each step makes the assumptions explicit and the implementation correct. 


All software programs can be described as functions that take arguments and return results. That doesn't mean that all functions are derived. As an example of software that is a function but isn't derived, consider the A* routing algorithm. An algorithm outlines a sequence of steps for accomplishing a function.

While all programs could be written in Lean (because each program is a function), not all functions are derived mathematically. As a trivial example, printing "hello world" is not a derived function. In contrast, the first example in this post, the distance a projectile flies, is derived from the equations of motion. What distinguishes "hello world" and A* routing from the cannon ball trajectory?

The distinction is that the cannon ball example is a numerical simulation of a tangible scenario, whereas "hello world" is not describing physically-constrained reality. 

For numerical simulations, Lean can formally verify the derivation and the formula used for analytical calculation. Keeping both aspects in Lean results in a clear chain of custody. 

For algorithms (e.g., A* routing, "hello world"), the verification is to show that the implementation is consistent with the requirements. Here languages like Dafny and F* are relevant.

More on F*:

More on Dafny:


Floats in Lean

float is not a ring.
Nor is there an injection; inf is not a real

relation between Inference Rules in the Physics Derivation Graph and Proofs in Lean

In this post I explore the concept that each derivation can be phrased as a proof of the initial declaration and the final result. Also, each step in a derivation can be phrased as a proof.

Lean Proofs of Derivation Steps

As per https://stackoverflow.com/questions/41946310/how-to-prove-a-b-%E2%86%92-a-1-b-1-in-lean Lean can prove that

(a=b) -> (a+1=b+1)

In comparison, a PDG Inference Rule is more generic:

add __ to both sides of (LHS=RHS) to get (LHS+__=RHS+__)

The PDG Inference Rule is generic because the types of LHS and RHS are undefined. Are they Real? Complex? Matrices?

The relevance of types for inference rules is because mixing types may not work. "Add 1 to both sides of (LHS=RHS)" won't work if LHS and RHS are 2x2 matrices.  

Friday, June 16, 2023

Translating between Physics Derivation Graph concepts and features in the Lean Theorem prover

In the blog post I try to figure out how all of those concepts map to features in Lean Theorem prover.

Concepts and relations of concepts in the Physics Derivation Graph

In the Physics Derivation Graph a derivation is comprised of steps. Each step has one inference rule. Inference rules can have

  • zero or more input expressions
  • zero or more output expressions
  • zero or more feed values
Each expression is comprised of a LHS, RHS, and relation. "Relation" can be =, >, <, <=, >=.
The LHS and RHS and Feed values are comprised of symbols (e.g., a, b, x, y) and operators (e.g., *,+,/). 
Symbols are variables (e.g., a, b, x, y) or constants (\pi, e).

How Physics Derivation Graph concepts map to Lean


I think a PDG input expression is a proposition in Lean.
I think a PDG step is a theorem in Lean. 
Maybe the PDG output expression is a goal in Lean?
I think a PDG inference rule is a tactic in Lean. See https://leanprover.github.io/reference/tactics.html

"The type of a function that can inspect the proof state, modify it, and potentially return something of type A (or fail) is called tactic A.
source: https://leanprover-community.github.io/extras/tactic_writing.html


Equivalence of the PDG derivation step "add 2 to both sides of a=b to get a+2=b+2" with using Lean for the proof "(a=b) -> (a+2=b+2)"

In the Physics Derivation Graph the expressions "a=b" and "a+2=b+2" are related by the inference rule "add __ to both sides".

In Lean, "a=b" is a proposition. We have to specify that a is Real and b is Real. Then we can prove that
(a=b) -> (a+2=b+2)

Work in progress -- try something like
see also

Thursday, June 15, 2023

computer algebra system (CAS) is inadequate for the Physics Derivation Graph (PDG)

I'm beginning to appreciate that a computer algebra system (CAS) is not sufficient for the Physics Derivation Graph (PDG). The evidence of this is that the variables I'm defining can be real or complex; that is not distinguished by the computer algebra system.

The simple story of starting with

a = b
and then adding 2 to both sides to get
a+2 = b+2
is appropriate for a computer algebra system. But if "a" is a matrix then the operation is invalid. The only way to distinguish "scalar a" from "vector a" from "matrix a" is to specify the difference. [SymPy does have support for predicates -- https://docs.sympy.org/latest/guides/assumptions.html#predicates .]

In the Physics Derivation Graph I want to be more specific about the possible values of a and b. Even for non-physics derivations like the Euler equations, there are assumptions about the possible values of each variable.

I don't know Lean, but I also don't know the foundational concepts of theorems and proofs.
Is a step a theorem?
Is a derivation a theorem?
The role of inference rules in steps in derivations does not map to anything in a theorem.

Sunday, June 11, 2023

chain of custody for formally-verified software

Relating disparate sources of knowledge in science involves:

  • Formally-verified Mathematical Physics (e.g., in Lean). Purpose: verify the mathematical model is consistent with specified axioms.
  • Formally-verified software; see https://physicsderivationgraph.blogspot.com/2022/10/tla-comparison.html for a list.
  • Performant parallelized software (e.g., MPI + OpenMP + Fortran or C/C++) for High Performance Computing (HPC).
  • Peer-reviewed journal articles, e.g., arxiv; rendered using Latex. [Of the four, this has historically been closest to the focus of the Physics Derivation Graph.]

Each of these content sources are independent and involve expressing a mathematical model in different ways. 


While kernels of mathematical models can be implemented in formally-verified software, a lot of scientific computing uses High Performance Computing (HPC). In the HPC realm the compilers and libraries and runtimes can all be sources of bugs. 

Need to compile or interpret software with a verified compiler or interpreter. 


How can the consistency of content across sources be ensured? 

There are 6 bilateral transitions for the 4 sources. For example, how does the model transition between theorem prover (e.g., Lean) and formally-verified software implementation?


Another possible issue: provenance

May need to track provenance of the source code to binaries. Is the verified algorithm what was provided to the compiler? Is the binary I'm currently using related to the compiler output? Need to be able to distinguish "binary I don't know the origin of" from "binary that has a known chain of custody." 

This could be just a log of hashes coupled to metadata for the "where did this come from." The provenance needs to include versions for compilers and libraries and runtimes. The binary should be reproducible. See https://en.wikipedia.org/wiki/Reproducible_builds

Saturday, June 10, 2023

Finding Derivations of Newton's Law of Universal Gravitation online

Question: was Newton's law of universal gravitation found empirically (from measurements) or can it be derived mathematically? The short answer is yes -- both. The historical process is separate from what can be done now.

Empirical (historical) route

The second paragraph of the Wikipedia article on Newton's Law of Universal Gravitation says, "This is a general physical law derived from empirical observations by what Isaac Newton called inductive reasoning." There's a video on YouTube describing that Newton started with

  • acceleration of gravity on earth, g = 9.8 m/s^2
  • distance between Earth and Moon = 60*(radius of earth)
  • radius of Earth = 
  • orbital period of moon = 27.32 days

Newton figured out how fast the Moon is circling the Earth using

 velocity = distance/time
where, in the case of the moon circling the Earth,
 distance the moon travels around the Earth = circumference = 2*pi*r_{orbit of Moon}

Plugging in numbers, velocity of Moon around Earth = 1022 m/s. That can then be plugged into the centripetal acceleration,

a_{centripetal} = v^2/r
How does a_{centripetal} compare to the gravitational acceleration g?
g/a_{centripetal} = 60^2

Noticing the 60 is common to the ratio and the distance between the Earth and the Moon, Newton figures that gravitation follows an inverse square law. Newton then checked this against data from observational studies of planets.

That's a big leap to F = G*(M*m)/(r^2), so are there more mathematical routes?

Mathematical Derivations

From nasa.gov

I first found NASA's classroom materials. There are some leaps that I wasn't able to follow. The same content of that page is duplicated on a related NASA page. The derivation starts with F=ma and a_{centripetal} = v^2/r. The author mentions Kepler's Third Law but says T^2 \approx R^3 (which is dimenionally inconsistent) when they mean T^2 \propto R^3. The misuse of \approx and \propto continues throughout the rest of the derivation.

velocity = distance/time
and the distance here is the circumfrence, 2*pi*r, so
period T = (2*pi*R)/v

Drop the 2*pi to get

period v \approx R/T
Square both sides and apply Kepler's Third law
T^2 \propto R^3
to get
v^2 \propto 1/R

The second source of my confusion is subscripting versus superscripting -- v_2 versus v^2.

F = (m*(v^2))/R

I tried submitting a correction to NASA's feedback page but couldn't since the Captcha is missing. :(


From a tutorial

Next I found another student-oriented page that has a derivation which is even less helpful than NASA's. The derivation presented starts from angular speed and F=mr\omega^2.


YouTube tutorial

Happily I found this helpful video from Daniel M, "Deriving Newton's Law of Universal Gravitation".

automating entry of derivations into the Physics Derivation Graph website

What would it take to integrate support for symbol detection and conversion to SymPy for a single step in a derivation?
  1. user provides initial expression in Latex to web UI.
  2. computer parses symbols and operators from Latex
  3. computer searches Physics Derivation Graph database of symbols and operators to find candidate symbols
  4. computer provides candidate symbols to user and prompts, "which of the following symbols were you referring to?"
  5. computer parses expression to SymPy, returns AST to user, and prompts, "is this the AST you meant?"
  6. if yes, continue; if no, go back to step 1 or provide corrections to AST.
  7. user provides next expression in Latex
  8. computer parses symbols and operators from Latex
  9. if symbols match symbols used in this derivation, then associate with those; otherwise 
  10. computer searches Physics Derivation Graph database of symbols and operators to find candidate symbols
  11. if computer had to search PDG database, then computer provides candidate symbols to user and prompts, "which of the following symbols were you referring to?"
  12. computer parses expression from step 7 to SymPy, returns AST to user, and prompts, "is this the AST you meant?"
  13. computer uses brute force to check every inference rule using a CAS against the provided expressions to "guess" the inference rule. 
  14. if valid inference rule is found, continue to next expression; if no valid inference rule is found, prompt user to provide inference rule.
  15. Given the inference rule and associated expressions, use the CAS to verify the step.

Tuesday, June 6, 2023

historical evolution of a git repo

JSON-like output
git log --date=format-local:'%Y-%m-%d %H:%M:%S' \
--pretty=format:'{%n  "commit": "%H",%n  "author": "%aN <%aE>",%n  "date": "%ad",%n  "message": "%f"%n},' > all_logs.dat

as per https://stackoverflow.com/a/34778736/1164295 and https://gist.github.com/textarcana/1306223 which points to https://gist.github.com/textarcana/1306223

python3 -c "import json; 
with open('all_entries','r') as fh:
    content = json.load(fh)
print(content)"
Single line is better:
git log --date=format-local:'%Y-%m-%d %H:%M:%S' --pretty=format:"%H%x09%ae%x09%ad%x09%s" > all_hash

TODO:

  • how many commits per year?
  • sample the git repo at a given frequency and count number of files in the sample

general approach:

git clone [remote_address_here] my_repo
cd my_repo
git reset --hard [ENTER HERE THE COMMIT HASH YOU WANT]

as per https://stackoverflow.com/a/3555202/1164295

loop over relevant hashes:
git clone https://github.com/allofphysicsgraph/proofofconcept.git
cd proofofconcept
find . -type f | grep -v ".git" | wc -l
    3381
git reset --hard f12795798d2537d3fec80ba2b4d33396e52011bd
find . -type f | grep -v ".git" | wc -l
       2
number of commits in a year:
cat all_hash | grep 2014- | wc -l
      17
for year in {2014..2023}; do commits_per_year=`cat all_hash | grep ${year}- | wc -l`; echo $year $commits_per_year; done
2014 17
2015 234
2016 62
2017 41
2018 81
2019 30
2020 790
2021 67
2022 90
2023 5
for year in {2014..2023}; do this_hash=`cat all_hash | grep $year | head -n 1 | cut -c-40`; git reset --hard $this_hash; file_count=`find . -type f | grep -v ".git" | wc -l`; echo $this_hash $year $file_count; done > counts_per_year.dat
cat counts_per_year.dat | grep -v HEAD
4289c2a3311d4e051bdab3b0d99f49b25dab6bc3 2014 1027
b81d6ddba5a2015d328975607318d7e7755b27aa 2015 3339
26b0d9fc8c49ede12c897b4bf4cd050765747a81 2016 2098
eec25f59649a4cc9e9e8b166355793b58b742672 2017 2194
201822fd2025349f8749b9433533d0d54c7363b3 2018 3007
918245c17bece668f868ce7201976e2d49dc1743 2019 3022
bd4fb0528c1a46ed2fac13aa16f77508aaa43e67 2020 3150
7dd27b734673e20e405cd26acbdf7d237cf73e33 2021 3343
ad8dfc5931922788f32a21f10906d97c50f7ca36 2022 3384
9df026b16827dfe97fc8a44c4063e493c21a49d4 2023 3384

Sunday, June 4, 2023

summarization, information retrieval, and creative synthesis

Large Language Models like ChatGPT are a hot topic due to the novelty of results in multiple application domains. Stepping back from the hype, the central capabilities seem to include summarization of content, information retrieval, and creative synthesis. Unfortunately those are not separate categories -- the summarization or information retrieval can contain hallucinations that get stated confidently.

Focusing on the topic of information retrieval and setting aside hallucinations, let's consider alternative mechanisms for search:  
  • plain text search, like what Google supports
  • boolean logic, i.e., AND/OR/NOT
  • use of special indicators like wild cards, quotes for exact search
  • regular expressions
  • graph queries for inference engines that support inductive, deductive, and abduction
Except for the last, those search mechanisms all return specific results from a previously collected set of sources. 

--> I expect conventional search to remain important. There are cases where I really am looking for a specific document and not a summarization.

--> Specialized search capabilities like regular expressions and wild cards will remain relevant for matching specific text strings. An LLM might provide suggestions on designing the regex?

--> Graph queries rely on bespoke databases that LLMs are not trained on currently. I'm not aware of any reason these can't be combined. 

The Physics Derivation Graph effectively provides a knowledge graph for mathematical Physics. Combining this with machine learning is feasible.

use of the Physics Derivation Graph is driven by incentives for individuals

Semantic tagging of documents has the potential of enriching the reader's experience because content is easier to search. The burden of work is on the document author to provide the right tags. Worse, the document author has to find tags that are common to uses in other documents -- consistency of tags is necessary for search. This extra work of 1) tagging and 2) using consistent tags are reasons semantic enrichment hasn't become mainstream. 

The Physics Derivation Graph faces a similar challenge. If the Physics Derivation Graph relies on using appropriately annotated symbols (effectively equivalent to a subset of semantic tags), then the PDG has the same burdens of work on individual authors. 

The incentive for the individual researcher authoring a paper to use the Physics Derivation Graph is when there's integration with a computer algebra system that can check the correctness of steps. Then the author benefits from immediate feedback before sharing with others for review.

Annotating symbols probably isn't sufficient to motivate the work, but integration with a computer algebra system could provide incentive. Currently, the use of a computer algebra system requires detailed steps to be specified by the author. 

There are ways to partially automate both symbol annotation and specifying steps. For symbol annotation, the computer could guess from context which symbols are being used. In a similar reliance on context, the user could provide leaps in specifying a derivation that the computer then tries to fill in with the detailed steps.

Wednesday, May 31, 2023

OpenAI's process supervision for math problems and relevance to the Physics Derivation Graph

OpenAI just announced (see https://openai.com/research/improving-mathematical-reasoning-with-process-supervision) progress on solving math problems using process supervision during training.

The data on https://github.com/openai/prm800k/tree/main comes from https://github.com/hendrycks/math (which is for https://arxiv.org/pdf/2103.03874.pdf) and there are examples in that data which come from https://artofproblemsolving.com/wiki/index.php/2015_AIME_II_Problems/Problem_6

AoPS describes itself as "Math texts, online classes, and more for students in grades 5-12."

The problems are constrained and feel very artificial. See for example https://artofproblemsolving.com/wiki/index.php/Mock_AIME_1_Pre_2005_Problems/Problem_4

The training data doesn't have inference rules, so the output from the LLM doesn't have inference rules. As a consequence, the output of the LLM cannot be confirmed by a Computer Algebra System. The output text needs to be validated by a human. LLMs are hallucinating answers that sound reasonable, so checking each step is still vital. 

The ability to resolve distinct variables across all of Mathematical Physics is beyond the scope of the training data. 

On a positive note, if the Physics Derivation Graph content existed, I now think an LLM-based approach could be used to make progress in Mathematical Physics.

Saturday, May 27, 2023

tracing Python in JSON-based workflow is untenable

I added

def mytrace(frame, event, arg):
    if event == "call":
        print("call", frame.f_code.co_name, frame.f_locals)
    elif event == "return":
        print("return", frame.f_code.co_name, arg)
    return mytrace

sys.settrace(mytrace)

to https://github.com/allofphysicsgraph/proofofconcept/blob/gh-pages/v7_pickle_web_interface/flask/controller.py but the output wasn't that useful since I'm passing the entire database as JSON. The full JSON shows up in almost every argument and return value, making the output of the trace unreadable.

When I switch to the Neo4j/Cypher-based approach, the trace might be more usable.

Monday, May 1, 2023

Omniscient project management

The Physics Derivation Graph relies on a diverse set of skills. To speed up the development process we could identify separable tasks and then spread the tasks among a team of contributors. Collaboration requires coordination, and that coordination can be top-down or organic or a mixture.

This post focuses on the top-down approach and assumes an omniscient view. 

A standard data structure in project management is the Gantt chart. A Gantt chart uses information about tasks, task dependencies, task durations, and dates to create a visualization associated with a project.

task ID task description task duration [days] depends on tasks earliest start date
14235 something useful 3 N/A 2022-03-01
25532 hard work 2 [14235] N/A
3456252 keeping busy 3 [25532] N/A

That table can be visualized with tasks versus time:

Visualization of a Gantt chart. Four tasks. Task 2 and 3 depend on task 1 being completed. Task 4 depends on task 2 being completed.

 

That data structure doesn't account for staffing, skills, equipment, or budget. The  Gantt chart doesn't account for uncertainty of task duration, nor alternative paths.

Gantt charts present a single path

Project management involves contingency planning.  

IF this THEN
   that 
ELSE
   other

Every conditional statement is a branching of possible paths, each a separate Gantt chart.

A single Gantt chart is a snapshot of a single path.


Staffing, budget, equipment, skills, uncertainty

Augmenting the basic Gantt chart means extending the table data structure to something like
task ID task description task duration [days] depends on tasks earliest start date depends on equipment minimum skill set and level uncertainty in duration [days]
14235 something useful 3 N/A 2022-03-01 [Photoshop] photo editing, intermediate +/-1
25532 hard work 2 [14235] N/A [Excel] math, beginner; text editing, beginner +2
3456252 keeping busy 3 [25532] N/A Chrome browser clicking on links, beginner 0

That information needs to be augmented with a cost table for equipment:

equipment cost per day [USD] acquisition cost [USD]
Photoshop 0 100
Excel 0 20
Chrome browser 0 0

Lastly, we need people who can do the tasks.

person name hourly cost [USD] skill and level dates available
Alice 20 Excel, beginner; text editing, intermediate [2022-01-02, 2022-01-03, 2022-01-04]
Bob 15 Excel, intermediate; Math, beginner [2022-02-01, 2022-02-15, 2022-02-24]
Charlie 24 photo editing, beginner [2022-01-12, 2022-01-23, 2022-01-24]

Caveat: the above model is focused exclusively on experts doing tasks using equipment. The model does not account for managers, nor does the model account for support staff. The model could include any scope of tasks, but a boundary needs to be drawn somewhere to avoid becoming Seldon's psychohistory. The problem of tasks existing outside the model is the risk that out-of-model tasks block project progress or alter the project cost. Anything outside the model could be an invisible dependency.

Derived project views

The following views can be derived from the three tables above:
  • standard task Gantt chart
  • project duration histogram. (Each "task duration" has an uncertainty that can be aggregated and results in variance.)
  • per-person activity schedule -- who works on what when. A prioritization based on task dependencies and when people with skills are available
  • cost per day -- the spend rate

Blockers inhibiting the omniscient project management view

Even though the issue can be formulated into a set of data structures

Blockers are the amount of time needed to 

  • gather the relevant information and keep the information up-to-date as the situation evolves
  • document the information and tune the model
  • survey the skills of the workforce
  • have the workforce track their time spent on a task
  • define each task, along with a "definition of done"
  • track costs of the workforce and equipment
  • identifying conditional paths and tracking which alternative was selected

Blockers that aren't time-based:

  • inability to break project into atomic tasks (where "atomic" is based on skill set and skill level)
  • can break project into tasks, but unable to identify relevant skills for task

The centralization of this model is merely to construct a narrative. Software like Atlassian's Jira is a way of distributing the task tracking rather than try to administer the project in a centralized top-down approach.

Conclusion

The top-down omniscient view of project management is an unrealistic fantasy. However, it might be a helpful artifact for negotiation among decision makers. The alternative (where decision makers don't have a quantitative model to argue about) devolves into reliance on personal relationships, turf battles, and political factions. Bureaucratic processes evolve as a substitute for the lack of top-down omniscient view of project management. 

Saturday, April 22, 2023

intermittent Internal Server Error on webpage - activity log of diagnosis

My login to the server provides an overview,

Welcome to Ubuntu 20.04.2 LTS (GNU/Linux 5.4.0-45-generic x86_64)

  System information as of Sat Apr 22 23:49:00 UTC 2023

  System load:                      0.09
  Usage of /:                       70.8% of 24.06GB
  Memory usage:                     72%
  Swap usage:                       0%
  Processes:                        131
  Users logged in:                  1

I first confirmed disk utilization.

$ df -h
Filesystem      Size  Used Avail Use% Mounted on
udev            474M     0  474M   0% /dev
tmpfs            99M  1.2M   97M   2% /run
/dev/vda1        25G   18G  7.1G  71% /

I next looked at the error logs. When the error occurred, the fault trace ended with

  File "/home/appuser/app/controller.py", line 3424, in review_derivation
    dat = clib.read_db(path_to_db)
  File "/home/appuser/app/common_lib.py", line 142, in read_db
    for row in cur.execute("SELECT * FROM data"):
sqlite3.OperationalError: no such table: data
  
Probably a race condition in the Python? If so, this problem is due to my hack of writing the database to SQL. My motivation to resolve this issue is low because I had intended to switch to Neo4j. I haven't complete the migration from JSON/SQL to Neo4j yet.

I used top and saw 2 and 3 instances of gunicorn

I checked for redundant Docker containers running but saw only what's expected:

$ docker ps
CONTAINER ID   IMAGE                           COMMAND                  CREATED       STATUS       PORTS                                                                      NAMES
632ee101f714   v7_pickle_web_interface_nginx   "nginx -g 'daemon of…"   4 weeks ago   Up 4 weeks   0.0.0.0:80->80/tcp, :::80->80/tcp, 0.0.0.0:443->443/tcp, :::443->443/tcp   v7_pickle_web_interface_nginx_1
80bb13ec66ca   v7_pickle_web_interface_flask   "gunicorn --reload -…"   4 weeks ago   Up 4 weeks   5000/tcp                                                                   v7_pickle_web_interface_flask_1

Sunday, March 26, 2023

OpenModelica on Mac using Docker -- command line and GUI

"Modelica is a non-proprietary, object-oriented, equation based language to conveniently model complex physical systems."

(source)

"Modelica is the language for solving systems of ordinary differential, algebraic, continuous, and discrete equations."

(source)

https://modelica.org/tools.html
https://openmodelica.org/

Source code: https://github.com/OpenModelica/OpenModelica

Running Modelica using Docker

In a terminal on your Mac, run:

ip=$(ifconfig en0 | grep inet | awk '$1=="inet" {print $2}') 
Xhost +$ip 
docker run -it -v ~/.Xauthority:/root/.Xauthority -e DISPLAY=$ip:0  openmodelica/openmodelica:v1.20.0-gui /bin/bash
Source: Docker instructions, which also had the commands for linux:
docker run -it --rm -e "HOME=$HOME" -e "DISPLAY=$DISPLAY" --network=host --user "$UID" -v "$HOME:$HOME" -v "$PWD:$PWD" -w "$PWD" openmodelica/openmodelica:v1.20.0-gui
From https://openmodelica.org/useresresources/userdocumentation/ see https://openmodelica.org/doc/OpenModelicaUsersGuide/OpenModelicaUsersGuide-latest.pdf After launching the Docker container, in the command prompt I ran
root@54d835361dc8:/# OMShell-terminal
OMShell Copyright 1997-2022, Open Source Modelica Consortium (OSMC)
Distributed under OMSC-PL and GPL, see www.openmodelica.org

To get help on using OMShell and OpenModelica, type "help()" and press enter
Set shortOutput flag: true

>>> x := 1:12
{1,2,3,4,5,6,7,8,9,10,11,12}

>>> quit()
I launched the GUI using
# OMEdit 
QStandardPaths: XDG_RUNTIME_DIR not set, defaulting to '/tmp/runtime-root'
libGL error: No matching fbConfigs or visuals found
libGL error: failed to load driver: swrast

On Mac using XQuartz I see


Questions: https://stackoverflow.com/questions/tagged/openmodelica


Comment threads:

Saturday, February 4, 2023

Medical knowledge as a probabilistic decision tree

Medical reasoning can sound like a large decision tree ("if this then that"). This post documents the nuances that render a decision tree data structure inadequate. 

  • Nuances about input data
    • Extracting facts relevant to diagnosis is challenging. 
      • A parent of an infant may report their baby is not eating much, but does that mean the baby is refusing food, sleepy, crying, vomiting...
    • Looking merely at the current symptoms is inadequate. Patient history matters. Family history can matter.
    • distinguishing irrelevant information is important. Temporal correlation does not mean causation.
    • There are varying degrees of uncertainty about data quality. For example, I would discount the data from a person who does not tell their story well, and put a greater weight on a lab test. But for someone who tells their story well, the history features may sway more than their lab. 
    • How questions get asked matter
      • "Does your family have a history of arrhythmia?" will get a "no," but
        • "Have people in your family drowned or died in a car accident?" would get a yes because arrhythmia can lead to drowning and accidents.
        • "did any babies in the family have hearing problems?"
    • Patients don't know the precise medical jargon
      • "Does your family have a history heart attacks?" is likely actually a different medical cause when the patient doesn't know the jargon or the specifics about cholesterol.
    • Humans are not uniform, and the differences can matter. 
      • "male versus female" isn't an easy binary in all cases
      • "age" isn't a scalar positive number
        • age since birth ("post-gestational age")
        • age since conception ("gestational age")
        • cognitive ability versus temporal age versus physical dexterity

    • Decisions
      • A lot of the reasoning is probabilistic rather than definitive. The exact probabilities are also unknown -- one is dealing with relative probabilities. 
      • Discarding data should be weighted by the consequence of removing the data
    • Causal explanations based on physiology can be used to discard information, or give insight about additional symptoms to ask about. [Writing down all of physiology is a separate task.]
    • The differential list should include not only a ranking of most likely diagnoses but also diagnoses that one should not miss. This is one area where some doctors say that doctors are better than nurse practitioners. The nurse practitioner tells the patient the most likely diagnosis, but the doctor knows other diagnoses that are less likely, but should not be missed and counsel accordingly. In other words, just guessing based on a "most likely" diagnosis is insufficient. Are there "do not miss" outcomes that could be explanatory for the diagnosis?
    • Suggestions for action by the patient includes, "what to do if this other symptom arises" or "what to do if this symptom persists"



    The clinical decision analysis using decision tree
    doi 10.4178/epih/e2014025