Magos Logis Logan @jmw150@qoto.org

@extrn

^The topology section of the thesis I linked to.

@extrn

It was an informal discussion in our research group.

But the need for topology came in because it was a debate on the flexibility of real number tensors versus what programs can do in practice. So I boiled both of them down to sets and am looking at their behavoir.

The modularity issue in deep learning is just the connected property. But it is pretty easy to introduce a noncontinuous function. In fact, this is common.

https://knowledge.uchicago.edu/record/2215

The issue is that connectedness is a valuable property to use, most of the time. So deeper networks are better. More data is better.

Program synthesis is also aided by the connected property, but relies on it less. So, not useful for modularity per se, but it can probably bridge larger data dead spots, or rough patches in data.

@mathman

^a

Seeing how a set theory can be used through topology to talk about geometric notions such as connectedness of points, is fascinating.

It also solves a current debate about artificial neuron-based versus sbolic logical reasoning. No idea why topology is optional at my school.

@lucifargundam

Sure. They are different. Human minds can understand the vitali set. Machine learning's best tools are only able to approximate borel measurable sets, despite taking the name of "universal approximators".

https://cognitivemedium.com/magic_paper/assets/Hornik.pdf

Humans are cool.

I should be reading about automated reasoning logics. But cognitive stuff is good too.

https://www.frontiersin.org/articles/10.3389/fnins.2014.00265/full

@oblate @cope @bun

Too bad they do not offer that course anymore, too abstract for a CS freshman these days.

@cope @bun

Sometimes computer scientists are scientists, or mathematicians. But they are always technologists.

@cope @bun

This is one of my favorite lecture series.

@oblate @lupyuen

Nobody wants to pay for formal methods programmers. So they will be fixing bugs and having their stuff stolen for the rest of eternity.

@sapphire @BowsacNoodle @johnbudd1350 @Agartha_Noble @hikari

Downside: potentially no internet

My boss gave me 133 or so pages of math to read before Friday morning. I need to find something in this kind of logic to improve upon before then. Sleep should be happening now.

What’s Decidable About Program Verification Modulo Axioms?
https://arxiv.org/pdf/1910.10889.pdf

Decidable Synthesis of Programs with Uninterpreted Functions
https://arxiv.org/pdf/1910.09744.pdf

Decidable Verification of Uninterpreted Programs
https://arxiv.org/pdf/1811.00192.pdf

@johnabs @lucifargundam

This looks like it is the same book.
https://www.cs.utexas.edu/~swarat/pubs/PGL-049-Plain.pdf

Possible free access through univerities
https://ieeexplore.ieee.org/document/9646874

@gentooman

> You will comply, even as the technology moves on from the point that such rituals make sense.

Classic Java culture of programmers.

@gentooman

Yeah. Rust is basically just Java, for people too young to remember how over-marketed Java was.

@johnabs

It is more advanced. Yes. Very, more so than regular programs in a lot of ways.

It is a concept that comes out of the formal methods community. A more descriptive title is more like "automated program synthesis via mathematical logic and deep learning".

Things are getting interesting. The book is only about 90 pages long.

But in summary, it becoming possible to make programs that are both bug free, and can cover a problem domain that cannot be feasibly solved with simple manual programming.

https://www.amazon.com/Neurosymbolic-Programming-Foundations-Trends-Languages/dp/1680839349