New Year’s Memoir – 2024 Edition

September

Somehow amidst the (mostly) weekend partying and dancing, I’d wrapped up draft 4 of the formal ethics project and prepared a lengthy presentation for our annual AI and theorem proving conference, AITP. Eyeing the peak of the year, Dent Parrachée (3697 m), the highest in the area. I think a trail opened up (according to Mapy.cz), probably thanks to glacial melting 👀😅. This was my debut at an academic conference in my trusty, cutesy cat ears. Generally appreciated 🥳.

Be the change you wish to see in the world.

Mahatma Gandhi¹Ok, not really: see Quote Investigator.

There was much todo about LLMs and to what extent they can do mathematics and conjecturing — “close but no cigar” (yet). Some more projects working on the Logic <-> Language mapping thanks to Transformer models, too, such as this talk by Adam Pease. David Herel and Tomas Mikolov’s talk on getting LLMs to ‘think’ about how much time they need to think on a task was interesting: “thinking tokens”.

I really find Thibault Gauthier, Miroslav Olsak, and Josef Urban’s work on “Alien Coding“ fascinating: they use RNNs and NMTs to do program synthesis in some simple (hand-crafted) programming languages to generate integer sequences from the OEIS²The On-Line Encyclopedia of Integer Sequences®³And a link to the presentation..

I also found the presentation by Eric Mjolsness fascinating: on mathematical modeling of complex physical and biological (neuronal) systems and what will be needed to do theorem proving of this domain. I could benefit from reading the slides again 🤓. 

Presenting work-in-progress in the middle of the conference was quite fruitful. Various attendees appreciated seeing the work and some provided insightful feedback. The best pointer I received to date is thanks to András Kornai who pointed me to the epically historic work of David Fuenmayor and Christoph Benzmüller⁴🌐 in formalizing a normative ethical theorem in Isabelle/HOL: Alan Gewirth’s Proof for the Principle of Generic Consistency. The Argument is roughly as follows⁵Paraphrased directly from their paper.:

1. I act for some purpose E, that is, I am a purposeful agent.
2. E is subjectively good.
3. My freedom is a necessary condition for my agency, to attain any purpose.
4. Freedom is a necessary good.
5. I have a claim right to my freedom.
6. Every purposeful agent has a claim right to its freedom.

Fuenmayor and Benzmüller found versions of the axioms regarding subjective goods, purpose, freedom and wellbeing, claim rights, etc., in such a manner that the proof works in Isabelle/HOL. An additional cool aspect is that they try to take the state-of-the-art analytic philosophy approaches to modeling perspectival judgments and formalize them. This is one of the weaknesses of working in SUMO that I discussed in the second worklog: how to model situations. To this end, they use a dyadic deontic logic with conditional obligations and a modal system for “dialectic necessity” based on “Kaplan’s logical framework LD”. It seems generally acknowledged that to do “real-world reasoning“⁶Commonly called “commonsense reasoning”., one will need to work with multiple modal systems interleaved together, which becomes quite subtle. Benzmuller is a big proponent of showing that Shallow Semantic Embeddings can work in HOL as a universal meta-logical reasoning system, i.e., defining the domain-specific logics in HOL. Ben Goertzel et al. have also long been proponents of this approach⁷See Meta-MeTTa: an operational semantics for MeTTa for their recent programming language to this end.

What’s the significance of this? 

If you disagree with Gewirth’s theorem, then there should a particular property of the definitions or logical set-up that you disagree with. 

Perhaps the perspectival modeling via Kaplan’s logical framework doesn’t capture the semantics properly? One meaning postulate I consider suspiciously strong is “explicationGoodness3”, of which they write, “The third axiom, however, has been added by us as an implicit premise in order to render Gewirth’s proof as correct. This axiom aims at representing the intuitive notion of “seeking the good”.” In essence, they tried to find the minimal axiom needed to allow the proof to hold. explicationGoodness3 states that, “In all possible contexts, for all purposes P and agents A, if P is possible, then P is obligatory if P is necessarily good for A.” Are all necessary goods obligatory to fulfill? This certainly seems debatable. Picking apart precisely what the statement means already requires careful study. There is an open invitation for someone to find a more soundly convincing set of premises for the proof 😉.

The main point is that now the debate about whether this normative ethical theorem holds or not can be very precise and held at the level of definitions, logical frameworks, and how they map up with reality. Yay!

Below is a screenshot of the core proof:

The view from the forts near Aussois is quite scenic. As this is a photo blog, have some beautiful snapshots of the usual hike up the mountains. I find it interesting how these alpine strolls are becoming like regular hikes around the communal cottage 🤠.

In ecosexual spirit, I decided to kiss this majestic mountain cock, which happened to point directly at the peak. Also, this cute mountain goat followed me around a bit 🙂🐐. I found the source of one of the streams: Lac des Chaix Feetsie. The water is chillllly. 

The lake wound up being the peak of my climb. I tried to take an “easy way up” this little ditch, which became increasingly like bouldering and cutting across to the barely visible trail proved difficult in landside-prone territory. I saw someone heading down the path, so it seems probably doable. I turned back and made it down in record time for dinner 🤤.

On the way home, which was already complicated due to rockslides near the tracks canceling the trains through the Alps, there was an incident with a person on the tracks between Torino and Milano, causing 230-minute delays. Missing my flight, I stayed in Turin for a day. I stumbled upon a cute sculpture park, Panchina degli innamorati, I think.

Back in Prague for a week of focused work before The FroCoS and TABLEAUX conferences came to our office building. The Automated Reasoning with Connection Calculi (AReCCa) workshop was educationally interesting. Another fascination of mine is the sections on “non-wellfounded proof theory”, which usually seem to work with some form of a μ-calculus (using least/greatest fixed point operators). One talk explored using determinizing automata within a proof system, which is very philosophically evocative⁸Proof Systems for the Modal μ-Calculus Obtained by Determinizing Automata. I love how TABLEAUX presents a zoo of people working on interesting logical systems most people don’t touch as they’re too underdeveloped, while also blending in some AI for theorem proving 😉🤓.

Before the next stop, Dubai, we had a balfolk event in the Prague woods to celebrate the coming of Autumn. One of my favorites, Tzadik Katamar, felt perfect to dance in the dark woods as if we are frolicking night elves ~

So then, I went to Dubai for the OpenCog Hyperon meetup as an educated representative from the ATP community (who’s also roughly kept up with their AGI architecture plans). Meeting all these people I’d intersected with online was good. They’re mostly warm, jovial chaps. Gaining more insight into the state of affairs, the plumbing of the MeTTa language, and its integration with Rholang, etc was good. Seeing foundational debates about new programming languages is also very.. interesting. Thus is the value of face-to-face gatherings 😊.

---