Crossposted from the AI Alignment Forum. May contain more technical jargon than usual.

Infra-Exercises, Part 1

1st Sep 2022

2Gurkenglas

2Charlie Steiner

2S. Verona Lišková

2Coafos

2maxnadeau

3Jack Parker

2Algon

1Thomas Larsen

1Algon

1Frank_R

New Comment

10 comments, sorted by Click to highlight new comments since: Today at 12:31 PM

2.3: I claim that the definition "m is the infimum of S := ∀x:x≤m⇔x≤S" is better: It should make for prettier proofs, and expresses "m eliminates ∀s∈S for purposes of testing ≤".

Have this marvelously pretty proof of 3b:

Theorem: {monotone, 1-Lipschitz, 0-increasing, concave}

Proof:

is monotone iff . is 1-Lipschitz iff . is 0-increasing iff . is concave iff convex combination:. It thus suffices to show that for enough .

We'd like to say . The first needs precisely that be monotone, which all of the above are. The second is being monotone at the premise. The third is equality when is (which all of the above are), characterizing the very definition of on functions.

Open: Does 3a characterize affine? Can the full set of p for which this goes through be succinctly described?

5c:

I had rejected this answer as unfair. This sort of trolling should be overseen personally.

In section 1: When the 'affine' word is commonly used, the mixture coeffecient (denoted there by ) can be any real number. When , then it's still an affine combination, but a more precise tern could be 'convex combination'.

However, as you work with function spaces, convexity in a function space is different then being a convex function, so maybe some new notation should be introduced.

Nitpicks: Def 2.4 builds on the obvious generalisation of Def 2.3, not Def 2.3 itself. Also, Def. 2.3 is a little poorly worded, and should make clear that "~~not all sets ~~^{[1]}all sets of reals which are bounded below have an infimum". I think it would be helpful for those with no background in proofs if you had an exercise to justify the use of "the" when talking about the supremum of a set. Or even link it to the idea of a lower bound at all.

More to come as I read through this.

EDIT: I think you probably want to point people to guides on how to prove things so that people without maths backgrounds know what task they're meant to be accomplishing. Otherwise they might go through this text and be hopelessly stuck or think they've proven something when they really haven't. Plus, having the ability to notice the difference between a proof and the intuition behind a proof is quite important for doing mathsy stuff, and Vanessa's agenda is amongst the more mathy alignment agendas.

^{^}Ignore the struck through text.

I have two questions that may be slightly off-topic and a minor remark:

- Is a list of open and tractable problems related to Infra-Bayesianism somewhere available?
- Do you plan to publish the results of the Infra-Bayesianism series in a peer-reviewed journal? I understand that there are certain downsides; mostly that it requires a lot of work, that the whole series may be too long for a journal article and that the peer review process takes much time. However, if your work is citeable, it could attract more researchers, who are able to contribute.
- On page 22, you should include the condition a(bv) = (ab)v into the definition of a vector space.

There have been a few remarks about how my and Vanessa’s posts on Infra-Bayesianism seem interesting, but that it's quite a formidable body of work to chew through.

So anyone interested in learning Inframeasure theory to the level of proficiency where they are actually able to develop their own proofs about it and casually deploy it as a tool on other problems is probably not best served by the existing posts. You can only go so far by reading about something without ever applying it.

And so, to help people get a taste for the underlying math, I have constructed a sheet of exercises analogous to Scott's exercise sheets about fixpoints, to guide the reader through inventing most of the basic theory for themselves.

Said problem sheet was dramatically improved by Jack Parker, Connall Garrod, and Thomas Larsen as part of a SERI project, by including proof sketches, relevant definitions, and commentary, and generally making the whole exercise sheet dramatically more polished than it would otherwise be. Several others also contributed to testing out the exercises and providing solutions and feedback, most prominently, Viktoria Malyasova.

This first sheet focuses on introducing Inframeasures, and working through the Fundamental Theorem of Inframeasures. Admittedly, this is a bit distant from much of the later work (further problem sheets are upcoming), but it

isa very important result to have a solid understanding of.There is more information on how to approach the problems in the introduction of the document. We may potentially release more problem sheets in the future, depending on what the feedback to this one looks like. And if the polished versions are not created, I will publish the unpolished ones.

The link to the problems is right here.