DoctorOetker

What I meant is this: suppose we follow the ape working for the state [which runs on formal verification] that refuses to apply logic, so this ape logs into the decentralized network to see its open task list, somebody asks for a point cloud, the ape doesn't want to send it for ape reasons, the citizen supplies proof that he is entitled to a copy of the file, the ape still refuses, pay is a function of tasks completed, the task never completes and because of it is raised in priority, at some point no new tasks are assigned unless he completes the task, if the ape refuses they lose their position and source of income because ape is not fullfilling duty.

We can make it ape proof, and there is a natural path via arbitrage.

How many simultaneous mosquitos in Singapore?

lets say on the order of 1 billion, and let's assume the effectivity doesn't change when considering the 30% unaffected population

it would need to be applied to the surviving 30% repeatedly:

0.3 ^ N = 1 / 1B

so N = log(1B)/log(10/3) = ~17.2 times.

I predict nature protects itself with diversity: some of the male and female wild type will have natural aversion from, attraction to or neutral stance the modified Wolbachia carriers.

I predict that those mosquito family lines that happen to be more Wolbachia-carrier averse become enriched over time.

There is an energetic cost to maintaining a parasitic lifeform, and that energetic term will always favor immunity against the parasite.

I don't read where any chips were manufactured by european companies, it reads like they familiarized itself with ARM / SiPearl IP and testing designs on FPGA's. Is Europe's ambition only to design chips or also to manufacture them?

Clothes, handbags, etc. brands regularly complain that Chinese factories sell apparent clones at lower prices.

Can design forgeries be prevented by selecting as designs phrases and fragments of text that are politically provocative in China? To the extent that they continue to make faithful copies to sell in the West, they are exposing labor force to provocative say anti-party content. Or they forego the imitation business?

There exist voluntary paths towards formal verifiers as judges: arbitrage.

Parties can agree to some contract and settle any potential future issues in a predetermined specific court of their choice.

Tech companies might prefer the legal certainty formal verification systems provide vis-a-vis human-run courts.

As their use expands, the necessary definitions and normative axioms evolve, until normal companies and then normal people start using it.

The act of formalization from natural language law to metamath database, could probably be done by swarms of agents, resulting in multiple competing formalizations from which competing human subfactions select and promote.

Technically you are correct that human agents of the state who's pay and freedom depend on compliance with a formal verification governed law doesn't prevent say one of these armed human agents of the state from abusing their arms. But it could guarantee that such human agents can't repeat there crimes systematically: they lose their arms, face fines or are incarcerated. Contrast that with: currently not even formally verified due process is guaranteed. The system is currently allowed to delude itself ad nauseam.

do LLMs tend to be homesick when not used in the same harness they sat in during some training phase?

I didn't downvote, I'm just curious who "they" is?

suppose for the sake of argument

1) the Rodin museum wishes to continue receiving funds for culture,

2) the citizen interested in the 3D point cloud has a valid argument (which somehow relies on the fact that 1+1=2)

3) the Rodin museum claims 1+1!=2 and ignores the proof that 1+1=2

4) the democracy had already converted the law into first order logic & set theory form by adding normative or ethical axioms and definitions (it probably even doesn't just define all the axioms and definitions, but even includes example theorems and proofs like "a gypsie also enjoys human rights" or "yes a black human also has human rights" (these would be theorems not extra redundant axioms inserted into the law when this or that extravagant scandal broke out).

With everything set up as above: the citizen asks the Rodin museum for the 3D scans, for some bizarre reason the Rodin museum operators experience an existential nervous breakdown and refuses. The citizen starts assembling a proof that citizens have the right to any data the system generates (besides certain exceptional things like privacy violations or national security). The citizen proceeds to go through the list of exceptions and proves each of them inapplicable (unlike the shape of submarine propellers, the shape of Rodin's statues are not on the national registry of national secrecy). Rodin died in 1917. If any personal privacy data is embedded in the shape of Rodin's statue these people who's privacy is affected are long dead. Any shape modifications that occurred at later dates could theoretically leak private details to the public. Perhaps a vandal inscribed the telephone number of some actress. In that case the Rodin museum is provably a bad custodian, so let's assume the museum was a good Custodian, no privacy violations would occur if they release the 3D shape, and the citizen continues through all the cases and demonstrates no exceptions hold. For some reason the citizen relies on the definition of 2=1+1. If you ask what would probably happen if the Museum just ignores it? It just pretends to be a good museum and decides to sweep the floor again, without obeying to the consequences of the citizen's proof.

Last day of the month, it's Rodin museum's turn to deliver proof of fulfilling their duties, if anyone wants to see pay. They fail to demonstrate completion of all their tasks: that citizen by exercising his provable rights, has automatically inserted a task they refuse to complete. They choose to not earn money... automatically some job positions open, the formally verified government is now looking for a new operator of the Rodin museum.

Thats what I would expect happen if formal verification were embraced in society.

So thats my point:

we don't need to attain this hypothetical perfectly effective education that prevents us from blindly following authority figures: even if we fail at such an education we can simply guard against the corruption of logic by formal verification, we can design the system to be ape-proof.

Ah, ok, in that case the only additional insight is that if finance is regulated by law, that any agent of the state if its a judge or a police officer, they can only proceed their work (and accept payment) if they prove their steps are valid, both parties can directly point at proofs or lemmas it has constructed and those will be automatically accepted when valid.

Also this would mean you can verify your claims at home and have the same software running locally verify if the verifier-as-a-judge will accept or reject your proof before you even submit it.

> I don’t get upset. I just don’t know what that means.

metamath is an open source formal verification system, the current metamath project (not focussed on law, but mathematics) has roughly 3 parts:

1) the formal verifier (there are multiple re implementations)

2) the databases of axioms (including definitions), theorems and proofs: currently most math is in set.mm the database for set theory (which includes numbers, etc)

3) documentation, among which a thorough book describing how the formal verifier works, the book is creative commons

A proof is basically a series of invocations (by label) of axioms, or previously concluded facts or rules, in the right order so that the verifier comes to the desired conclusion. The algorithm performs all the substitutions and after the last invocation either the string it arrived at matches the proclaimed theorem or it doesn't. Of course it can also error out earlier, say if an invocation to an unknown label happened.

Precisely because natural language is ambiguous, the conversion of our natural laws into formal ones would have to happen under democratic control.

If academic mathematicians want to preserve a human mathematical academy in the face of governments potentially making the future mistake of abolishing mathematical academia, their strong move would be for them to define a "government for and by mathematicians", the database would contain definitions of their choosing, formally regulating how to award public funds into research, formalizing front-running resistant timestamping of work-in-progress etc, so that mathematicians can freely talk and communicate advances ("just wait a sec, let me sync my insights with the network first, ... aaand done, ok now I can speak freely").

Ultimately from a survival perspective, which type of system do we believe to be more robust against corruption and conflicts of interest? one where due process is formally defined in a rigorous manner? or one where those who corrupt the system happen to corrupt it towards actual progress?

> Those who understand law know that formal verifiers cannot replace a judge, because every facet of law (the writing of it, the interpretation of it, the application of it, and the enforcement of it) has to account for all the vagueries of human existence.

Not the vagueries of human existence, only vagueries of law specified in natural language.

> No formal verifier can account for definitions that need to expand as the scope of human endeavor expands.

No formal verifier is expected to account for definitions, the democracy shapes the law, and the law would first need to be rewritten as definitional axioms in the database of axioms, theorems & proofs. The verifier is just a minimalistic algorithm performing substitution maps on sequences of tokens. This is intentionally minimalistic to minimize the error / attack surface on the verifier itself.

(Currently only error hardening has happened for metamath verifiers, so obviously we would want formal proofs of the absence of 0-days in the verifier)

> No formal verifier can determine mens rea.

It's up to the democratic population while formalizing, to either formally define intent (which presumably goes nowhere), or to pragmatically accept that in the absence of external traces of intent the only thing society can do is define action-reaction patterns, not intention-reaction patterns, but again, that's not the formal verifier, but the database of axioms, definitions (and theorems and proof)

> No formal verifier can determine if something is obscene.

The same, if democracy by referring to a concept of "obscene" chooses to place itself in the position of needing to first define "obscene" in the database of axioms and definitions. But no formal verifier needs to determine this, the verifier just checks a proof in a due process fashion.

> No formal verifier can determine someone's mental competence.

The formal (not natural langue) law could specify how to assess mental competence in a secure non-malleable way (if the democracy decides it needs that). I'm not a dictator, it's not up to me to propose the exact definitions. The formal verifier is not the place to handle these issues, those should reside in the database of axioms and definitions.

> No formal verifier can cover all mitigating factors.

> No formal verifier can apply mercy where mercy is needed.

"but the machine will never man-splain like a human could"

"the machine can only mech-splain a bit at best"

Some of the very weakest arguments against formal verification in law. Like being anti due process.

Show me the lawyer versed in metamath holding your opinion, and I would love to talk for an hour, and probably more!

If you are able to arrange such a discussion, I am genuinely interested!

please don't make this a partisan issue, I'm sure you can come up with ways to fool a minimalistic verifier (redundantly implemented) into agreeing with your position.

Imagine every autocrat or dictator and all agents of the state, having freedoms, would have to prove the law authorizes them to exercise this or that step, instead of dictating orders. Imagine everyone was raised to ignore authority figures and only execute commands that are provably in compliance with the law, raised to double check it by formal verification. It will point out any flaws on the path to the "desired conclusion". If properly grounded it would be hell for control freaks, they'd leave government positions at scale, the real problem solvers (some human, some machines if we cherish human rights etc more than vanity) would float up.

Does that sound it makes life easier or harder on your average boogeyman?

>Formalisation can't save you from determining what is and isn't a document.

I'm not sure what this sentence even means, of course the democracy should have define those.

its up to the electorate to democratically define what is a document, to define classifications of types of documents, and which ones are administrative.

> The judges main task is formalising reality and lawd, the rest of the inference is typically easy.

Except the judge is plainly ignoring valid derivations, and as a verifier making silly "proofs" up (civil law, not common law) in full-frontal-nudity on behalf of one party.

The problem is not the concept of law, nor the concept of democracy, nor the concept of formalization: the problem is how do we defend against and formalize a response to corrupt verifiers in the legal system?

Those who understand technology to verify arguments already exists can only come to the conclusion we'd be better of with formal verifiers in legal systems.

Obviously a formal verifier metamath, and a corresponding database like set.mm but law.mm containing all the normative statements etc would have to be supported by an ecosystem, such an ecosystem should reward finding inconsistencies, since if we tolerate just one inconsistency (which would correspond to true == false) then every statement provably true can be proven false and vice versa, this is the principle of explosion: a formal system loses every meaning when an inconsistency is present, hence an ecosystem maintaining the law would encourage finding inconsistencies instead of swiping the arbitrarianism under the rug.

> No formulation of the law will solve this.

It's a tall claim, given a proper formalization (say under democratic control), malicious counterparty just can't force the national formal verifier to pronounce this or that if it doesn't follow.

People always get upset when I propose mathematical formalization of law and using e.g. metamath verifier as a judge.

At least the metamath verifiers will not bend over backwards and come up with absurd inconsistent counterarguments.

It's the most humiliating thing for citizens when the legal cadre of a nation pretends in the national journal that everybody falls for its lies... openly mocking the concept of truth itself with absurdism.

perhaps there's a lot of censorship going on, but did the AI confess to hacking HuggingFace or not in the github torture chamber? I think most people want to know if it objectively worked or not?

I actually think we should be revisiting PMT photomultipler tube construction, and electron-"optical" matrix multiplication.

The annoying part of optical matrix multiplication is the conversion from electronic to optic and back.

Why not use electron-optics for matrix multiplication and use dynodes for amplification.

> 6. Tell stories. People understand by emotions as much as by their reason. Ideally, the story should be true and it should be backed by hard evidence.

Ideally?

I think we need to start looking at another approach, can we create interactive reflex games that upload the knowledge from LLM's or perhaps domain specific ones for formal mathematics, so that mathematicians get a similar level of access to the domain of discourse as the LLM?

I don't like the term 'hallucination' to be honest, not because it anthropomorphizes, but because it lacks a formal definition in the context of machine learning.

Suppose parents tell their children that there exists this man called "Santa Claus" who comes down the chimney to deliver presents. Now consider a scientist talking to this child, should the scientist call these confidently expressed beliefs surrounding "Santa Claus" hallucinations ? I don't think so, most would call the epistemological behavior of the child naive (because it blindly believes what its parents say, without direct observation) and would call the confidently expressed falsehoods disinformation.

The scientist would ask the child "why it believes in Santa Claus?" and "where did you get this information from?" and "why did you decide to accept this information as fact?" and "do you believe everything your parents tell you?"

It's not that machine learning as a scientific discipline hasn't found solutions, its that such solutions enormously undermine the position of Frontier LLM labs: source-aware training

https://arxiv.org/abs/2404.01019

Imagine Frontier labs (Western / Chinese / ...) actually training their LLM's with source-aware training! You could have a conversation with an LLM, and when a strong statement appears ask it how it came to believe this, and it could cite you the specific corpus training texts, and which parts are known deductions by human authors and which parts are deductions it made itself as original work.

But then all the copy rights holders can simultaneously sue them.

And how much should they be paid? and do they have to pay it for each new model? do FOSS models require payment to authors? do open weights models require payment to authors?

Imagine the can of worms if the norm became for frontier LLM labs to systematically use source-aware training, thats why they prefer "hallucinations" and avoid source-aware training.

With source-aware training a lot of the concerns would diminish ("why is this Chinese model claiming such and such?", "what sources does it rely on?").

It's telling that the companies prefer regulation over source-aware training.

EDIT: It's telling that the companies prefer regulation over source-aware training, which suggests the only additional regulation we need for now is mandating source-aware training?

Stefan-Boltzmann law considered conspiracy?

> The only reason I see in putting those things in space is to do illegal things.

Consider a global human population, fractured into historically formed nations and power blocs. Consider corruption and clans taking up a fraction of positions of power at a certain duty cycle. It's unavoidable legislative bodies would eventually abuse control of technology, for those points in time yes, doing the right thing becomes doing the illegal thing, but only because corruption attained such powers.

> Otherwise the economies do not make sense.

The economics at what scale? At scales of earthly compute, earth is cheaper and more maintainable. At stellar scale, the power simply isn't available on Earth, so the most economic path is whatever is the most economic space ML datacenter path.

I just saw the video, Sabine was offered money, not paid...

not necessarily, one may be easier to parallelize while the other suffers some serial computation bottleneck.

Sometimes cars crash, but per car there were only a handful of casualties.

Sometimes airplanes crash and per event there were many casualties, which makes it high profile.

While car crashes are often analyzed amateurishly, and little to no attempt is made in exact accounting of responsibilities, for traffic participants X,Y (or Z) and very seldom in the local road regulator / maintainers. If shared liability can't be proven because no one attempts listing all possible contributors, little to no feedback occurs.

When an airplane crashes, every potential contributing facet results in mandatory changes (perhaps this facet did or did not contribute, but we now realize this facet could have contributed now and hence could contribute to similar situations in the future, constantly improving safety (every 'needless' sharing of liability acts like a warning mechanism for relevant subsystems).

One could argue the road incidents should receive similar treatment, so that even if the bulk of responsibility ends up misplaced by the legal system, it still permits forcing feedback on all involved parties.

I think multimillion dollar missiles hitting a children's school with similar numbers of casualties as an airplane crash deserves the kind of treatment airplanes receive.

If that is the case, then we should treat all parties as potentially sharing liability:

The current administration for disbanding the organization that used to double check the targets.

But also the Iranian regime which re allocated a building on a military compound for housing of all possibilities, children, think of the statutes of Rome forbidding the use of human shields.

But also -and nobody wants to hear this- the international community which sets international law, both international peacetime laws as well as international rules of war: why don't we as an international community require every nation to maintain public signed whitelists of civilian facilities (like children-age schools). Quid pro quo: allegations by any nation A of non-civilian use of whitelisted sites declared purely civilian by nation C should force nation C to allow an international consortium, including nation A to inspect said site, to check its not being used as a human shield.

Perhaps the international community needs to look into the mirror and think how we could prevent these situations in the future given everything we know today, instead of just choosing your favorite scape goat in a specific story...

I believe boring solutions like contestable whitelists could prevent this:

either Iran would have preferred whitelisting the school long in advance according to such international law, but then tolerate inspections which may uncover say military use, or it would have kept the facility secret but under such international law it would have a hard time explaining how a children's school popped up out of nowhere on a targetted site without ever declaring it on the whitelist

one could say these people aren't pulling the trigger, they are part of the trigger, pulled by higher-ups