Tim, That use should be something that would benefit people. Good luck with it.
On Wed, 17 Jan 2024, 1:18 pm Tim Daly, <[email protected]> wrote: > I have GPT systems running locally. It is possible to feed the systems > text files for training. Once trained they can answer questions related > to the training. It will be interesting to convert the book to text and > train the system on the book. At minimum it might make an interesting > "help" facility capable of responding to natural language questions. > > On Monday, January 15, 2024 at 10:05:54 PM UTC-5 [email protected] > wrote: > >> Tim, notice though that the only intelligence here is what is provided by >> human intelligence. None of the various systems have any inherent >> intelligence. >> >> My youngest granddaughter has just turned 1 and I have been spending time >> watching her develop intelligence and the difference between her and any of >> the current systems is possibly on the order of a million orders of >> magnitude with the systems being the primitive level. >> >> As I said above, these systems can have possible use cases but only if >> humans are controlling them intelligently. It is a matter of finding >> specific use cases that work for us. >> >> An appropriate analogy is summed up as: fire is a good servant but a >> destructive master. >> >> On Tue, 16 Jan 2024, 1:00 pm Tim Daly, <[email protected]> wrote: >> >>> There is an interesting example of proof earlier in the video: >>> https://youtu.be/3pb_-oLfWJ4?t=298 >>> >>> Reinforcement learning (using the Bellman equation[0]) needs >>> the ability to at least decide if it succeeds and can use information >>> about success in intermediate steps to rapidly improve. It also >>> needs a set of actions that can be performed at each step. >>> Reinforcement learning has conquered gaming with this structure. >>> >>> LEAN provides a database of theorems, definitions, and tactics >>> that can be applied at each step of a proof. It provides feedback >>> about the local success of each action. It provides global success >>> once the proof completes. Thus all of the elements needed by >>> reinforcement learning are available in proof systems. LEAN's >>> theorems are strongly typed. >>> >>> When training GPT-like systems, reinforcement training is the last >>> step (see Karpathy's slide 3): >>> https://karpathy.ai/stateofgpt.pdf >>> It is straightforward to customize a GPT-like system with LEAN's >>> mathematical knowledge to focus on proofs. >>> >>> We use group theory as our organizational skeleton. One of the steps >>> to integrating LEAN and computer algebra is aligning LEAN's axiom >>> structure with our category/domain structure (my current research). >>> Once that is done then theorems, such as a commutative theorem, >>> can be inherited and available to prove a function in a domain. >>> >>> We use Buchberger's Groebner basis algorithm. This algorithm has >>> already been proven in Coq and is in use[1]. >>> >>> It is only a matter of time before the axioms which support the Risch >>> algorithm are proven. That will form the basis of proof of our current >>> implementation. >>> >>> Because we are strongly typed and use a group theory scaffold we >>> are in a unique position to formalize our algorithms. >>> >>> The combination of proof systems and computer algebra will be a >>> large step in computational mathematics. >>> >>> Tim >>> >>> >>> [0] Bellman Equation >>> https://en.wikipedia.org/wiki/Bellman_equation >>> >>> [1] Connecting Gröbner Bases Programs with Coq to do Proofs in Algebra, >>> Geometry and Arithmetics >>> https://arxiv.org/abs/1007.3615 >>> >>> >>> >>> >>> >>> On Monday, January 15, 2024 at 6:59:46 PM UTC-5 Dima Pasechnik wrote: >>> >>>> On Mon, Jan 15, 2024 at 10:45 PM Hill Strong <[email protected]> >>>> wrote: >>>> > >>>> > No artificial stupidity (AI) will ever or should ever be considered >>>> as [a trustworthy co-author in mathematical research]. At best, these >>>> systems could be a possibly useful tool in the hands of those who know >>>> their subject field. In the hands of everyone else they will be like young >>>> children using power tools - a dangerous proposition at best and an utter >>>> disaster at worse. >>>> > >>>> > There is far too much unthinking hype about the subject even by the >>>> researchers in the field. >>>> >>>> Well, we all know Doron Zeilberger's co-author: >>>> https://sites.math.rutgers.edu/~zeilberg/ekhad.html >>>> >>>> In this sense it's not new at all. More powerful, yes, but still... >>>> >>>> > >>>> > On Tue, 16 Jan 2024, 12:10 am Tim Daly, <[email protected]> wrote: >>>> >> >>>> >> "When integrated with tools such as formal proof verifiers, >>>> >> internet search, and symbolic math packages, I expect, say, >>>> >> 2026-level AI, when used properly, will be a trustworthy >>>> >> co-author in mathematical research, and in many other fields >>>> >> as well" -- Terrance Tao >>>> >> https://youtu.be/3pb_-oLfWJ4?t=358 >>>> >> >>>> >> I might add that it would be important that the computer algebra >>>> >> algorithms be proven correct. >>>> >> >>>> >> -- >>>> >> You received this message because you are subscribed to the Google >>>> Groups "FriCAS - computer algebra system" group. >>>> >> To unsubscribe from this group and stop receiving emails from it, >>>> send an email to [email protected]. >>>> >> To view this discussion on the web visit >>>> https://groups.google.com/d/msgid/fricas-devel/11e29cc8-7c91-4ad2-a56b-d380db9a33e3n%40googlegroups.com. >>>> >>>> > >>>> > -- >>>> > You received this message because you are subscribed to the Google >>>> Groups "FriCAS - computer algebra system" group. >>>> > To unsubscribe from this group and stop receiving emails from it, >>>> send an email to [email protected]. >>>> > To view this discussion on the web visit >>>> https://groups.google.com/d/msgid/fricas-devel/CAEnaMTGr_Vk3qa-7X%3DVcPpmwuhEdcKySsngh1UaTmsTRgX9Lwg%40mail.gmail.com. >>>> >>>> >>> -- >>> You received this message because you are subscribed to the Google >>> Groups "FriCAS - computer algebra system" group. >>> To unsubscribe from this group and stop receiving emails from it, send >>> an email to [email protected]. >>> >> To view this discussion on the web visit >>> https://groups.google.com/d/msgid/fricas-devel/6ec0fcdb-1c96-4d5d-95df-35b52e3d97e1n%40googlegroups.com >>> <https://groups.google.com/d/msgid/fricas-devel/6ec0fcdb-1c96-4d5d-95df-35b52e3d97e1n%40googlegroups.com?utm_medium=email&utm_source=footer> >>> . >>> >> -- > You received this message because you are subscribed to the Google Groups > "FriCAS - computer algebra system" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/fricas-devel/217ae176-b177-48f6-9a31-05a0758b5820n%40googlegroups.com > <https://groups.google.com/d/msgid/fricas-devel/217ae176-b177-48f6-9a31-05a0758b5820n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- You received this message because you are subscribed to the Google Groups "FriCAS - computer algebra system" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/fricas-devel/CAEnaMTHRmFe%2BK0NKf7Aq7A3u7cxgwQAauO14TTOMi%3DFcKSqTSw%40mail.gmail.com.
