nuntium

한어Русский языкEnglishFrançaisIndonesianSanskrit日本語DeutschPortuguêsΕλληνικάespañolItalianoSuomalainenLatina

Nova Sapientia Report

Editor: Editorial Department

[Introductio ad Novam Sapientiam]. Modo nunc, Google DeepMind exemplar mathematicum recentissimum IMO Mathematicae Olympiadis argenteum numisma vicit! Non solum decem quattuor quaestionum cum perfectis ustulo, tantum 1 punctum ab auro numismatis, sed etiam tantum 19 secundis ad quaestionem solvendam accepit .

AI IMO Mathematica Olympias numisma argenteum vicit!

Modo Google DeepMind denuntiavit quaestiones reales huius anni Olympias Internationalis Mathematicae suo AI systemate productas esse.

Inter eos, AI non solum 4 quaestionum peractas feliciter, sed etiam plenas marcas accepit pro qualibet quaestione, quae summae sexaginta numismatis argentei — 28 punctorum aequivalet.

Hoc effectum est tantum 1 punctum ab auro numisma!

Inter 609 decertantes, tantum 58 numismata aurea vicit

In certatione officiali, homines decertantes suas responsiones in duabus sessionibus submittent, cum termino 4.5 horarum singulis diebus.

Interestingly, solum AI paucas minutas minutas ad unum e stionibus respondere solum cepit, reliquae vero quaestiones tres integros dies sumpserunt, quod dici potest esse tempus grave.

Quae hoc tempore magnas contributiones fecerunt, duo AI systemata-AlphaProof et AlphaGeometria II.

Maximus punctus: 2024 IMO in notitia horum duorum AIs non est disciplina.

Scott Wu, unus ex fundatoribus post AI fabrum Devinum (ter IOI numismatis auri) lamentatus est, "Cum haedus essem, Olympiades omnes habebam .

In hoc anno in certamine IMO, sex sunt quaestiones competitiones quae algebra, combinatorica, geometria et theoriae numeri sunt. Sex viae quattuor faciunt, gradu AI sentiamus.

AI facultatem rationis mathematicae professoris impulsus est

Novimus omnes priorem AI limitatum in solvendis quaestionibus mathematicis ob limitationes ratiocinandi facultates et disciplinas datas.

Duo AI lusores qui simul visi sunt hodie hanc limitationem fregit. sunt, respectively--

- AlphaProof, nova ratio formalis ratiocinandi mathematicae subnixa ad supplementum doctrinae

- AlphaGeometria II, problematum geometricum secundo solvendi systema

Responsa a duobus AIs data sunt iuxta normas a celeberrimo mathematicorum Professore Timotheo Gowers (IMO Gold Medalist et Agri Medalist) et Dr. Josephus Myers (duo-time IMO Gold Medalist et Praeses IMO 2024 Quaestio Electio Committee) .

In fine, AlphaProof recte solvitur duae quaestiones algebraicae et unus numerus theoriae quaestionis. Una e difficilioribus quaestionibus solvebatur a sola 5 contentione hominum in IMO huius anni;

Solae duae quaestiones mathematicae combinatoriales non victae sunt.

Timotheus Gowers Professor etiam valde abhorrent per gradatim process--

Quod propositum cum tali solutione non-obvia ascendere posset, est vere gravis et longe ultra id quod expectavi praesentem artis statum.

AlphaProof

AlphaProof est systema capax ad probandas propositiones mathematicas in lingua formali Lean.

Componit praeordinatum exemplar linguae magnae cum AlphaZero supplementi studiorum algorithm, quod se docuit ad latrunculorum, shogi, et Go.

Praecipua utilitas linguarum formalium est ut formaliter verificari possint ad probationes rationis mathematicae pertinentes. Attamen earum applicatio in machina discendi limitata est propter limitatam quantitatem notitiarum hominum ab hominibus scriptae.

E contra, linguarum naturalium innixus aditus, licet accessus ad magnas rerum notitias, probabiles, sed falsas, intermedias ratiocinandi gradus ac solutiones producere potest.

Ad hoc devincendum, Google DeepMind investigatores pulchre Geminorum exemplar ad problema linguae naturalium enuntiationes formales enuntiationes automatice transferendae sunt, magnam bibliothecam in qua formales difficultates variae difficultatis construunt, ita pontem inter duos campos complementarios aedificant.

Cum solvendo problema, AlphaProof candidatos solutiones generat et eas probat vel improbat quaerendo gradus probationis possibilis in Lean.

Unaquaeque probatio, quae invenitur et verificatur, ad exemplar linguae AlphaProof confirmandum adhibetur ut difficultates difficiliores in futuro solvere possit.

AlphaProof instituendi, investigatores decies probaverunt vel improbaverunt quaestiones, amplis difficultatibus et locis thematis mathematici ab hebdomadibus usque ad et durante certamine.

In certamine, ansam quoque paedagogicam adhibebant confirmando probationes in variationibus quaestionis auctoris sui ipsius, donec integra solutio inventa est.

Infographica fluxus AlphaProof supplementi discendi rudimenta ansa: circa unum decies centena milia problemata mathematica informalia a retis formalibus in linguam mathematicam formalem transferuntur; , Solvere provocantes difficultates

AlphaGeometria 2

AlphaGeometria 2, upgraded versionem AlphaGeometriae, est systema hybrida neural-symbolica a integro innixa in lingua Geminorum exemplarium.

Secundum ordinem magnitudinis magis synthetica notitia quam generatio prior, potest problemata geometrica difficiliora solvere, inter aequationes motus objecti, angulos, proportiones, distantias, &c.

Praeterea figuram machinam notat quae duo ordines magnitudinis velocior est quam antecessor eius. Cum novae difficultates offenduntur, nova mechanismo cognitionis communicans utitur quae variarum arborum investigationum coniunctiones provectas ad difficultates difficiliores solvendas sinit.

Priusquam hoc anno IMO participaret, AlphaGeometria II multum successus iam consecutus est: potuit LXXXIII% problematum geometriae IMO solvere ante 25 annos, cum prima generatio tantum 53% solvere potuit.

In hoc IMO, celeritas AlphaGeometriae 2 abhorrent omnes - intra 19 secundis recipiendi formalem quaestionem, quaestio 4 solvitur!

Quaestio 4 requirit probationem summam ∠KIL et ∠XPY aequalem esse 180°. AlphaGeometria 2 suadet punctum E construere in linea BI ita ut AEB=90°.punctum E medium L ipsius AB determinare adiuvat, multa similia triangulorum paria constituens, ut ABE~YBI et ALE~ IPC, ita conclusionem probans.

AI problema-solvenda

Dignum est memorare has interrogationes primum manuale in linguam mathematicam formalem transferendam, antequam AI subiciatur.
P1

Generaliter, prima quaestio (P1) in singulis IMO experimentis est facilior.

Retizantes dixerunt, "P1 solum mathematicam scientiam alta schola requirit, et homines lusores intra 60 minutas complere solent."

Prima quaestio IMO 2024 maxime proprietates numeri reales α examinat, et requirit numerum realem α invenire qui certis conditionibus satisfacit.

Rectam responsum dedit AI - α etiam integer est. Ita, quam exacte respondetur?

In primo gradu problema solvendi, AI primum theorema dedit, quod dextra laevaque aequalia sunt.

Constitutus in sinistro repraesentat omnes numeros reales α conditionibus occurrentes, pro quolibet integro positivo n, n dividere posse i*α⌋ ab 1 ad n; numerus par, ac verus numerus α = k.

Sequens probatio in duas partes dividitur.

Primum proba quod in dextro positum est subset sinistrum.

Deinde proba quod in sinistro positum est subset posito dextrorsum.

Usque ad codicis finem, AI ascendentem cum aequatione clavis ⌊(n+1)*α⌋ = ⌊α⌋+2n(l-⌊α⌋), aequatione utens ad probandum α esse debet. aequus numerus.

Postremo DeepMind tria axiomata comprehendit, quae AI in processu problemati solvendo nititur: propext, Classical.choice, et Quot.sound.

Sequens est quaestio absoluta processus solutionis P1: https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P1/index.html

P2

Secunda quaestio relationem inter binos integros positivos (a, b) examinat, quod proprietatem maximi divisoris communis implicat.

Responsio soluta AI est:

Theorema est quod pro duobus integris positivis (a, b) quae certis conditionibus satisfacit, suum propositum solum capere potest (1,1).

In sequenti problemati-solvente processu, probatio consili ab AI assumpta primo pro- banda est (1,1) conditionibus datarum satisfacere, ac deinde hanc solam solutionem probare.

Proba (1,1) solutionem finalem, utendo g=2, N=3.

Quod si solutio (a, b) sit, tum ab+1 dividere debet g.

In hoc processu, AI usus est theorema Euleri et proprietates operationum modulationum ad ratiocinandum.

Denique ostende a=b=1 solam esse solutionem possibilem.

Sequens est quaestio absoluta processus solutionis P2: https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P2/index.html

P4

P4 est quaestio geometrica probatio quae requirit angulum geometricum specificam relationem probare.

Ut supra dictum est, hoc per AlphaGeometriam 2 in 19 secundis confectum est, novum testimonium ponens.

Pendere solutionem datam, sicut in prima generatione AlphaGeometria, puncta auxiliaria in omnibus solutionibus exemplar linguae ipso generantur.

In probatione, omnis angulus semita eliminationi Gaussianae utitur, et d(AB)−d(CD) aequalis est angulo directionali ab AB ad CD (modulo π).

Per processum problema solvendum, AI manually paria triangulorum similium et triangulorum congruentium (rubro notata) signabit.

Gradus deinde ad problema AlphaGeometriae solvendum, quod "recontradictionis methodo" utendo perficitur.

Primum utere Lean ad formalizes propositiones probandas et inspiciendas constructionem geometricam.

Clavis gradus in probatione talis est.

Vide infra picturam ad processum absolutum problema solvendum: https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P4/index.html

P6

Sexta IMO quaestio est "bulla ultima", quae scrutatur proprietates officiorum et requirit conclusiones specificas de numeris rationalibus.

AI solvit, c=2.

Inspiciamus primum theorematis constitutionis, quae proprietates "Aquaesulianae functionis" definit, et declarat omnibus talibus functionibus valorem statutum f(r)+f(-r) ad summum 2 elementa habere.

Probatio militaris est imprimis probare quod cuilibet functioni Aquaesulianae, valor ipsius f(r)+f(-r) ad summum 2 elementa habet. Tum munus specificum Aquaesuianae construe ita ut f(r)+f(-r) valores prorsus 2 diversos habeat.

Probe cum f(0)=0, f(x)+f(-x) ad summum duos valores diversos ducere, probareque Aquaesulianum munus non esse f(0)≠0.

Munus f(x)=-x+2⌈x⌉ construe atque hoc munus esse Aquaesulianum proba.

Denique probate ad hoc munus f(-1)+f(1) =0 et f(1/2)+f(-1/2)=2 duo valores diversi.

Sequens est processus problematis absolutus: https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P6/index.html

Quaestiones mathematicas facere potes, sed scire potes utra maior sit, 9.11 an 9.9?

Andreas Gao, investigator Universitatis Stanfordiae et Sequoiae, significationem huius AI breakthrough — affirmavit.

Res praecipua est quod quaestiones recentissimae IMO examinis in institutione positae non continentur. Hoc magni momenti est quia ostendit AI posse novas, invisibilis difficultates tractare.

Praeterea problemata geometrica ab AI feliciter solvenda semper gravissima aestimata sunt propter loci naturam (intuitivam cogitationem et imaginationem spatialem requirunt).

Jim Fan, senior physicus in Nvidia, longum articulum misit dicens magna exemplaria exsistentia arcana —

Argenti nomismata in mathematica olympiadibus vincere possunt et in quaestionibus saepe peccant sicut "Qui numerus maior est, 9.11 vel 9.9?"

Non solum Gemini, sed etiam GPT-4o, Claude-3.5, et Llama-3 100 recte respondere non possunt.

Exercendo exempla AI, vastissimas regiones extra intelligentiam nostram exploramus.In processus, perquam mirabilem indagavimus aream - exoplaneta quae Terrae similis est sed vallium fatuorum plena est.

Hoc irrationabile videtur, sed explicare possumus eam per institutionem datae distributionis;

AlphaProof and AlphaGeometria 2 exercentur in argumentis formalibus et machinamentis symbolicis domain specialibus. Aliquatenus meliores sunt ad problemata Olympias specializata solvenda, licet in communi proposito structa sint LLM. Disciplina constituto GPT-4o miscetur cum magna copia codicis GitHub data, quae notitias mathematicas longe superet. Inter emendationes programmata "v9.11 > v9.9" data distributione serio pervertunt. Ergo hic error aliquatenus est intelligibilis.

Caput Google tincidunt dixit exempla quae difficilia mathematica et physica solvere possunt problemata praecipuum iter ad AGI esse, et hodie alium gradum in hac via sumpsimus.

Alii retiarii dixerunt nimiam informationem hac septimana esse.

Notae:

https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/

https://x.com/DrJimFan/status/181521330298356181